Skip to content

Instantly share code, notes, and snippets.

@mniip

mniip/cd.v

Last active November 12, 2020 17:09
Show Gist options
  • Save mniip/ede303e5e81dd0b8f79a59820e533841 to your computer and use it in GitHub Desktop.
Save mniip/ede303e5e81dd0b8f79a59820e533841 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
cd.v
Inductive opt {A : Type} : bool -> Type :=
| Nothing : opt false
| Just : A -> opt true.
Arguments opt : clear implicits.
Definition mkOpt {A : Type} {b : bool} (x : A) : opt A b :=
if b return opt A b then Just x else Nothing.
Definition mapOpt {A B : Type} {b : bool} (h : A -> B) (o : opt A b) : opt B b :=
match o with
| Nothing => Nothing
| Just x => Just (h x)
end.
Inductive flow : Type :=
Flow : bool -> bool -> flow.
Inductive conn : Type :=
| Conn : forall (b : bool), opt flow b -> conn.
Inductive perFlow {A : Type} : flow -> Type :=
| PerFlow : forall {ur dl}, opt A ur -> opt A dl -> perFlow (Flow ur dl).
Arguments perFlow : clear implicits.
Definition isUR (c : conn) : bool :=
match c with
| Conn true (Just (Flow ur _)) => ur
| _ => false
end.
Definition isDL (c : conn) : bool :=
match c with
| Conn true (Just (Flow _ dl)) => dl
| _ => false
end.
Inductive perConn {A : Type} {c : conn} : Type :=
| PerConn : opt A (isUR c) -> opt A (isDL c) -> perConn.
Arguments perConn : clear implicits.
Definition mkPerConn {A : Type} {c : conn} : A -> A -> perConn A c :=
fun ur dl => PerConn (mkOpt ur) (mkOpt dl).
Inductive dir {A : Type} : Type :=
Dir : A -> A -> A -> A -> dir.
Arguments dir : clear implicits.
Inductive perDir {A : Type} {f : A -> Type} : dir A -> Type :=
| PerDir : forall {u r d l}, f u -> f r -> f d -> f l -> perDir (Dir u r d l).
Arguments perDir {A} f.
Definition perUR {A ur dl} (m : opt A ur) : opt A (isUR (Conn true (Just (Flow ur dl)))) := m.
Definition perDL {A ur dl} (m : opt A dl) : opt A (isDL (Conn true (Just (Flow ur dl)))) := m.
Definition noConn : conn := Conn false Nothing.
Definition perNoConn {A} : perConn A noConn := PerConn (Nothing : opt A (isUR noConn)) Nothing.
Inductive graph_element : forall (dc : dir conn), perDir (perConn Type) dc -> Type :=
| ge_object : forall (X : Type) {r l : conn},
graph_element (Dir noConn (* TODO *) r noConn l) (PerDir perNoConn (mkPerConn X X) perNoConn (mkPerConn X X))
| ge_morphism : forall {X Y : Type} (f : X -> Y) {horiz ur dl},
graph_element (Dir (Conn (negb horiz) (mkOpt (Flow ur dl))) (Conn horiz (mkOpt (Flow ur dl))) (Conn (negb horiz) (mkOpt (Flow ur dl))) (Conn horiz (mkOpt (Flow ur dl)))) (PerDir (mkPerConn Y X) (mkPerConn Y X) (mkPerConn X Y) (mkPerConn X Y))
| ge_isomorphism : forall {X Y : Type} (f : X -> Y) (g : Y -> X) {horiz},
graph_element (Dir (Conn (negb horiz) (mkOpt (Flow true true))) (Conn horiz (mkOpt (Flow true true))) (Conn (negb horiz) (mkOpt (Flow true true))) (Conn horiz (mkOpt (Flow true true)))) (PerDir (mkPerConn Y X) (mkPerConn Y X) (mkPerConn Y X) (mkPerConn Y X))
| ge_junction : forall u r d l {X : Type},
graph_element (Dir u r d l) (PerDir (mkPerConn X X) (mkPerConn X X) (mkPerConn X X) (mkPerConn X X))
| ge_line_ur : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir (Conn true (Just (Flow a b))) (Conn true (Just (Flow b a))) noConn noConn) (PerDir (PerConn (perUR X) (perDL Y)) (PerConn (perUR Y) (perDL X)) perNoConn perNoConn)
| ge_line_v : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir (Conn true (Just (Flow a b))) noConn (Conn true (Just (Flow a b))) noConn) (PerDir (PerConn (perUR X) (perDL Y)) perNoConn (PerConn (perUR X) (perDL Y)) perNoConn)
| ge_line_ul : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir (Conn true (Just (Flow a b))) noConn noConn (Conn true (Just (Flow a b)))) (PerDir (PerConn (perUR X) (perDL Y)) perNoConn perNoConn (PerConn (perUR X) (perDL Y)))
| ge_line_dr : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir noConn (Conn true (Just (Flow a b))) (Conn true (Just (Flow a b))) noConn) (PerDir perNoConn (PerConn (perUR X) (perDL Y)) (PerConn (perUR X) (perDL Y)) perNoConn)
| ge_line_h : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir noConn (Conn true (Just (Flow a b))) noConn (Conn true (Just (Flow a b)))) (PerDir perNoConn (PerConn (perUR X) (perDL Y)) perNoConn (PerConn (perUR X) (perDL Y)))
| ge_line_dl : forall {a b} {X : opt Type a} {Y : opt Type b},
graph_element (Dir noConn noConn (Conn true (Just (Flow a b))) (Conn true (Just (Flow b a)))) (PerDir perNoConn perNoConn (PerConn (perUR X) (perDL Y)) (PerConn (perUR Y) (perDL X)))
| ge_diode_u : forall {X : Type},
graph_element (Dir (Conn true (Just (Flow true false))) noConn (Conn true (Just (Flow true false))) noConn) (PerDir (PerConn (perUR (Just X)) (perDL Nothing)) perNoConn (PerConn (perUR (Just X)) (perDL Nothing)) perNoConn)
| ge_diode_r : forall {X : Type},
graph_element (Dir noConn (Conn true (Just (Flow true false))) noConn (Conn true (Just (Flow true false)))) (PerDir perNoConn (PerConn (perUR (Just X)) (perDL Nothing)) perNoConn (PerConn (perUR (Just X)) (perDL Nothing)))
| ge_diode_d : forall {X : Type},
graph_element (Dir (Conn true (Just (Flow false true))) noConn (Conn true (Just (Flow false true))) noConn) (PerDir (PerConn (perUR Nothing) (perDL (Just X))) perNoConn (PerConn (perUR Nothing) (perDL (Just X))) perNoConn)
| ge_diode_l : forall {X : Type},
graph_element (Dir noConn (Conn true (Just (Flow false true))) noConn (Conn true (Just (Flow false true)))) (PerDir perNoConn (PerConn (perUR Nothing) (perDL (Just X))) perNoConn (PerConn (perUR Nothing) (perDL (Just X)))).
Inductive perList {A : Type} {f : A -> Type} : list A -> Type :=
| PerNil : perList nil
| PerCons : forall {x xs}, (f x) -> perList xs -> perList (cons x xs).
Arguments perList {A} f.
Definition consConn (c : conn) (l : list flow) : list flow :=
match c with
| Conn _ (Just f) => cons f l
| _ => l
end.
Definition connToFlow {A : Type} {f : flow} (C : perConn A (Conn true (Just f))) : perFlow A f :=
match f, C with
| Flow _ _, PerConn i o => PerFlow i o
end.
Definition perConsConn {c : conn} {l : list flow} (C : perConn Type c) (L : perList (perFlow Type) l) : perList (perFlow Type) (consConn c l) :=
match c, C with
| Conn b mf, C => match mf return perConn _ (Conn _ mf) -> perList _ (consConn (Conn _ mf) _) with
| Nothing => fun _ => L
| Just f => fun C => PerCons (connToFlow C) L
end C
end.
Inductive graph_row : forall (u : list flow) (r : conn) (d : list flow) (l : conn), perList (perFlow Type) u -> perConn Type r -> perList (perFlow Type) d -> perConn Type l -> Type :=
| gr_nil : forall {h H}, graph_row nil h nil h PerNil H PerNil H
| gr_cons : forall {u r d l U R D L us ds e US DS E}, graph_element (Dir u r d l) (PerDir U R D L) -> graph_row us e ds r US E DS R -> graph_row (consConn u us) e (consConn d ds) l (perConsConn U US) E (perConsConn D DS) L.
Inductive closed_graph_row : forall (u : list flow) (d : list flow), perList (perFlow Type) u -> perList (perFlow Type) d -> Type :=
| cgr : forall {u d U D}, graph_row u noConn d noConn U perNoConn D perNoConn -> closed_graph_row u d U D.
Inductive graph : forall (u : list flow) (d : list flow), perList (perFlow Type) u -> perList (perFlow Type) d -> Type :=
| g_nil : forall {v V}, graph v v V V
| g_cons : forall {u d e U D E}, closed_graph_row u d U D -> graph d e D E -> graph u e U E.
Inductive closed_graph : Type :=
| cg : graph nil nil PerNil PerNil -> closed_graph.
Require Import List.
Inductive edge (tm : list Type) (i j : nat) : Type :=
| FunEdge : forall {X Y}, nth_error tm i = Some X -> nth_error tm j = Some Y -> (X -> Y) -> edge tm i j
| IdEdge : forall {X}, nth_error tm i = Some X -> nth_error tm j = Some X -> edge tm i j .
Definition edgeList (tm : list Type) : Type := list { '(pair i j) : _ & edge tm i j }.
Theorem nth_error_app1' {A : Type} (l1 : list A) (l2 : list A) (n : nat) (a : A) :
nth_error l1 n = Some a -> nth_error (app l1 l2) n = Some a.
Proof.
revert l1. induction n as [ | n IH]; simpl.
+ intros [ | b l1].
- discriminate.
- simpl. exact id.
+ intros [ | b l1].
- discriminate.
- simpl. apply IH.
Defined.
Theorem nth_error_app2' {A : Type} (l1 : list A) (l2 : list A) (n : nat) :
nth_error (app l1 l2) (length l1 + n) = nth_error l2 n.
Proof.
induction l1; simpl.
+ reflexivity.
+ assumption.
Defined.
Definition edgeShift {l1 l2 : list Type} : edgeList l2 -> edgeList (app l1 l2).
Proof.
apply map.
intros [[i j] e].
exists (pair (length l1 + i) (length l1 + j)).
destruct e as [X Y eX eY h | X ei ej].
+ unshelve eapply (FunEdge _ _ _ _ _ h); rewrite nth_error_app2'; assumption.
+ eapply IdEdge; rewrite nth_error_app2'; eassumption.
Defined.
Definition edgeExtend {l1 l2 : list Type} : edgeList l1 -> edgeList (app l1 l2).
Proof.
apply map.
intros [[i j] e].
exists (pair i j).
destruct e as [X Y eX eY h | X ei ej].
+ unshelve eapply (FunEdge _ _ _ _ _ h); apply nth_error_app1'; assumption.
+ eapply IdEdge; apply nth_error_app1'; eassumption.
Defined.
Inductive perOpt {A : Type} {f : A -> Type} : forall {b : bool}, opt A b -> Type :=
| PerNothing : perOpt Nothing
| PerJust : forall {x : A}, f x -> perOpt (Just x).
Arguments perOpt {A} f {b}.
Inductive perPerConn {A : Type} {f : A -> Type} : forall (c : conn), perConn A c -> Type :=
| PerPerConn : forall {b mf ur dl}, perOpt f ur -> perOpt f dl -> perPerConn (Conn b mf) (PerConn ur dl).
Arguments perPerConn {A} f {c}.
Definition proj1PPC {A f b mf ur dl} (ppc : perPerConn f (PerConn ur dl : perConn A (Conn b mf))) : perOpt f ur :=
match ppc with
| PerPerConn x _ => x
end.
Definition proj2PPC {A f b mf ur dl} (ppc : perPerConn f (PerConn ur dl : perConn A (Conn b mf))) : perOpt f dl :=
match ppc with
| PerPerConn _ x => x
end.
Inductive perPerDir {A : Type} {f : A -> Type} {h : forall a, f a -> Type} : forall (d : dir A), perDir f d -> Type :=
| PerPerDir : forall {u r d l U R D L}, h u U -> h r R -> h d D -> h l L -> perPerDir (Dir u r d l) (PerDir U R D L).
Arguments perPerDir {A f} h {d}.
Definition indexing (tm : list Type) (X : Type) : Type := { i & nth_error tm i = Some X }.
Definition indexingShift (l : list Type) (tm : list Type) (X : Type) : indexing tm X -> indexing (app l tm) X.
Proof.
intros [i]. exists (length l + i).
rewrite nth_error_app2'. assumption.
Defined.
Definition indexingExtend (tm : list Type) (l : list Type) (X : Type) : indexing tm X -> indexing (app tm l) X.
Proof.
intros [i]. exists i.
apply nth_error_app1'.
assumption.
Defined.
Definition elemEdges {dc : dir conn} {DC : perDir (perConn Type) dc} :
graph_element dc DC -> { tm & edgeList tm * perPerDir (fun _ => perPerConn (indexing tm)) DC }%type.
Proof.
intros [].
+ exists (cons X nil).
split. { exact nil. }
constructor; try (constructor; constructor).
- destruct r as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
- destruct l as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
+ destruct ur; destruct dl.
- exists (cons Y (cons X nil)).
split.
{
refine (cons _ nil). exists (1, 0).
unshelve eapply (FunEdge _ _ _ _ _ f).
all: reflexivity.
}
constructor; constructor; try constructor; destruct horiz.
all: simpl in *.
all: constructor.
1,3,6,8: exists 0.
5,6,7,8: exists 1.
all: reflexivity.
- exists (cons Y (cons X nil)).
split.
{
refine (cons _ nil). exists (1, 0).
unshelve eapply (FunEdge _ _ _ _ _ f).
all: reflexivity.
}
constructor; constructor; try constructor; destruct horiz.
all: simpl in *.
all: constructor.
1,2: exists 0.
3,4: exists 1.
all: reflexivity.
- exists (cons Y (cons X nil)).
split.
{
refine (cons _ nil). exists (1, 0).
unshelve eapply (FunEdge _ _ _ _ _ f).
all: reflexivity.
}
constructor; constructor; try constructor; destruct horiz.
all: simpl in *.
all: constructor.
3,4: exists 0.
1,2: exists 1.
all: reflexivity.
- exists nil.
split. { exact nil. }
constructor; constructor; try constructor; destruct horiz.
all: simpl in *. all: constructor.
+ exists (cons Y (cons X nil)).
split.
{
refine (cons _ (cons _ nil)).
+ exists (1, 0).
unshelve eapply (FunEdge _ _ _ _ _ f).
all: reflexivity.
+ exists (0, 1).
unshelve eapply (FunEdge _ _ _ _ _ g).
all: reflexivity.
}
destruct horiz. all: simpl in *.
- constructor; constructor; constructor.
1,3: exists 0.
3,4: exists 1.
all: reflexivity.
- constructor; constructor; constructor.
1,3: exists 0.
3,4: exists 1.
all: reflexivity.
+ exists (cons X nil).
split. { exact nil. }
constructor.
- destruct u as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
- destruct r as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
- destruct d as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
- destruct l as [? [ | [[] []]]].
all: unfold mkPerConn, mkOpt; simpl.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,3: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,4: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,4: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,4: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,4: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct X as [ | X]; destruct Y as [ | Y].
- exists nil. split. { exact nil. }
repeat constructor.
- exists (cons Y nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
- exists (cons Y (cons X nil)). split. { exact nil. }
constructor; constructor; constructor.
2,3: exists 0.
1,4: exists 1.
all: reflexivity.
+ exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
+ exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
+ exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
+ exists (cons X nil). split. { exact nil. }
constructor; constructor; constructor.
all: exists 0.
all: reflexivity.
Defined.
Inductive perPerFlow {A : Type} {F : A -> Type} : forall (f : flow), perFlow A f -> Type :=
| PerPerFlow : forall {ur dl UR DL}, perOpt F UR -> perOpt F DL -> perPerFlow (Flow ur dl) (PerFlow UR DL).
Arguments perPerFlow {A} F {f}.
Definition proj1PPF {A f ur dl UR DL} (ppf : perPerFlow f (PerFlow UR DL : perFlow A (Flow ur dl))) : perOpt f UR :=
match ppf with
| PerPerFlow x _ => x
end.
Definition proj2PPF {A f ur dl UR DL} (ppf : perPerFlow f (PerFlow UR DL : perFlow A (Flow ur dl))) : perOpt f DL :=
match ppf with
| PerPerFlow _ x => x
end.
Definition perConnToPerFlow {A : Type} {F : A -> Type} {ur dl UR DL} (q : perPerConn F (PerConn UR DL : perConn A (Conn true (Just (Flow ur dl))))) : perPerFlow F (connToFlow (PerConn UR DL)).
Proof.
unshelve eapply (perPerConn_rect A F (fun '(Conn b mf) => match b, mf in opt _ b return forall (p : perConn A (Conn b mf)), @perPerConn A F (Conn b mf) p -> Type with true, (Just f) => fun p _ => perPerFlow F (connToFlow p) | _, _ => fun _ _ => unit end) _ _ _ q).
(* fuck *)
simpl. intros ? [ | []].
+ constructor.
+ intros ur' dl' UR' DL'. simpl.
apply PerPerFlow; assumption.
Defined.
Inductive perPerList {A : Type} {f : A -> Type} {h : forall a, f a -> Type} : forall (l : list A), perList f l -> Type :=
| PerPerNil : perPerList nil PerNil
| PerPerCons : forall {x xs X XS}, h x X -> perPerList xs XS -> perPerList (cons x xs) (PerCons X XS).
Arguments perPerList {A f} h {l}.
Definition headPPL {A f h x xs X XS} (ppl : @perPerList A f h (cons x xs) (PerCons X XS)) : h x X :=
match ppl in perPerList _ pl return match pl with
| PerNil => unit
| PerCons X _ => h _ X
end with
| PerPerNil => tt
| PerPerCons z _ => z
end.
Definition tailPPL {A f h x xs X XS} (ppl : @perPerList A f h (cons x xs) (PerCons X XS)) : perPerList h XS :=
match ppl in perPerList _ pl return match pl with
| PerNil => unit
| PerCons _ XS => perPerList h XS
end with
| PerPerNil => tt
| PerPerCons _ zs => zs
end.
Definition optShift {o} {O : opt Type o} (l1 : list Type) (l2 : list Type) :
perOpt (indexing l2) O -> perOpt (indexing (app l1 l2)) O.
Proof.
intros [].
+ exact PerNothing.
+ apply PerJust.
apply indexingShift.
assumption.
Defined.
Definition optExtend {o} {O : opt Type o} (l1 : list Type) (l2 : list Type) :
perOpt (indexing l1) O -> perOpt (indexing (app l1 l2)) O.
Proof.
intros [].
+ exact PerNothing.
+ apply PerJust.
apply indexingExtend.
assumption.
Defined.
Definition flowShift {f} {F : perFlow Type f} (l1 : list Type) (l2 : list Type) :
perPerFlow (indexing l2) F -> perPerFlow (indexing (app l1 l2)) F.
Proof.
intros []. apply PerPerFlow.
+ apply optShift. assumption.
+ apply optShift. assumption.
Defined.
Definition flowExtend {f} {F : perFlow Type f} (l1 : list Type) (l2 : list Type) :
perPerFlow (indexing l1) F -> perPerFlow (indexing (app l1 l2)) F.
Proof.
intros []. apply PerPerFlow.
+ apply optExtend. assumption.
+ apply optExtend. assumption.
Defined.
Definition connShift {c} {C : perConn Type c} (l1 : list Type) (l2 : list Type) :
perPerConn (indexing l2) C -> perPerConn (indexing (app l1 l2)) C.
Proof.
intros []. apply PerPerConn.
+ apply optShift. assumption.
+ apply optShift. assumption.
Defined.
Definition connExtend {c} {C : perConn Type c} (l1 : list Type) (l2 : list Type) :
perPerConn (indexing l1) C -> perPerConn (indexing (app l1 l2)) C.
Proof.
intros []. apply PerPerConn.
+ apply optExtend. assumption.
+ apply optExtend. assumption.
Defined.
Definition listShift {fs} {FS : perList (perFlow Type) fs} (l1 : list Type) (l2 : list Type) :
perPerList (fun _ => perPerFlow (indexing l2)) FS -> perPerList (fun _ => perPerFlow (indexing (app l1 l2))) FS.
Proof.
intros qs. induction qs as [ | ? ? ? ? q qs IH].
+ exact PerPerNil.
+ apply PerPerCons.
- apply flowShift. exact q.
- exact IH.
Defined.
Definition listExtend {fs} {FS : perList (perFlow Type) fs} (l1 : list Type) (l2 : list Type) :
perPerList (fun _ => perPerFlow (indexing l1)) FS -> perPerList (fun _ => perPerFlow (indexing (app l1 l2))) FS.
Proof.
intros qs. induction qs as [ | ? ? ? ? q qs IH].
+ exact PerPerNil.
+ apply PerPerCons.
- apply flowExtend. exact q.
- exact IH.
Defined.
Definition indexingCons {c fs} {C : perConn Type c} {FS : perList (perFlow Type) fs} (l1 : list Type) (l2 : list Type) :
perPerConn (indexing l1) C -> perPerList (fun _ => perPerFlow (indexing l2)) FS -> perPerList (fun _ => perPerFlow (indexing (app l1 l2))) (perConsConn C FS).
Proof.
intros q qs.
destruct c as [? [ | f]]; simpl.
+ apply listShift. exact qs.
+ apply PerPerCons.
- apply flowExtend.
destruct f as [ur dl]. destruct C as [UR DL].
apply perConnToPerFlow. exact q.
- apply listShift. exact qs.
Defined.
Import EqNotations.
Definition rowEdges {u r d l U R D L} :
graph_row u r d l U R D L -> { tm & edgeList tm * perPerList (fun _ => perPerFlow (indexing tm)) U * perPerConn (indexing tm) R * perPerList (fun _ => perPerFlow (indexing tm)) D * perPerConn (indexing tm) L }%type.
Proof.
intros row. induction row as [ | ? ? ? ? ? ? ? ? ? ? ? ? ? ? elem row IH].
+ destruct H as [ur dl].
destruct h as [? [ | f]].
- simpl in *.
exists nil. split; [split; [split; [split | ] | ] | ].
1: exact nil.
all: constructor.
1,3: exact (match ur with Nothing => PerNothing | Just _ => tt end).
1,2: exact (match dl with Nothing => PerNothing | Just _ => tt end).
- destruct f as [UR DL]. simpl in *.
destruct ur as [ | X]; destruct dl as [ | Y].
* exists nil. repeat constructor.
* exists (cons Y nil). split; [split; [split; [split | ] | ] | ].
1: exact nil.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
* exists (cons X nil). split; [split; [split; [split | ] | ] | ].
1: exact nil.
all: constructor; constructor.
all: exists 0.
all: reflexivity.
* exists (cons Y (cons X nil)). split; [split; [split; [split | ] | ] | ].
1: exact nil.
all: constructor; constructor.
2,4: exists 0.
1,4: exists 1.
all: reflexivity.
+ destruct IH as [tmR [[[[elR]]]]].
destruct (elemEdges elem) as [tmE [elE q]].
refine (match q in @perPerDir _ _ _ dc DC return match DC with PerDir U R D L => perPerConn (indexing tmR) R -> {tm : list Type &
(edgeList tm * perPerList (fun a : flow => perPerFlow (indexing tm)) (perConsConn U US) * perPerConn (indexing tm) E *
perPerList (fun a : flow => perPerFlow (indexing tm)) (perConsConn D DS) * perPerConn (indexing tm) L)%type} end with PerPerDir _ _ _ _ => _ end p2).
intros ?.
(* fuck 2 *)
exists (app tmE tmR).
split; [split; [split; [split | ] | ] | ].
- assert (elC : edgeList (app tmE tmR)).
{ (* fuck 3 *)
clear p10 p9 p7 p6 p5 p3 c2 c1 c q elE p2 p1 p0 p elR row elem E DS US e ds us L D R U l d r u.
rename c0 into c, p4 into C, p8 into q1, X into q2.
apply (@connExtend _ _ _ tmR) in q1.
apply (@connShift _ _ tmE) in q2.
destruct q1 as [? mf ? ? ri li]. destruct mf as [ | f].
+ simpl in *. exact nil.
+ destruct f as [L R].
set (q21 := proj1PPC q2).
set (q22 := proj2PPC q2).
simpl in *. destruct ri as [ | X [i ei]]; destruct li as [ | Y [j ej]].
- exact nil.
- refine (cons _ nil). inversion q22 as [ | ? [k ek]].
exists (k, j). eapply IdEdge; eassumption.
- refine (cons _ nil). inversion q21 as [ | ? [k ek]].
exists (i, k). eapply IdEdge; eassumption.
- refine (cons _ (cons _ nil)).
* inversion q22 as [ | ? [k ek]].
exists (k, j). eapply IdEdge; eassumption.
* inversion q21 as [ | ? [k ek]].
exists (i, k). eapply IdEdge; eassumption.
}
exact (app elC (app (edgeExtend elE) (edgeShift elR))).
- apply indexingCons; assumption.
- apply connShift. assumption.
- apply indexingCons; assumption.
- apply connExtend. assumption.
Defined.
Definition closedRowEdges {u U d D} :
closed_graph_row u d U D -> { tm & edgeList tm * perPerList (fun _ => perPerFlow (indexing tm)) U * perPerList (fun _ => perPerFlow (indexing tm)) D }%type.
Proof.
intros [? ? ? ? gr].
destruct (rowEdges gr) as [tm [[[[el]]]]].
exists tm. split; try split; assumption.
Defined.
Definition graphEdges {u U d D} :
graph u d U D -> { tm & edgeList tm * perPerList (fun _ => perPerFlow (indexing tm)) U * perPerList (fun _ => perPerFlow (indexing tm)) D }%type.
Proof.
intros g. induction g as [ | ? ? ? ? ? ? cgr g IH ].
+ induction V as [ | f fs F FS IH ].
- exists nil. split; try split. { exact nil. }
all: exact PerPerNil.
- destruct IH as [tm [[el]]].
destruct F as [? ? U D].
destruct U as [ | X]; destruct D as [ | Y].
* exists tm. split; try split. { exact el. }
all: constructor; try (constructor; constructor); assumption.
* exists (cons Y tm).
split; try split. { exact (@edgeShift (cons _ nil) _ el). }
all: constructor; try (constructor; constructor).
1,3: exists 0; reflexivity.
all: apply (listShift (cons Y nil)).
all: assumption.
* exists (cons X tm).
split; try split. { exact (@edgeShift (cons _ nil) _ el). }
all: constructor; try (constructor; constructor).
1,3: exists 0; reflexivity.
all: apply (listShift (cons X nil)).
all: assumption.
* exists (cons Y (cons X tm)).
split; try split. { exact (@edgeShift (cons _ (cons _ nil)) _ el). }
all: constructor; try (constructor; constructor).
2,5: exists 0; reflexivity.
1,3: exists 1; reflexivity.
all: apply (listShift (cons Y (cons X nil))).
all: assumption.
+ destruct IH as [tmG [[elG v]]].
destruct (closedRowEdges cgr) as [tmR [[elR] w]].
exists (app tmR tmG). split; try split.
- (* fuck 4 *)
apply (@listExtend _ _ _ tmG) in w.
apply (@listShift _ _ tmR) in v.
assert (elC : edgeList (tmR ++ tmG)).
{
clear p p0 elG elR cgr g U E u e.
induction D as [ | f fs F FS IH ].
+ exact nil.
+ set (vh := headPPL v). set (vs := tailPPL v).
set (wh := headPPL w). set (ws := tailPPL w).
refine (app _ (IH vs ws)).
destruct F.
destruct (proj1PPF vh) as [ | X [i ei]]; destruct (proj2PPF vh) as [ | Y [j ej]].
- exact nil.
- refine (cons _ nil).
set (W := proj2PPF wh). inversion W as [ | ? [k ek]].
exists (k, j). eapply IdEdge; eassumption.
- refine (cons _ nil).
set (W := proj1PPF wh). inversion W as [ | ? [k ek]].
exists (i, k). eapply IdEdge; eassumption.
- refine (cons _ (cons _ nil)).
* set (W := proj2PPF wh). inversion W as [ | ? [k ek]].
exists (k, j). eapply IdEdge; eassumption.
* set (W := proj1PPF wh). inversion W as [ | ? [k ek]].
exists (i, k). eapply IdEdge; eassumption.
}
exact (app elC (app (edgeExtend elR) (edgeShift elG))).
- apply listExtend. assumption.
- apply listShift. assumption.
Defined.
Definition closedGraphEdges : closed_graph -> { tm & edgeList tm }.
Proof.
intros [g]. destruct (graphEdges g) as [tm [[el]]].
exists tm. exact el.
Defined.
Inductive path {tm : list Type} : nat -> nat -> Type :=
| NilPath : forall {i}, path i i
| ConsPath : forall {i j k}, edge tm i j -> path j k -> path i k.
Arguments path : clear implicits.
Fixpoint funEdgeList {tm i j} (p : path tm i j) : list (nat * nat) :=
match p with
| NilPath => nil
| @ConsPath _ m n _ (FunEdge _ _ _ _ _ _) p => cons (pair m n) (funEdgeList p)
| ConsPath (IdEdge _ _ _ _ _) p => funEdgeList p
end.
Definition consUniq {A} (eqb : A -> A -> bool) (x : A) (l : list A) : list A :=
match find (eqb x) l with
| Some _ => l
| None => cons x l
end.
Fixpoint appUniq {A} (eqb : A -> A -> bool) (l1 l2 : list A) : list A :=
match l1 with
| nil => l2
| cons x l1 => consUniq eqb x (appUniq eqb l1 l2)
end.
Import PeanoNat.
Fixpoint list_eqb {A} (eqb : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
| nil, nil => true
| cons x l1, cons y l2 => eqb x y && list_eqb eqb l1 l2
| _, _ => false
end.
Definition samePath {tm i j} (p1 p2 : path tm i j) : bool :=
list_eqb (fun '(i1, j1) '(i2, j2) => andb (Nat.eqb i1 i2) (Nat.eqb i2 j2)) (funEdgeList p1) (funEdgeList p2).
Fixpoint snocPath {tm i j k} (e : edge tm j k) (xs : path tm i j) : path tm i k :=
match xs, e with
| NilPath, e => ConsPath e NilPath
| ConsPath x xs, e => ConsPath x (snocPath e xs)
end.
Fixpoint catPath {tm : list Type} {i j k : nat} (xs : path tm i j) : path tm j k -> path tm i k :=
match xs with
| NilPath => id
| ConsPath x xs => fun ys => ConsPath x (catPath xs ys)
end.
Inductive ixList {f : nat -> Type} : Type :=
| ixNil : ixList
| ixCons : f 0 -> @ixList (fun n => f (S n)) -> ixList.
Arguments ixList : clear implicits.
Fixpoint nat_add_0_r (n : nat) : n + 0 = n :=
match n with
| 0 => eq_refl
| S n => match nat_add_0_r n with
| eq_refl => eq_refl
end
end.
Fixpoint nat_add_S (n m : nat) : S n + m = n + S m :=
match n return S n + m = n + S m with
| 0 => eq_refl
| S n => match nat_add_S n m in _ = z return S (S n + m) = S z with
| eq_refl => eq_refl
end
end.
Fixpoint ix_nth {f : nat -> Type} (l : ixList f) (n : nat) : option (f n) :=
match l with
| ixNil => None
| ixCons x l => match n with
| 0 => Some x
| S n => ix_nth l n
end
end.
Fixpoint ix_replicate {f : nat -> Type} (n : nat) (x : forall {n}, f n) : ixList f :=
match n with
| 0 => ixNil
| S n => ixCons x (ix_replicate n (fun _ => x))
end.
Fixpoint ix_map_nth {f : nat -> Type} (n : nat) (F : f n -> f n) (l : ixList f) : ixList f :=
match l with
| ixNil => ixNil
| ixCons x l => match n, F with
| 0, F => ixCons (F x) l
| S n, F => ixCons x (ix_map_nth n F l)
end
end.
Fixpoint ix_zip_with {f g h : nat -> Type} (F : forall {n}, f n -> g n -> h n) (l1 : ixList f) (l2 : ixList g) : ixList h :=
match l1, l2 with
| ixCons x l1, ixCons y l2 => ixCons (F x y) (ix_zip_with (fun _ => F) l1 l2)
| _, _ => ixNil
end.
Fixpoint ix_map {f g : nat -> Type} (F : forall {n}, f n -> g n) (l : ixList f) : ixList g :=
match l with
| ixCons x l => ixCons (F x) (ix_map (fun _ => F) l)
| ixNil => ixNil
end.
Fixpoint ix_foldr {f : nat -> Type} {R : Type} (F : forall {n}, f n -> R -> R) (Z : R) (l : ixList f) : R :=
match l with
| ixCons x l => F x (ix_foldr (fun _ => F) Z l)
| ixNil => Z
end.
Definition pathMap (tm : list Type) := ixList (fun i => ixList (fun j => list (path tm i j))).
Definition propPath {tm j k} (e : edge tm j k) (ep : pathMap tm) : pathMap tm -> pathMap tm.
Proof.
apply ix_map. simpl. intros i.
apply ix_map. simpl. intros l.
apply (appUniq samePath).
assert (list (path tm k l)) as ts.
{
destruct (ix_nth ep k) as [r | ]; simpl.
2: exact nil.
destruct (ix_nth r l) as [ts | ]; simpl.
2: exact nil.
exact ts.
}
assert (list (path tm i j)) as hs.
{
destruct (ix_nth ep i) as [r | ]; simpl.
2: exact nil.
destruct (ix_nth r j) as [hs | ]; simpl.
2: exact nil.
exact hs.
}
refine (map _ (list_prod hs ts)).
intros [h t].
exact (catPath h (ConsPath e t)).
Defined.
Fixpoint edgePaths {tm} (el : edgeList tm) : pathMap tm :=
match el with
| nil => ix_replicate (length tm) (fun i => ix_replicate (length tm) (fun j =>
match Nat.eq_dec i j with
| left eq => cons (rew eq in NilPath) nil
| _ => nil
end))
| cons (existT _ (pair i j) e) el => let ep := edgePaths el in
propPath e ep ep
end.
Fixpoint nonId {tm i j} (p : path tm i j) : bool :=
match p with
| NilPath => false
| ConsPath (FunEdge _ _ _ _ _ _) _ => true
| ConsPath (IdEdge _ _ _ _ _) p => nonId p
end.
Fixpoint nonTrivial {tm : list Type} (ep : pathMap tm) : list { '(i, j) : _ & list (path tm i j) } :=
ix_foldr (fun i r => app (ix_foldr (fun j ps =>
match length (filter nonId ps) with
| S (S _) => cons (existT _ (pair i j) ps)
| _ => id
end) nil r)) nil ep.
Definition ssEq {A : Type} {X Y : A} (p : Some X = Some Y) : X = Y :=
match p with
| eq_refl => eq_refl
end.
Inductive funChain {X : Type} : Type -> Type :=
| FunId : funChain X
| FunCompose : forall {Y Z}, (X -> Y) -> @funChain Y Z -> funChain Z.
Arguments funChain : clear implicits.
Fixpoint encodePath {tm X Y i j} (p : path tm i j) : nth_error tm i = Some X -> nth_error tm j = Some Y -> funChain X Y :=
match p in path _ i j return nth_error tm i = Some X -> nth_error tm j = Some Y -> funChain X Y with
| NilPath => fun ei ej => match rew [fun z => z = _] ei in ej with
| eq_refl => FunId
end
| ConsPath (@FunEdge _ _ _ Z W ez ew f) p => fun ei ej => let g := encodePath p ew ej : funChain W Y in
let f := rew <- [fun z => z -> _] (ssEq (rew [fun z => z = _] ei in ez) : X = Z) in f : X -> W in FunCompose f g
| ConsPath (@IdEdge _ _ _ Z ez ew) p => fun ei ej => encodePath p (rew <- rew [fun z => z = _] ei in ez in ew) ej
end.
Notation "f ∘ g" := (fun x => f (g x)) (at level 40, left associativity).
Fixpoint denotePath' {X Y Z} (f : X -> Y) (g : funChain Y Z) : X -> Z :=
match g with
| FunId => f
| FunCompose f' g => denotePath' f' g ∘ f
end.
Definition denotePath {X Y} (g : funChain X Y) : X -> Y :=
match g with
| FunId => id
| FunCompose f g => denotePath' f g
end.
Definition conjunct {A} (l : list A) (f : A -> Prop) : Prop :=
match l with
| nil => True
| cons x l => (fix con x l := match l with
| nil => f x
| cons y l => f x /\ con y l
end) x l
end.
Definition encodeEq {tm i j} (l : list (path tm i j)) : Prop :=
match nth_error tm i as I, nth_error tm j as J return nth_error tm i = I -> nth_error tm j = J -> Prop with
| Some X, Some Y => fun ei ej =>
match l with
| nil => True
| cons p l => conjunct l (fun p' => denotePath (encodePath p ei ej) = denotePath (encodePath p' ei ej))
end
| _, _ => fun _ _ => False
end eq_refl eq_refl.
Definition commutes : { tm & edgeList tm } -> Prop :=
fun '(existT _ tm el) => conjunct (nonTrivial (edgePaths el))
(fun '(existT _ p ps) => match p, ps with pair _ _, ps => encodeEq ps end).
Declare Custom Entry cd_element.
Declare Custom Entry cd_row.
Declare Custom Entry cd.
Notation "┼" := (ge_junction (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _)))) (in custom cd_element at level 0).
Notation "├" := (ge_junction (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) noConn) (in custom cd_element at level 0).
Notation "┴" := (ge_junction (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) noConn (Conn true (Just (Flow _ _)))) (in custom cd_element at level 0).
Notation "┤" := (ge_junction (Conn true (Just (Flow _ _))) noConn (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _)))) (in custom cd_element at level 0).
Notation "┬" := (ge_junction noConn (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _))) (Conn true (Just (Flow _ _)))) (in custom cd_element at level 0).
Notation "└" := (ge_line_ur) (in custom cd_element at level 0).
Notation "│" := (ge_line_v) (in custom cd_element at level 0).
Notation "┘" := (ge_line_ul) (in custom cd_element at level 0).
Notation "─" := (ge_line_h) (in custom cd_element at level 0).
Notation "┌" := (ge_line_dr) (in custom cd_element at level 0).
Notation "┐" := (ge_line_dl) (in custom cd_element at level 0).
Notation "▲" := (ge_diode_u) (in custom cd_element at level 0).
Notation "▶" := (ge_diode_r) (in custom cd_element at level 0).
Notation "▼" := (ge_diode_d) (in custom cd_element at level 0).
Notation "◀" := (ge_diode_l) (in custom cd_element at level 0).
Notation "x" := (cgr (gr_cons x (@gr_nil noConn perNoConn))) (in custom cd_row at level 0, x custom cd_element).
Notation "x y .. z" := (cgr (gr_cons x (gr_cons y .. (gr_cons z (@gr_nil noConn perNoConn)) ..))) (in custom cd_row at level 0, x custom cd_element, z custom cd_element).
Notation "x" := (ge_object x) (in custom cd_element at level 0, x constr at level 0).
Notation "[ f ]" := (ge_morphism f) (in custom cd_element at level 0, f constr at level 0).
Notation "[ f / g ]" := (ge_isomorphism f g) (in custom cd_element at level 0, f constr at level 0, g constr).
Notation "▌ x ▌ .. ▌ z " := (closedGraphEdges (cg (g_cons x (.. (g_cons z (@g_nil nil PerNil)) ..)))) (at level 1, x custom cd_row, z custom cd_row).
Goal forall X Y Z W,
forall (f : X -> Y) (g : Y -> W) (h : X -> Z) (k : Z -> W),
commutes
▌ ┌X──[f]──▶Y┐
▌ │ │
▌[h] [g]
▌ │ │
▌ ▼ ▼
▌ └Z──[k]──▶W┘ .
Proof.
intros. compute.
Abort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment