Add termination

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,24 @@
-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 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 +28,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 +38,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.

theories/common.v

@@ -1,41 +1,70 @@
-Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
+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.
 
-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 +76,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 +88,90 @@ 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 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.

theories/executable.v

@@ -1,58 +1,165 @@
 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).
+From Ltac2 Require Import Ltac2.
+Import Ltac2.Constr.
+Set Default Proof Mode "Classic".
 
-Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
+
+Require Import ssreflect ssrbool.
+From Hammer Require Import Tactics.
+
+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 _ _ => (~~ ishf a) && (~~ ishf b)
+  | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b)
+  | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b)
+  | PNat, PNat => true
+  | PUniv _, PUniv _ => true
+  | PBind _ _ _, PBind _ _ _ => true
+  | _,_=> false
+  end.
+
+Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
+
+Inductive eq_view : PTm -> PTm -> Type :=
+| V_AbsAbs a b :
+  eq_view (PAbs a) (PAbs b)
+| V_AbsNeu a b :
+  ~~ ishf b ->
+  eq_view (PAbs a) b
+| V_NeuAbs a b :
+  ~~ ishf a ->
+  eq_view a (PAbs b)
+| V_VarVar i j :
+  eq_view (VarPTm i) (VarPTm j)
+| V_PairPair a0 b0 a1 b1 :
+  eq_view (PPair a0 b0) (PPair a1 b1)
+| V_PairNeu a0 b0 u :
+  ~~ ishf u ->
+  eq_view (PPair a0 b0) u
+| V_NeuPair u a1 b1 :
+  ~~ ishf u ->
+  eq_view u (PPair a1 b1)
+| V_ZeroZero :
+  eq_view PZero PZero
+| V_SucSuc a b :
+  eq_view (PSuc a) (PSuc b)
+| V_AppApp u0 b0 u1 b1 :
+  eq_view (PApp u0 b0) (PApp u1 b1)
+| V_ProjProj p0 u0 p1 u1 :
+  eq_view (PProj p0 u0) (PProj p1 u1)
+| V_IndInd P0 u0 b0 c0  P1 u1 b1 c1 :
+  eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+| V_NatNat :
+  eq_view PNat PNat
+| V_BindBind p0 A0 B0 p1 A1 B1 :
+  eq_view (PBind p0 A0 B0) (PBind p1 A1 B1)
+| V_UnivUniv i j :
+  eq_view (PUniv i) (PUniv j)
+| V_Others a b :
+  tm_conf a b ->
+  eq_view a b.
+
+Equations tm_to_eq_view (a b : PTm) : eq_view a b :=
+  tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b;
+  tm_to_eq_view (PAbs a) (PApp b0 b1) := V_AbsNeu a (PApp b0 b1) _;
+  tm_to_eq_view (PAbs a) (VarPTm i) := V_AbsNeu a (VarPTm i) _;
+  tm_to_eq_view (PAbs a) (PProj p b) := V_AbsNeu a (PProj p b) _;
+  tm_to_eq_view (PAbs a) (PInd P u b c) := V_AbsNeu a (PInd P u b c) _;
+  tm_to_eq_view (VarPTm i) (PAbs a) := V_NeuAbs (VarPTm i) a _;
+  tm_to_eq_view (PApp b0 b1) (PAbs b) := V_NeuAbs (PApp b0 b1) b _;
+  tm_to_eq_view (PProj p b) (PAbs a) := V_NeuAbs (PProj p b) a _;
+  tm_to_eq_view (PInd P u b c) (PAbs a) := V_NeuAbs (PInd P u b c) a _;
+  tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j;
+  tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1;
+  (* tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; *)
+  tm_to_eq_view (PPair a0 b0) (VarPTm i) := V_PairNeu a0 b0 (VarPTm i) _;
+  tm_to_eq_view (PPair a0 b0) (PApp c0 c1) := V_PairNeu a0 b0 (PApp c0 c1) _;
+  tm_to_eq_view (PPair a0 b0) (PProj p c) := V_PairNeu a0 b0 (PProj p c) _;
+  tm_to_eq_view (PPair a0 b0) (PInd P t0 t1 t2) := V_PairNeu a0 b0 (PInd P t0 t1 t2) _;
+  (* tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; *)
+  tm_to_eq_view (VarPTm i) (PPair a1 b1) := V_NeuPair (VarPTm i) a1 b1 _;
+  tm_to_eq_view (PApp t0 t1) (PPair a1 b1) := V_NeuPair (PApp t0 t1) a1 b1 _;
+  tm_to_eq_view (PProj t0 t1) (PPair a1 b1) := V_NeuPair (PProj t0 t1) a1 b1 _;
+  tm_to_eq_view (PInd t0 t1 t2 t3) (PPair a1 b1) := V_NeuPair (PInd t0 t1 t2 t3) a1 b1 _;
+  tm_to_eq_view PZero PZero := V_ZeroZero;
+  tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b;
+  tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1;
+  tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1;
+  tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1;
+  tm_to_eq_view PNat PNat := V_NatNat;
+  tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j;
+  tm_to_eq_view (PBind p0 A0 B0)  (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1;
+  tm_to_eq_view a b := V_Others a b _.
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
 | A_AbsAbs a b :
-  algo_dom a b ->
+  algo_dom_r a b ->
   (* --------------------- *)
   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_r 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_r (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_r a0 a1 ->
-  algo_dom b0 b1 ->
+  algo_dom_r 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_r a0 (PProj PL u) ->
-  algo_dom a1 (PProj PR u) ->
+  algo_dom_r 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_r (PProj PL u) a0 ->
-  algo_dom (PProj PR u) a1 ->
+  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 A0 A1 ->
+  algo_dom_r A0 A1 ->
-  algo_dom B0 B1 ->
+  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)
@@ -68,78 +175,314 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
   ishne u0 ->
   ishne u1 ->
   algo_dom u0 u1 ->
-  algo_dom a0 a1 ->
+  algo_dom_r a0 a1 ->
   (* ------------------------- *)
   algo_dom (PApp u0 a0) (PApp u1 a1)
 
-| A_HRedL a a' b  :
+| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
-  HRed.R a a' ->
+  ishne u0 ->
-  algo_dom a' b ->
+  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 :
+  HRed.nf a ->
+  HRed.nf b ->
+  tm_conf a b ->
   algo_dom a b
 
-| A_HRedR a b b'  :
+with algo_dom_r : PTm  -> PTm -> Prop :=
-  ishne a \/ ishf a ->
+| A_NfNf a b :
-  HRed.R b b' ->
+  algo_dom 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 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.
 
-Definition fin_eq {n} (i j : fin n) : bool.
+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.
+
+Lemma algo_dom_no_hred (a b : PTm) :
+  algo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
 Proof.
-  induction n.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
-  - by exfalso.
+Qed.
-  - refine (match i , j with
+
-            | None, None => true
+Derive Signature for algo_dom algo_dom_r.
-            | Some i, Some j => IHn i j
+
-            | _, _ => false
+Fixpoint hred (a : PTm) : option (PTm) :=
-            end).
+    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 fin_eq_dec {n} (i j : fin n) :
+Ltac2 destruct_algo () :=
-  Bool.reflect (i = j) (fin_eq i j).
+  lazy_match! goal with
-Proof.
+  | [h : algo_dom ?a ?b |- _ ] =>
-  revert i j. induction n.
+      if is_var a then destruct $a; ltac1:(done)  else
-  - destruct i.
+        (if is_var b then destruct $b; ltac1:(done) else ())
-  - destruct i; destruct j.
+  end.
-    + 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) :
+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].
+
+#[derive(equations=no)]Equations check_equal (a b : PTm) (h : algo_dom a b) :
   bool by struct h :=
