Makefile

@@ -6,7 +6,7 @@ theories: $(COQMAKEFILE) FORCE
 validate: $(COQMAKEFILE) FORCE
 	$(MAKE) -f $(COQMAKEFILE) validate
 
-$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
+$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 	$(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE)
 
 install: $(COQMAKEFILE)
@@ -15,13 +15,13 @@ install: $(COQMAKEFILE)
 uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
-theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v : syntax.sig
-	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
+theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
+	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v theories/Autosubst2/unscoped.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 
 FORCE:

theories/Autosubst2/fintype.v

@@ -0,0 +1,419 @@
+(** * Autosubst Header for Scoped Syntax
+    Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact.
+
+Version: December 11, 2019.
+*)
+Require Import core.
+Require Import Setoid Morphisms Relation_Definitions.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
+  match p with eq_refl => eq_refl end.
+
+Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
+  match q with eq_refl => match p with eq_refl => eq_refl end end.
+
+(** ** Primitives of the Sigma Calculus
+    We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type.
+*)
+
+Fixpoint fin (n : nat) : Type :=
+  match n with
+  | 0 => False
+  | S m => option (fin m)
+  end.
+
+(** Renamings and Injective Renamings
+     _Renamings_ are mappings between finite types.
+*)
+Definition ren (m n : nat) : Type := fin m -> fin n.
+
+Definition id {X} := @Datatypes.id X.
+
+Definition idren {k: nat} : ren k k := @Datatypes.id (fin k).
+
+(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *)
+Definition var_zero {n : nat} : fin (S n) := None.
+
+Definition null {T} (i : fin 0) : T := match i with end.
+
+Definition shift {n : nat} : ren n (S n) :=
+  Some.
+
+(** Extension of Finite Mappings
+    Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows:
+*)
+Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X :=
+  match m with
+  | None => x
+  | Some i => f i
+  end.
+
+#[ export ]
+Hint Opaque scons : rewrite.
+
+(** ** Type Class Instances for Notation *)
+
+(** *** Type classes for renamings. *)
+
+Class Ren1 (X1  : Type) (Y Z : Type) :=
+  ren1 : X1 -> Y -> Z.
+
+Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
+  ren2 : X1 -> X2 -> Y -> Z.
+
+Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
+  ren3 : X1 -> X2 -> X3 -> Y -> Z.
+
+Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
+  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
+
+Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
+  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
+
+Module RenNotations.
+  Notation "s ⟨ xi1 ⟩" := (ren1  xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
+
+  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
+
+  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
+End RenNotations.
+
+(** *** Type Classes for Substiution *)
+
+Class Subst1 (X1 : Type) (Y Z: Type) :=
+  subst1 : X1 -> Y -> Z.
+
+Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
+  subst2 : X1 -> X2 -> Y  -> Z.
+
+Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
+  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
+
+Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
+  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
+
+Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
+  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
+
+Module SubstNotations.
+  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
+
+  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
+End SubstNotations.
+
+(** ** Type Class for Variables *)
+Class Var X Y :=
+  ids : X -> Y.
+
+
+(** ** Proofs for substitution primitives *)
+
+(** Forward Function Composition
+    Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour.
+    That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *)
+
+Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
+
+Module CombineNotations.
+  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
+
+  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
+
+  #[ global ]
+  Open Scope fscope.
+  #[ global ]
+  Open Scope subst_scope.
+End CombineNotations.
+
+Import CombineNotations.
+
+
+(** Generic lifting operation for renamings *)
+Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) :=
+  var_zero .: xi >> shift.
+
+(** Generic proof that lifting of renamings composes. *)
+Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
+  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
+Proof.
+  intros [x|].
+  - cbn. unfold funcomp. now rewrite <- E.
+  - reflexivity.
+Qed.
+
+Arguments up_ren_ren {k l m} xi zeta rho E.
+
+Lemma fin_eta {X} (f g : fin 0 -> X) :
+  pointwise_relation _ eq f g.
+Proof. intros []. Qed.
+
+(** Eta laws *)
+Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) :
+  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_eta_id' {n : nat} :
+  pointwise_relation (fin (S n)) eq (var_zero .: shift) id.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) :
+  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
+Proof. intros x. destruct x; reflexivity. Qed.
+
+(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *)
+(*   pointwise_relation _ eq (funcomp (scons s f) shift) f. *)
+(* Proof. *)
+(*   reflexivity. *)
+(* Qed. *)
+
+(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *)
+(*   (scons s f (shift x)) = f x. *)
+(* Proof. *)
+(*   reflexivity. *)
+(* Qed. *)
+
+(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
+#[export] Instance scons_morphism {X: Type} {n:nat} :
+  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n).
+Proof.
+  intros t t' -> sigma tau H.
+  intros [x|].
+  cbn. apply H.
+  reflexivity.
+Qed.
+
+#[export] Instance scons_morphism2 {X: Type} {n: nat} :
+  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n).
+Proof.
+  intros ? t -> sigma tau H ? x ->.
+  destruct x as [x|].
+  cbn. apply H.
+  reflexivity.
+Qed.
+
+(** ** Variadic Substitution Primitives *)
+
+Fixpoint shift_p (p : nat) {n} : ren n (p + n) :=
+  fun n => match p with
+        | 0 => n
+        | S p => Some (shift_p p n)
+        end.
+
+Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n)  -> X.
+Proof.
+  destruct m.
+  - intros n f g. exact g.
+  - intros n f g. cbn. apply scons.
+    + exact (f var_zero).
+    + apply scons_p.
+      * intros z. exact (f (Some z)).
+      * exact g.
+Defined.
+
+#[export] Hint Opaque scons_p : rewrite.
+
+#[export] Instance scons_p_morphism {X: Type} {m n:nat} :
+  Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n).
+Proof.
+  intros sigma sigma' Hsigma tau tau' Htau.
+  intros x.
+  induction m.
+  - cbn. apply Htau.
+  - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
+    destruct x as [x|].
+    + cbn. apply IHm.
+      intros ?. apply Hsigma.
+    + cbn. apply Hsigma.
+Qed.
+
+#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} :
+  Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n).
+Proof.
+  intros sigma sigma' Hsigma tau tau' Htau ? x ->.
+  induction m.
+  - cbn. apply Htau.
+  - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
+    destruct x as [x|].
+    + cbn. apply IHm.
+      intros ?. apply Hsigma.
+    + cbn. apply Hsigma.
+Qed.
+
+Definition zero_p {m : nat} {n} : fin m -> fin (m + n).
+Proof.
+  induction m.
+  - intros [].
+  - intros [x|].
+    + exact (shift_p 1 (IHm x)).
+    + exact var_zero.
+Defined.
+
+Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z:
+  (scons_p  f g) (zero_p  z) = f z.
+Proof.
+ induction m.
+  - inversion z.
+  - destruct z.
+    + simpl. simpl. now rewrite IHm.
+    + reflexivity.
+Qed.
+
+Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) :
+  pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f.
+Proof.
+  intros z.
+  unfold funcomp.
+  induction m.
+  - inversion z.
+  - destruct z.
+    + simpl. now rewrite IHm.
+    + reflexivity.
+Qed.
+
+Lemma scons_p_tail' X  m n (f : fin m -> X) (g : fin n -> X) z :
+  scons_p  f g (shift_p m z) = g z.
+Proof. induction m; cbn; eauto. Qed.
+
+Lemma scons_p_tail_pointwise X  m n (f : fin m -> X) (g : fin n -> X) :
+  pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g.
+Proof. intros z. induction m; cbn; eauto. Qed.
+
+Lemma destruct_fin {m n} (x : fin (m + n)):
+  (exists x', x = zero_p  x') \/ exists x', x = shift_p m x'.
+Proof.
+  induction m; simpl in *.
+  - right. eauto.
+  - destruct x as [x|].
+    + destruct (IHm x) as [[x' ->] |[x' ->]].
+      * left. now exists (Some x').
+      * right. eauto.
+    + left. exists None. eauto.
+Qed.
+
+Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) :
+  pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)).
+Proof.
+  intros x.
+  destruct (destruct_fin x) as [[x' ->]|[x' ->]].
+  (* TODO better way to solve this? *)
+  - revert x'.
+    apply pointwise_forall.
+    change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h).
+    now setoid_rewrite scons_p_head_pointwise.
+  - revert x'.
+    apply pointwise_forall.
+    change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h).
+    change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)).
+    now rewrite !scons_p_tail_pointwise.
+Qed.
+
+
+Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z:
+  (forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z.
+Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed.
+
+(** Generic n-ary lifting operation. *)
+Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n)  :=
+   scons_p  (zero_p ) (xi >> shift_p _).
+
+Arguments upRen_p p {m n} xi.
+
+(** Generic proof for composition of n-ary lifting. *)
+Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
+  forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x.
+Proof.
+  intros x. destruct (destruct_fin x) as [[? ->]|[? ->]].
+  - unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'.
+  - unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'.
+    now rewrite <- E.
+Qed.
+
+
+Arguments zero_p m {n}.
+Arguments scons_p  {X} m {n} f g.
+
+Lemma scons_p_eta {X} {m n} {f : fin m -> X}
+      {g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}:
+  (forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z.
+Proof.
+  intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]].
+  - rewrite scons_p_head'. eauto.
+  - rewrite scons_p_tail'. eauto.
+Qed.
+
+Arguments scons_p_eta {X} {m n} {f g} h {z}.
+Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}.
+
+(** ** Notations for Scoped Syntax *)
+
+Module ScopedNotations.
+  Include RenNotations.
+  Include SubstNotations.
+  Include CombineNotations.
+
+(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
+
+  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
+
+  Notation "↑" := (shift) : subst_scope.
+
+  #[global]
+  Open Scope fscope.
+  #[global]
+  Open Scope subst_scope.
+End ScopedNotations.
+
+
+(** ** Tactics for Scoped Syntax *)
+
+Tactic Notation "auto_case" tactic(t) :=  (match goal with
+                                           | [|- forall (i : fin 0), _] => intros []; t
+                                           | [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t
+                                           | [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t
+                                           | [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t
+                                           | [|- forall (i : fin (S _)), _] =>  intros [?|]; t
+                                           end).
+
+#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances.
+
+(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
+Ltac fsimpl :=
+  repeat match goal with
+         | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
+         | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
+         | [|- context [id ?s]] => change (id s) with s
+         | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *)
+         (* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *)
+         | [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s
+         | [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m)
+           (* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *)
+         | [|- context[idren >> ?f]] => change (idren >> f) with f
+         | [|- context[?f >> idren]] => change (f >> idren) with f
+         | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
+         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce
+         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce
+         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
+         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
+         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
+         | [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce
+         | [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce
+         (* | _ => progress autorewrite with FunctorInstances *)
+         | [|- context[funcomp (scons_p _ _ _) (zero_p _)]] =>
+           first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ]
+         | [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head'
+         | [|- context[funcomp (scons_p _ _ _) (shift_p _)]] =>
+           first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ]
+         | [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail'
+         | _ => first [progress minimize | progress cbn [shift scons scons_p] ]
+         end.

theories/Autosubst2/unscoped.v

@@ -1,213 +0,0 @@
-(** * Autosubst Header for Unnamed Syntax
-
-Version: December 11, 2019.
- *)
-
-(* Adrian:
- I changed this library a bit to work better with my generated code.
- 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
- 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
-Require Import core.
-Require Import Setoid Morphisms Relation_Definitions.
-
-Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
-  match p with eq_refl => eq_refl end.
-
-Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
-  match q with eq_refl => match p with eq_refl => eq_refl end end.
-
-(** ** Primitives of the Sigma Calculus. *)
-
-Definition shift  := S.
-
-Definition var_zero := 0.
-
-Definition id {X} := @Datatypes.id X.
-
-Definition scons {X: Type} (x : X) (xi : nat -> X) :=
-  fun n => match n with
-        | 0 => x
-        | S n => xi n
-        end.
-
-#[ export ]
-Hint Opaque scons : rewrite.
-
-(** ** Type Class Instances for Notation
-Required to make notation work. *)
-
-(** *** Type classes for renamings. *)
-
-Class Ren1 (X1  : Type) (Y Z : Type) :=
-  ren1 : X1 -> Y -> Z.
-
-Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
-  ren2 : X1 -> X2 -> Y -> Z.
-
-Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
-  ren3 : X1 -> X2 -> X3 -> Y -> Z.
-
-Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
-  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
-
-Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
-  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
-
-Module RenNotations.
-  Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
-
-  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
-
-  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
-End RenNotations.
-
-(** *** Type Classes for Substiution *)
-
-Class Subst1 (X1 : Type) (Y Z: Type) :=
-  subst1 : X1 -> Y -> Z.
-
-Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
-  subst2 : X1 -> X2 -> Y  -> Z.
-
-Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
-  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
-
-Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
-  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
-
-Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
-  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
-
-Module SubstNotations.
-  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
-
-  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
-End SubstNotations.
-
-(** *** Type Class for Variables *)
-
-Class Var X Y :=
-  ids : X -> Y.
-
-#[export] Instance idsRen : Var nat nat := id.
-
-(** ** Proofs for the substitution primitives. *)
-
-Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
-
-Module CombineNotations.
-  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
-
-  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
-
-  #[ global ]
-  Open Scope fscope.
-  #[ global ]
-  Open Scope subst_scope.
-End CombineNotations.
-
-Import CombineNotations.
-
-
-(** A generic lifting of a renaming. *)
-Definition up_ren (xi : nat -> nat) :=
-  0 .: (xi >> S).
-
-(** A generic proof that lifting of renamings composes. *)
-Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) :
-  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
-Proof.
-  intros [|x].
-  - reflexivity.
-  - unfold up_ren. cbn. unfold funcomp. f_equal. apply E.
-Qed.
-
-(** Eta laws. *)
-Lemma scons_eta' {T} (f : nat -> T) :
-  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
-Proof. intros x. destruct x; reflexivity. Qed.
-
-Lemma scons_eta_id' :
-  pointwise_relation _ eq (var_zero .: shift) id.
-Proof. intros x. destruct x; reflexivity. Qed.
-
-Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
-  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
-Proof. intros x. destruct x; reflexivity. Qed.
-
-(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
-#[export] Instance scons_morphism {X: Type} :
-  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
-Proof.
-  intros ? t -> sigma tau H.
-  intros [|x].
-  cbn. reflexivity.
-  apply H.
-Qed.
-
-#[export] Instance scons_morphism2 {X: Type} :
-  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
-Proof.
-  intros ? t -> sigma tau H ? x ->.
-  destruct x as [|x].
-  cbn. reflexivity.
-  apply H.
-Qed.
-
-(** ** Generic lifting of an allfv predicate *)
-Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p.
-
-(** ** Notations for unscoped syntax *)
-Module UnscopedNotations.
-  Include RenNotations.
-  Include SubstNotations.
-  Include CombineNotations.
-  
-  (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
-
-  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
-
-  Notation "↑" := (shift) : subst_scope.
-
-  #[global]
-  Open Scope fscope.
-  #[global]
-  Open Scope subst_scope.
-End UnscopedNotations.
-
-(** ** Tactics for unscoped syntax *)
-
-(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *)
-Tactic Notation "auto_case" tactic(t) :=  (match goal with
-                                           | [|- forall (i : nat), _] => intros []; t
-                                           end).
-
-
-(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
-Ltac fsimpl :=
-  repeat match goal with
-         | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
-         | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
-         | [|- context [id ?s]] => change (id s) with s
-         | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h))
-         | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v
-         | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v
-         | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n)
-         | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
-         | [|- context[var_zero]] =>  change var_zero with 0
-         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f)
-         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta'
-         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
-         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
-         (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
-         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
-         | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
-                        end.

theories/fp_red.v

@@ -7,7 +7,7 @@ Require Import Arith.Wf_nat.
 Require Import Psatz.
 From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
 From Hammer Require Import Tactics.
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
 
 Ltac2 spec_refl () :=
   List.iter
@@ -22,7 +22,7 @@ Ltac spec_refl := ltac2:(spec_refl ()).
 
 (* Trying my best to not write C style module_funcname *)
 Module Par.
-  Inductive R : PTm -> PTm ->  Prop :=
+  Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (***************** Beta ***********************)
   | AppAbs a0 a1 b0 b1 :
     R a0 a1 ->
@@ -72,35 +72,35 @@ Module Par.
   | Bot :
     R PBot PBot.
 
-  Lemma refl (a : PTm) : R a a.
-    elim : a; hauto ctrs:R.
+  Lemma refl n (a : PTm n) : R a a.
+    elim : n /a; hauto ctrs:R.
   Qed.
 
-  Lemma AppAbs' a0 a1 (b0 b1 t : PTm) :
+  Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) :
     t = subst_PTm (scons b1 VarPTm) a1 ->
     R a0 a1 ->
     R b0 b1 ->
     R (PApp (PAbs a0) b0) t.
   Proof. move => ->. apply AppAbs. Qed.
 
-  Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t :
+  Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t :
     t = (if p is PL then a1 else b1) ->
     R a0 a1 ->
     R b0 b1 ->
     R (PProj p (PPair a0 b0)) t.
   Proof.  move => > ->. apply ProjPair. Qed.
 
-  Lemma AppEta' (a0 a1 b : PTm) :
+  Lemma AppEta' n (a0 a1 b : PTm n) :
     b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) ->
     R a0 a1 ->
     R a0 b.
   Proof. move => ->; apply AppEta. Qed.
 
-  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
-    move => h. move : ξ.
-    elim : a b /h.
+    move => h. move : m ξ.
+    elim : n a b /h.
     move => *; apply : AppAbs'; eauto; by asimpl.
     all : match goal with
           | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl
@@ -109,23 +109,23 @@ Module Par.
   Qed.
 
 
-  Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) :
+  Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
   Proof.
-    move => + h. move : ρ0 ρ1. elim : a b/h.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ0 ρ1 hρ /=.
+    move => + h. move : m ρ0 ρ1. elim : n a b/h.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=.
       eapply AppAbs' with (a1 := subst_PTm (up_PTm_PTm ρ1) a1); eauto.
       by asimpl.
-      hauto l:on use:renaming inv:nat.
+      hauto l:on use:renaming inv:option.
     - hauto lq:on rew:off ctrs:R.
-    - hauto l:on inv:nat use:renaming ctrs:R.
+    - hauto l:on inv:option use:renaming ctrs:R.
     - hauto lq:on use:ProjPair'.
-    - move => a0 a1 ha iha ρ0 ρ1 hρ /=.
+    - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=.
       apply : AppEta'; eauto. by asimpl.
     - hauto lq:on ctrs:R.
     - sfirstorder.
-    - hauto l:on inv:nat ctrs:R use:renaming.
+    - hauto l:on inv:option ctrs:R use:renaming.
     - hauto q:on ctrs:R.
     - qauto l:on ctrs:R.
     - qauto l:on ctrs:R.
@@ -134,16 +134,16 @@ Module Par.
     - qauto l:on ctrs:R.
   Qed.
 
-  Lemma substing (a b : PTm) (ρ : nat -> PTm) :
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
     R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof. hauto l:on use:morphing, refl. Qed.
 
-  Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) :
+  Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
     move E : (ren_PTm ξ a) => u h.
-    move : ξ a E. elim : u b/h.
-    - move => a0 a1 b0 b1 ha iha hb ihb ξ []//=.
+    move : n ξ a E. elim : m u b/h.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=.
       move => c c0 [+ ?]. subst.
       case : c => //=.
       move => c [?]. subst.
@@ -153,7 +153,7 @@ Module Par.
       eexists. split.
       apply AppAbs; eauto.
       by asimpl.
-    - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ξ []//=.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//=.
       move => []//= t t0 t1 [*]. subst.
       spec_refl.
       move : iha => [? [*]].
@@ -162,43 +162,43 @@ Module Par.
       eexists. split.
       apply AppPair; hauto. subst.
       by asimpl.
-    - move => p a0 a1 ha iha ξ []//= p0 []//= t [*]. subst.
+    - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjAbs; eauto. by asimpl.
-    - move => p a0 a1 b0 b1 ha iha hb ihb ξ []//= p0 []//= t t0[*].
+    - move => n p a0 a1 b0 b1 ha iha hb ihb m ξ []//= p0 []//= t t0[*].
       subst. spec_refl.
       move : iha => [b0 [? ?]].
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => a0 a1 ha iha ξ a ?. subst.
+    - move => n a0 a1 ha iha m ξ a ?. subst.
       spec_refl. move : iha => [a0 [? ?]]. subst.
       eexists. split. apply AppEta; eauto.
       by asimpl.
-    - move => a0 a1 ha iha ξ a ?. subst.
+    - move => n a0 a1 ha iha m ξ a ?. subst.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply PairEta; eauto.
       by asimpl.
-    - move => i ξ []//=.
+    - move => n i m ξ []//=.
       hauto l:on.
-    - move => a0 a1 ha iha ξ []//= t [*]. subst.
+    - move => n a0 a1 ha iha m ξ []//= t [*]. subst.
       spec_refl.
       move  :iha => [b0 [? ?]]. subst.
       eexists. split. by apply AbsCong; eauto.
       done.
-    - move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0 [*]. subst.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst.
       spec_refl.
       move : iha => [b0 [? ?]]. subst.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by apply AppCong; eauto.
       done.
-    - move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0[*]. subst.
+    - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0[*]. subst.
       spec_refl.
       move : iha => [b0 [? ?]]. subst.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split=>/=. by apply PairCong; eauto.
       done.
-    - move => p a0 a1 ha iha ξ []//= p0 t [*]. subst.
+    - move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst.
       spec_refl.
       move : iha => [b0 [? ?]]. subst.
       eexists. split. by apply ProjCong; eauto.
@@ -359,7 +359,7 @@ Module RPar.
     R a b ->
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
-  Proof. hauto q:on inv:nat. Qed.
+  Proof. hauto q:on inv:option. Qed.
 
   Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
@@ -399,7 +399,7 @@ Module RPar.
     R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
   Proof.
     move => h0 h1. apply morphing => //=.
-    qauto l:on ctrs:R inv:nat.
+    qauto l:on ctrs:R inv:option.
   Qed.
 
   Lemma var_or_const_imp {n} (a b : PTm n) :
@@ -595,7 +595,7 @@ Module RPar'.
     R a b ->
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
-  Proof. hauto q:on inv:nat. Qed.
+  Proof. hauto q:on inv:option. Qed.
 
   Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
@@ -633,7 +633,7 @@ Module RPar'.
     R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
   Proof.
     move => h0 h1. apply morphing => //=.
-    qauto l:on ctrs:R inv:nat.
+    qauto l:on ctrs:R inv:option.
   Qed.
 
   Lemma var_or_const_imp {n} (a b : PTm n) :
@@ -786,7 +786,7 @@ Module ERed.
     move => h. move : m ρ. elim : n a b / h => n.
     move => a m ρ /=.
     apply : AppEta'; eauto. by asimpl.
-    all : hauto ctrs:R inv:nat use:renaming.
+    all : hauto ctrs:R inv:option use:renaming.
   Qed.
 
 End ERed.
@@ -892,11 +892,11 @@ Module EPar.
       apply : AppEta'; eauto. by asimpl.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
-    - hauto l:on ctrs:R use:renaming inv:nat.
+    - hauto l:on ctrs:R use:renaming inv:option.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
-    - hauto l:on ctrs:R use:renaming inv:nat.
+    - hauto l:on ctrs:R use:renaming inv:option.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
   Qed.
@@ -907,7 +907,7 @@ Module EPar.
     R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1).
   Proof.
     move => h0 h1. apply morphing => //.
-    hauto lq:on ctrs:R inv:nat.
+    hauto lq:on ctrs:R inv:option.
   Qed.
 
 End EPar.
@@ -1018,7 +1018,7 @@ Module RPars.
   Lemma substing n (a b : PTm (S n)) c :
     rtc RPar.R a b ->
     rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
-  Proof. hauto lq:on use:morphing inv:nat. Qed.
+  Proof. hauto lq:on use:morphing inv:option. Qed.
 
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
     (forall i, var_or_const (ρ i)) ->
@@ -1099,7 +1099,7 @@ Module RPars'.
   Lemma substing n (a b : PTm (S n)) c :
     rtc RPar'.R a b ->
     rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
-  Proof. hauto lq:on use:morphing inv:nat. Qed.
+  Proof. hauto lq:on use:morphing inv:option. Qed.
 
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
     (forall i, var_or_const (ρ i)) ->
@@ -2328,7 +2328,7 @@ Proof.
       have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder.
       move => h. apply wn_abs.
       move : h. apply wn_antirenaming.
-      hauto lq:on rew:off inv:nat.
+      hauto lq:on rew:off inv:option.
     + hauto q:on inv:RPar'.R ctrs:rtc b:on.
 Qed.
 

theories/typing.v

@@ -1,251 +0,0 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-
-Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
-Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
-Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
-Reserved Notation "⊢ Γ" (at level 70).
-Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
-| T_Var i Γ A :
-  ⊢ Γ ->
-  lookup i Γ A ->
-  Γ ⊢ VarPTm i ∈ A
-
-| T_Bind Γ i p (A : PTm) (B : PTm) :
-  Γ ⊢ A ∈ PUniv i ->
-  cons A Γ ⊢ B ∈ PUniv i ->
-  Γ ⊢ PBind p A B ∈ PUniv i
-
-| T_Abs Γ (a : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  (cons A Γ) ⊢ a ∈ B ->
-  Γ ⊢ PAbs a ∈ PBind PPi A B
-
-| T_App Γ (b a : PTm) A B :
-  Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B
-
-| T_Pair Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊢ PPair a b ∈ PBind PSig A B
-
-| T_Proj1 Γ (a : PTm) A B :
-  Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ PProj PL a ∈ A
-
-| T_Proj2 Γ (a : PTm) A B :
-  Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
-
-| T_Univ Γ i :
-  ⊢ Γ ->
-  Γ ⊢ PUniv i ∈ PUniv (S i)
-
-| T_Nat Γ i :
-  ⊢ Γ ->
-  Γ ⊢ PNat ∈ PUniv i
-
-| T_Zero Γ :
-  ⊢ Γ ->
-  Γ ⊢ PZero ∈ PNat
-
-| T_Suc Γ (a : PTm) :
-  Γ ⊢ a ∈ PNat ->
-  Γ ⊢ PSuc a ∈ PNat
-
-| T_Ind Γ P (a : PTm) b c i :
-  cons PNat Γ ⊢ P ∈ PUniv i ->
-  Γ ⊢ a ∈ PNat ->
-  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
-  Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P
-
-| T_Conv Γ (a : PTm) A B :
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ A ≲ B ->
-  Γ ⊢ a ∈ B
-
-with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
-(* Structural *)
-| E_Refl Γ (a : PTm ) A :
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ a ≡ a ∈ A
-
-| E_Symmetric Γ (a b : PTm) A :
-  Γ ⊢ a ≡ b ∈ A ->
-  Γ ⊢ b ≡ a ∈ A
-
-| E_Transitive Γ (a b c : PTm) A :
-  Γ ⊢ a ≡ b ∈ A ->
-  Γ ⊢ b ≡ c ∈ A ->
-  Γ ⊢ a ≡ c ∈ A
-
-(* Congruence *)
-| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
-  Γ ⊢ A0 ∈ PUniv i ->
-  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
-  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
-
-| E_Abs Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  (cons A Γ) ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
-
-| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
-  Γ ⊢ a0 ≡ a1 ∈ A ->
-  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
-
-| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a0 ≡ a1 ∈ A ->
-  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
-  Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
-
-| E_Proj1 Γ (a b : PTm) A B :
-  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
-  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
-
-| E_Proj2 Γ i (a b : PTm) A B :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
-  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
-
-| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
-  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
-  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
-  Γ ⊢ a0 ≡ a1 ∈ PNat ->
-  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
-  (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
-  Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
-
-| E_SucCong Γ (a b : PTm) :
-  Γ ⊢ a ≡ b ∈ PNat ->
-  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
-
-| E_Conv Γ (a b : PTm) A B :
-  Γ ⊢ a ≡ b ∈ A ->
-  Γ ⊢ A ≲ B ->
-  Γ ⊢ a ≡ b ∈ B
-
-(* Beta *)
-| E_AppAbs Γ (a : PTm) b A B i:
-  Γ ⊢ PBind PPi A B ∈ PUniv i ->
-  Γ ⊢ b ∈ A ->
-  (cons A Γ) ⊢ a ∈ B ->
-  Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
-
-| E_ProjPair1 Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A
-
-| E_ProjPair2 Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ∈ A ->
-  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
-
-| E_IndZero Γ P i (b : PTm) c :
-  (cons PNat Γ) ⊢ P ∈ PUniv i ->
-  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
-  Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
-
-| E_IndSuc Γ P (a : PTm) b c i :
-  (cons PNat Γ) ⊢ P ∈ PUniv i ->
-  Γ ⊢ a ∈ PNat ->
-  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
-  Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
-
-(* Eta *)
-| E_AppEta Γ (b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
-
-| E_PairEta Γ (a : PTm ) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
-
-with LEq : list PTm -> PTm -> PTm -> Prop :=
-(* Structural *)
-| Su_Transitive Γ (A B C : PTm) :
-  Γ ⊢ A ≲ B ->
-  Γ ⊢ B ≲ C ->
-  Γ ⊢ A ≲ C
-
-(* Congruence *)
-| Su_Univ Γ i j :
-  ⊢ Γ ->
-  i <= j ->
-  Γ ⊢ PUniv i ≲ PUniv j
-
-| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
-  Γ ⊢ A0 ∈ PUniv i ->
-  Γ ⊢ A1 ≲ A0 ->
-  (cons A0 Γ) ⊢ B0 ≲ B1 ->
-  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
-
-| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
-  Γ ⊢ A1 ∈ PUniv i ->
-  Γ ⊢ A0 ≲ A1 ->
-  (cons A1 Γ) ⊢ B0 ≲ B1 ->
-  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
-
-(* Injecting from equalities *)
-| Su_Eq Γ (A : PTm) B i  :
-  Γ ⊢ A ≡ B ∈ PUniv i ->
-  Γ ⊢ A ≲ B
-
-(* Projection axioms *)
-| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
-  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
-  Γ ⊢ A1 ≲ A0
-
-| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
-  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
-  Γ ⊢ A0 ≲ A1
-
-| Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 :
-  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
-  Γ ⊢ a0 ≡ a1 ∈ A1 ->
-  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
-
-| Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
-  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
-  Γ ⊢ a0 ≡ a1 ∈ A0 ->
-  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
-
-with Wff : list PTm -> Prop :=
-| Wff_Nil :
-  ⊢ nil
-| Wff_Cons Γ (A : PTm) i :
-  ⊢ Γ ->
-  Γ ⊢ A ∈ PUniv i ->
-  (* -------------------------------- *)
-  ⊢ (cons A Γ)
-
-where
-"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
-
-Scheme wf_ind := Induction for Wff Sort Prop
-  with wt_ind := Induction for Wt Sort Prop
-  with eq_ind := Induction for Eq Sort Prop
-  with le_ind := Induction for LEq Sort Prop.
-
-Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.
-
-(* Lemma lem : *)
-(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
-(*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
-(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *)
-(*   (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *)
-(* Proof. apply wt_mutual. ... *)