(***********************************************************) (** A formal inductive dependently-typed construction of *) (** semi-simplicial sets, together with some examples *) (** See "A dependently-typed construction of semi-simplicial types" *) (** by Hugo Herbelin *) (***********************************************************) (* This file was mainly developed from November 2012 to March 2012, and cleaned a little bit in January 2013 *) (***********************************************************) (** * 1. Preliminaries *) (***********************************************************) (***********************************************************) (** ** Notations *) (***********************************************************) (** Extra notations for transport *) Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H) (at level 10, H' at level 10). Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H) (at level 10, H' at level 10). Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H) (at level 10, H' at level 10). Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H) (at level 10, H' at level 10). Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H) (at level 10, H' at level 10, only parsing). Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H) (at level 10, H' at level 10, format "'[' 'rew' H in '/' H' ']'"). (** Nice notations for a couple of iteration of successor and predecessor *) Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). Notation "p .+2" := (S (S p)) (at level 1, left associativity, format "p .+2"). Notation "p .+3" := (S (S (S p))) (at level 1, left associativity, format "p .+3"). Notation "p .-1" := (pred p) (at level 1, left associativity, format "p .-1"). (** Notations for sigma-types *) Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1"). Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2"). Notation "{{ x , y }}" := (existT _ x y) (at level 0, format "{{ x , '/ ' y }}"). (***********************************************************) (** Operators on and properties of equality proofs *) (***********************************************************) Lemma rew_pair_apply : forall A (P Q : A->Type) a b (x:P a) (y:Q a) z (H:a=b), (rew H in x, rew H in y) = z -> rew [fun a => (P a * Q a)%type] H in (x,y) = z. Proof. destruct H. intro H. exact H. Defined. Lemma rew_pair : forall A (P Q : A->Type) a b (x:P a) (y:Q a) (H:a=b), (rew H in x, rew H in y) = rew [fun a => (P a * Q a)%type] H in (x,y). Proof. destruct H. reflexivity. Defined. Lemma map_subst : forall {A} {P Q:A->Type} (f : forall a, P a -> Q a) {a b} (H:a=b) (x:P a), rew H in f a x = f b (rew H in x). destruct H. trivial. Defined. Lemma map_subst_map : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall a, P a -> Q (f a)), forall {a b} (H:a=b) (x:P a), rew f_equal f H in g a x = g b (rew H in x). destruct H. trivial. Defined. Lemma rew_swap : forall A (P:A->Type) a b (H:a=b) (x:P a) (y:P b), rew H in x = y -> x = rew <- H in y. Proof. destruct H. trivial. Defined. Lemma rew_compose : forall A (P:A->Type) a b c (H:a=b) (H':b=c) (x:P a), rew H' in rew H in x = rew (eq_trans H H') in x. Proof. destruct H'. trivial. Defined. Lemma rew_map : forall A B (P:B->Type) (f:A->B) a b (H:a=b) (x:P (f a)), rew [fun x => P (f x)] H in x = rew f_equal f H in x. Proof. destruct H. trivial. Defined. Lemma f_equal_dep : forall {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a)) {a1 a2 : A} {b1:B a1} {b2:B a2} (H : a1 = a2), rew H in b1 = b2 -> rew f_equal f H in g a1 b1 = g a2 b2. Proof. destruct H. destruct 1. reflexivity. Defined. Lemma mk_sig_eq: forall {A P} {a1 a2:A} {b1:P a1} {b2:P a2}, forall H:a1=a2, (rew H in b1) = b2 -> {{a1,b1}} = {{a2,b2}}. Proof. destruct H. destruct 1. reflexivity. Defined. Lemma mk_sig_eq_map : forall A A' B B' (f:A -> A') (g:forall a:A, B a -> B' (f a)) {a1 a2:A} {b1:B a1} {b2:B a2}, forall (H:a1=a2) (H': rew H in b1 = b2), f_equal (fun x => {{f x.1, g x.1 x.2}}) (mk_sig_eq H H') = mk_sig_eq (f_equal f H) (f_equal_dep f g H H'). Proof. destruct H. destruct H'. reflexivity. Defined. Lemma eq_trans_map : forall {A B} {a1 a2 a3:A} {b1:B a1} {b2:B a2} {b3:B a3}, forall (H1:a1=a2) (H2:a2=a3) (H1': rew H1 in b1 = b2) (H2': rew H2 in b2 = b3), rew eq_trans H1 H2 in b1 = b3. Proof. intros. destruct H2. exact (eq_trans H1' H2'). Defined. Lemma mk_sig_eq_trans : forall {A B} {a1 a2 a3:A} {b1:B a1} {b2:B a2} {b3:B a3}, forall (H1:a1=a2) (H1': rew H1 in b1 = b2), forall (H2:a2=a3) (H2': rew H2 in b2 = b3), eq_trans (mk_sig_eq H1 H1') (mk_sig_eq H2 H2') = mk_sig_eq (eq_trans H1 H2) (eq_trans_map H1 H2 H1' H2'). Proof. destruct H2, H2'. reflexivity. Defined. Theorem mk_sig_congr : forall {A P} {a1 a2:A} {b1:P a1} {b2:P a2}, forall {H1 H2:a1=a2} {H1': rew H1 in b1 = b2} {H2': rew H2 in b1 = b2}, forall (H: H1 = H2), rew [fun H => rew H in b1 = b2] H in H1' = H2' -> mk_sig_eq H1 H1' = mk_sig_eq H2 H2'. Proof. destruct H. destruct 1. reflexivity. Qed. (***********************************************************) (** Less than and properties about it *) (***********************************************************) Inductive le (n:nat) : nat -> Type := | le_n : n <= n | le_P m : n.+1 <= m -> n <= m where "n <= m" := (le n m) : nat_scope. Implicit Arguments le_P [n m]. Implicit Arguments le_n [n]. Theorem le_trans : forall {n m p}, n <= m -> m <= p -> n <= p. Proof. induction 1; intro Hmp. - assumption. - apply le_P, IHle. assumption. Defined. Theorem le_n_S : forall {n m}, n <= m -> n.+1 <= m.+1. Proof. induction 1; auto using le. Defined. Lemma LES {p q} : p <= q -> p <= q.+1. Proof. intros * H. apply le_P, le_n_S, H. Defined. Theorem le_0 : forall n, 0 <= n. Proof. induction n. apply le_n. apply le_P, le_n_S. assumption. Defined. Theorem le_pred : forall {n m}, n <= m -> pred n <= pred m. Proof. induction 1. apply le_n. destruct n; simpl. assumption. apply le_P; assumption. Defined. Theorem le_Sn_0 : forall n, n.+1 <= 0 -> False. Proof. intros n H. remember 0 as m. change (match n.+1 with 0 => True | _ => False end). induction H. - subst. auto. - destruct IHle; auto. Defined. Theorem le_pred_out : forall {n m}, n.+1 <= m -> {m':nat & m'.+1 = m}. Proof. destruct m. - intros H. exfalso; apply le_Sn_0 with n. assumption. - intros _; exists m; auto. Defined. Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl. Proof. induction n. - change (match 0 as n return 0=n -> Prop with | 0 => fun x => x = eq_refl | _ => fun _ => True end x). destruct x; reflexivity. - specialize IHn with (f_equal pred x). change eq_refl with (f_equal S (@eq_refl _ n)). rewrite <- IHn; clear IHn. change (match S n as n' return S n = n' -> Prop with | 0 => fun _ => True | S n' => fun x => x = f_equal S (f_equal pred x) end x). pattern (S n) at 2 3, x. destruct x; reflexivity. Defined. Theorem eq_rect_eq_nat : forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = rew h in x. Proof. intros. rewrite (UIP_refl_nat p h). reflexivity. Defined. Theorem le_Sn_n : forall n, n.+1 <= n -> False. Proof. induction n; intros H. apply (le_Sn_0 _ H). apply IHn; clear IHn. apply (@le_pred n.+2 n.+1). assumption. Defined. Theorem le_uniqueness : forall (n m : nat) (p q : n <= m), p = q. Proof. induction p; intro q. - change le_n with (rew [fun n0 => n <= n0] eq_refl in le_n). generalize (eq_refl n). destruct q; intro e. + rewrite <- eq_rect_eq_nat; trivial. + exfalso. rewrite e in q. apply le_Sn_n in q. assumption. - change (le_P p) with (rew [fun n0 => n <= n0] eq_refl in (le_P p)). generalize (eq_refl (S m)). destruct q; intro e. + contradiction (le_Sn_n n). + rewrite (IHp q). rewrite <- eq_rect_eq_nat. reflexivity. Defined. Lemma le_uniqueness_unique : forall {n m} (H1 H2:n<=m) H, le_uniqueness n m H1 H2 = H. Proof. intros. transitivity (eq_trans (le_uniqueness n m H1 H2) (eq_sym (le_uniqueness n m H2 H2))). - destruct (le_uniqueness n m H2 H2). reflexivity. - destruct H. destruct (le_uniqueness n m H1 H1). reflexivity. Defined. Lemma le_uniqueness_refl : forall {n m} (H:n<=m), le_uniqueness n m H H = eq_refl. Proof. intros; apply le_uniqueness_unique. Defined. Lemma le_shift : forall m n (H H':m.+1<=n) (P:m<=n -> Type) (x:P (le_P H)), rew le_uniqueness m n (le_P H) (le_P H') in x = rew [fun H => P (le_P H)] le_uniqueness m.+1 n H H' in x. Proof. intros. destruct (le_uniqueness m.+1 n H H'). rewrite le_uniqueness_refl. reflexivity. Defined. Theorem LPP : forall {n m}, n.+1 <= m.+1 -> n <= m. Proof. intros. apply (le_pred H). Defined. Theorem LUP : forall {m n} p, m <= n -> m <= p + n. Proof. fix 3. intros * H. destruct p. - exact H. - simpl plus. apply le_P, le_n_S, LUP, H. (* W/o the simpl, plus remains unfolded in the proof *) Defined. Opaque LUP. Definition LSS {n m} (H:n<=m) := le_n_S H. Opaque LSS. Lemma plus_n_Sm : forall n m, (n + m).+1 = n + m.+1. Proof. intros; induction n. - reflexivity. - simpl; apply f_equal, IHn. Defined. Theorem LSWING : forall {n m p}, n <= m + p.+1 -> n <= m.+1 + p. Proof. intros. simpl. rewrite plus_n_Sm. assumption. Defined. Lemma LSWINGPP : forall m n p (H:m.+1<=p.+1+n.+1), (LSWING (LPP H) = LPP (LSWING H)). Proof. intros. apply le_uniqueness. Defined. Lemma LSWINGES : forall m n p (H:m<=p+n.+1), (@LSWING m p.+1 n (LES H) = LES (LSWING H)). Proof. intros. apply le_uniqueness. Defined. (***********************************************************) (** * 2. Combinations over a dependent operator *) (***********************************************************) (***********************************************************) (** Branching over a non-empty interval *) (***********************************************************) Set Asymmetric Patterns. Section Branching. Fixpoint subbranching n c (Hc : c <= n) : forall (X : forall c, c <= n -> Type), Type := match Hc in _ <= n return (forall c, c <= n -> Type) -> Type with | le_n => fun X => unit | le_P _ Hc => fun X => (X c.+1 Hc * subbranching _ c.+1 Hc X)%type end. Definition branching n c (Hc : c <= n) (X : forall c, c <= n -> Type) := (X c Hc * subbranching n c Hc X)%type. Fixpoint get n c i X (Hci:c<=i) (Hi:i<=n) {struct Hci} : branching n c (le_trans Hci Hi) X -> X i Hi. Proof. destruct Hci as [|i Hci]; simpl; intros u. - exact (fst u). - eapply get with (c:=c.+1). eexact (snd u). Defined. Definition subbranching_step n c Hrc X Y : (forall Hrc, branching n c.+1 Hrc X -> branching n c.+1 Hrc Y) -> subbranching n c Hrc X -> subbranching n c Hrc Y. Proof. destruct Hrc; intros IH H. - exact tt. - apply IH, H. Defined. End Branching. (***********************************************************) (** Combinations over a dependent "face" operator [d] *) (***********************************************************) Section Combinations. Context {F : nat -> Type} (Y : F 0 -> Type). Section Choices. Context (n:nat) (d : forall {p} i, i<=p+n -> F p.+1 -> F p) . Fixpoint choices p c (Hc:c<=n) : F p -> Type := match p with | 0 => fun x => Y x | p.+1 => fun x => branching n c Hc (fun c Hc => choices p c Hc (d p c (LUP p Hc) x)) end. End Choices. Definition commute1 n (d: forall p i, i<=p+n -> F p.+1 -> F p) := forall p j k (Hjk:j.+1<=k.+1) (Hrj:j<=p+n) (HrkS:k.+1<=(p+n).+1) (x:F p.+2), d p k (LPP HrkS) (d p.+1 j (LES Hrj) x) = d p j Hrj (d p.+1 k.+1 HrkS x). Definition commute2 n d (dcomm:commute1 n d) := forall p i j k x (HrkP:k.+2<=(p+n).+2) (Hij:i.+1<=j.+1) (Hik:i.+1<=k.+1) (Hri:i<=p+n) (HjkS:j.+2<=k.+2) (Hrj:j.+1<=(p+n).+1) (HjPk:j.+1<=k.+1) (HikS:i.+1<=k.+2) (Hij':i.+1<=j.+1), rew [fun H => d _ _ _ (d _ _ H _) = _] (le_uniqueness _ _ (LPP (LES Hrj)) (LES (LPP Hrj))) in eq_trans (f_equal (d p k (LPP (LPP HrkP))) (dcomm p.+1 i j Hij (LES Hri) (LES Hrj) x)) (eq_trans (dcomm p i k Hik Hri (LPP HrkP) (d p.+2 j.+1 (LES Hrj) x)) (f_equal (d p i Hri) (dcomm p.+1 j.+1 k.+1 HjkS Hrj HrkP x))) = eq_trans (dcomm p j k HjPk (LPP Hrj) (LPP HrkP) (d p.+2 i (LES (LES Hri)) x)) (eq_trans (f_equal (d p j (LPP Hrj)) (dcomm p.+1 i k.+1 HikS (LES Hri) HrkP x)) (dcomm p i j Hij' Hri Hrj (d p.+2 k.+2 HrkP x))). Section Filter_step. Variable p : nat. Hypothesis (filter : forall n d (dcomm:commute1 n d) p k c (Hrc : c <= n) (Hlk : c <= k) (Hrk : k <= p + n) x, choices n d p.+1 c Hrc x -> choices n d p c Hrc (d p k Hrk x)). Fixpoint filter_step n d (dcomm:commute1 n d) i c (Hrc : c <= n) (Hli : c <= i) (Hri : i <= p.+1 + n) x {struct Hli} : choices n d p.+2 c Hrc x -> choices n d p.+1 c Hrc (d p.+1 i Hri x). Proof. intros s. change p.+2 with (id p.+1).+1 in s. Opaque id. simpl in s. Transparent id. unfold id in *. destruct Hli as [|i Hli]. - rewrite <- (le_uniqueness _ _ (LUP p.+1 Hrc) Hri). exact (fst s). - split. + destruct (le_pred_out Hli) as (i',<-). rename i' into i. simpl in s, Hri. (* needed, otherwise plus remains unfolded in H below *) rewrite <- (dcomm p c i Hli (LUP _ Hrc) Hri). apply (filter n d dcomm p i c Hrc (LPP Hli) (LPP Hri) (d p.+1 c (LUP _ Hrc) x) (fst s)). + eapply subbranching_step. intros Hrc0. * change p.+2 with (id p.+1).+1 in filter_step. Opaque id. simpl in filter_step. Transparent id. unfold id in *. apply (filter_step n d dcomm i c.+1). assumption. * simpl in s; apply (snd s). Defined. End Filter_step. Fixpoint filter n d (dcomm:commute1 n d) p {struct p} : forall i c (Hrc:c<=n) (Hli:c<=i) (Hri:i<=p+n) x, choices n d p.+1 c Hrc x -> choices n d p c Hrc (d p i Hri x). Proof. destruct p. - intros i c Hrc Hli Hri x s. simpl. red in s. pattern i, Hri. (* Shouldn't *) apply (get n c i _ Hli Hri). change n with (0+n). (* Shouldn't *) rewrite <- (le_uniqueness _ _ Hrc (le_trans Hli Hri)). assumption. - apply filter_step; assumption. Defined. Theorem filter_commute1 n d (dcomm:commute1 n d) (fcomm:commute2 n d dcomm) : forall p j k c (Hrc : c <= n) (Hlk : c <= k) (HlkS : c <= k.+1) (Hjk : j.+1 <= k.+1) (Hrj : j <= p + n) (Hlj : c <= j) (HrkS : k.+1 <= (p + n).+1) (* needed to avoid plus to be expanded *) (x : F p.+2) (y : choices n d p.+2 c Hrc x), rew [fun x : F p => choices n d p c Hrc x] dcomm p j k Hjk Hrj HrkS x in filter n d dcomm p k c Hrc Hlk (LPP HrkS) (d p.+1 j (LES Hrj) x) (filter n d dcomm p.+1 j c Hrc Hlj (LES Hrj) x y) = filter n d dcomm p j c Hrc Hlj Hrj (d p.+1 k.+1 HrkS x) (filter n d dcomm p.+1 k.+1 c Hrc HlkS HrkS x y). Proof. Implicit Arguments filter [n d dcomm]. Implicit Arguments filter_step [n filter d dcomm]. induction p; intros. (* p=0 *) - simpl. induction Hlj as [c|c j]. + simpl. destruct (le_uniqueness _ n _ Hrj). rewrite <- (le_uniqueness _ _ (le_P Hjk) HlkS). (* feed HlkS for reduction *) rewrite <- (le_uniqueness _ _ (LPP Hjk) Hlk). (* prepare for reflexivity *) rewrite (@le_uniqueness_refl c n.+1). reflexivity. + (* c <= i-1 <= k-2 <= n *) assert (Hlk' := le_trans Hlj (LPP Hjk)). (*clearbody Hlk'.*) rewrite <- (le_uniqueness _ _ (le_P Hlk') Hlk). (* feed for reduction *) rewrite <- (le_uniqueness _ _ (le_P (LSS Hlk)) HlkS). (* feed for reduction *) simpl. set (Pj := fun H:c<=n => Y (d O c H (d 1 j (LES Hrj) x))). set (Qj H:= subbranching n c H (fun c H => Y (d O c H (d 1 j (LES Hrj) x)))). rewrite <- (rew_pair _ Pj Qj). set (Pk := fun H:c<=n => Y (d O c H (d 1 k.+1 HrkS x))). set (Qk H:= subbranching n c H (fun c H => Y (d O c H (d 1 k.+1 HrkS x)))). rewrite <- (rew_pair _ Pk Qk). simpl. simpl. destruct (le_uniqueness _ _ (le_P (le_trans Hlk' (LPP HrkS))) Hrc). simpl. do 2 rewrite le_shift. apply IHHlj. - (* p.+1 *) induction Hlj as [c|c j]. + change p.+1 with (id p.+1). Opaque id. simpl filter at 2. Transparent id. unfold id. change (p.+1+n).+1 with (p+n).+2. simpl filter at 2. destruct (le_uniqueness c (p+n).+1 _ Hrj). rewrite <- (le_uniqueness _ _ (le_P Hjk) HlkS). (* feed for reduction *) rewrite <- (le_uniqueness _ _ (LPP Hjk) Hlk). rewrite le_uniqueness_refl. reflexivity. + Opaque filter_step. simpl filter in *. Transparent filter_step. assert (Hlk' := le_trans Hlj (LPP Hjk)). rewrite <- (le_uniqueness _ _ (le_P Hlk') Hlk). rewrite <- (le_uniqueness _ _ (le_P (LSS Hlk)) HlkS). Opaque choices. change (le_P Hlj) with (id (le_P Hlj)). Opaque id. simpl filter_step at 1. Transparent id. unfold id. Transparent choices. set (P x:= choices n d p c Hrc (d p c (LUP p Hrc) x)). set (Q x:= subbranching n c Hrc (fun c0 Hc => choices n d p c0 Hc (d p c0 (@LUP c0 n p Hc) x))). rewrite <- (rew_pair _ P Q). (* for P and Q not to be given, a powerful h.o. unification is needed *) unfold P, Q. clear P Q. Opaque choices. change (le_P (LSS Hlk)) with (id (le_P (LSS Hlk))). Opaque id. simpl filter_step at 4. Transparent id. unfold id. Transparent choices. apply f_equal2. (* Why "f_equal" is so slow? *) * fold plus. simpl. destruct (le_pred_out Hlk') as (k',e). move e before k. generalize dependent k. intros k e. rewrite <- e. intros. simpl. clear k e. rename k' into k. destruct (le_pred_out Hlj) as (j',e). move e before j. generalize dependent j. intros j e. rewrite <- e. intros. simpl. clear j e. rename j' into j. set (f:=filter p k c _ _ _). set (z:=filter_step p j c _ _ _ _ _). rewrite <- (map_subst f _ z). set (f':=filter p j c _ _ _). set (z':=filter_step p k.+1 c _ _ _ _ _). rewrite <- (map_subst f' _ z'). unfold f', z', f, z. clear f' z' f z. simpl in HrkS. (* needed to avoid plus appearing unfolded after next line *) rewrite <- (IHp j) with (Hlk:=LPP Hlk') (Hjk:=LPP Hjk). rewrite rew_map with (f:=d p c (LUP _ Hrc)). rewrite rew_map with (f:=d p k _). do 2 rewrite rew_compose. rewrite rew_map with (f:=d p j _). do 2 rewrite rew_compose. Transparent LUP LPP. Require Import Setoid. setoid_rewrite <- (fcomm _ _ _ _ _ _ Hlj Hlk' _ Hjk). unfold LUP. destruct (eq_trans _ (eq_trans _ _)). Opaque le_uniqueness. simpl. set (f:=fun H => d p k (LPP (LPP HrkS)) (d p.+1 j H (d p.+2 c (LES (LES (LUP p Hrc))) x))). fold plus. generalize (@LES j (p+n) (@LPP j (p+n) Hrj)). generalize (@LPP j (p+n).+1 (@LES j.+1 (p+n).+1 Hrj)). intros. rewrite (le_uniqueness j (p+n).+1 l l0). simpl (rew eq_refl in _). reflexivity. * destruct Hrc. { simpl. destruct (dcomm _ _ _ _ _ _ _). reflexivity. } { simpl. apply IHHlj. } Implicit Arguments filter []. Implicit Arguments filter_step []. Defined. End Combinations. (***********************************************************) (** * 3. The main construction *) (***********************************************************) Definition Type2 := Type. Definition Type1 := Type : Type2. (** The type of a truncated family of (augmented) semi-simplicial types *) (** The main component is [sst] which is the Sigma-type of points, segments, *) (** triangles, up to some points, augmented at its origin with a "color" *) (* To have "n" a component of the record is not a very good idea; it would have been more natural to have it as a parameter of the record *) Record SSTYPE := { order : nat; sst : Type2; F : sst -> nat -> Type1; d : forall {X:sst} p k, k <= p+order -> F X p.+1 -> F X p; dcomm : forall (X:sst) p i k (Hik:i.+1<=k.+1) (Hri:i<=p+order) (HrkS:k.+1<=(p+order).+1) (x:F X p.+2), d p k (LPP HrkS) (d p.+1 i (LES Hri) x) = d p i Hri (d p.+1 k.+1 HrkS x) }. Section SSTYPE. Axiom UIP : forall A (x y : A) (H1 H2 : x = y), H1 = H2. (* Some intermediate lemma to avoid the proof of sstype to be too large *) Lemma dcommS : forall (sstype : nat -> SSTYPE) (n : nat) (ordern := order (sstype n) : nat) (sstn := sst (sstype n) : Type2) (Fn := F (sstype n) : sst (sstype n) -> nat -> Type1) (dn := @d (sstype n) : forall (X : sst (sstype n)) (p k : nat), k <= p + order (sstype n) -> F (sstype n) X p.+1 -> F (sstype n) X p) (dcommn := dcomm (sstype n) : forall X, commute1 (F:=Fn X) ordern (dn X)) (orderSn := ordern.+1 : nat) (sstSn := {X : sstn & Fn X 0 -> Type1} : Type) (FSn := (fun (X : sstSn) (p : nat) => {x : Fn X.1 p.+1 & choices X.2 ordern (dn X.1) p.+1 0 (le_0 ordern) x}) : sstSn -> nat -> Type) (dSn := (fun (X : sstSn) (p i : nat) (H : i <= p + ordern.+1) (x : FSn X p.+1) => {{dn X.1 p.+1 i (LSWING H) x.1, filter X.2 ordern (dn X.1) (dcommn X.1) p.+1 i 0 (le_0 ordern) (le_0 i) (LSWING H) x.1 x.2}}) : forall (X : sstSn) (p i : nat), i <= p + ordern.+1 -> FSn X p.+1 -> {x:_& choices X.2 ordern (dn X.1) p.+1 0 (le_0 ordern) x}), forall (X : sstSn), commute1 (F:=FSn X) orderSn (dSn X). Proof. intros. red. intros. change (p+?n).+1 with (p.+1+n) in HrkS. set (IHn' := dcommn X.1 p.+1 j k Hjk (LSWING Hrj) (LSWING HrkS) x.1). unfold dSn at 1 3. rewrite LSWINGPP. unfold dSn. rewrite LSWINGES. refine (mk_sig_eq IHn' _). apply filter_commute1. red. intros. apply UIP. Defined. (** The construction of what is a n-truncated family of (augmented) semi-simplicial types *) Fixpoint sstype (n:nat) : SSTYPE. Proof. destruct n. - exact {| order := 0; sst := unit; F X p := unit; d X p k H x := x; dcomm X p i k Hik Hri HrkS x := eq_refl |}. - refine (let ordern := (sstype n).(order) in let sstn := (sstype n).(sst) in let Fn := (sstype n).(F) in let dn := (sstype n).(@d) in let dcommn := (sstype n).(dcomm) in let orderSn := ordern.+1 in let sstSn := {X:sstn & Fn X 0 -> Type1} in let FSn (X:sstSn) p := {x:Fn X.1 (p.+1) & choices X.2 ordern (dn X.1) p.+1 0 (le_0 ordern) x} in let dSn {X:sstSn} p i (H:i<=p+ordern.+1) (x:FSn X p.+1) := {{ (dn X.1 p.+1 i (LSWING H) x.1), (filter X.2 ordern (dn X.1) (dcommn X.1) p.+1 i 0 (le_0 ordern) (le_0 i) (LSWING H) x.1 x.2) }} in {| order := orderSn; sst := sstSn; F := FSn; d X := dSn; dcomm X := dcommS sstype n X |}). Defined. End SSTYPE. (**************************************************************************) (** * 4 The family of (augmented) semi-simplicial types properly speaking *) (**************************************************************************) (** It is defined coinductively *) Notation F_of n := (sstype n).(F). CoInductive SST_of n (X:sst (sstype n)) : Type := cons { this : F_of n X 0 -> Type; next : SST_of n.+1 {{X,this}} }. Implicit Arguments cons [n X]. Implicit Arguments this [n X]. Implicit Arguments next [n X]. Definition nextpair n (XS : {X : sst (sstype n) & SST_of n X }) : {X: sst (sstype n.+1) & SST_of n.+1 X} := {{ {{XS.1, this XS.2}}, next XS.2 }}. Notation SST := (SST_of 0 tt). Fixpoint nextpairfrom n (S : SST) : {X: sst (sstype n) & SST_of n X} := match n with | 0 => {{tt,S}} | n.+1 => nextpair n (nextpairfrom n S) end. Definition thissst n (S : SST) : sst (sstype n) := (nextpairfrom n S).1. Definition thisSST n (S : SST) : SST_of n (thissst n S) := (nextpairfrom n S).2. Definition thisX n (S : SST) : F_of n (thissst n S) 0 -> Type := this (thisSST n S). Section Faces. Variable S : SST. (** The type of augmented n-semi-simplex in family of semi-simplicial S *) (** total 1 = points *) (** total 2 = segments *) (** total 3 = triangles *) Definition total n := {x:F_of n (thissst n S) 0 & thisX n S x}. (** The usual face operation from an augmented n-semi-simplex in family S *) Definition face n i (H:i<=order (sstype n)) (x:total n.+1) : total n := {{ (sstype n).(d) 0 i H x.1.1, get _ 0 i _ (le_0 i) H (rew [fun H => branching _ _ H _] le_uniqueness _ _ (le_0 (order (sstype n))) (le_trans (le_0 i) H) in x.1.2) }}. Example test : forall x, face 1 1 le_n (face 2 1 (le_P le_n) x) = face 1 1 le_n (face 2 2 le_n x). (* The following exhausts the memory and fails: vm_compute. *) Admitted. (** Some limited examples of computing faces *) Remove Printing Let sigT. Remove Printing Let prod. Notation "x .l" := (match x with {{p, _}} => p end) (at level 1, left associativity, format "x .l"). Notation "x .r" := (match x with {{_, p}} => p end) (at level 1, left associativity, format "x .r"). Notation "x ._l" := (match x as y return _ with {{p, _}} => p end) (at level 1, left associativity, format "x ._l"). Notation "x ._r" := (match x as y return _ with {{_, p}} => p end) (at level 1, left associativity, format "x ._r"). Notation "x ._1" := (match x with (p, _) => p end) (at level 1, left associativity, format "x ._1"). Notation "x ._2" := (match x with (_, p) => p end) (at level 1, left associativity, format "x ._2"). Notation "x ._this" := (match x with cons p _ => p end) (at level 1, left associativity, format "x ._this"). Notation "x ._next" := (match x with cons _ p => p end) (at level 1, left associativity, format "x ._next"). Notation "x ._this" := (match x as y return _ with cons p _ => p end) (at level 1, left associativity, format "x ._this"). Notation "x ._next" := (match x as y return _ with cons _ p => p end) (at level 1, left associativity, format "x ._next"). Notation "x ._this" := (match x as y return _ with cons p _ => p end) (at level 1, left associativity, format "x ._this"). Notation "x ._next" := (match x as y return _ with cons _ p => p end) (at level 1, left associativity, format "x ._next"). Notation "[ x × .. × y ]" := (x * .. (y * unit) ..)%type (at level 0). Time Eval vm_compute in total 2. (* The following exhausts the memory and fails: Time Eval vm_compute in sstype 2. *) End Faces. (***********************) (** * 5. Examples *) (***********************) (** Product *) Section Product. Variables S1 S2:SST. Record Product n := { sstprod : (sstype n).(sst); proj1 : forall p, F_of n sstprod p -> F_of n (thissst n S1) p; proj2 : forall p, F_of n sstprod p -> F_of n (thissst n S2) p; projcomm1 : forall (p i : nat) (Hi : i <= p + (order _)) x, (proj1 p (d _ p i Hi x) = d _ p i Hi (proj1 p.+1 x)); projcomm2 : forall (p i : nat) (Hi : i <= p + (order _)) x, (proj2 p (d _ p i Hi x) = d _ p i Hi (proj2 p.+1 x)) }. Lemma map_subbranching : forall n c (Hc : c <= n) {A B} (X : forall c0 : nat, c0 <= n -> A -> Type) (Y : forall c0 : nat, c0 <= n -> B -> Type) (f : A -> B), (forall c Hc x, X c Hc x -> Y c Hc (f x)) -> forall x, subbranching n c Hc (fun c Hc => X c Hc x) -> subbranching n c Hc (fun c Hc => Y c Hc (f x)). Proof. intros * H x s. revert n c Hc X Y H s. fix 3. destruct Hc as [|n]; intros. - exact tt. - split. + apply H, (fst s). + apply (map_subbranching n c.+1 Hc X Y H (snd s)). Defined. Lemma map_branching : forall n {A B} (X : forall c0 : nat, c0 <= n -> A -> Type) (Y : forall c0 : nat, c0 <= n -> B -> Type) (f : A -> B), (forall c Hc x, X c Hc x -> Y c Hc (f x)) -> forall c (Hc : c <= n) x, branching n c Hc (fun c Hc => X c Hc x) -> branching n c Hc (fun c Hc => Y c Hc (f x)). Proof. intros * H * s; split. - apply H, (fst s). - apply map_subbranching with X. assumption. apply (snd s). Defined. Lemma map_choices : forall {n} {F G:nat -> Type} (Y:F 0 -> Type) (Z:G 0 -> Type) {f:forall p, F p -> G p} (g:forall x, Y x -> Z (f _ x)) {d e} (h:forall p i Hi x, f p (d _ i Hi x) = e _ i Hi (f _ x)) p c Hc x, choices Y n d p c Hc x -> choices Z n e p c Hc (f p x). Proof. induction p; intros. - apply g. assumption. - simpl in X |- *. apply (map_branching n (fun c Hc x => choices Y _ d0 _ _ Hc (d0 _ _ (LUP p Hc) x)) (fun c Hc x => choices _ _ _ _ _ _ (e _ _ _ x))). + intros. rewrite <- h. apply IHp. assumption. + assumption. Defined. Definition pcommute1 n F0 G (d0:forall p i, i <= p+n -> F0 p.+1 -> F0 p) (e:forall p i, i <= p+n -> G p.+1 -> G p) f := forall (p i : nat) (Hri : i <= p + n) (x : F0 p.+1), f p (d0 p i Hri x) = e p i Hri (f p.+1 x). Definition pcommute2 n F0 G d0 e f (dcomm0 : commute1 n d0) (ecomm : commute1 n e) (pcomm : pcommute1 n F0 G d0 e f) := forall p i k Hik Hli Hri x, eq_trans (f_equal (f p) (dcomm0 p i k Hik (LUP p Hli) Hri x)) (eq_trans (pcomm p i (LUP p Hli) (d0 p.+1 k.+1 Hri x)) (f_equal (e p i (LUP p Hli)) (pcomm p.+1 k.+1 Hri x))) = eq_trans (pcomm p k (LPP Hri) (d0 p.+1 i (LUP p.+1 Hli) x)) (eq_trans (f_equal (e p k (LPP Hri)) (pcomm p.+1 i (LUP p.+1 Hli) x)) (ecomm p i k Hik (LUP p Hli) Hri (f p.+2 x))). Lemma map_choices_filter_commute : forall {n} {F G:nat -> Type} (Y:F 0 -> Type) (Z:G 0 -> Type) f g d e dcomm ecomm (pcomm1 : pcommute1 n F G d e f) (pcomm2 : pcommute2 n F G d e f dcomm ecomm pcomm1) p c Hc i Hri Hli x y, rew pcomm1 p i Hri x in map_choices Y Z g pcomm1 p c Hc (d p i (Hri) x) (filter Y n d dcomm p i c Hc Hli Hri x y) = filter Z n e ecomm p i c Hc Hli Hri (f p.+1 x) (map_choices Y Z g pcomm1 p.+1 c Hc x y). Proof. intros. generalize dependent c. generalize dependent i. induction p; intros. - change 1 with (id 1). Opaque id. simpl. Transparent id. unfold id. generalize dependent Hc. intro. rewrite (le_uniqueness c n Hc (le_trans Hli Hri)). intro y. rewrite (le_uniqueness_refl). Opaque map_choices. simpl (rew eq_refl in _). Transparent map_choices. induction Hli as [|c]. + Transparent LUP. simpl. reflexivity. + Opaque map_choices. simpl. Transparent map_choices. apply IHHli. apply (le_trans Hli Hri). - change (p.+1) with (id p.+1). Opaque id. simpl. Transparent id. unfold id. Implicit Arguments map_branching [A B X Y f]. Implicit Arguments map_subbranching [A B X Y f]. simpl (map_choices _ _ _ _ p.+1) at 1. lazy beta. simpl (filter _ _ _ _ p.+1). induction Hli as [|c i]. + Opaque le_uniqueness. simpl. destruct (le_uniqueness _ _ (le_P (le_n_S (LUP p Hc))) Hri). reflexivity. + Opaque map_choices choices map_branching (*filter_step*). Opaque LUP. simpl. destruct (le_pred_out Hli) as (i',Heq). destruct Heq. simpl. rename i' into i. Transparent map_branching. unfold map_branching at 1. simpl fst. simpl snd. Transparent choices. set (P y := @choices G Z n e p c Hc (e p c (@LUP c n p Hc) y)). set (Q y := subbranching n c Hc (fun (c0 : nat) (Hc0 : le c0 n) => @choices G Z n e p c0 Hc0 (e p c0 (@LUP c0 n p Hc0) y))). rewrite <- (rew_pair _ P Q). apply f_equal2. * clear IHHli. rewrite <- (map_subst (filter Z n e ecomm p i c Hc (LPP Hli) (LPP Hri))). rewrite <- IHp. rewrite <- (map_subst (map_choices Y Z g pcomm1 p c Hc)). fold (choices Z n e). fold plus. unfold P. rewrite rew_map with (f:=e p c (LUP p Hc)). rewrite rew_map with (f:=f p). do 2 rewrite rew_compose. rewrite rew_map with (f:=e p i (LPP Hri)). do 2 rewrite rew_compose. f_equal. apply pcomm2. * destruct Hc; simpl. { destruct (pcomm1 _ _ _ _). reflexivity. } { unfold map_branching in IHHli. apply IHHli. } Defined. Fixpoint product n : Product n. Proof. destruct n as [|n]. - refine {| sstprod := tt : sst (sstype 0); proj1 := fun p x => tt; proj2 := fun p x => tt; projcomm1 p i Hi x := eq_refl; projcomm2 p i Hi x := eq_refl |}. - set (Xprod := fun x : F_of n (sstprod n (product n)) 0 => ((thissst n.+1 S1).2 (proj1 n (product n) 0 x) * (thissst n.+1 S2).2 (proj2 n (product n) 0 x))%type). refine {| sstprod := existT (fun X => (F_of n) X 0 -> Type) (sstprod n (product n)) Xprod : sst (sstype n.+1); proj1 p x := {{proj1 n (product n) p.+1 x.1, map_choices Xprod (thissst n.+1 S1).2 (fun x => @fst _ _) (projcomm1 n (product n)) _ _ _ x.1 x.2}}; proj2 p x := {{proj2 n (product n) p.+1 x.1, map_choices Xprod (thissst n.+1 S2).2 (fun x => @snd _ _) (projcomm2 n (product n)) _ _ _ x.1 x.2}}; projcomm1 := _; projcomm2 := _ |}. + intros. change (order (_ n)) with (order (sstype n)). change (sst (_ n)) with (sst (sstype n)). change (F (_ n)) with (F (sstype n)). change (@d (_ n)) with (@d (sstype n)). Opaque choices filter dcomm. simpl (d (sstype n.+1)). lazy beta. simpl proj1. simpl projT1. apply mk_sig_eq with (H:=projcomm1 _ (product n) _ _ _ _). Opaque thissst map_choices. simpl {{_,_}}.2 at 1 2. apply map_choices_filter_commute. red; intros. apply UIP. + intros. change (order (_ n)) with (order (sstype n)). change (sst (_ n)) with (sst (sstype n)). change (F (_ n)) with (F (sstype n)). change (@d (_ n)) with (@d (sstype n)). Opaque choices filter dcomm. simpl (d (sstype n.+1)). lazy beta. simpl proj2. simpl projT1. apply mk_sig_eq with (H:=projcomm2 _ (product n) _ _ _ _). Opaque thissst map_choices. simpl {{_,_}}.2 at 1 2. apply map_choices_filter_commute. red; intros. apply UIP. Defined. (* The next definition needs a lot of memory in Coq 8.4; the rest of the section can be skipped if memory is too low; trunk from Jan 2014 is ok *) CoFixpoint PRODUCT_of n : SST_of n (sstprod _ (product n)) := cons (sstprod _ (product n.+1)).2 (PRODUCT_of n.+1). Definition PRODUCT : SST := PRODUCT_of 0. End Product. (** Standard simplices *) (** We reach here some limit of Coq *) Section Standard. Notation "x < y" := (x.+1 <= y). Record Standard n := { sststandard : sst (sstype n); mklt : F (sstype n) sststandard 0 -> F (sstype n) sststandard 0 -> Type1; mklin : F (sstype n) sststandard 0 -> Type1 }. Definition standard (m:nat) n : Standard n. set (Y0 := tt : sst (sstype 0)). set (Y1 := {{Y0, fun _ : unit => unit : Type1}} : sst (sstype 1)). set (Y2 := {{Y1, fun _ => {p:nat & p<=m} : Type1}} : sst (sstype 2)). destruct n. refine {| sststandard := Y0; mklt := fun _ _ => unit; mklin := fun _ => unit |}. destruct n. refine {| sststandard := Y1; mklt := fun _ _ => unit; mklin := fun _ => unit |}. induction n. refine {| sststandard := Y2; mklt := _; mklin := _ |}. { intros (x1,(_,((y1,_),_))) (x,(_,((y2,_),_))). exact (y1 < y2). } { intros (x,((y1,_),((y2,_),_))). exact (y1 < y2). } set (Yn := {{sststandard _ IHn, mklin n.+2 IHn}} : sst (sstype n.+3)). refine {| sststandard := Yn; mklt := _; mklin := _ |}. { change (n.+2) with (id n.+2). Opaque id. simpl. Transparent id. unfold id. intros (x1,_) (x2,_). set (x1' := d (sstype n.+2) 0 1 (le_n_S (le_0 _)) x1). set (x2' := d (sstype n.+2) 0 1 (le_n_S (le_0 _)) x2). apply (mklt _ IHn x1' x2'). } { change (n.+2) with (id n.+2). Opaque id. simpl. Transparent id. unfold id. intros (x,_). set (x1 := d (sstype _) 0 0 (le_0 _) x). set (x2 := d (sstype n.+2) 0 1 (le_n_S (le_0 _)) x). apply prod. apply (mklin _ IHn x1). apply (mklt _ IHn x1 x2). } Admitted. (* Proof is completed but "Defined." runs out of memory *) (** If "standard" were definable, we could define the following: CoFixpoint STANDARD_of m n : SST_of n (sststandard _ (standard m n)) := @cons _ (sststandard n.+1 (standard m n.+1)).1 (sststandard _ (standard m n.+1)).2 (STANDARD_of m n.+1). Definition STANDARD m : SST := STANDARD_of m 0. *) End Standard.