Prove PairEta

Makefile

@@ -16,12 +16,12 @@ uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
 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
+	autosubst -f -v ge813 -s ucoq -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
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
 
 FORCE:

syntax.sig

@@ -16,7 +16,6 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
-PBot : PTm
 PNat : PTm
 PZero : PTm
 PSuc : PTm -> PTm

theories/Autosubst2/fintype.v

@@ -1,419 +0,0 @@
-(** * 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

@@ -0,0 +1,213 @@
+(** * 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/admissible.v

@@ -1,45 +1,88 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
+Derive Inversion wff_inv with (forall Γ, ⊢ Γ) Sort Prop.
 
-Lemma Wff_Cons_Inv n Γ (A : PTm n) :
+Lemma T_Abs Γ (a : PTm ) A B :
-  ⊢ funcomp (ren_PTm shift) (scons A Γ) ->
+  (cons A Γ) ⊢ a ∈ B ->
-  ⊢ Γ /\ exists i, Γ ⊢ A ∈ PUniv i.
-Proof.
-  elim /wff_inv => //= _.
-  move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
-  Equality.simplify_dep_elim.
-  have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
-  move /(_ var_zero) : (h).
-  rewrite /funcomp. asimpl.
-  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
-  move => ?. subst.
-  have : Γ0 = Γ. extensionality i.
-  move /(_ (Some i)) : h.
-  rewrite /funcomp. asimpl.
-  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
-  done.
-  move => ?. subst. sfirstorder.
-Qed.
-
-Lemma T_Abs n Γ (a : PTm (S n)) A B :
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
   Γ ⊢ PAbs a ∈ PBind PPi A B.
 Proof.
   move => ha.
-  have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have [i hB] : exists i, (cons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
-  have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
+  have hΓ : ⊢  (cons A Γ) by sfirstorder use:wff_mutual.
-  move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
+  hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
-  hauto lq:on rew:off use:T_Bind', typing.T_Abs.
 Qed.
 
-Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+
+Lemma App_Inv Γ (b a : PTm) U :
+  Γ ⊢ PApp b a ∈ U ->
+  exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
+Proof.
+  move E : (PApp b a) => u hu.
+  move : b a E. elim : Γ u U / hu => //=.
+  - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
+    exists A,B.
+    repeat split => //=.
+    have [i] : exists i, Γ ⊢ PBind PPi A B ∈  PUniv i by sfirstorder use:regularity.
+    hauto lq:on use:bind_inst, E_Refl.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+
+Lemma Abs_Inv Γ (a : PTm) U :
+  Γ ⊢ PAbs a ∈ U ->
+  exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
+Proof.
+  move E : (PAbs a) => u hu.
+  move : a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B i hP _ ha _ a0 [*]. subst.
+    exists A, B. repeat split => //=.
+    hauto lq:on use:E_Refl, Su_Eq.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+
+
+Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
+  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+Proof.
+  move => a b Γ A ha.
+  move /App_Inv : ha.
+  move => [A0][B0][ha][hb]hS.
+  move /Abs_Inv : ha => [A1][B1][ha]hS0.
+  have hb' := hb.
+  move /E_Refl in hb.
+  have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
+  move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
+  move => h.
+  apply : E_Conv; eauto.
+  apply : E_AppAbs; eauto.
+  eauto using T_Conv.
+Qed.
+
+Lemma T_Eta Γ A a B :
+  A :: Γ ⊢ a ∈ B ->
+  A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B.
+Proof.
+  move => ha.
+  have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff.
+  have hΓ : ⊢ Γ by hauto lq:on inv:Wff.
+  eapply T_App' with (B  := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift.
+  econstructor; eauto. sauto l:on use:renaming.
+  apply T_Var => //.
+  by constructor.
+Qed.
+
+Lemma E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
 Proof.
   move => h0 h1.
@@ -49,7 +92,7 @@ Proof.
   firstorder.
 Qed.
 
-Lemma E_App n Γ (b0 b1 a0 a1 : PTm n) A B :
+Lemma E_App Γ (b0 b1 a0 a1 : PTm ) A B :
   Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
@@ -59,7 +102,7 @@ Proof.
   move : E_App h. by repeat move/[apply].
 Qed.
 
-Lemma E_Proj2 n Γ (a b : PTm n) A B :
+Lemma E_Proj2 Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
 Proof.
@@ -67,3 +110,155 @@ Proof.
   have [i] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto l:on use:regularity.
   move : E_Proj2 h; by repeat move/[apply].
 Qed.
+
+Lemma E_FunExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PPi A B ->
+  Γ ⊢ b ∈ PBind PPi A B ->
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B.
+Proof.
+  hauto l:on use:regularity, E_FunExt.
+Qed.
+
+Lemma E_PairExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B. hauto l:on use:regularity, E_PairExt. Qed.
+
+Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 :
+  renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 ->
+  renaming_ok Γ Ξ (funcomp ξ0 ξ1).
+  rewrite /renaming_ok => h0 h1 i A.
+  move => {}/h1 {}/h0.
+  by asimpl.
+Qed.
+
+Lemma E_AppEta Γ (b : PTm) A B :
+  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
+Proof.
+  move => h.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
+  have [j [hA hB]] : exists i, Γ ⊢ A ∈ PUniv i /\ A :: Γ ⊢ B ∈ PUniv i by hauto lq:on use:Bind_Inv.
+  have {i} {}hPi : Γ ⊢ PBind PPi A B ∈ PUniv j by sfirstorder use:T_Bind, wff_mutual.
+  have hΓ : ⊢ A :: Γ by hauto lq:on use:Bind_Inv, Wff_Cons'.
+  have hΓ' :  ⊢ ren_PTm shift A :: A :: Γ by sauto lq:on use:renaming, renaming_shift inv:Wff.
+  apply E_FunExt; eauto.
+  apply T_Abs.
+  eapply T_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  change (PBind _ _ _) with (ren_PTm shift (PBind PPi A B)).
+
+  eapply renaming; eauto.
+  apply renaming_shift.
+  constructor => //.
+  by constructor.
+
+  apply : E_Transitive. simpl.
+  apply E_AppAbs' with (i := j)(A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B); eauto.
+  by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  constructor => //.
+  by constructor.
+  asimpl.
+  eapply T_App' with (A := ren_PTm shift (ren_PTm shift A)) (B := ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B)); cycle 2.
+  constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift.
+  by constructor. asimpl. substify. by asimpl.
+  have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))=  (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl.
+  eapply renaming; eauto. by eauto using renaming_shift, renaming_comp.
+  asimpl. renamify.
+  eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  sauto lq:on use:renaming, renaming_shift, E_Refl.
+  constructor. constructor=>//. constructor.
+Qed.
+
+Lemma Proj1_Inv Γ (a : PTm ) U :
+  Γ ⊢ PProj PL a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
+Proof.
+  move E : (PProj PL a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    eapply regularity in ha.
+    move : ha => [i].
+    move /Bind_Inv => [j][h _].
+    by move /E_Refl /Su_Eq in h.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Proj2_Inv Γ (a : PTm) U :
+  Γ ⊢ PProj PR a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
+Proof.
+  move E : (PProj PR a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    have ha' := ha.
+    eapply regularity in ha.
+    move : ha => [i ha].
+    move /T_Proj1 in ha'.
+    apply : bind_inst; eauto.
+    apply : E_Refl ha'.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Pair_Inv Γ (a b : PTm ) U :
+  Γ ⊢ PPair a b ∈ U ->
+  exists A B, Γ ⊢ a ∈ A /\
+         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
+         Γ ⊢ PBind PSig A B ≲ U.
+Proof.
+  move E : (PPair a b) => u hu.
+  move : a b E. elim : Γ u U / hu => //=.
+  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
+    exists A,B. repeat split => //=.
+    move /E_Refl /Su_Eq : hS. apply.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => a b Γ A.
+  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move /Su_Sig_Proj1 in hS.
+  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair1; eauto.
+Qed.
+
+Lemma E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
+Proof.
+  move => a b Γ A. move /Proj2_Inv.
+  move => [A0][B0][ha]h.
+  have hr := ha.
+  move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
+  have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using  E_ProjPair1 with wt.
+  move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
+  apply : E_Conv; eauto.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair2; eauto.
+Qed.
+
+
+Lemma E_PairEta Γ a A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PPair (PProj PL a) (PProj PR a) ≡ a ∈ PBind PSig A B.
+Proof.
+  move => h.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto use:regularity.
+  apply E_PairExt => //.
+  eapply T_Pair; eauto with wt.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto with wt.
+  apply E_ProjPair2.
+  apply : T_Proj2; eauto with wt.
+Qed.

theories/common.v

@@ -1,41 +1,71 @@
-Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect ssrbool.
+From Equations Require Import Equations.
+Derive NoConfusion for nat PTag BTag PTm.
+Derive EqDec for BTag PTag PTm.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
+From stdpp Require Import relations (rtc(..)).
 
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+Inductive lookup : nat -> list PTm -> PTm -> Prop :=
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
+| here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A)
+| there i Γ A B :
+  lookup i Γ A ->
+  lookup (S i) (cons B Γ) (ren_PTm shift A).
 
-Lemma up_injective n m (ξ : fin n -> fin m) :
+Lemma lookup_deter i Γ A B :
-  (forall i j, ξ i = ξ j -> i = j) ->
+  lookup i Γ A ->
-  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+  lookup i Γ B ->
+  A = B.
+Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed.
+
+Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
+Proof.  move => ->. apply here. Qed.
+
+Lemma there' i Γ A B U : U = ren_PTm shift A -> lookup i Γ A ->
+                       lookup (S i) (cons B Γ) U.
+Proof. move => ->. apply there. Qed.
+
+Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A).
+
+Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=
+  forall i A, lookup i Δ A -> lookup (ξ i) Γ (ren_PTm ξ A).
+
+Definition ren_inj (ξ : nat -> nat) := forall i j, ξ i = ξ j -> i = j.
+
+Lemma up_injective (ξ : nat -> nat) :
+  ren_inj ξ ->
+  ren_inj (upRen_PTm_PTm ξ).
 Proof.
-  sblast inv:option.
+  move => h i j.
+  case : i => //=; case : j => //=.
+  move => i j. rewrite /funcomp. hauto lq:on rew:off unfold:ren_inj.
 Qed.
 
 Local Ltac2 rec solve_anti_ren () :=
   let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
   intro $x;
   lazy_match! Constr.type (Control.hyp x) with
-  | fin _ -> _ _ => (ltac1:(case;hauto lq:on rew:off use:up_injective))
+  | nat -> nat => (ltac1:(case => *//=; qauto l:on use:up_injective unfold:ren_inj))
   | _ => solve_anti_ren ()
   end.
 
 Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
-Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+Lemma ren_injective (a b : PTm) (ξ : nat -> nat) :
-  (forall i j, ξ i = ξ j -> i = j) ->
+  ren_inj ξ ->
   ren_PTm ξ a = ren_PTm ξ b ->
   a = b.
 Proof.
-  move : m ξ b. elim : n / a => //; try solve_anti_ren.
+  move : ξ b. elim : a => //; try solve_anti_ren.
+  move => p ihp ξ []//=. hauto lq:on inv:PTm, nat ctrs:- use:up_injective.
 Qed.
 
 Inductive HF : Set :=
 | H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
 
-Definition ishf {n} (a : PTm n) :=
+Definition ishf (a : PTm) :=
   match a with
   | PPair _ _ => true
   | PAbs _ => true
@@ -47,7 +77,7 @@ Definition ishf {n} (a : PTm n) :=
   | _ => false
   end.
 
-Definition toHF {n} (a : PTm n) :=
+Definition toHF (a : PTm) :=
   match a with
   | PPair _ _ => H_Pair
   | PAbs _ => H_Abs
@@ -59,54 +89,513 @@ Definition toHF {n} (a : PTm n) :=
   | _ => H_Bot
   end.
 
-Fixpoint ishne {n} (a : PTm n) :=
+Fixpoint ishne (a : PTm) :=
   match a with
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
-  | PBot => true
   | PInd _ n _ _ => ishne n
   | _ => false
   end.
 
-Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
+Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false.
 
-Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
+Definition isuniv (a : PTm) := if a is PUniv _ then true else false.
 
-Definition ispair {n} (a : PTm n) :=
+Definition ispair (a : PTm) :=
   match a with
   | PPair _ _ => true
   | _ => false
   end.
 
-Definition isnat {n} (a : PTm n) := if a is PNat then true else false.
+Definition isnat (a : PTm) := if a is PNat then true else false.
 
-Definition iszero {n} (a : PTm n) := if a is PZero then true else false.
+Definition iszero (a : PTm) := if a is PZero then true else false.
 
-Definition issuc {n} (a : PTm n) := if a is PSuc _ then true else false.
+Definition issuc (a : PTm) := if a is PSuc _ then true else false.
 
-Definition isabs {n} (a : PTm n) :=
+Definition isabs (a : PTm) :=
   match a with
   | PAbs _ => true
   | _ => false
   end.
 
-Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition tm_nonconf (a b : PTm) : bool :=
+  match a, b with
+  | PAbs _, _ => (~~ ishf b) || isabs b
+  | _, PAbs _ => ~~ ishf a
+  | VarPTm _, VarPTm _ => true
+  | PPair _ _, _ => (~~ ishf b) || ispair b
+  | _, PPair _ _ => ~~ ishf a
+  | PZero, PZero => true
+  | PSuc _, PSuc _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | PNat, PNat => true
+  | PUniv _, PUniv _ => true
+  | PBind _ _ _, PBind _ _ _ => true
+  | _,_=> false
+  end.
+
+Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
+
+Definition ishf_ren (a : PTm)  (ξ : nat -> nat) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
 
-Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition isabs_ren (a : PTm)  (ξ : nat -> nat) :
   isabs (ren_PTm ξ a) = isabs a.
 Proof. case : a => //=. Qed.
 
-Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ispair_ren (a : PTm)  (ξ : nat -> nat) :
   ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
 
-Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ishne_ren (a : PTm)  (ξ : nat -> nat) :
   ishne (ren_PTm ξ a) = ishne a.
-Proof. move : m ξ. elim : n / a => //=. Qed.
+Proof. move : ξ. elim : a => //=. Qed.
 
-Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A :
+Lemma renaming_shift Γ A :
-  renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift.
+  renaming_ok (cons A Γ) Γ shift.
-Proof. sfirstorder. Qed.
+Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed.
+
+Lemma subst_scons_id (a : PTm) :
+  subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) a = a.
+Proof.
+  have E : subst_PTm VarPTm a = a by asimpl.
+  rewrite -{2}E.
+  apply ext_PTm. case => //=.
+Qed.
+
+Module HRed.
+    Inductive R : PTm -> PTm ->  Prop :=
+  (****************** Beta ***********************)
+  | AppAbs a b :
+    R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
+
+  | ProjPair p a b :
+    R (PProj p (PPair a b)) (if p is PL then a else b)
+
+  | IndZero P b c :
+    R (PInd P PZero b c) b
+
+  | IndSuc P a b c :
+    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+
+  (*************** Congruence ********************)
+  | AppCong a0 a1 b :
+    R a0 a1 ->
+    R (PApp a0 b) (PApp a1 b)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (PProj p a0) (PProj p a1)
+  | IndCong P a0 a1 b c :
+    R a0 a1 ->
+    R (PInd P a0 b c) (PInd P a1 b c).
+
+    Definition nf a := forall b, ~ R a b.
+End HRed.
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
+| A_AbsAbs a b :
+  algo_dom_r a b ->
+  (* --------------------- *)
+  algo_dom (PAbs a) (PAbs b)
+
+| A_AbsNeu a u :
+  ishne u ->
+  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
+  (* --------------------- *)
+  algo_dom (PAbs a) u
+
+| A_NeuAbs a u :
+  ishne u ->
+  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
+  (* --------------------- *)
+  algo_dom u (PAbs a)
+
+| A_PairPair a0 a1 b0 b1 :
+  algo_dom_r a0 a1 ->
+  algo_dom_r b0 b1 ->
+  (* ---------------------------- *)
+  algo_dom (PPair a0 b0) (PPair a1 b1)
+
+| A_PairNeu a0 a1 u :
+  ishne u ->
+  algo_dom_r a0 (PProj PL u) ->
+  algo_dom_r a1 (PProj PR u) ->
+  (* ----------------------- *)
+  algo_dom (PPair a0 a1) u
+
+| A_NeuPair a0 a1 u :
+  ishne u ->
+  algo_dom_r (PProj PL u) a0 ->
+  algo_dom_r (PProj PR u) a1 ->
+  (* ----------------------- *)
+  algo_dom u (PPair a0 a1)
+
+| A_ZeroZero :
+  algo_dom PZero PZero
+
+| A_SucSuc a0 a1 :
+  algo_dom_r a0 a1 ->
+  algo_dom (PSuc a0) (PSuc a1)
+
+| A_UnivCong i j :
+  (* -------------------------- *)
+  algo_dom (PUniv i) (PUniv j)
+
+| A_BindCong p0 p1 A0 A1 B0 B1 :
+  algo_dom_r A0 A1 ->
+  algo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
+
+| A_NatCong :
+  algo_dom PNat PNat
+
+| A_VarCong i j :
+  (* -------------------------- *)
+  algo_dom (VarPTm i) (VarPTm j)
+
+| A_AppCong u0 u1 a0 a1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r a0 a1 ->
+  (* ------------------------- *)
+  algo_dom (PApp u0 a0) (PApp u1 a1)
+
+| A_ProjCong p0 p1 u0 u1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  (* ---------------------  *)
+  algo_dom (PProj p0 u0) (PProj p1 u1)
+
+| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom_r P0 P1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r b0 b1 ->
+  algo_dom_r c0 c1 ->
+  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+
+| A_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  tm_conf a b ->
+  algo_dom a b
+
+with algo_dom_r : PTm  -> PTm -> Prop :=
+| A_NfNf a b :
+  algo_dom a b ->
+  algo_dom_r a b
+
+| A_HRedL a a' b  :
+  HRed.R a a' ->
+  algo_dom_r a' b ->
+  (* ----------------------- *)
+  algo_dom_r a b
+
+| A_HRedR a b b'  :
+  HRed.nf a ->
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  (* ----------------------- *)
+  algo_dom_r a b.
+
+Scheme algo_ind := Induction for algo_dom Sort Prop
+  with algor_ind := Induction for algo_dom_r Sort Prop.
+
+Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
+#[export]Hint Constructors algo_dom algo_dom_r : adom.
+
+Definition stm_nonconf a b :=
+  match a, b with
+  | PUniv _, PUniv _ => true
+  | PBind PPi _ _, PBind PPi _ _ => true
+  | PBind PSig _ _, PBind PSig _ _ => true
+  | PNat, PNat => true
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Definition neuneu_nonconf a b :=
+  match a, b with
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Lemma stm_tm_nonconf a b :
+  stm_nonconf a b -> tm_nonconf a b.
+Proof. apply /implyP.
+       destruct a ,b =>//=; hauto lq:on inv:PTag, BTag.
+Qed.
+
+Definition stm_conf a b := ~~ stm_nonconf a b.
+
+Lemma tm_stm_conf a b :
+  tm_conf a b -> stm_conf a b.
+Proof.
+  rewrite /tm_conf /stm_conf.
+  apply /contra /stm_tm_nonconf.
+Qed.
+
+Inductive salgo_dom : PTm -> PTm -> Prop :=
+| S_UnivCong i j :
+  (* -------------------------- *)
+  salgo_dom (PUniv i) (PUniv j)
+
+| S_PiCong  A0 A1 B0 B1 :
+  salgo_dom_r A1 A0 ->
+  salgo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1)
+
+| S_SigCong  A0 A1 B0 B1 :
+  salgo_dom_r A0 A1 ->
+  salgo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1)
+
+| S_NatCong :
+  salgo_dom PNat PNat
+
+| S_NeuNeu a b :
+  neuneu_nonconf a b ->
+  algo_dom a b ->
+  salgo_dom a b
+
+| S_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  stm_conf a b ->
+  salgo_dom a b
+
+with salgo_dom_r : PTm -> PTm -> Prop :=
+| S_NfNf a b :
+  salgo_dom a b ->
+  salgo_dom_r a b
+
+| S_HRedL a a' b  :
+  HRed.R a a' ->
+  salgo_dom_r a' b ->
+  (* ----------------------- *)
+  salgo_dom_r a b
+
+| S_HRedR a b b'  :
+  HRed.nf a ->
+  HRed.R b b' ->
+  salgo_dom_r a b' ->
+  (* ----------------------- *)
+  salgo_dom_r a b.
+
+#[export]Hint Constructors salgo_dom salgo_dom_r : sdom.
+Scheme salgo_ind := Induction for salgo_dom Sort Prop
+  with salgor_ind := Induction for salgo_dom_r Sort Prop.
+
+Combined Scheme salgo_dom_mutual from salgo_ind, salgor_ind.
+
+Lemma hf_no_hred (a b : PTm) :
+  ishf a ->
+  HRed.R a b ->
+  False.
+Proof. hauto l:on inv:HRed.R. Qed.
+
+Lemma hne_no_hred (a b : PTm) :
+  ishne a ->
+  HRed.R a b ->
+  False.
+Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
+
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [_ : is_true (ishne ?a) |- is_true (stm_conf ?a _) ] =>
+      if Constr.is_var a then destruct $a; ltac1:(done) else ()
+  | [|- is_true (stm_conf _ _)] =>
+      unfold stm_conf; ltac1:(done)
+  end.
+
+Ltac destruct_salgo := ltac2:(destruct_salgo ()).
+
+Lemma algo_dom_r_inv a b :
+  algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma A_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  algo_dom_r a' b ->
+  algo_dom_r a b.
+  induction 1; sfirstorder use:A_HRedL.
+Qed.
+
+Lemma A_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  algo_dom a b' ->
+  algo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a.
+Proof. case : a; case : b => //=. Qed.
+
+Lemma algo_dom_no_hred (a b : PTm) :
+  algo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+
+Lemma A_HRedR' a b b' :
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  algo_dom_r a b.
+Proof.
+  move => hb /algo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:algo_dom_no_hred.
+  hauto lq:on use:A_HRedsL, A_HRedsR.
+Qed.
+
+Lemma algo_dom_sym :
+  (forall a b (h : algo_dom a b), algo_dom b a) /\
+    (forall a b (h : algo_dom_r a b), algo_dom_r b a).
+Proof.
+  apply algo_dom_mutual; try qauto use:tm_conf_sym,A_HRedR' db:adom.
+Qed.
+
+Lemma salgo_dom_r_inv a b :
+  salgo_dom_r a b -> exists a0 b0, salgo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma S_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  salgo_dom_r a' b ->
+  salgo_dom_r a b.
+  induction 1; sfirstorder use:S_HRedL.
+Qed.
+
+Lemma S_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  salgo_dom a b' ->
+  salgo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma stm_conf_sym a b : stm_conf a b = stm_conf b a.
+Proof. case : a; case : b => //=; hauto lq:on inv:PTag, BTag. Qed.
+
+Lemma salgo_dom_no_hred (a b : PTm) :
+  salgo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred, algo_dom_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+Lemma S_HRedR' a b b' :
+  HRed.R b b' ->
+  salgo_dom_r a b' ->
+  salgo_dom_r a b.
+Proof.
+  move => hb /salgo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:salgo_dom_no_hred.
+  hauto lq:on use:S_HRedsL, S_HRedsR.
+Qed.
+
+Ltac solve_conf := intros; split;
+      apply S_Conf; solve [destruct_salgo | sfirstorder ctrs:salgo_dom use:hne_no_hred, hf_no_hred].
+
+Ltac solve_basic := hauto q:on ctrs:salgo_dom, salgo_dom_r, algo_dom use:algo_dom_sym.
+
+Lemma algo_dom_salgo_dom :
+  (forall a b, algo_dom a b -> salgo_dom a b /\ salgo_dom b a) /\
+    (forall a b, algo_dom_r a b -> salgo_dom_r a b /\ salgo_dom_r b a).
+Proof.
+  apply algo_dom_mutual => //=; try first [solve_conf | solve_basic].
+  - case; case; hauto lq:on ctrs:salgo_dom use:algo_dom_sym inv:HRed.R unfold:HRed.nf.
+  - move => a b ha hb hc. split;
+      apply S_Conf; hauto l:on use:tm_conf_sym, tm_stm_conf.
+  - hauto lq:on ctrs:salgo_dom_r use:S_HRedR'.
+Qed.
+
+Fixpoint hred (a : PTm) : option (PTm) :=
+    match a with
+    | VarPTm i => None
+    | PAbs a => None
+    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
+    | PApp a b =>
+        match hred a with
+        | Some a => Some (PApp a b)
+        | None => None
+        end
+    | PPair a b => None
+    | PProj p (PPair a b) => if p is PL then Some a else Some b
+    | PProj p a =>
+        match hred a with
+        | Some a => Some (PProj p a)
+        | None => None
+        end
+    | PUniv i => None
+    | PBind p A B => None
+    | PNat => None
+    | PZero => None
+    | PSuc a => None
+    | PInd P PZero b c => Some b
+    | PInd P (PSuc a) b c =>
+        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+    | PInd P a b c =>
+        match hred a with
+        | Some a => Some (PInd P a b c)
+        | None => None
+        end
+    end.
+
+Lemma hred_complete (a b : PTm) :
+  HRed.R a b -> hred a = Some b.
+Proof.
+  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
+Qed.
+
+Lemma hred_sound (a b : PTm):
+  hred a = Some b -> HRed.R a b.
+Proof.
+  elim : a b; hauto q:on dep:on ctrs:HRed.R.
+Qed.
+
+Lemma hred_deter (a b0 b1 : PTm) :
+  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
+Proof.
+  move /hred_complete => + /hred_complete. congruence.
+Qed.
+
+Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
+  destruct (hred a) eqn:eq.
+  right. exists p. by apply hred_sound in eq.
+  left. move => b /hred_complete. congruence.
+Defined.
+
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. Qed.
+
+Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b.
+Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed.

theories/executable.v

@@ -1,145 +1,350 @@
 From Equations Require Import Equations.
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
-  common typing preservation admissible fp_red structural soundness.
+Require Import Logic.PropExtensionality (propositional_extensionality).
-Require Import algorithmic.
-From stdpp Require Import relations (rtc(..), nsteps(..)).
 Require Import ssreflect ssrbool.
-
+Import Logic (inspect).
-Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
+From Ltac2 Require Import Ltac2.
-| A_AbsAbs a b :
+Import Ltac2.Constr.
-  algo_dom a b ->
+Set Default Proof Mode "Classic".
-  (* --------------------- *)
-  algo_dom (PAbs a) (PAbs b)
-
-| A_AbsNeu a u :
-  ishne u ->
-  algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
-  (* --------------------- *)
-  algo_dom (PAbs a) u
-
-| A_NeuAbs a u :
-  ishne u ->
-  algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
-  (* --------------------- *)
-  algo_dom u (PAbs a)
-
-| A_PairPair a0 a1 b0 b1 :
-  algo_dom a0 a1 ->
-  algo_dom b0 b1 ->
-  (* ---------------------------- *)
-  algo_dom (PPair a0 b0) (PPair a1 b1)
-
-| A_PairNeu a0 a1 u :
-  ishne u ->
-  algo_dom a0 (PProj PL u) ->
-  algo_dom a1 (PProj PR u) ->
-  (* ----------------------- *)
-  algo_dom (PPair a0 a1) u
-
-| A_NeuPair a0 a1 u :
-  ishne u ->
-  algo_dom (PProj PL u) a0 ->
-  algo_dom (PProj PR u) a1 ->
-  (* ----------------------- *)
-  algo_dom u (PPair a0 a1)
-
-| A_UnivCong i j :
-  (* -------------------------- *)
-  algo_dom (PUniv i) (PUniv j)
-
-| A_BindCong p0 p1 A0 A1 B0 B1 :
-  algo_dom A0 A1 ->
-  algo_dom B0 B1 ->
-  (* ---------------------------- *)
-  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
-
-| A_VarCong i j :
-  (* -------------------------- *)
-  algo_dom (VarPTm i) (VarPTm j)
-
-| A_ProjCong p0 p1 u0 u1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  (* ---------------------  *)
-  algo_dom (PProj p0 u0) (PProj p1 u1)
-
-| A_AppCong u0 u1 a0 a1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  algo_dom a0 a1 ->
-  (* ------------------------- *)
-  algo_dom (PApp u0 a0) (PApp u1 a1)
-
-| A_HRedL a a' b  :
-  HRed.R a a' ->
-  algo_dom a' b ->
-  (* ----------------------- *)
-  algo_dom a b
-
-| A_HRedR a b b'  :
-  ishne a \/ ishf a ->
-  HRed.R b b' ->
-  algo_dom a b' ->
-  (* ----------------------- *)
-  algo_dom a b.
 
 
-Definition fin_eq {n} (i j : fin n) : bool.
+Require Import ssreflect ssrbool.
-Proof.
+From Hammer Require Import Tactics.
-  induction n.
+
-  - by exfalso.
+Ltac2 destruct_algo () :=
-  - refine (match i , j with
+  lazy_match! goal with
-            | None, None => true
+  | [h : algo_dom ?a ?b |- _ ] =>
-            | Some i, Some j => IHn i j
+      if is_var a then destruct $a; ltac1:(done)  else
+        (if is_var b then destruct $b; ltac1:(done) else ())
+  end.
+
+
+Ltac check_equal_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [h : algo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
+  | _ => idtac
+  end.
+
+Ltac solve_check_equal :=
+  try solve [intros *;
+  match goal with
+  | [|- _ = _] => sauto
+  | _ => idtac
+  end].
+
+Global Set Transparent Obligations.
+
+Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
+
+Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
+  match a, b with
+  | VarPTm i, VarPTm j => nat_eqdec i j
+  | PAbs a, PAbs b => check_equal_r a b _
+  | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PPair a0 b0, PPair a1 b1 =>
+      check_equal_r a0 a1 _ && check_equal_r b0 b1 _
+  | PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PNat, PNat => true
+  | PZero, PZero => true
+  | PSuc a, PSuc b => check_equal_r a b _
+  | PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _
+  | PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _
+  | PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 =>
+      check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _
+  | PUniv i, PUniv j => nat_eqdec i j
+  | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _
   | _, _ => false
-            end).
+  end
-Defined.
+with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool :=
+  match fancy_hred a with
+  | inr a' => check_equal_r (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_equal_r a (proj1_sig b') _
+            | inl hb' => check_equal a b _
+            end
+  end.
 
-Lemma fin_eq_dec {n} (i j : fin n) :
-  Bool.reflect (i = j) (fin_eq i j).
-Proof.
-  revert i j. induction n.
-  - destruct i.
-  - destruct i; destruct j.
-    + specialize (IHn f f0).
-      inversion IHn; subst.
-      simpl. rewrite -H.
-      apply ReflectT.
-      reflexivity.
-      simpl. rewrite -H.
-      apply ReflectF.
-      injection. tauto.
-    + by apply ReflectF.
-    + by apply ReflectF.
-    + by apply ReflectT.
-Defined.
-
-
-Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
-  bool by struct h :=
-  check_equal a b h with (@idP (ishne a || ishf a)) := {
-    | Bool.ReflectT _ _ => _
-    | Bool.ReflectF _ _ => _
-    }.
-
-
-  (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
-  (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
-  (* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
-  (*   check_equal a0 b0 _ && check_equal a1 b1 _; *)
-  (* check_equal (PUniv i) (PUniv j) _ := _; *)
 Next Obligation.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
+  inversion h; subst => //=.
+  exfalso. sfirstorder use:algo_dom_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
+  exfalso. sfirstorder.
+Defined.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
+  destruct b' as [b' hb']. simpl.
+  inversion h; subst.
+  - exfalso.
+    sfirstorder use:algo_dom_no_hred.
+  - exfalso.
+    sfirstorder.
+  - assert (b' = b'0) by eauto using hred_deter. by subst.
+Defined.
+
+(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
+Next Obligation.
+  move => /= a b hdom ha _ hb _.
+  inversion hdom; subst.
+  - assumption.
+  - exfalso; sfirstorder.
+  - exfalso; sfirstorder.
+Defined.
+
+Lemma check_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h.
+Proof. reflexivity. Qed.
+
+Lemma check_equal_abs_neu a u neu h : check_equal (PAbs a) u (A_AbsNeu a u neu h) = check_equal_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) h.
+Proof. case : u neu h => //=.  Qed.
+
+Lemma check_equal_neu_abs a u neu h : check_equal u (PAbs a) (A_NeuAbs a u neu h) = check_equal_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a h.
+Proof. case : u neu h => //=.  Qed.
+
+Lemma check_equal_pair_pair a0 b0 a1 b1 a h :
+  check_equal (PPair a0 b0) (PPair a1 b1) (A_PairPair a0 a1 b0 b1 a h) =
+    check_equal_r a0 a1 a && check_equal_r b0 b1 h.
+Proof. reflexivity. Qed.
+
+Lemma check_equal_pair_neu a0 a1 u neu h h'
+  : check_equal (PPair a0 a1) u (A_PairNeu a0 a1 u neu h h') = check_equal_r a0 (PProj PL u) h && check_equal_r a1 (PProj PR u) h'.
+Proof.
+  case : u neu h h' => //=.
+Qed.
+
+Lemma check_equal_neu_pair a0 a1 u neu h h'
+  : check_equal u (PPair a0 a1) (A_NeuPair a0 a1 u neu h h') = check_equal_r  (PProj PL u) a0 h && check_equal_r (PProj PR u) a1 h'.
+Proof.
+  case : u neu h h' => //=.
+Qed.
+
+Lemma check_equal_bind_bind p0 A0 B0 p1 A1 B1 h0 h1 :
+  check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) (A_BindCong p0 p1 A0 A1 B0 B1 h0 h1) =
+    BTag_eqdec p0 p1 &&  check_equal_r A0 A1 h0 && check_equal_r  B0 B1 h1.
+Proof. reflexivity. Qed.
+
+Lemma check_equal_proj_proj p0 u0 p1 u1 neu0 neu1 h :
+  check_equal (PProj p0 u0) (PProj p1 u1) (A_ProjCong p0 p1 u0 u1 neu0 neu1 h) =
+    PTag_eqdec p0 p1 && check_equal u0 u1 h.
+Proof. reflexivity. Qed.
+
+Lemma check_equal_app_app u0 a0 u1 a1 hu0 hu1 hdom hdom' :
+  check_equal (PApp u0 a0) (PApp u1 a1) (A_AppCong u0 u1 a0 a1 hu0 hu1 hdom hdom') =
+    check_equal u0 u1 hdom && check_equal_r a0 a1 hdom'.
+Proof. reflexivity. Qed.
+
+Lemma check_equal_ind_ind P0 u0 b0 c0 P1 u1 b1 c1 neu0 neu1 domP domu domb domc :
+  check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+    (A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP domu domb domc) =
+    check_equal_r P0 P1 domP && check_equal u0 u1 domu && check_equal_r b0 b1 domb && check_equal_r c0 c1 domc.
+Proof. reflexivity. Qed.
+
+Lemma hred_none a : HRed.nf a -> hred a = None.
+Proof.
+  destruct (hred a) eqn:eq;
+  sfirstorder use:hred_complete, hred_sound.
+Qed.
+
+Ltac simp_check_r := with_strategy opaque [check_equal] simpl in *.
+
+Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom.
+Proof.
+  have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred.
+  have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
+  simp_check_r.
+  destruct (fancy_hred a).
+  destruct (fancy_hred b).
+  reflexivity.
+  exfalso. hauto l:on use:hred_complete.
+  exfalso. hauto l:on use:hred_complete.
+Qed.
+
+Lemma check_equal_hredl a b a' ha doma :
+  check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
+Proof.
   simpl.
-  intros ih.
+  destruct (fancy_hred a).
-Admitted.
+  - hauto q:on unfold:HRed.nf.
+  - destruct s as [x ?].
+    have ? : x = a' by eauto using hred_deter. subst.
+    simpl.
+    f_equal.
+    apply PropExtensionality.proof_irrelevance.
+Qed.
 
-Search (Bool.reflect (is_true _) _).
+Lemma check_equal_hredr a b b' hu r a0 :
-Check idP.
+  check_equal_r a b (A_HRedR a b b' hu r a0) =
+    check_equal_r a b' a0.
+Proof.
+  simpl.
+  destruct (fancy_hred a).
+  - simpl.
+    destruct (fancy_hred b) as [|[b'' hb']].
+    + hauto lq:on unfold:HRed.nf.
+    + simpl.
+      have ? : (b'' = b') by eauto using hred_deter. subst.
+      f_equal.
+      apply PropExtensionality.proof_irrelevance.
+  - exfalso.
+    sfirstorder use:hne_no_hred, hf_no_hred.
+Qed.
 
-Definition metric {n} k (a b : PTm n) :=
+Lemma check_equal_univ i j :
-  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
+  check_equal (PUniv i) (PUniv j) (A_UnivCong i j) = nat_eqdec i j.
-  nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
+Proof. reflexivity. Qed.
 
-Search (nat -> nat -> bool).
+Lemma check_equal_conf a b nfa nfb nfab :
+  check_equal a b (A_Conf a b nfa nfb nfab) = false.
+Proof. destruct a; destruct b => //=. Qed.
+
+#[export]Hint Rewrite check_equal_abs_abs check_equal_abs_neu check_equal_neu_abs check_equal_pair_pair check_equal_pair_neu check_equal_neu_pair check_equal_bind_bind check_equal_hredl check_equal_hredr check_equal_nfnf check_equal_conf : ce_prop.
+
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [h : salgo_dom ?a ?b |- _ ] =>
+      if is_var a then destruct $a; ltac1:(done)  else
+        (if is_var b then destruct $b; ltac1:(done) else ())
+  end.
+
+Ltac check_sub_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
+  | _ => idtac
+  end.
+
+Local Obligation Tactic := try solve [check_sub_triv | sfirstorder].
+
+Program Fixpoint check_sub (a b : PTm) (h : salgo_dom a b) {struct h} :=
+  match a, b with
+  | PBind PPi A0 B0, PBind PPi A1 B1 =>
+      check_sub_r A1 A0 _ && check_sub_r B0 B1 _
+  | PBind PSig A0 B0, PBind PSig A1 B1 =>
+      check_sub_r A0 A1 _ && check_sub_r B0 B1 _
+  | PUniv i, PUniv j =>
+      PeanoNat.Nat.leb i j
+  | PNat, PNat => true
+  | PApp _ _ , PApp _ _ => check_equal a b _
+  | VarPTm _, VarPTm _ => check_equal a b _
+  | PInd _ _ _ _, PInd _ _ _ _ => check_equal a b _
+  | PProj _ _, PProj _ _ => check_equal a b _
+  | _, _ => false
+  end
+with check_sub_r (a b : PTm) (h : salgo_dom_r a b) {struct h} :=
+  match fancy_hred a with
+  | inr a' => check_sub_r (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_sub_r a (proj1_sig b') _
+            | inl hb' => check_sub  a b _
+            end
+  end.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
+  inversion h; subst => //=.
+  exfalso. sfirstorder use:salgo_dom_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
+  exfalso. sfirstorder.
+Defined.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
+  destruct b' as [b' hb']. simpl.
+  inversion h; subst.
+  - exfalso.
+    sfirstorder use:salgo_dom_no_hred.
+  - exfalso.
+    sfirstorder.
+  - assert (b' = b'0) by eauto using hred_deter. by subst.
+Defined.
+
+(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
+Next Obligation.
+  move => /= a b hdom ha _ hb _.
+  inversion hdom; subst.
+  - assumption.
+  - exfalso; sfirstorder.
+  - exfalso; sfirstorder.
+Defined.
+
+Lemma check_sub_pi_pi A0 B0  A1 B1 h0 h1 :
+  check_sub (PBind PPi A0 B0) (PBind PPi A1 B1) (S_PiCong A0 A1 B0 B1 h0 h1) =
+    check_sub_r A1 A0 h0 && check_sub_r B0 B1 h1.
+Proof. reflexivity. Qed.
+
+Lemma check_sub_sig_sig A0 B0  A1 B1 h0 h1 :
+  check_sub (PBind PSig A0 B0) (PBind PSig A1 B1) (S_SigCong A0 A1 B0 B1 h0 h1) =
+    check_sub_r A0 A1 h0 && check_sub_r B0 B1 h1.
+Proof. reflexivity. Qed.
+
+Lemma check_sub_univ_univ i j :
+  check_sub (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j.
+Proof. reflexivity. Qed.
+
+Lemma check_sub_nfnf a b dom : check_sub_r a b (S_NfNf a b dom) = check_sub a b dom.
+Proof.
+  have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
+  have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
+  simpl.
+  destruct (fancy_hred b)=>//=.
+  destruct (fancy_hred a) =>//=.
+  destruct s as [a' ha']. simpl.
+  hauto l:on use:hred_complete.
+  destruct s as [b' hb']. simpl.
+  hauto l:on use:hred_complete.
+Qed.
+
+Lemma check_sub_hredl a b a' ha doma :
+  check_sub_r a b (S_HRedL a a' b ha doma) = check_sub_r a' b doma.
+Proof.
+  simpl.
+  destruct (fancy_hred a).
+  - hauto q:on unfold:HRed.nf.
+  - destruct s as [x ?].
+    have ? : x = a' by eauto using hred_deter. subst.
+    simpl.
+    f_equal.
+    apply PropExtensionality.proof_irrelevance.
+Qed.
+
+Lemma check_sub_hredr a b b' hu r a0 :
+  check_sub_r a b (S_HRedR a b b' hu r a0) =
+    check_sub_r a b' a0.
+Proof.
+  simpl.
+  destruct (fancy_hred a).
+  - simpl.
+    destruct (fancy_hred b) as [|[b'' hb']].
+    + hauto lq:on unfold:HRed.nf.
+    + simpl.
+      have ? : (b'' = b') by eauto using hred_deter. subst.
+      f_equal.
+      apply PropExtensionality.proof_irrelevance.
+  - exfalso.
+    sfirstorder use:hne_no_hred, hf_no_hred.
+Qed.
+
+Lemma check_sub_neuneu a b i a0 : check_sub a b (S_NeuNeu a b i a0) = check_equal a b a0.
+Proof. destruct a,b => //=. Qed.
+
+Lemma check_sub_conf a b n n0 i : check_sub a b (S_Conf a b n n0 i) = false.
+Proof. destruct a,b=>//=; ecrush inv:BTag. Qed.
+
+#[export]Hint Rewrite check_sub_neuneu check_sub_conf check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.

theories/executable_correct.v

@@ -0,0 +1,259 @@
+From Equations Require Import Equations.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common executable algorithmic.
+Require Import ssreflect ssrbool.
+From stdpp Require Import relations (rtc(..)).
+From Hammer Require Import Tactics.
+
+Lemma coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b.
+Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed.
+
+Lemma coqeq_no_hred a b : a ↔ b -> HRed.nf a /\ HRed.nf b.
+Proof. induction 1;
+         qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf.
+Qed.
+
+Lemma coqleq_no_hred a b : a ⋖ b -> HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred, coqeqr_no_hred unfold:HRed.nf.
+Qed.
+
+Lemma coqeq_neuneu u0 u1 :
+  ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
+Proof.
+  inversion 3; subst => //=.
+Qed.
+
+Lemma coqeq_neuneu' u0 u1 :
+  neuneu_nonconf u0 u1 ->
+  u0 ↔ u1 ->
+  u0 ∼ u1.
+Proof.
+  induction 2 => //=; destruct u => //=.
+Qed.
+
+Lemma check_equal_sound :
+  (forall a b (h : algo_dom a b), check_equal a b h -> a ↔ b) /\
+  (forall a b (h : algo_dom_r a b), check_equal_r a b h -> a ⇔ b).
+Proof.
+  apply algo_dom_mutual.
+  - move => a b h.
+    move => h0.
+    rewrite check_equal_abs_abs.
+    constructor. tauto.
+  - move => a u i h0 ih h.
+    apply CE_AbsNeu => //.
+    apply : ih. simp check_equal tm_to_eq_view in h.
+    by rewrite check_equal_abs_neu in h.
+  - move => a u i h ih h0.
+    apply CE_NeuAbs=>//.
+    apply ih.
+    by rewrite check_equal_neu_abs in h0.
+  - move => a0 a1 b0 b1 a ha h.
+    move => h0.
+    rewrite check_equal_pair_pair. move /andP => [h1 h2].
+    sauto lq:on.
+  - move => a0 a1 u neu h ih h' ih' he.
+    rewrite check_equal_pair_neu in he.
+    apply CE_PairNeu => //; hauto lqb:on.
+  - move => a0 a1 u i a ha a2 hb.
+    rewrite check_equal_neu_pair => *.
+    apply CE_NeuPair => //; hauto lqb:on.
+  - sfirstorder.
+  - hauto l:on use:CE_SucSuc.
+  - move => i j /sumboolP.
+    hauto lq:on use:CE_UnivCong.
+  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1 h2.
+    rewrite check_equal_bind_bind in h2.
+    move : h2.
+    move /andP => [/andP [h20 h21] h3].
+    move /sumboolP : h20 => ?. subst.
+    hauto l:on use:CE_BindCong.
+  - sfirstorder.
+  - move => i j /sumboolP ?.  subst.
+    apply : CE_NeuNeu. apply CE_VarCong.
+  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
+    rewrite check_equal_app_app in hE.
+    move /andP : hE => [h0 h1].
+    sauto lq:on use:coqeq_neuneu.
+  - move => p0 p1 u0 u1 neu0 neu1 h ih he.
+    apply CE_NeuNeu.
+    rewrite check_equal_proj_proj in he.
+    move /andP : he => [/sumboolP ? h1]. subst.
+    sauto lq:on use:coqeq_neuneu.
+  - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
+    rewrite check_equal_ind_ind.
+    move /andP => [/andP [/andP [h0 h1] h2 ] h3].
+    sauto lq:on use:coqeq_neuneu.
+  - move => a b n n0 i. by rewrite check_equal_conf.
+  - move => a b dom h ih. apply : CE_HRed; eauto using rtc_refl.
+    rewrite check_equal_nfnf in ih.
+    tauto.
+  - move => a a' b ha doma ih hE.
+    rewrite check_equal_hredl in hE. sauto lq:on.
+  - move => a b b' hu r a0 ha hb. rewrite check_equal_hredr in hb.
+    sauto lq:on rew:off.
+Qed.
+
+Ltac ce_solv := move => *; simp ce_prop in *; hauto qb:on rew:off inv:CoqEq, CoqEq_Neu.
+
+Lemma check_equal_complete :
+  (forall a b (h : algo_dom a b), ~ check_equal a b h -> ~ a ↔ b) /\
+  (forall a b (h : algo_dom_r a b), ~ check_equal_r a b h -> ~ a ⇔ b).
+Proof.
+  apply algo_dom_mutual.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - ce_solv.
+  - move => i j.
+    rewrite check_equal_univ.
+    case : nat_eqdec => //=.
+    ce_solv.
+  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1.
+    rewrite check_equal_bind_bind.
+    move /negP.
+    move /nandP.
+    case. move /nandP.
+    case. move => h. have : p0 <> p1  by sauto lqb:on.
+    clear. move => ?. hauto lq:on rew:off inv:CoqEq, CoqEq_Neu.
+    hauto qb:on inv:CoqEq,CoqEq_Neu.
+    hauto qb:on inv:CoqEq,CoqEq_Neu.
+  - simp check_equal. done.
+  - move => i j. move => h. have {h} : ~ nat_eqdec i j by done.
+    case : nat_eqdec => //=. ce_solv.
+  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
+    rewrite check_equal_app_app.
+    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
+  - move => p0 p1 u0 u1 neu0 neu1 h ih.
+    rewrite check_equal_proj_proj.
+    move /negP /nandP. case.
+    case : PTag_eqdec => //=. sauto lq:on.
+    sauto lqb:on.
+  - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
+    rewrite check_equal_ind_ind.
+    move => + h.
+    inversion h; subst.
+    inversion H; subst.
+    move /negP /nandP.
+    case. move/nandP.
+    case. move/nandP.
+    case. qauto b:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+  - rewrite /tm_conf.
+    move => a b n n0 i. simp ce_prop.
+    move => _. inversion 1; subst => //=.
+    + destruct b => //=.
+    + destruct a => //=.
+    + destruct b => //=.
+    + destruct a => //=.
+    + hauto l:on inv:CoqEq_Neu.
+  - move => a b h ih.
+    rewrite check_equal_nfnf.
+    move : ih => /[apply].
+    move => + h0.
+    have {h} [? ?] : HRed.nf a /\ HRed.nf b by sfirstorder use:algo_dom_no_hred.
+    inversion h0; subst.
+    hauto l:on use:hreds_nf_refl.
+  - move => a a' b h dom.
+    simp ce_prop => /[apply].
+    move => + h1. inversion h1; subst.
+    inversion H; subst.
+    + sfirstorder use:coqeq_no_hred unfold:HRed.nf.
+    + have ? : y = a' by eauto using hred_deter. subst.
+      sauto lq:on.
+  - move => a b b' u hr dom ihdom.
+    rewrite check_equal_hredr.
+    move => + h. inversion h; subst.
+    have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred.
+    move => {}/ihdom.
+    inversion H0; subst.
+    + have ? : HRed.nf b'0 by hauto l:on use:coqeq_no_hred.
+      sfirstorder unfold:HRed.nf.
+    + sauto lq:on use:hred_deter.
+Qed.
+
+Ltac simp_sub := with_strategy opaque [check_equal] simpl in *.
+
+Lemma check_sub_sound :
+  (forall a b (h : salgo_dom a b), check_sub a b h -> a ⋖ b) /\
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h -> a ≪ b).
+Proof.
+  apply salgo_dom_mutual; try done.
+  - simpl. move => i j [];
+    sauto lq:on use:Reflect.Nat_leb_le.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
+    simp ce_prop.
+    hauto lqb:on ctrs:CoqLEq.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
+    simp ce_prop.
+    hauto lqb:on ctrs:CoqLEq.
+  - qauto ctrs:CoqLEq.
+  - move => a b i a0.
+    simp ce_prop.
+    move => h. apply CLE_NeuNeu.
+    hauto lq:on use:check_equal_sound, coqeq_neuneu', coqeq_symmetric_mutual.
+  - move => a b n n0 i.
+    by simp ce_prop.
+  - move => a b h ih. simp ce_prop. hauto l:on.
+  - move => a a' b hr h ih.
+    simp ce_prop.
+    sauto lq:on rew:off.
+  - move => a b b' n r dom ihdom.
+    simp ce_prop.
+    move : ihdom => /[apply].
+    move {dom}.
+    sauto lq:on rew:off.
+Qed.
+
+Lemma check_sub_complete :
+  (forall a b (h : salgo_dom a b), check_sub a b h = false -> ~ a ⋖ b) /\
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h = false -> ~ a ≪ b).
+Proof.
+  apply salgo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
+  - move => i j /=.
+    move => + h. inversion h; subst => //=.
+    sfirstorder use:PeanoNat.Nat.leb_le.
+    hauto lq:on inv:CoqEq_Neu.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
+    move /nandP.
+    case.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
+    move /nandP.
+    case.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
+  - move => a b i hs. simp ce_prop.
+    move => + h. inversion h; subst => //=.
+    move => /negP h0.
+    eapply check_equal_complete in h0.
+    apply h0. by constructor.
+  - move => a b s ihs. simp ce_prop.
+    move => h0 h1. apply ihs =>//.
+    have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
+    inversion h1; subst.
+    hauto l:on use:hreds_nf_refl.
+  - move => a a' b h dom.
+    simp ce_prop => /[apply].
+    move => + h1. inversion h1; subst.
+    inversion H; subst.
+    + sfirstorder use:coqleq_no_hred unfold:HRed.nf.
+    + have ? : y = a' by eauto using hred_deter. subst.
+      sauto lq:on.
+  - move => a b b' u hr dom ihdom.
+    rewrite check_sub_hredr.
+    move => + h. inversion h; subst.
+    have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred.
+    move => {}/ihdom.
+    inversion H0; subst.
+    + have ? : HRed.nf b'0 by hauto l:on use:coqleq_no_hred.
+      sfirstorder unfold:HRed.nf.
+    + sauto lq:on use:hred_deter.
+Qed.

theories/preservation.v

@@ -1,91 +1,20 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Lemma App_Inv n Γ (b a : PTm n) U :
-  Γ ⊢ PApp b a ∈ U ->
-  exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
-Proof.
-  move E : (PApp b a) => u hu.
-  move : b a E. elim : n Γ u U / hu => n //=.
-  - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
-    exists A,B.
-    repeat split => //=.
-    have [i] : exists i, Γ ⊢ PBind PPi A B ∈  PUniv i by sfirstorder use:regularity.
-    hauto lq:on use:bind_inst, E_Refl.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
 
-Lemma Abs_Inv n Γ (a : PTm (S n)) U :
+Lemma Ind_Inv Γ P (a : PTm) b c U :
-  Γ ⊢ PAbs a ∈ U ->
-  exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
-Proof.
-  move E : (PAbs a) => u hu.
-  move : a E. elim : n Γ u U / hu => n //=.
-  - move => Γ a A B i hP _ ha _ a0 [*]. subst.
-    exists A, B. repeat split => //=.
-    hauto lq:on use:E_Refl, Su_Eq.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Proj1_Inv n Γ (a : PTm n) U :
-  Γ ⊢ PProj PL a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
-Proof.
-  move E : (PProj PL a) => u hu.
-  move :a E. elim : n Γ u U / hu => n //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    eapply regularity in ha.
-    move : ha => [i].
-    move /Bind_Inv => [j][h _].
-    by move /E_Refl /Su_Eq in h.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Proj2_Inv n Γ (a : PTm n) U :
-  Γ ⊢ PProj PR a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
-Proof.
-  move E : (PProj PR a) => u hu.
-  move :a E. elim : n Γ u U / hu => n //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    have ha' := ha.
-    eapply regularity in ha.
-    move : ha => [i ha].
-    move /T_Proj1 in ha'.
-    apply : bind_inst; eauto.
-    apply : E_Refl ha'.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Pair_Inv n Γ (a b : PTm n) U :
-  Γ ⊢ PPair a b ∈ U ->
-  exists A B, Γ ⊢ a ∈ A /\
-         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
-         Γ ⊢ PBind PSig A B ≲ U.
-Proof.
-  move E : (PPair a b) => u hu.
-  move : a b E. elim : n Γ u U / hu => n //=.
-  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
-    exists A,B. repeat split => //=.
-    move /E_Refl /Su_Eq : hS. apply.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Ind_Inv n Γ P (a : PTm n) b c U :
   Γ ⊢ PInd P a b c ∈ U ->
-  exists i, funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i /\
+  exists i, (cons PNat Γ) ⊢ P ∈ PUniv i /\
        Γ ⊢ a ∈ PNat /\
        Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P /\
-      funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
+          (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
        Γ ⊢ subst_PTm (scons a VarPTm) P ≲ U.
 Proof.
   move E : (PInd P a b c)=> u hu.
-  move : P a b c E. elim : n Γ u U / hu => n //=.
+  move : P a b c E. elim : Γ u U / hu => //=.
   - move => Γ P a b c i hP _ ha _ hb _ hc _ P0 a0 b0 c0 [*]. subst.
     exists i. repeat split => //=.
     have : Γ ⊢ subst_PTm (scons a VarPTm) P ∈ subst_PTm (scons a VarPTm) (PUniv i) by hauto l:on use:substing_wt.
@@ -93,57 +22,79 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+Lemma E_Abs Γ a b A B :
-  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+  A :: Γ ⊢ a ≡ b ∈ B ->
+  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
 Proof.
-  move => n a b Γ A ha.
-  move /App_Inv : ha.
-  move => [A0][B0][ha][hb]hS.
-  move /Abs_Inv : ha => [A1][B1][ha]hS0.
-  have hb' := hb.
-  move /E_Refl in hb.
-  have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
-  have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
-  move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
-  move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
   move => h.
-  apply : E_Conv; eauto.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff.
-  apply : E_AppAbs; eauto.
+  have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity.
-  eauto using T_Conv.
+  have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
+  have hΓ' : ⊢ A::Γ by eauto with wt.
+  set k := max i j.
+  have [? ?] : i <= k /\ j <= k by lia.
+  have {}hA : Γ ⊢ A ∈ PUniv k by hauto l:on use:T_Conv, Su_Univ.
+  have {}hB : A :: Γ ⊢ B ∈ PUniv k by hauto lq:on use:T_Conv, Su_Univ.
+  have hPi : Γ ⊢ PBind PPi A B ∈ PUniv k by eauto with wt.
+  apply : E_FunExt; eauto with wt.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  apply : E_Transitive => /=. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  apply /E_Symmetric /E_Transitive. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  asimpl. rewrite !subst_scons_id. by apply E_Symmetric.
 Qed.
 
-Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+Lemma E_Pair Γ a0 b0 a1 b1 A B i :
-    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+  Γ ⊢ 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.
 Proof.
-  move => n a b Γ A.
+  move => hSig ha hb.
-  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity.
-  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\
-  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+                     Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity.
-  move /Su_Sig_Proj1 in hS.
+  have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt.
-  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac].
-  apply : E_Conv; eauto.
+  apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl.
-  apply : E_ProjPair1; eauto.
+  have ea : Γ ⊢ PProj PL (PPair a0 b0) ≡ a0 ∈ A by eauto with wt.
+  have : Γ ⊢ PProj PR (PPair a0 b0) ≡ b0 ∈ subst_PTm (scons a0 VarPTm) B by eauto with wt.
+  have : Γ ⊢ PProj PL (PPair a1 b1) ≡ a1 ∈ A by eauto using E_ProjPair1 with wt.
+  have : Γ ⊢ PProj PR (PPair a1 b1) ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B.
+  apply : E_Conv; eauto using E_ProjPair2 with wt.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto using E_Symmetric.
+  move => *.
+  apply : E_PairExt; eauto using E_Symmetric, E_Transitive.
+  apply : E_Conv. by eauto using E_Symmetric, E_Transitive.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. by eauto. apply /E_Symmetric /E_Transitive.
+  by eauto using E_ProjPair1.
+  eauto.
 Qed.
 
-Lemma Suc_Inv n Γ (a : PTm n) A :
+Lemma Suc_Inv Γ (a : PTm) A :
   Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
 Proof.
   move E : (PSuc a) => u hu.
   move : a E.
-  elim : n Γ u A /hu => //=.
+  elim : Γ u A /hu => //=.
-  - move => n Γ a ha iha a0 [*]. subst.
+  - move => Γ a ha iha a0 [*]. subst.
     split => //=. eapply wff_mutual in ha.
     apply : Su_Eq.
     apply E_Refl. by apply T_Nat'.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma RRed_Eq n Γ (a b : PTm n) A :
+Lemma RRed_Eq Γ (a b : PTm) A :
   Γ ⊢ a ∈ A ->
   RRed.R a b ->
   Γ ⊢ a ≡ b ∈ A.
 Proof.
-  move => + h. move : Γ A. elim : n a b /h => n.
+  move => + h. move : Γ A. elim : a b /h.
   - apply E_AppAbs.
   - move => p a b Γ A.
     case : p => //=.
@@ -159,7 +110,7 @@ Proof.
         apply : Su_Sig_Proj2; eauto.
       move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
       move {hS}.
-      move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
+      move => ?. apply : E_Conv; eauto. apply : typing.E_ProjPair2; eauto.
   - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
   - move => P a b c Γ A.
     move /Ind_Inv.
@@ -214,7 +165,7 @@ Proof.
   - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
 Qed.
 
-Theorem subject_reduction n Γ (a b A : PTm n) :
+Theorem subject_reduction Γ (a b A : PTm) :
   Γ ⊢ a ∈ A ->
   RRed.R a b ->
   Γ ⊢ b ∈ A.

theories/soundness.v

@@ -1,15 +1,15 @@
-Require Import Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.unscoped Autosubst2.syntax.
 Require Import fp_red logrel typing.
 From Hammer Require Import Tactics.
 
 Theorem fundamental_theorem :
-  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
+  (forall Γ, ⊢ Γ -> ⊨ Γ) /\
-  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
+  (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
-  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
+  (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
-  (forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
+  (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
-  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
+  apply wt_mutual; eauto with sem.
   Unshelve. all : exact 0.
 Qed.
 
-Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Lemma synsub_to_usub : forall Γ (a b : PTm), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
 Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.

theories/termination.v

@@ -0,0 +1,5 @@
+Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable.
+From Hammer Require Import Tactics.
+Require Import ssreflect ssrbool.
+From stdpp Require Import relations (nsteps (..), rtc(..)).
+Import Psatz.

theories/typing.v

@@ -1,240 +1,230 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 
 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 : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
-| T_Var n Γ (i : fin n) :
+| T_Var i Γ A :
   ⊢ Γ ->
-  Γ ⊢ VarPTm i ∈ Γ i
+  lookup i Γ A ->
+  Γ ⊢ VarPTm i ∈ A
 
-| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
+| T_Bind Γ i p (A : PTm) (B : PTm) :
   Γ ⊢ A ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ PUniv i ->
   Γ ⊢ PBind p A B ∈ PUniv i
 
-| T_Abs n Γ (a : PTm (S n)) A B i :
+| T_Abs Γ (a : PTm) A B i :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
   Γ ⊢ PAbs a ∈ PBind PPi A B
 
-| T_App n Γ (b a : PTm n) 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 n Γ (a b : PTm n) A B i :
+| 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 n Γ (a : PTm n) A B :
+| T_Proj1 Γ (a : PTm) A B :
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ∈ A
 
-| T_Proj2 n Γ (a : PTm n) A B :
+| T_Proj2 Γ (a : PTm) A B :
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 
-| T_Univ n Γ i :
+| T_Univ Γ i :
   ⊢ Γ ->
-  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
+  Γ ⊢ PUniv i ∈ PUniv (S i)
 
-| T_Nat n Γ i :
+| T_Nat Γ i :
   ⊢ Γ ->
-  Γ ⊢ PNat : PTm n ∈ PUniv i
+  Γ ⊢ PNat ∈ PUniv i
 
-| T_Zero n Γ :
+| T_Zero Γ :
   ⊢ Γ ->
-  Γ ⊢ PZero : PTm n ∈ PNat
+  Γ ⊢ PZero ∈ PNat
 
-| T_Suc n Γ (a : PTm n) :
+| T_Suc Γ (a : PTm) :
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ PSuc a ∈ PNat
 
-| T_Ind s Γ P (a : PTm s) b c i :
+| T_Ind Γ P (a : PTm) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  cons PNat Γ ⊢ P ∈ PUniv i ->
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) 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 n Γ (a : PTm n) A B :
+| T_Conv Γ (a : PTm) A B :
   Γ ⊢ a ∈ A ->
   Γ ⊢ A ≲ B ->
   Γ ⊢ a ∈ B
 
-with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
+with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| E_Refl n Γ (a : PTm n) A :
+| E_Refl Γ (a : PTm ) A :
   Γ ⊢ a ∈ A ->
   Γ ⊢ a ≡ a ∈ A
 
-| E_Symmetric n Γ (a b : PTm n) A :
+| E_Symmetric Γ (a b : PTm) A :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ b ≡ a ∈ A
 
-| E_Transitive n Γ (a b c : PTm n) A :
+| E_Transitive Γ (a b c : PTm) A :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ b ≡ c ∈ A ->
   Γ ⊢ a ≡ c ∈ A
 
 (* Congruence *)
-| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
-  ⊢ Γ ->
   Γ ⊢ A0 ∈ PUniv i ->
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
 
-| E_Abs n Γ (a b : PTm (S n)) A B i :
+| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
-
-| E_App n Γ i (b0 b1 a0 a1 : PTm n) 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 n Γ (a0 a1 b0 b1 : PTm n) A B i :
+| E_Proj1 Γ (a b : PTm) A B :
-  Γ ⊢ 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 n Γ (a b : PTm n) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
 
-| E_Proj2 n Γ i (a b : PTm n) A B :
+| 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 n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
+| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
   Γ ⊢ a0 ≡ a1 ∈ PNat ->
   Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
-  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) 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 n Γ (a b : PTm n) :
+| E_SucCong Γ (a b : PTm) :
   Γ ⊢ a ≡ b ∈ PNat ->
   Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
 
-| E_Conv n Γ (a b : PTm n) A B :
+| E_Conv Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ A ≲ B ->
   Γ ⊢ a ≡ b ∈ B
 
 (* Beta *)
-| E_AppAbs n Γ (a : PTm (S n)) b A B i:
+| E_AppAbs Γ (a : PTm) b A B i:
   Γ ⊢ PBind PPi A B ∈ PUniv i ->
   Γ ⊢ b ∈ A ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
   Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
 
-| E_ProjPair1 n Γ (a b : PTm n) A B i :
+| 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 n Γ (a b : PTm n) A B i :
+| 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 n Γ P i (b : PTm n) c :
+| E_IndZero Γ P i (b : PTm) c :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) 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 s Γ P (a : PTm s) b c i :
+| E_IndSuc Γ P (a : PTm) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) 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_FunExt Γ (a b : PTm) A B i :
-| E_AppEta n Γ (b : PTm n) A B i :
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
-  ⊢ Γ ->
+  Γ ⊢ a ∈ PBind PPi A B ->
-  Γ ⊢ 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
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B
 
-| E_PairEta n Γ (a : PTm n) A B i :
+| E_PairExt Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ PBind PSig A B ∈ PUniv i ->
   Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B
 
-with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| Su_Transitive  n Γ (A B C : PTm n) :
+| Su_Transitive Γ (A B C : PTm) :
   Γ ⊢ A ≲ B ->
   Γ ⊢ B ≲ C ->
   Γ ⊢ A ≲ C
 
 (* Congruence *)
-| Su_Univ n Γ i j :
+| Su_Univ Γ i j :
   ⊢ Γ ->
   i <= j ->
-  Γ ⊢ PUniv i : PTm n ≲ PUniv j
+  Γ ⊢ PUniv i ≲ PUniv j
 
-| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i :
+| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
-  ⊢ Γ ->
   Γ ⊢ A0 ∈ PUniv i ->
   Γ ⊢ A1 ≲ A0 ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1 ->
   Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
 
-| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i :
+| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
-  ⊢ Γ ->
   Γ ⊢ A1 ∈ PUniv i ->
   Γ ⊢ A0 ≲ A1 ->
-  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
+  (cons A1 Γ) ⊢ B0 ≲ B1 ->
   Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
 
 (* Injecting from equalities *)
-| Su_Eq n Γ (A : PTm n) B i  :
+| Su_Eq Γ (A : PTm) B i  :
   Γ ⊢ A ≡ B ∈ PUniv i ->
   Γ ⊢ A ≲ B
 
 (* Projection axioms *)
-| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
   Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
   Γ ⊢ A1 ≲ A0
 
-| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
   Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
   Γ ⊢ A0 ≲ A1
 
-| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
+| 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 n Γ (a0 a1 A0 A1 : PTm n) B0 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 : forall {n}, (fin n -> PTm n) -> Prop :=
+with Wff : list PTm -> Prop :=
 | Wff_Nil :
-  ⊢ null
+  ⊢ nil
-| Wff_Cons n Γ (A : PTm n) i :
+| Wff_Cons Γ (A : PTm) i :
   ⊢ Γ ->
   Γ ⊢ A ∈ PUniv i ->
   (* -------------------------------- *)
-  ⊢ funcomp (ren_PTm shift) (scons A Γ)
+  ⊢ (cons A Γ)
 
 where
 "Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
@@ -245,10 +235,3 @@ Scheme wf_ind := Induction for Wff 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. ... *)