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 ucoq -o theories/Autosubst2/syntax.v syntax.sig
+	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 
 FORCE:

syntax.sig

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

theories/Autosubst2/fintype.v

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

theories/Autosubst2/unscoped.v

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

theories/admissible.v

@@ -1,88 +1,45 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Derive Inversion wff_inv with (forall Γ, ⊢ Γ) Sort Prop.
+Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
 
-Lemma T_Abs Γ (a : PTm ) A B :
-  (cons A Γ) ⊢ a ∈ B ->
+Lemma Wff_Cons_Inv n Γ (A : PTm n) :
+  ⊢ funcomp (ren_PTm shift) (scons A Γ) ->
+  ⊢ Γ /\ 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, (cons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
-  have hΓ : ⊢  (cons A Γ) by sfirstorder use:wff_mutual.
-  hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
+  have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
+  move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
+  hauto lq:on rew:off use:T_Bind', typing.T_Abs.
 Qed.
 
-
-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 :
+Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
 Proof.
   move => h0 h1.
@@ -92,7 +49,7 @@ Proof.
   firstorder.
 Qed.
 
-Lemma E_App Γ (b0 b1 a0 a1 : PTm ) A B :
+Lemma E_App n Γ (b0 b1 a0 a1 : PTm n) A B :
   Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
@@ -102,7 +59,7 @@ Proof.
   move : E_App h. by repeat move/[apply].
 Qed.
 
-Lemma E_Proj2 Γ (a b : PTm) A B :
+Lemma E_Proj2 n Γ (a b : PTm n) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
 Proof.
@@ -110,155 +67,3 @@ 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,601 +1,97 @@
-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.
+Require Import Autosubst2.fintype Autosubst2.syntax ssreflect.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
-From stdpp Require Import relations (rtc(..)).
 
-Inductive lookup : nat -> list PTm -> PTm -> Prop :=
-| 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 lookup_deter i Γ A B :
-  lookup i Γ A ->
-  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.
-  move => h i j.
-  case : i => //=; case : j => //=.
-  move => i j. rewrite /funcomp. hauto lq:on rew:off unfold:ren_inj.
-Qed.
+Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
 
 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
-  | nat -> nat => (ltac1:(case => *//=; qauto l:on use:up_injective unfold:ren_inj))
+  | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2))
   | _ => solve_anti_ren ()
   end.
 
 Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
-Lemma ren_injective (a b : PTm) (ξ : nat -> nat) :
-  ren_inj ξ ->
+Lemma up_injective n m (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
+  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+Proof.
+  sblast inv:option.
+Qed.
+
+Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
   ren_PTm ξ a = ren_PTm ξ b ->
   a = b.
 Proof.
-  move : ξ b. elim : a => //; try solve_anti_ren.
-  move => p ihp ξ []//=. hauto lq:on inv:PTm, nat ctrs:- use:up_injective.
+  move : m ξ b.
+  elim : n / a => //; try solve_anti_ren.
+
+  move => n a iha m ξ []//=.
+  move => u hξ [h].
+  apply iha in h. by subst.
+  destruct i, j=>//=.
+  hauto l:on.
+
+  move => n p A ihA B ihB m ξ []//=.
+  move => b A0 B0  hξ [?]. subst.
+  move => ?. have ? : A0 = A by firstorder. subst.
+  move => ?. have : B = B0. apply : ihB; eauto.
+  sauto.
+  congruence.
 Qed.
 
-Inductive HF : Set :=
-| H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
-
-Definition ishf (a : PTm) :=
+Definition ishf {n} (a : PTm n) :=
   match a with
   | PPair _ _ => true
   | PAbs _ => true
   | PUniv _ => true
   | PBind _ _ _ => true
-  | PNat => true
-  | PSuc _ => true
-  | PZero => true
   | _ => false
   end.
 
-Definition toHF (a : PTm) :=
-  match a with
-  | PPair _ _ => H_Pair
-  | PAbs _ => H_Abs
-  | PUniv _ => H_Univ
-  | PBind p _ _ => H_Bind p
-  | PNat => H_Nat
-  | PSuc _ => H_Suc
-  | PZero => H_Zero
-  | _ => H_Bot
-  end.
-
-Fixpoint ishne (a : PTm) :=
+Fixpoint ishne {n} (a : PTm n) :=
   match a with
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
-  | PInd _ n _ _ => ishne n
+  | PBot => true
   | _ => false
   end.
 
-Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false.
+Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
 
-Definition isuniv (a : PTm) := if a is PUniv _ then true else false.
+Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
 
-Definition ispair (a : PTm) :=
+Definition ispair {n} (a : PTm n) :=
   match a with
   | PPair _ _ => true
   | _ => false
   end.
 
-Definition isnat (a : PTm) := if a is PNat then true else false.
-
-Definition iszero (a : PTm) := if a is PZero then true else false.
-
-Definition issuc (a : PTm) := if a is PSuc _ then true else false.
-
-Definition isabs (a : PTm) :=
+Definition isabs {n} (a : PTm n) :=
   match a with
   | PAbs _ => true
   | _ => false
   end.
 
-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) :
+Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
 
-Definition isabs_ren (a : PTm)  (ξ : nat -> nat) :
+Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   isabs (ren_PTm ξ a) = isabs a.
 Proof. case : a => //=. Qed.
 
-Definition ispair_ren (a : PTm)  (ξ : nat -> nat) :
+Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
 
-Definition ishne_ren (a : PTm)  (ξ : nat -> nat) :
+Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   ishne (ren_PTm ξ a) = ishne a.
-Proof. move : ξ. elim : a => //=. Qed.
-
-Lemma renaming_shift Γ A :
-  renaming_ok (cons A Γ) Γ shift.
-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.
+Proof. move : m ξ. elim : n / a => //=. Qed.

theories/executable.v

@@ -1,350 +1,145 @@
 From Equations Require Import Equations.
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
-Require Import Logic.PropExtensionality (propositional_extensionality).
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
+  common typing preservation admissible fp_red structural soundness.
+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 :=
+| A_AbsAbs a b :
+  algo_dom 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 (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.
 
 
-Require Import ssreflect ssrbool.
-From Hammer Require Import Tactics.
-
-Ltac2 destruct_algo () :=
-  lazy_match! goal with
-  | [h : algo_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_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 _
+Definition fin_eq {n} (i j : fin n) : bool.
+Proof.
+  induction n.
+  - by exfalso.
+  - refine (match i , j with
+            | None, None => true
+            | Some i, Some j => IHn i j
             | _, _ => false
-  end
-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.
-
-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.
+            end).
 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'.
+Lemma fin_eq_dec {n} (i j : fin n) :
+  Bool.reflect (i = j) (fin_eq i j).
 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).
+  revert i j. induction n.
+  - destruct i.
+  - destruct i; destruct j.
+    + specialize (IHn f f0).
+      inversion IHn; subst.
+      simpl. rewrite -H.
+      apply ReflectT.
       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.
-  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_equal_hredr a b b' hu r a0 :
-  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.
-
-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.
-
-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.
+      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 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.
+  intros ih.
+Admitted.
 
-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.
+Search (Bool.reflect (is_true _) _).
+Check idP.
 
-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.
+Definition metric {n} k (a b : PTm n) :=
+  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 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.
+Search (nat -> nat -> bool).

theories/executable_correct.v

@@ -1,259 +0,0 @@
-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,100 +1,119 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-
-Lemma Ind_Inv Γ P (a : PTm) b c U :
-  Γ ⊢ PInd P a b c ∈ U ->
-  exists i, (cons PNat Γ) ⊢ P ∈ PUniv i /\
-       Γ ⊢ a ∈ PNat /\
-       Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P /\
-          (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
-       Γ ⊢ subst_PTm (scons a VarPTm) P ≲ U.
+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 : (PInd P a b c)=> u hu.
-  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.
-    eauto using E_Refl, Su_Eq.
+  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 E_Abs Γ a b A B :
-  A :: Γ ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
+Lemma Abs_Inv n Γ (a : PTm (S n)) 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 E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+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.
-  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff.
-  have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity.
-  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.
+  apply : E_Conv; eauto.
+  apply : E_AppAbs; eauto.
+  eauto using T_Conv.
 Qed.
 
-Lemma E_Pair Γ a0 b0 a1 b1 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.
+Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
 Proof.
-  move => hSig ha hb.
-  have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity.
-  have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\
-                     Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity.
-  have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt.
-  have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac].
-  apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl.
-  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.
+  move => n 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 Suc_Inv Γ (a : PTm) A :
-  Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
-Proof.
-  move E : (PSuc a) => u hu.
-  move : a E.
-  elim : Γ u A /hu => //=.
-  - 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 Γ (a b : PTm) A :
+Lemma RRed_Eq n Γ (a b : PTm n) A :
   Γ ⊢ a ∈ A ->
   RRed.R a b ->
   Γ ⊢ a ≡ b ∈ A.
 Proof.
-  move => + h. move : Γ A. elim : a b /h.
+  move => + h. move : Γ A. elim : n a b /h => n.
   - apply E_AppAbs.
   - move => p a b Γ A.
     case : p => //=.
@@ -110,14 +129,7 @@ Proof.
         apply : Su_Sig_Proj2; eauto.
       move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
       move {hS}.
-      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.
-    move => [i][hP][ha][hb][hc]hSu.
-    apply : E_Conv; eauto.
-    apply : E_IndSuc'; eauto.
-    hauto l:on use:Suc_Inv.
+      move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
   - qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
   - move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
     have {}/iha iha := ih0.
@@ -158,14 +170,9 @@ Proof.
     have {}/ihA ihA := h1.
     apply : E_Conv; eauto.
     apply E_Bind'; eauto using E_Refl.
-  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
-  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
-  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
-  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
-  - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
 Qed.
 
-Theorem subject_reduction Γ (a b A : PTm) :
+Theorem subject_reduction n Γ (a b A : PTm n) :
   Γ ⊢ a ∈ A ->
   RRed.R a b ->
   Γ ⊢ b ∈ A.

theories/soundness.v

@@ -1,15 +1,15 @@
-Require Import Autosubst2.unscoped Autosubst2.syntax.
+Require Import Autosubst2.fintype Autosubst2.syntax.
 Require Import fp_red logrel typing.
 From Hammer Require Import Tactics.
 
 Theorem fundamental_theorem :
-  (forall Γ, ⊢ Γ -> ⊨ Γ) /\
-  (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
-  (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
-  (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
-  apply wt_mutual; eauto with sem.
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
+  (forall n Γ (a b : PTm n), Γ ⊢ 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 Γ (a b : PTm), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ 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

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