-  check_equal a b h with (@idP (ishne a || ishf a)) := {
+  check_equal a b h with tm_to_eq_view a b :=
-    | Bool.ReflectT _ _ => _
+  check_equal _ _ h (V_VarVar i j) := nat_eqdec i j;
-    | Bool.ReflectF _ _ => _
+  check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv);
-    }.
+  check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
+  check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
+  check_equal _ _ h (V_PairPair a0 b0 a1 b1) :=
+    check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_PairNeu a0 b0 u _) :=
+    check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv);
+  check_equal _ _ h (V_NeuPair u a1 b1 _) :=
+    check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv);
+  check_equal _ _ h V_NatNat := true;
+  check_equal _ _ h V_ZeroZero := true;
+  check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv);
+  check_equal _ _ h (V_ProjProj p0 a p1 b) :=
+    PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv);
+  check_equal _ _ h (V_AppApp a0 b0 a1 b1) :=
+    check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) :=
+    check_equal_r P0 P1 ltac:(check_equal_triv) &&
+      check_equal u0 u1 ltac:(check_equal_triv) &&
+      check_equal_r b0 b1 ltac:(check_equal_triv) &&
+      check_equal_r c0 c1 ltac:(check_equal_triv);
+  check_equal _ _ h (V_UnivUniv i j) := nat_eqdec i j;
+  check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) :=
+    BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv);
+  check_equal _ _ _ _ := false
+
+  (* check_equal a b h := false; *)
+  with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
+  bool by struct h0 :=
+    check_equal_r a b h with (fancy_hred a) :=
+      check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _;
+      check_equal_r a b h (inl h')  with (fancy_hred b) :=
+        | inr b' := check_equal_r a (proj1_sig b') _;
+                 | inl h'' := check_equal a b _.
 
 
-  (* 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.
+  intros.
+  inversion h; subst => //=.
+  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
+  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
+Defined.
+
+Next Obligation.
+  intros.
+  destruct h.
+  exfalso. sfirstorder use: algo_dom_no_hred.
+  exfalso. sfirstorder.
+  assert (  b' = b'0)by eauto using hred_deter. subst.
+  apply h.
+Defined.
+
+Next Obligation.
+  simpl. intros.
+  inversion h; subst =>//=.
+  exfalso. sfirstorder use:algo_dom_no_hred.
+  move {h}.
+  assert (a' = a'0) by eauto using hred_deter, hred_sound. by subst.
+  exfalso. sfirstorder use:hne_no_hred, hf_no_hred.
+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.
+
+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.
   simpl.
-  intros ih.
+  rewrite /check_equal_r_functional.
-Admitted.
+  destruct (fancy_hred a).
+  simpl.
+  destruct (fancy_hred b).
+  reflexivity.
+  exfalso. hauto l:on use:hred_complete.
+  exfalso. hauto l:on use:hred_complete.
+Qed.
 
-Search (Bool.reflect (is_true _) _).
+Lemma check_equal_hredl a b a' ha doma :
-Check idP.
+  check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
+Proof.
+  simpl.
+  rewrite /check_equal_r_functional.
+  destruct (fancy_hred a).
+  - hauto q:on unfold:HRed.nf.
+  - destruct s as [x ?].
+    rewrite /check_equal_r_functional.
+    have ? : x = a' by eauto using hred_deter. subst.
+    simpl.
+    f_equal.
+    apply PropExtensionality.proof_irrelevance.
+Qed.
 
-Definition metric {n} k (a b : PTm n) :=
+Lemma check_equal_hredr a b b' hu r a0 :
-  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
+  check_equal_r a b (A_HRedR a b b' hu r a0) =
-  nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
+    check_equal_r a b' a0.
+Proof.
+  simpl. rewrite /check_equal_r_functional.
+  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.
 
-Search (nat -> nat -> bool).
+Lemma check_equal_univ i j :
+  check_equal (PUniv i) (PUniv j) (A_UnivCong i j) = nat_eqdec i j.
+Proof. reflexivity. Qed.
+
+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.

theories/executable_correct.v

@@ -0,0 +1,179 @@
+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.
+
+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.
+
+
+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 coqeq_neuneu u0 u1 :
+  ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
+Proof.
+  inversion 3; subst => //=.
+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 => 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 => 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 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.
+
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. 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 => 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 => 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 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.

theories/preservation.v

@@ -1,15 +1,15 @@
-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.
 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 :
+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 : n Γ u U / hu => n //=.
+  move : b a E. elim : Γ u U / hu => //=.
   - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
     exists A,B.
     repeat split => //=.
@@ -18,24 +18,24 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma Abs_Inv n Γ (a : PTm (S n)) U :
+Lemma Abs_Inv Γ (a : PTm) U :
   Γ ⊢ PAbs a ∈ U ->
-  exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
+  exists A B, (cons 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 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 Proj1_Inv n Γ (a : PTm n) U :
+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 : n Γ u U / hu => n //=.
+  move :a E. elim : Γ u U / hu => //=.
   - move => Γ a A B ha _ a0 [*]. subst.
     exists A, B. split => //=.
     eapply regularity in ha.
@@ -45,12 +45,12 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma Proj2_Inv n Γ (a : PTm n) U :
+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 : n Γ u U / hu => n //=.
+  move :a E. elim : Γ u U / hu => //=.
   - move => Γ a A B ha _ a0 [*]. subst.
     exists A, B. split => //=.
     have ha' := ha.
@@ -62,30 +62,30 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma Pair_Inv n Γ (a b : PTm n) U :
+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 : n Γ u U / hu => n //=.
+  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 Ind_Inv n Γ P (a : PTm n) b c U :
+Lemma Ind_Inv Γ P (a : PTm) 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,10 +93,10 @@ 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_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 => n a b Γ A ha.
+  move => a b Γ A ha.
   move /App_Inv : ha.
   move => [A0][B0][ha][hb]hS.
   move /Abs_Inv : ha => [A1][B1][ha]hS0.
@@ -112,10 +112,10 @@ Proof.
   eauto using T_Conv.
 Qed.
 
-Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
     Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
 Proof.
-  move => n a b Γ A.
+  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.
@@ -125,25 +125,25 @@ Proof.
   apply : 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 => //=.
@@ -214,7 +214,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].
   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,14 @@
+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 (..)).
+
+Definition term_metric k (a b : PTm) :=
+  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
+
+Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
+Proof.
+  elim /Wf_nat.lt_wf_ind.
+  move => n ih a b h.
+  case : (fancy_hred a); cycle 1.
+  move => [a' ha']. apply : A_HRedL; eauto.

theories/typing.v

@@ -1,240 +1,237 @@
-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_Abs Γ (a b : PTm) A B i :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B ->
+  (cons A Γ) ⊢ a ≡ b ∈ B ->
   Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
 
-| E_App n Γ i (b0 b1 a0 a1 : PTm n) A B :
+| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
 
-| E_Pair n Γ (a0 a1 b0 b1 : PTm n) A B i :
+| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
   Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
 
-| E_Proj1 n Γ (a b : PTm n) A B :
+| E_Proj1 Γ (a b : PTm) 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_AppEta n Γ (b : PTm n) A B i :
+| E_AppEta Γ (b : PTm) A B i :
-  ⊢ Γ ->
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊢ b ∈ PBind PPi A B ->
   Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
 
-| E_PairEta n Γ (a : PTm n) A B i :
+| E_PairEta Γ (a : PTm ) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
 
-with LEq : 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).