From 2f04bcc75cf06bb4b760e7588f79ad13cdc70b91 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sat, 25 Jan 2025 16:08:21 -0700 Subject: [PATCH] Add a mostly finished eta postponement proof --- .gitignore | 63 + Makefile | 27 + _CoqProject | 2 + syntax.sig | 15 + theories/Autosubst2/core.v | 159 ++ theories/Autosubst2/fintype.v | 419 +++++ theories/Autosubst2/syntax.v | 824 ++++++++++ theories/fp_red.v | 2722 +++++++++++++++++++++++++++++++++ 8 files changed, 4231 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 _CoqProject create mode 100644 syntax.sig create mode 100644 theories/Autosubst2/core.v create mode 100644 theories/Autosubst2/fintype.v create mode 100644 theories/Autosubst2/syntax.v create mode 100644 theories/fp_red.v diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..5894672 --- /dev/null +++ b/.gitignore @@ -0,0 +1,63 @@ +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mlg.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.coq-native +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache +native_compute_profile_*.data + +# generated timing files +*.timing.diff +*.v.after-timing +*.v.before-timing +*.v.timing +time-of-build-after.log +time-of-build-before.log +time-of-build-both.log +time-of-build-pretty.log + +# generated coq files + +# emacs temporary files +*~ + +*.aux +*.bbl +*.blg +*.out +*.log +paper/paper-output.tex +paper/rules.tex +paper/paper-output.pdf +proofs +proofs.zip +CoqMakefile +CoqMakefile.conf \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..ef5b76f --- /dev/null +++ b/Makefile @@ -0,0 +1,27 @@ +COQMAKEFILE=CoqMakefile + +theories: $(COQMAKEFILE) FORCE + $(MAKE) -f $(COQMAKEFILE) + +validate: $(COQMAKEFILE) FORCE + $(MAKE) -f $(COQMAKEFILE) validate + +$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + $(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE) + +install: $(COQMAKEFILE) + $(MAKE) -f $^ install + +uninstall: $(COQMAKEFILE) + $(MAKE) -f $(COQMAKEFILE) uninstall + +theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig + autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig + +.PHONY: clean FORCE + +clean: + test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) ) + rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + +FORCE: diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..24173e2 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,2 @@ +-R theories ImpredIrrel +theories diff --git a/syntax.sig b/syntax.sig new file mode 100644 index 0000000..d052897 --- /dev/null +++ b/syntax.sig @@ -0,0 +1,15 @@ +PTm(VarPTm) : Type +PTag : Type +Ty : Type + +Fun : Ty -> Ty -> Ty +Prod : Ty -> Ty -> Ty +Void : Ty + +PL : PTag +PR : PTag + +PAbs : Ty -> (bind PTm in PTm) -> PTm +PApp : PTm -> PTm -> PTm +PPair : PTm -> PTm -> PTm +PProj : PTag -> PTm -> PTm diff --git a/theories/Autosubst2/core.v b/theories/Autosubst2/core.v new file mode 100644 index 0000000..ec6ba13 --- /dev/null +++ b/theories/Autosubst2/core.v @@ -0,0 +1,159 @@ +(* Function composition *) + +Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) := + fun x => g (f x). + +Lemma funcomp_assoc {W X Y Z} (g: Y -> Z) (f: X -> Y) (h: W -> X) : + funcomp g (funcomp f h) = (funcomp (funcomp g f) h). +Proof. + reflexivity. +Qed. + + +(** ** Functor Instances + +Exemplary functor instances needed to make Autosubst's generation possible for functors. +Two things are important: +1. The names are fixed. +2. For Coq to check termination, also the proofs have to be closed with Defined. + *) + +(** *** List Instance *) +Require Import List. + +Notation "'list_map'" := map. + +Definition list_ext {A B} {f g : A -> B} : + (forall x, f x = g x) -> forall xs, list_map f xs = list_map g xs. + intros H. induction xs. reflexivity. + cbn. f_equal. apply H. apply IHxs. +Defined. + +Definition list_id {A} { f : A -> A} : + (forall x, f x = x) -> forall xs, list_map f xs = xs. +Proof. + intros H. induction xs. reflexivity. + cbn. rewrite H. rewrite IHxs; eauto. +Defined. + +Definition list_comp {A B C} {f: A -> B} {g: B -> C} {h} : + (forall x, (funcomp g f) x = h x) -> forall xs, map g (map f xs) = map h xs. +Proof. + induction xs. reflexivity. + cbn. rewrite <- H. f_equal. apply IHxs. +Defined. + +(** *** Prod Instance *) + +Definition prod_map {A B C D} (f : A -> C) (g : B -> D) (p : A * B) : + C * D. +Proof. + destruct p as [a b]. split. + exact (f a). exact (g b). +Defined. + +Definition prod_id {A B} {f : A -> A} {g : B -> B} : + (forall x, f x = x) -> (forall x, g x = x) -> forall p, prod_map f g p = p. +Proof. + intros H0 H1. destruct p. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +Definition prod_ext {A B C D} {f f' : A -> C} {g g': B -> D} : + (forall x, f x = f' x) -> (forall x, g x = g' x) -> forall p, prod_map f g p = prod_map f' g' p. +Proof. + intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +Definition prod_comp {A B C D E F} {f1 : A -> C} {g1 : C -> E} {h1 : A -> E} {f2: B -> D} {g2: D -> F} {h2 : B -> F}: + (forall x, (funcomp g1 f1) x = h1 x) -> (forall x, (funcomp g2 f2) x = h2 x) -> forall p, prod_map g1 g2 (prod_map f1 f2 p) = prod_map h1 h2 p. +Proof. + intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +(** *** Option Instance *) + +Definition option_map {A B} (f : A -> B) (p : option A) : + option B := +match p with + | Some a => Some (f a) + | None => None +end. + +Definition option_id {A} {f : A -> A} : + (forall x, f x = x) -> forall p, option_map f p = p. +Proof. + intros H. destruct p ; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +Definition option_ext {A B} {f f' : A -> B} : + (forall x, f x = f' x) -> forall p, option_map f p = option_map f' p. +Proof. + intros H. destruct p as [a|] ; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +Definition option_comp {A B C} {f : A -> B} {g : B -> C} {h : A -> C}: + (forall x, (funcomp g f) x = h x) -> + forall p, option_map g (option_map f p) = option_map h p. +Proof. + intros H. destruct p as [a|]; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +#[export] Hint Rewrite in_map_iff : FunctorInstances. + +(* Declaring the scopes that all our notations will live in *) +Declare Scope fscope. +Declare Scope subst_scope. + +Ltac eta_reduce := + repeat match goal with + | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *) + end. + +Ltac minimize := + repeat match goal with + | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *) + | [|- context[fun x => ?g (?f x)]] => change (fun x => g (f x)) with (funcomp g f) (* funcomp folding *) + end. + +(* had to add this tactic abbreviation because I could not print a setoid_rewrite with the arrow *) +Ltac setoid_rewrite_left t := setoid_rewrite <- t. + +Ltac check_no_evars := + match goal with + | [|- ?x] => assert_fails (has_evar x) + end. + +Require Import Setoid Morphisms. + +Lemma pointwise_forall {X Y:Type} (f g: X -> Y) : + (pointwise_relation _ eq f g) -> forall x, f x = g x. +Proof. + trivial. +Qed. + +#[export] Instance funcomp_morphism {X Y Z} : + Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp. +Proof. + cbv - [funcomp]. + intros g0 g1 Hg f0 f1 Hf x. + unfold funcomp. rewrite Hf, Hg. + reflexivity. +Qed. + +#[export] Instance funcomp_morphism2 {X Y Z} : + Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> eq ==> eq) funcomp. +Proof. + intros g0 g1 Hg f0 f1 Hf ? x ->. + unfold funcomp. rewrite Hf, Hg. + reflexivity. +Qed. + +Ltac unfold_funcomp := match goal with + | |- context[(funcomp ?f ?g) ?s] => change ((funcomp f g) s) with (f (g s)) + end. diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v new file mode 100644 index 0000000..99508b6 --- /dev/null +++ b/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. diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v new file mode 100644 index 0000000..b37b721 --- /dev/null +++ b/theories/Autosubst2/syntax.v @@ -0,0 +1,824 @@ +Require Import core fintype. + +Require Import Setoid Morphisms Relation_Definitions. + + +Module Core. + +Inductive PTag : Type := + | PL : PTag + | PR : PTag. + +Lemma congr_PL : PL = PL. +Proof. +exact (eq_refl). +Qed. + +Lemma congr_PR : PR = PR. +Proof. +exact (eq_refl). +Qed. + +Inductive Ty : Type := + | Fun : Ty -> Ty -> Ty + | Prod : Ty -> Ty -> Ty + | Void : Ty. + +Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) + (H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0)) + (ap (fun x => Fun t0 x) H1)). +Qed. + +Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) + (H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0)) + (ap (fun x => Prod t0 x) H1)). +Qed. + +Lemma congr_Void : Void = Void. +Proof. +exact (eq_refl). +Qed. + +Inductive PTm (n_PTm : nat) : Type := + | VarPTm : fin n_PTm -> PTm n_PTm + | PAbs : Ty -> PTm (S n_PTm) -> PTm n_PTm + | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm + | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm + | PProj : PTag -> PTm n_PTm -> PTm n_PTm. + +Lemma congr_PAbs {m_PTm : nat} {s0 : Ty} {s1 : PTm (S m_PTm)} {t0 : Ty} + {t1 : PTm (S m_PTm)} (H0 : s0 = t0) (H1 : s1 = t1) : + PAbs m_PTm s0 s1 = PAbs m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PAbs m_PTm x s1) H0)) + (ap (fun x => PAbs m_PTm t0 x) H1)). +Qed. + +Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} + {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PApp m_PTm s0 s1 = PApp m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp m_PTm x s1) H0)) + (ap (fun x => PApp m_PTm t0 x) H1)). +Qed. + +Lemma congr_PPair {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} + {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PPair m_PTm s0 s1 = PPair m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair m_PTm x s1) H0)) + (ap (fun x => PPair m_PTm t0 x) H1)). +Qed. + +Lemma congr_PProj {m_PTm : nat} {s0 : PTag} {s1 : PTm m_PTm} {t0 : PTag} + {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PProj m_PTm s0 s1 = PProj m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0)) + (ap (fun x => PProj m_PTm t0 x) H1)). +Qed. + +Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) : + fin (S m) -> fin (S n). +Proof. +exact (up_ren xi). +Defined. + +Lemma upRen_list_PTm_PTm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) + : fin (plus p m) -> fin (plus p n). +Proof. +exact (upRen_p p xi). +Defined. + +Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm := + match s with + | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0) + | PAbs _ s0 s1 => PAbs n_PTm s0 (ren_PTm (upRen_PTm_PTm xi_PTm) s1) + | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1) + end. + +Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : + fin (S m) -> PTm (S n_PTm). +Proof. +exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)). +Defined. + +Lemma up_list_PTm_PTm (p : nat) {m : nat} {n_PTm : nat} + (sigma : fin m -> PTm n_PTm) : fin (plus p m) -> PTm (plus p n_PTm). +Proof. +exact (scons_p p (funcomp (VarPTm (plus p n_PTm)) (zero_p p)) + (funcomp (ren_PTm (shift_p p)) sigma)). +Defined. + +Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm +:= + match s with + | VarPTm _ s0 => sigma_PTm s0 + | PAbs _ s0 s1 => PAbs n_PTm s0 (subst_PTm (up_PTm_PTm sigma_PTm) s1) + | PApp _ s0 s1 => + PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PPair _ s0 s1 => + PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PProj _ s0 s1 => PProj n_PTm s0 (subst_PTm sigma_PTm s1) + end. + +Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm) + (Eq : forall x, sigma x = VarPTm m_PTm x) : + forall x, up_PTm_PTm sigma x = VarPTm (S m_PTm) x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upId_list_PTm_PTm {p : nat} {m_PTm : nat} + (sigma : fin m_PTm -> PTm m_PTm) (Eq : forall x, sigma x = VarPTm m_PTm x) + : forall x, up_list_PTm_PTm p sigma x = VarPTm (plus p m_PTm) x. +Proof. +exact (fun n => + scons_p_eta (VarPTm (plus p m_PTm)) + (fun n => ap (ren_PTm (shift_p p)) (Eq n)) (fun n => eq_refl)). +Qed. + +Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) +(Eq_PTm : forall x, sigma_PTm x = VarPTm m_PTm x) (s : PTm m_PTm) {struct s} + : subst_PTm sigma_PTm s = s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) + (idSubst_PTm sigma_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0) + (idSubst_PTm sigma_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) + end. + +Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) + (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : + forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap shift (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upExtRen_list_PTm_PTm {p : nat} {m : nat} {n : nat} + (xi : fin m -> fin n) (zeta : fin m -> fin n) + (Eq : forall x, xi x = zeta x) : + forall x, upRen_list_PTm_PTm p xi x = upRen_list_PTm_PTm p zeta x. +Proof. +exact (fun n => + scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))). +Qed. + +Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (zeta_PTm : fin m_PTm -> fin n_PTm) +(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm m_PTm) {struct s} : +ren_PTm xi_PTm s = ren_PTm zeta_PTm s := + match s with + | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0) + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) + (upExtRen_PTm_PTm _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) + end. + +Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) + (tau : fin m -> PTm n_PTm) (Eq : forall x, sigma x = tau x) : + forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upExt_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} + (sigma : fin m -> PTm n_PTm) (tau : fin m -> PTm n_PTm) + (Eq : forall x, sigma x = tau x) : + forall x, up_list_PTm_PTm p sigma x = up_list_PTm_PTm p tau x. +Proof. +exact (fun n => + scons_p_congr (fun n => eq_refl) + (fun n => ap (ren_PTm (shift_p p)) (Eq n))). +Qed. + +Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm n_PTm) (tau_PTm : fin m_PTm -> PTm n_PTm) +(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm m_PTm) {struct s} : +subst_PTm sigma_PTm s = subst_PTm tau_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) + (upExt_PTm_PTm _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) + end. + +Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) + (zeta : fin l -> fin m) (rho : fin k -> fin m) + (Eq : forall x, funcomp zeta xi x = rho x) : + forall x, + funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x. +Proof. +exact (up_ren_ren xi zeta rho Eq). +Qed. + +Lemma up_ren_ren_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m : nat} + (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m) + (Eq : forall x, funcomp zeta xi x = rho x) : + forall x, + funcomp (upRen_list_PTm_PTm p zeta) (upRen_list_PTm_PTm p xi) x = + upRen_list_PTm_PTm p rho x. +Proof. +exact (up_ren_ren_p Eq). +Qed. + +Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) +(rho_PTm : fin m_PTm -> fin l_PTm) +(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm m_PTm) +{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := + match s with + | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0) + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) + (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) + (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) + end. + +Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat} + (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : + forall x, + funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma up_ren_subst_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m_PTm : nat} + (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : + forall x, + funcomp (up_list_PTm_PTm p tau) (upRen_list_PTm_PTm p xi) x = + up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ _ n) + (scons_p_congr (fun z => scons_p_head' _ _ z) + (fun z => + eq_trans (scons_p_tail' _ _ (xi z)) + (ap (ren_PTm (shift_p p)) (Eq z))))). +Qed. + +Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm m_PTm) +{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) + (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) + (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) + (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) + (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) + end. + +Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} + (sigma : fin k -> PTm l_PTm) (zeta_PTm : fin l_PTm -> fin m_PTm) + (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : + forall x, + funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x = + up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => + eq_trans + (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm) + (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n)) + (eq_trans + (eq_sym + (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm) + (fun x => eq_refl) (sigma fin_n))) + (ap (ren_PTm shift) (Eq fin_n))) + | None => eq_refl + end). +Qed. + +Lemma up_subst_ren_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} + {m_PTm : nat} (sigma : fin k -> PTm l_PTm) + (zeta_PTm : fin l_PTm -> fin m_PTm) (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : + forall x, + funcomp (ren_PTm (upRen_list_PTm_PTm p zeta_PTm)) (up_list_PTm_PTm p sigma) + x = up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ _ n) + (scons_p_congr + (fun x => ap (VarPTm (plus p m_PTm)) (scons_p_head' _ _ x)) + (fun n => + eq_trans + (compRenRen_PTm (shift_p p) (upRen_list_PTm_PTm p zeta_PTm) + (funcomp (shift_p p) zeta_PTm) + (fun x => scons_p_tail' _ _ x) (sigma n)) + (eq_trans + (eq_sym + (compRenRen_PTm zeta_PTm (shift_p p) + (funcomp (shift_p p) zeta_PTm) (fun x => eq_refl) + (sigma n))) (ap (ren_PTm (shift_p p)) (Eq n)))))). +Qed. + +Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x) +(s : PTm m_PTm) {struct s} : +ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) + (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) + (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) + (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) + (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) + end. + +Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} + (sigma : fin k -> PTm l_PTm) (tau_PTm : fin l_PTm -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : + forall x, + funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x = + up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => + eq_trans + (compRenSubst_PTm shift (up_PTm_PTm tau_PTm) + (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl) + (sigma fin_n)) + (eq_trans + (eq_sym + (compSubstRen_PTm tau_PTm shift + (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl) + (sigma fin_n))) (ap (ren_PTm shift) (Eq fin_n))) + | None => eq_refl + end). +Qed. + +Lemma up_subst_subst_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} + {m_PTm : nat} (sigma : fin k -> PTm l_PTm) + (tau_PTm : fin l_PTm -> PTm m_PTm) (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : + forall x, + funcomp (subst_PTm (up_list_PTm_PTm p tau_PTm)) (up_list_PTm_PTm p sigma) x = + up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans + (scons_p_comp' (funcomp (VarPTm (plus p l_PTm)) (zero_p p)) _ _ n) + (scons_p_congr + (fun x => scons_p_head' _ (fun z => ren_PTm (shift_p p) _) x) + (fun n => + eq_trans + (compRenSubst_PTm (shift_p p) (up_list_PTm_PTm p tau_PTm) + (funcomp (up_list_PTm_PTm p tau_PTm) (shift_p p)) + (fun x => eq_refl) (sigma n)) + (eq_trans + (eq_sym + (compSubstRen_PTm tau_PTm (shift_p p) _ + (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n))) + (ap (ren_PTm (shift_p p)) (Eq n)))))). +Qed. + +Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x) +(s : PTm m_PTm) {struct s} : +subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) + (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) + (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) + (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) + (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) + end. + +Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) + (s : PTm m_PTm) : + ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s. +Proof. +exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renRen'_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm)) + (ren_PTm (funcomp zeta_PTm xi_PTm)). +Proof. +exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) + (s : PTm m_PTm) : + subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s. +Proof. +exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm)) + (subst_PTm (funcomp tau_PTm xi_PTm)). +Proof. +exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) + (s : PTm m_PTm) : + ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = + subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s. +Proof. +exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substRen_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm)) + (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)). +Proof. +exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) + (s : PTm m_PTm) : + subst_PTm tau_PTm (subst_PTm sigma_PTm s) = + subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s. +Proof. +exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm)) + (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)). +Proof. +exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma rinstInst_up_PTm_PTm {m : nat} {n_PTm : nat} (xi : fin m -> fin n_PTm) + (sigma : fin m -> PTm n_PTm) + (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : + forall x, + funcomp (VarPTm (S n_PTm)) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma rinstInst_up_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} + (xi : fin m -> fin n_PTm) (sigma : fin m -> PTm n_PTm) + (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : + forall x, + funcomp (VarPTm (plus p n_PTm)) (upRen_list_PTm_PTm p xi) x = + up_list_PTm_PTm p sigma x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ (VarPTm (plus p n_PTm)) n) + (scons_p_congr (fun z => eq_refl) + (fun n => ap (ren_PTm (shift_p p)) (Eq n)))). +Qed. + +Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (sigma_PTm : fin m_PTm -> PTm n_PTm) +(Eq_PTm : forall x, funcomp (VarPTm n_PTm) xi_PTm x = sigma_PTm x) +(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 s1 => + congr_PAbs (eq_refl s0) + (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) + (rinstInst_up_PTm_PTm _ _ Eq_PTm) s1) + | PApp _ s0 s1 => + congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) + | PProj _ s0 s1 => + congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) + end. + +Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) : + ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm n_PTm) xi_PTm) s. +Proof. +exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma rinstInst'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) : + pointwise_relation _ eq (ren_PTm xi_PTm) + (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)). +Proof. +exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma instId'_PTm {m_PTm : nat} (s : PTm m_PTm) : + subst_PTm (VarPTm m_PTm) s = s. +Proof. +exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +Qed. + +Lemma instId'_PTm_pointwise {m_PTm : nat} : + pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id. +Proof. +exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +Qed. + +Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s. +Proof. +exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). +Qed. + +Lemma rinstId'_PTm_pointwise {m_PTm : nat} : + pointwise_relation _ eq (@ren_PTm m_PTm m_PTm id) id. +Proof. +exact (fun s => + eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). +Qed. + +Lemma varL'_PTm {m_PTm : nat} {n_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm n_PTm) (x : fin m_PTm) : + subst_PTm sigma_PTm (VarPTm m_PTm x) = sigma_PTm x. +Proof. +exact (eq_refl). +Qed. + +Lemma varL'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm n_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm m_PTm)) + sigma_PTm. +Proof. +exact (fun x => eq_refl). +Qed. + +Lemma varLRen'_PTm {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) (x : fin m_PTm) : + ren_PTm xi_PTm (VarPTm m_PTm x) = VarPTm n_PTm (xi_PTm x). +Proof. +exact (eq_refl). +Qed. + +Lemma varLRen'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm m_PTm)) + (funcomp (VarPTm n_PTm) xi_PTm). +Proof. +exact (fun x => eq_refl). +Qed. + +Class Up_PTm X Y := + up_PTm : X -> Y. + +#[global] +Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := + (@subst_PTm m_PTm n_PTm). + +#[global] +Instance Up_PTm_PTm {m n_PTm : nat}: (Up_PTm _ _) := (@up_PTm_PTm m n_PTm). + +#[global] +Instance Ren_PTm {m_PTm n_PTm : nat}: (Ren1 _ _ _) := (@ren_PTm m_PTm n_PTm). + +#[global] +Instance VarInstance_PTm {n_PTm : nat}: (Var _ _) := (@VarPTm n_PTm). + +Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s [ sigma_PTm ]" := (subst_PTm sigma_PTm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "↑__PTm" := up_PTm (only printing) : subst_scope. + +Notation "↑__PTm" := up_PTm_PTm (only printing) : subst_scope. + +Notation "⟨ xi_PTm ⟩" := (ren_PTm xi_PTm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s ⟨ xi_PTm ⟩" := (ren_PTm xi_PTm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "'var'" := VarPTm ( at level 1, only printing) : subst_scope. + +Notation "x '__PTm'" := (@ids _ _ VarInstance_PTm x) +( at level 5, format "x __PTm", only printing) : subst_scope. + +Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : +subst_scope. + +#[global] +Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) + (@subst_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => + eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t') + (ext_PTm f_PTm g_PTm Eq_PTm s) t Eq_st). +Qed. + +#[global] +Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@subst_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s). +Qed. + +#[global] +Instance ren_PTm_morphism {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) + (@ren_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => + eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t') + (extRen_PTm f_PTm g_PTm Eq_PTm s) t Eq_st). +Qed. + +#[global] +Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@ren_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s). +Qed. + +Ltac auto_unfold := repeat + unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1, + Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1. + +Tactic Notation "auto_unfold" "in" "*" := repeat + unfold VarInstance_PTm, Var, ids, + Ren_PTm, Ren1, ren1, Up_PTm_PTm, + Up_PTm, up_PTm, Subst_PTm, + Subst1, subst1 in *. + +Ltac asimpl' := repeat (first + [ progress setoid_rewrite substSubst_PTm_pointwise + | progress setoid_rewrite substSubst_PTm + | progress setoid_rewrite substRen_PTm_pointwise + | progress setoid_rewrite substRen_PTm + | progress setoid_rewrite renSubst_PTm_pointwise + | progress setoid_rewrite renSubst_PTm + | progress setoid_rewrite renRen'_PTm_pointwise + | progress setoid_rewrite renRen_PTm + | progress setoid_rewrite varLRen'_PTm_pointwise + | progress setoid_rewrite varLRen'_PTm + | progress setoid_rewrite varL'_PTm_pointwise + | progress setoid_rewrite varL'_PTm + | progress setoid_rewrite rinstId'_PTm_pointwise + | progress setoid_rewrite rinstId'_PTm + | progress setoid_rewrite instId'_PTm_pointwise + | progress setoid_rewrite instId'_PTm + | progress + unfold up_list_PTm_PTm, up_PTm_PTm, upRen_list_PTm_PTm, + upRen_PTm_PTm, up_ren + | progress cbn[subst_PTm ren_PTm] + | progress fsimpl ]). + +Ltac asimpl := check_no_evars; + repeat + unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1, + Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1 + in *; asimpl'; minimize. + +Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J. + +Tactic Notation "auto_case" := auto_case ltac:(asimpl; cbn; eauto). + +Ltac substify := auto_unfold; try setoid_rewrite rinstInst'_PTm_pointwise; + try setoid_rewrite rinstInst'_PTm. + +Ltac renamify := auto_unfold; + try setoid_rewrite_left rinstInst'_PTm_pointwise; + try setoid_rewrite_left rinstInst'_PTm. + +End Core. + +Module Extra. + +Import +Core. + +Arguments VarPTm {n_PTm}. + +Arguments PProj {n_PTm}. + +Arguments PPair {n_PTm}. + +Arguments PApp {n_PTm}. + +Arguments PAbs {n_PTm}. + +#[global]Hint Opaque subst_PTm: rewrite. + +#[global]Hint Opaque ren_PTm: rewrite. + +End Extra. + +Module interface. + +Export Core. + +Export Extra. + +End interface. + +Export interface. + diff --git a/theories/fp_red.v b/theories/fp_red.v new file mode 100644 index 0000000..2781fc1 --- /dev/null +++ b/theories/fp_red.v @@ -0,0 +1,2722 @@ +From Ltac2 Require Ltac2. +Import Ltac2.Notations. +Import Ltac2.Control. +Require Import ssreflect ssrbool. +Require Import FunInd. +Require Import Arith.Wf_nat. +Require Import Psatz. +From stdpp Require Import relations (rtc (..), rtc_once, rtc_r). +From Hammer Require Import Tactics. +Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. + +Ltac2 spec_refl () := + List.iter + (fun a => match a with + | (i, _, _) => + let h := Control.hyp i in + try (specialize $h with (1 := eq_refl)) + end) (Control.hyps ()). + +Ltac spec_refl := ltac2:(spec_refl ()). + +Module ERed. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta A a : + R (PAbs A (PApp (ren_PTm shift a) (VarPTm var_zero))) a + | PairEta a : + R (PPair (PProj PL a) (PProj PR a)) a + + (*************** Congruence ********************) + | AbsCong A a0 a1 : + R a0 a1 -> + R (PAbs A a0) (PAbs A a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (PApp a0 b) (PApp a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (PApp a b0) (PApp a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (PPair a0 b) (PPair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (PPair a b0) (PPair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1). + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma AppEta' n A a (u : PTm n) : + u = (PAbs A (PApp (ren_PTm shift a) (VarPTm var_zero))) -> + R u a. + Proof. move => ->. apply AppEta. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + + move => n A a m ξ /=. + apply AppEta' with (A := A). by asimpl. + all : qauto ctrs:R. + Qed. + + Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : + R a b -> + R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. + move => h. move : m ρ. elim : n a b / h => n. + move => A a m ρ /=. + apply AppEta' with (A := A); eauto. by asimpl. + all : hauto ctrs:R inv:option use:renaming. + Qed. + +End ERed. + +Module RRed. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppAbs A a b : + R (PApp (PAbs A a) b) (subst_PTm (scons b VarPTm) a) + + | ProjPair p a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) + + (*************** Congruence ********************) + | AbsCong A a0 a1 : + R a0 a1 -> + R (PAbs A a0) (PAbs A a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (PApp a0 b) (PApp a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (PApp a b0) (PApp a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (PPair a0 b) (PPair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (PPair a b0) (PPair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1). + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. +End RRed. + +Inductive Wt {n} (Γ : fin n -> Ty) : PTm n -> Ty -> Prop := +| T_Var i : + Wt Γ (VarPTm i) (Γ i) +| T_Abs a A B : + Wt (scons A Γ) a B -> + Wt Γ (PAbs A a) (Fun A B) +| T_App b a A B : + Wt Γ b (Fun A B) -> + Wt Γ a A -> + Wt Γ (PApp b a) B +| T_Pair a b A B : + Wt Γ a A -> + Wt Γ b B -> + Wt Γ (PPair a b) (Prod A B) +| T_Proj p a A B : + Wt Γ a (Prod A B) -> + Wt Γ (PProj p a) (if p is PL then A else B). + +Module Wt. + Lemma renaming n m (Γ : fin n -> Ty) Δ (ξ : fin n -> fin m) a A : + (forall i, Γ i = Δ (ξ i)) -> + Wt Γ a A -> + Wt Δ (ren_PTm ξ a) A. + Proof. + move => + h. move : m Δ ξ. elim : n Γ a A / h; try hauto inv:option lq:on ctrs:Wt. + Qed. + + Lemma antirenaming n m (Γ : fin n -> Ty) Δ (ξ : fin n -> fin m) a A : + (forall i, Γ i = Δ (ξ i)) -> + Wt Δ (ren_PTm ξ a) A -> + Wt Γ a A. + Proof. + move E : (ren_PTm ξ a) => u + h. + move : n a ξ Γ E. + elim : m Δ u A / h=> n /=. + - hauto q:on ctrs:Wt inv:PTm. + - move => Γ a A B ha iha m []//= A0 p ξ Δ [? ?]. subst. + hauto q:on inv:option ctrs:Wt. + - move => Γ b a A B hb ihb ha iha m [] //=. + move => p p0 ξ Δ [*]. subst. + hauto lq:on rew:off ctrs:Wt. + - move => Γ a b A B ha iha hb ihb m []//=. + hauto lq:on ctrs:Wt. + - move => Γ p a A B ha iha m []//=. + move => p0 p1 ξ Δ [*]. subst. + hauto lq:on rew:off ctrs:Wt. + Qed. + + Local Lemma morphing_upren n m (Γ : fin n -> Ty) Δ + (ρ : fin n -> PTm m) A : + (forall i, Wt Δ (ρ i) (Γ i)) -> + (forall i, Wt (scons A Δ) ((up_PTm_PTm ρ) i) ((scons A Γ) i)). + Proof. + sblast inv:option use:renaming. + Qed. + + + Lemma morphing n m (Γ : fin n -> Ty) Δ (ρ : fin n -> PTm m) a A: + (forall i, Wt Δ (ρ i) (Γ i)) -> Wt Γ a A -> Wt Δ (subst_PTm ρ a) A. + Proof. + move => + h. move : m Δ ρ; + elim : n Γ a A /h; + hauto lq:on use:morphing_upren ctrs:Wt. + Qed. + + Lemma substing n (Γ : fin n -> Ty) a b A B: + Wt (scons B Γ) a A -> + Wt Γ b B -> + Wt Γ (subst_PTm (scons b VarPTm) a) A. + Proof. + move => h0 h1. apply : morphing; eauto. + hauto lq:on ctrs:Wt inv:option. + Qed. + + Lemma preservation_beta n Γ a b A : + @Wt n Γ a A -> + RRed.R a b -> + Wt Γ b A. + Proof. + move => + h0. move : Γ A. + elim : n a b /h0=> n //=; hauto lq:on inv:Wt ctrs:Wt use:substing. + Qed. + + Lemma typing_unique n Γ a A B : + @Wt n Γ a A -> + Wt Γ a B -> + A = B. + Proof. + move => h. move : B. + elim : n Γ a A /h=>//=; hauto lq:on rew:off ctrs:Wt inv:Wt. + Qed. + + Lemma preservation_eta n Γ a b A : + @Wt n Γ a A -> + ERed.R a b -> + Wt Γ b A. + Proof. + move => + h0. move : Γ A. + elim : n a b /h0=> n //=; try qauto inv:Wt ctrs:Wt use:substing. + - move => A a Γ ξ hA. + inversion hA; subst. + inversion H2; subst. + inversion H4; subst. + apply antirenaming with (Γ := Γ) in H1; + sfirstorder use:typing_unique. + - move => a Γ U. + inversion 1; subst. + inversion H2; subst. + inversion H4; subst. + suff : Prod A B0 = Prod A0 B by congruence. + eauto using typing_unique. + - hauto lq:on inv:Wt ctrs:Wt. + Qed. +End Wt. + + +Lemma eta_postponement n Γ a b c A : + @Wt n Γ a A -> + ERed.R a b -> + RRed.R b c -> + exists d, rtc RRed.R a d /\ ERed.R d c. +Proof. + move => + h. + move : Γ c A. + elim : n a b /h => //=. + - move => n A a Γ c A0 hA0 ha. + exists (PAbs A (PApp (ren_PTm shift c) (VarPTm var_zero))). + split. admit. + apply ERed.AppEta. + - move => n a Γ c A ha ha0. + exists (PPair (PProj PL c) (PProj PR c)). + split. admit. + apply ERed.PairEta. + - move => n A a0 a1 ha iha Γ c A0 ha0. + elim /RRed.inv => //= _. + move => A1 a2 a3 ha' [*]. subst. + inversion ha0; subst. + move : iha H2 ha'. repeat move/[apply]. + move => [d [h0 h1]]. + exists (PAbs A d). + split. admit. + hauto lq:on ctrs:ERed.R. + - move => n a0 a1 b ha iha Γ c A hab hab0. + elim /RRed.inv : hab0 => //= _. + move => A0 a2 b0 [*]. subst. + + inversion ha; subst. + * exists (subst_PTm (scons b VarPTm) a2). + split. + apply : rtc_l. + apply RRed.AppAbs. + asimpl. + apply rtc_once. apply RRed.AppAbs. + admit. + * exfalso. + move : hab. clear. + hauto lq:on inv:Wt. + * inversion hab; subst. + exists (subst_PTm (scons b VarPTm) a1). + split. + apply rtc_once. + apply RRed.AppAbs. + admit. + + move => a2 a3 b0 ha0 [*]. subst. + have : exists Γ A, @Wt n Γ a0 A by hauto lq:on inv:Wt. + move => [Γ0 [A0] hA0]. + move : iha hA0 ha0. repeat move /[apply]. + move => [d [h0 h1]]. + exists (PApp d b). + split. admit. + hauto lq:on ctrs:ERed.R. + + move => a2 b0 b1 hb [*]. subst. + sauto lq:on. + - move => n a b0 b1 hb ihb Γ c A hu hu'. + elim /RRed.inv : hu' => //=_. + + move => A0 a0 b2 [*]. subst. + admit. + + sauto lq:on. + + move => a0 b2 b3 hb0 [*]. subst. + have [? [? ]] : exists Γ A, @Wt n Γ b0 A by hauto lq:on inv:Wt. + move : ihb hb0. repeat move/[apply]. + move => [d [h0 h1]]. + exists (PApp a d). + split. admit. + sauto lq:on. + - move => n a0 a1 b ha iha Γ u A hu. + elim / RRed.inv => //= _. + + move => a2 a3 b0 h [*]. subst. + have [? [? ]] : exists Γ A, @Wt n Γ a0 A by hauto lq:on inv:Wt. + move : iha h. repeat move/[apply]. + move => [d [h0 h1]]. + exists (PPair d b). + split. admit. + sauto lq:on. + + move => a2 b0 b1 h [*]. subst. + sauto lq:on. + - move => n a b0 b1 hb ihb Γ c A hu. + elim / RRed.inv => //=_. + move => a0 a1 b2 ha [*]. subst. + + sauto lq:on. + + move => a0 b2 b3 hb0 [*]. subst. + have [? [? ]] : exists Γ A, @Wt n Γ b0 A by hauto lq:on inv:Wt. + move : ihb hb0. repeat move/[apply]. + move => [d [h0 h1]]. + exists (PPair a d). + split. admit. + sauto lq:on. + - + + +(* Trying my best to not write C style module_funcname *) +Module Par. + Inductive R {n} : PTm n -> PTm n -> Prop := + (***************** Beta ***********************) + | AppAbs a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) + | AppPair a0 a1 b0 b1 c0 c1: + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (PApp (PPair a0 b0) c0) (PPair (PApp a1 c1) (PApp b1 c1)) + | ProjAbs p a0 a1 : + R a0 a1 -> + R (PProj p (PAbs a0)) (PAbs (PProj p a1)) + | ProjPair p a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) + + (****************** Eta ***********************) + | AppEta a0 a1 : + R a0 a1 -> + R a0 (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) + | PairEta a0 a1 : + R a0 a1 -> + R a0 (PPair (PProj PL a1) (PProj PR a1)) + + (*************** Congruence ********************) + | Var i : R (VarPTm i) (VarPTm i) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | ConstCong k : + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. + + Lemma refl n (a : PTm n) : R a a. + elim : n /a; hauto ctrs:R. + Qed. + + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) t. + Proof. move => ->. apply AppAbs. Qed. + + Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : + t = (if p is PL then a1 else b1) -> + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) t. + Proof. move => > ->. apply ProjPair. Qed. + + Lemma AppEta' n (a0 a1 b : PTm n) : + b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) -> + R a0 a1 -> + R a0 b. + Proof. move => ->; apply AppEta. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + move => *; apply : AppAbs'; eauto; by asimpl. + all : match goal with + | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl + | _ => qauto ctrs:R use:ProjPair' + end. + Qed. + + + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + Proof. + move => + h. move : m ρ0 ρ1. elim : n a b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=. + eapply AppAbs' with (a1 := subst_PTm (up_PTm_PTm ρ1) a1); eauto. + by asimpl. + hauto l:on use:renaming inv:option. + - hauto lq:on rew:off ctrs:R. + - hauto l:on inv:option use:renaming ctrs:R. + - hauto lq:on use:ProjPair'. + - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=. + apply : AppEta'; eauto. by asimpl. + - hauto lq:on ctrs:R. + - sfirstorder. + - hauto l:on inv:option ctrs:R use:renaming. + - hauto q:on ctrs:R. + - qauto l:on ctrs:R. + - qauto l:on ctrs:R. + - hauto l:on inv:option ctrs:R use:renaming. + - qauto l:on ctrs:R. + - qauto l:on ctrs:R. + Qed. + + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. hauto l:on use:morphing, refl. Qed. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. + Proof. + move E : (ren_PTm ξ a) => u h. + move : n ξ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=. + move => c c0 [+ ?]. subst. + case : c => //=. + move => c [?]. subst. + spec_refl. + move : iha => [c1][ih0]?. subst. + move : ihb => [c2][ih1]?. subst. + eexists. split. + apply AppAbs; eauto. + by asimpl. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//=. + move => []//= t t0 t1 [*]. subst. + spec_refl. + move : iha => [? [*]]. + move : ihb => [? [*]]. + move : ihc => [? [*]]. + eexists. split. + apply AppPair; hauto. subst. + by asimpl. + - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst. + spec_refl. move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjAbs; eauto. by asimpl. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ξ []//= p0 []//= t t0[*]. + subst. spec_refl. + move : iha => [b0 [? ?]]. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by eauto using ProjPair. + hauto q:on. + - move => n a0 a1 ha iha m ξ a ?. subst. + spec_refl. move : iha => [a0 [? ?]]. subst. + eexists. split. apply AppEta; eauto. + by asimpl. + - move => n a0 a1 ha iha m ξ a ?. subst. + spec_refl. move : iha => [b0 [? ?]]. subst. + eexists. split. apply PairEta; eauto. + by asimpl. + - move => n i m ξ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ξ []//= t [*]. subst. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0[*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split=>/=. by apply PairCong; eauto. + done. + - move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. by apply ProjCong; eauto. + done. + - hauto q:on inv:PTm ctrs:R. + - hauto q:on inv:PTm ctrs:R. + - hauto q:on inv:PTm ctrs:R. + Qed. + +End Par. + +Module Pars. + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + rtc Par.R a b -> rtc Par.R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + induction 1; hauto lq:on ctrs:rtc use:Par.renaming. + Qed. + + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + rtc Par.R a b -> + rtc Par.R (subst_PTm ρ a) (subst_PTm ρ b). + induction 1; hauto l:on ctrs:rtc use:Par.substing. + Qed. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + rtc Par.R (ren_PTm ξ a) b -> exists b0, rtc Par.R a b0 /\ ren_PTm ξ b0 = b. + Proof. + move E :(ren_PTm ξ a) => u h. + move : a E. + elim : u b /h. + - sfirstorder. + - move => a b c h0 h1 ih1 a0 ?. subst. + move /Par.antirenaming : h0. + move => [b0 [h2 ?]]. subst. + hauto lq:on rew:off ctrs:rtc. + Qed. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:Par.R use:Par.refl. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc Par.R a0 a1 -> + rtc Par.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc Par.R a0 a1 -> + rtc Par.R b0 b1 -> + rtc Par.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc Par.R a0 a1 -> + rtc Par.R b0 b1 -> + rtc Par.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc Par.R a b -> + rtc Par.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + +End Pars. + +Definition var_or_const {n} (a : PTm n) := + match a with + | VarPTm _ => true + | PBot => true + | _ => false + end. + + +(***************** Beta rules only ***********************) +Module RPar. + Inductive R {n} : PTm n -> PTm n -> Prop := + (***************** Beta ***********************) + | AppAbs a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) + | AppPair a0 a1 b0 b1 c0 c1: + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (PApp (PPair a0 b0) c0) (PPair (PApp a1 c1) (PApp b1 c1)) + | ProjAbs p a0 a1 : + R a0 a1 -> + R (PProj p (PAbs a0)) (PAbs (PProj p a1)) + | ProjPair p a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) + + + (*************** Congruence ********************) + | Var i : R (VarPTm i) (VarPTm i) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | ConstCong k : + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma refl n (a : PTm n) : R a a. + Proof. + induction a; hauto lq:on ctrs:R. + Qed. + + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) t. + Proof. move => ->. apply AppAbs. Qed. + + Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : + t = (if p is PL then a1 else b1) -> + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) t. + Proof. move => > ->. apply ProjPair. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + move => *; apply : AppAbs'; eauto; by asimpl. + all : qauto ctrs:R use:ProjPair'. + Qed. + + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). + Proof. eauto using renaming. Qed. + + Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : + R a b -> + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). + Proof. hauto q:on inv:option. Qed. + + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). + Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. + + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + Proof. + move => + h. move : m ρ0 ρ1. + elim : n a b /h. + - move => *. + apply : AppAbs'; eauto using morphing_up. + by asimpl. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + Qed. + + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + R a b -> + R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. hauto l:on use:morphing, refl. Qed. + + Lemma cong n (a b : PTm (S n)) c d : + R a b -> + R c d -> + R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). + Proof. + move => h0 h1. apply morphing => //=. + qauto l:on ctrs:R inv:option. + Qed. + + Lemma var_or_const_imp {n} (a b : PTm n) : + var_or_const a -> + a = b -> ~~ var_or_const b -> False. + Proof. + hauto lq:on inv:PTm. + Qed. + + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (forall i, var_or_const (up_PTm_PTm ρ i)). + Proof. + move => h /= [i|]. + - asimpl. + move /(_ i) in h. + rewrite /funcomp. + move : (ρ i) h. + case => //=. + - sfirstorder. + Qed. + + Local Ltac antiimp := qauto l:on use:var_or_const_imp. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E : (subst_PTm ρ a) => u hρ h. + move : n ρ hρ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => c c0 [+ ?]. subst. + case : c => //=; first by antiimp. + move => c [?]. subst. + spec_refl. + have /var_or_const_up hρ' := hρ. + move : iha hρ' => /[apply] iha. + move : ihb hρ => /[apply] ihb. + spec_refl. + move : iha => [c1][ih0]?. subst. + move : ihb => [c2][ih1]?. subst. + eexists. split. + apply AppAbs; eauto. + by asimpl. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ. + move => []//=; + first by antiimp. + move => []//=; first by antiimp. + move => t t0 t1 [*]. subst. + have {}/iha := hρ => iha. + have {}/ihb := hρ => ihb. + have {}/ihc := hρ => ihc. + spec_refl. + move : iha => [? [*]]. + move : ihb => [? [*]]. + move : ihc => [? [*]]. + eexists. split. + apply AppPair; hauto. subst. + by asimpl. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 []//= t [*]; first by antiimp. subst. + have /var_or_const_up {}/iha := hρ => iha. + spec_refl. move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjAbs; eauto. by asimpl. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => p0 []//=; first by antiimp. move => t t0[*]. + subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by eauto using ProjPair. + hauto q:on. + - move => n i m ρ hρ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. + move => t [*]. subst. + have /var_or_const_up {}/iha := hρ => iha. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + by asimpl. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply PairCong; eauto. + by asimpl. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 t [*]. subst. + have {}/iha := (hρ) => iha. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjCong; eauto. reflexivity. + - hauto q:on ctrs:R inv:PTm. + - hauto q:on ctrs:R inv:PTm. + - hauto q:on ctrs:R inv:PTm. + Qed. +End RPar. + +(***************** Beta rules only ***********************) +Module RPar'. + Inductive R {n} : PTm n -> PTm n -> Prop := + (***************** Beta ***********************) + | AppAbs a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) + | ProjPair p a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) + + + (*************** Congruence ********************) + | Var i : R (VarPTm i) (VarPTm i) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | ConstCong k : + R (PConst k) (PConst k) + | UnivCong i : + R (PUniv i) (PUniv i) + | BotCong : + R PBot PBot. + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma refl n (a : PTm n) : R a a. + Proof. + induction a; hauto lq:on ctrs:R. + Qed. + + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) t. + Proof. move => ->. apply AppAbs. Qed. + + Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : + t = (if p is PL then a1 else b1) -> + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) t. + Proof. move => > ->. apply ProjPair. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + move => *; apply : AppAbs'; eauto; by asimpl. + all : qauto ctrs:R use:ProjPair'. + Qed. + + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). + Proof. eauto using renaming. Qed. + + Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : + R a b -> + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). + Proof. hauto q:on inv:option. Qed. + + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). + Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. + + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + Proof. + move => + h. move : m ρ0 ρ1. + elim : n a b /h. + - move => *. + apply : AppAbs'; eauto using morphing_up. + by asimpl. + - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto l:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + Qed. + + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + R a b -> + R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. hauto l:on use:morphing, refl. Qed. + + Lemma cong n (a b : PTm (S n)) c d : + R a b -> + R c d -> + R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). + Proof. + move => h0 h1. apply morphing => //=. + qauto l:on ctrs:R inv:option. + Qed. + + Lemma var_or_const_imp {n} (a b : PTm n) : + var_or_const a -> + a = b -> ~~ var_or_const b -> False. + Proof. + hauto lq:on inv:PTm. + Qed. + + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (forall i, var_or_const (up_PTm_PTm ρ i)). + Proof. + move => h /= [i|]. + - asimpl. + move /(_ i) in h. + rewrite /funcomp. + move : (ρ i) h. + case => //=. + - sfirstorder. + Qed. + + Local Ltac antiimp := qauto l:on use:var_or_const_imp. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E : (subst_PTm ρ a) => u hρ h. + move : n ρ hρ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => c c0 [+ ?]. subst. + case : c => //=; first by antiimp. + move => c [?]. subst. + spec_refl. + have /var_or_const_up hρ' := hρ. + move : iha hρ' => /[apply] iha. + move : ihb hρ => /[apply] ihb. + spec_refl. + move : iha => [c1][ih0]?. subst. + move : ihb => [c2][ih1]?. subst. + eexists. split. + apply AppAbs; eauto. + by asimpl. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => p0 []//=; first by antiimp. move => t t0[*]. + subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by eauto using ProjPair. + hauto q:on. + - move => n i m ρ hρ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. + move => t [*]. subst. + have /var_or_const_up {}/iha := hρ => iha. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + by asimpl. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply PairCong; eauto. + by asimpl. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 t [*]. subst. + have {}/iha := (hρ) => iha. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjCong; eauto. reflexivity. + - hauto q:on ctrs:R inv:PTm. + - move => n i n0 ρ hρ []//=; first by antiimp. + hauto l:on. + - hauto q:on inv:PTm ctrs:R. + Qed. +End RPar'. + + +Module EReds. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:ERed.R. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc ERed.R a b -> + rtc ERed.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc ERed.R a0 a1 -> + rtc ERed.R b0 b1 -> + rtc ERed.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc ERed.R a0 a1 -> + rtc ERed.R b0 b1 -> + rtc ERed.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc ERed.R a0 a1 -> + rtc ERed.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. +End EReds. + +Module EPar. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta a0 a1 : + R a0 a1 -> + R a0 (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) + | PairEta a0 a1 : + R a0 a1 -> + R a0 (PPair (PProj PL a1) (PProj PR a1)) + + (*************** Congruence ********************) + | Var i : R (VarPTm i) (VarPTm i) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | ConstCong k : + R (PConst k) (PConst k) + | UnivCong i : + R (PUniv i) (PUniv i) + | BotCong : + R PBot PBot. + + Lemma refl n (a : PTm n) : EPar.R a a. + Proof. + induction a; hauto lq:on ctrs:EPar.R. + Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + + move => n a0 a1 ha iha m ξ /=. + move /(_ _ ξ) /AppEta : iha. + by asimpl. + + all : qauto ctrs:R. + Qed. + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma AppEta' n (a0 a1 b : PTm n) : + b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) -> + R a0 a1 -> + R a0 b. + Proof. move => ->; apply AppEta. Qed. + + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + R a b -> + (forall i, R (ρ0 i) (ρ1 i)) -> + R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + Proof. + move => h. move : m ρ0 ρ1. elim : n a b / h => n. + - move => a0 a1 ha iha m ρ0 ρ1 hρ /=. + apply : AppEta'; eauto. by asimpl. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto l:on ctrs:R use:renaming inv:option. + - hauto q:on ctrs:R. + - hauto q:on ctrs:R. + - hauto q:on ctrs:R. + - hauto l:on ctrs:R use:renaming inv:option. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + Qed. + + Lemma substing n a0 a1 (b0 b1 : PTm n) : + R a0 a1 -> + R b0 b1 -> + R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1). + Proof. + move => h0 h1. apply morphing => //. + hauto lq:on ctrs:R inv:option. + Qed. + +End EPar. + + +Module OExp. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta a : + R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) + | PairEta a : + R a (PPair (PProj PL a) (PProj PR a)). + + Lemma merge n (t a b : PTm n) : + rtc R a b -> + EPar.R t a -> + EPar.R t b. + Proof. + move => h. move : t. elim : a b /h. + - eauto using EPar.refl. + - hauto q:on ctrs:EPar.R inv:R. + Qed. + + Lemma commutativity n (a b c : PTm n) : + EPar.R a b -> R a c -> exists d, R b d /\ EPar.R c d. + Proof. + move => h. + inversion 1; subst. + - hauto q:on ctrs:EPar.R, R use:EPar.renaming, EPar.refl. + - hauto lq:on ctrs:EPar.R, R. + Qed. + + Lemma commutativity0 n (a b c : PTm n) : + EPar.R a b -> rtc R a c -> exists d, rtc R b d /\ EPar.R c d. + Proof. + move => + h. move : b. + elim : a c / h. + - sfirstorder. + - hauto lq:on rew:off ctrs:rtc use:commutativity. + Qed. + +End OExp. + + +Local Ltac com_helper := + split; [hauto lq:on ctrs:RPar.R use: RPar.refl, RPar.renaming + |hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming]. + +Module RPars. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:RPar.R use:RPar.refl. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc RPar.R a b -> + rtc RPar.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc RPar.R a0 a1 -> + rtc RPar.R b0 b1 -> + rtc RPar.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc RPar.R a0 a1 -> + rtc RPar.R b0 b1 -> + rtc RPar.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc RPar.R a0 a1 -> + rtc RPar.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. + + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : + rtc RPar.R a0 a1 -> + rtc RPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). + Proof. + induction 1. + - apply rtc_refl. + - eauto using RPar.renaming, rtc_l. + Qed. + + Lemma weakening n (a0 a1 : PTm n) : + rtc RPar.R a0 a1 -> + rtc RPar.R (ren_PTm shift a0) (ren_PTm shift a1). + Proof. apply renaming. Qed. + + Lemma Abs_inv n (a : PTm (S n)) b : + rtc RPar.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar.R a a'. + Proof. + move E : (PAbs a) => b0 h. move : a E. + elim : b0 b / h. + - hauto lq:on ctrs:rtc. + - hauto lq:on ctrs:rtc inv:RPar.R, rtc. + Qed. + + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : + rtc RPar.R a b -> + rtc RPar.R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. induction 1; qauto l:on ctrs:rtc use:RPar.substing. Qed. + + Lemma substing n (a b : PTm (S n)) c : + rtc RPar.R a b -> + rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). + Proof. hauto lq:on use:morphing inv:option. Qed. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + rtc RPar.R (subst_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E :(subst_PTm ρ a) => u hρ h. + move : a E. + elim : u b /h. + - sfirstorder. + - move => a b c h0 h1 ih1 a0 ?. subst. + move /RPar.antirenaming : h0. + move /(_ hρ). + move => [b0 [h2 ?]]. subst. + hauto lq:on rew:off ctrs:rtc. + Qed. + +End RPars. + +Module RPars'. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:RPar'.R use:RPar'.refl. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc RPar'.R a b -> + rtc RPar'.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc RPar'.R a0 a1 -> + rtc RPar'.R b0 b1 -> + rtc RPar'.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc RPar'.R a0 a1 -> + rtc RPar'.R b0 b1 -> + rtc RPar'.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc RPar'.R a0 a1 -> + rtc RPar'.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. + + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : + rtc RPar'.R a0 a1 -> + rtc RPar'.R (ren_PTm ξ a0) (ren_PTm ξ a1). + Proof. + induction 1. + - apply rtc_refl. + - eauto using RPar'.renaming, rtc_l. + Qed. + + Lemma weakening n (a0 a1 : PTm n) : + rtc RPar'.R a0 a1 -> + rtc RPar'.R (ren_PTm shift a0) (ren_PTm shift a1). + Proof. apply renaming. Qed. + + Lemma Abs_inv n (a : PTm (S n)) b : + rtc RPar'.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar'.R a a'. + Proof. + move E : (PAbs a) => b0 h. move : a E. + elim : b0 b / h. + - hauto lq:on ctrs:rtc. + - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. + Qed. + + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : + rtc RPar'.R a b -> + rtc RPar'.R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. + + Lemma substing n (a b : PTm (S n)) c : + rtc RPar'.R a b -> + rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). + Proof. hauto lq:on use:morphing inv:option. Qed. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + rtc RPar'.R (subst_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E :(subst_PTm ρ a) => u hρ h. + move : a E. + elim : u b /h. + - sfirstorder. + - move => a b c h0 h1 ih1 a0 ?. subst. + move /RPar'.antirenaming : h0. + move /(_ hρ). + move => [b0 [h2 ?]]. subst. + hauto lq:on rew:off ctrs:rtc. + Qed. + +End RPars'. + +Lemma Abs_EPar n a (b : PTm n) : + EPar.R (PAbs a) b -> + (exists d, EPar.R a d /\ + rtc RPar.R (PApp (ren_PTm shift b) (VarPTm var_zero)) d) /\ + (exists d, + EPar.R a d /\ forall p, + rtc RPar.R (PProj p b) (PAbs (PProj p d))). +Proof. + move E : (PAbs a) => u h. + move : a E. + elim : n u b /h => //=. + - move => n a0 a1 ha iha b ?. subst. + specialize iha with (1 := eq_refl). + move : iha => [[d [ih0 ih1]] _]. + split; exists d. + + split => //. + apply : rtc_l. + apply RPar.AppAbs; eauto => //=. + apply RPar.refl. + by apply RPar.refl. + move :ih1; substify; by asimpl. + + split => // p. + apply : rtc_l. + apply : RPar.ProjAbs. + by apply RPar.refl. + eauto using RPars.ProjCong, RPars.AbsCong. + - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl). + move : iha => [_ [d [ih0 ih1]]]. + split. + + exists (PPair (PProj PL d) (PProj PR d)). + split; first by apply EPar.PairEta. + apply : rtc_l. + apply RPar.AppPair; eauto using RPar.refl. + suff h : forall p, rtc RPar.R (PApp (PProj p (ren_PTm shift a1)) (VarPTm var_zero)) (PProj p d) by + sfirstorder use:RPars.PairCong. + move => p. move /(_ p) /RPars.weakening in ih1. + apply relations.rtc_transitive with (y := PApp (ren_PTm shift (PAbs (PProj p d))) (VarPTm var_zero)). + by eauto using RPars.AppCong, rtc_refl. + apply relations.rtc_once => /=. + apply : RPar.AppAbs'; eauto using RPar.refl. + by asimpl. + + exists d. repeat split => //. move => p. + apply : rtc_l; eauto. + hauto q:on use:RPar.ProjPair', RPar.refl. + - move => n a0 a1 ha _ ? [*]. subst. + split. + + exists a1. split => //. + apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl. + + exists a1. split => // p. + apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl. +Qed. + +Lemma Pair_EPar n (a b c : PTm n) : + EPar.R (PPair a b) c -> + (forall p, exists d, rtc RPar.R (PProj p c) d /\ EPar.R (if p is PL then a else b) d) /\ + (exists d0 d1, rtc RPar.R (PApp (ren_PTm shift c) (VarPTm var_zero)) + (PPair (PApp (ren_PTm shift d0) (VarPTm var_zero))(PApp (ren_PTm shift d1) (VarPTm var_zero))) /\ + EPar.R a d0 /\ EPar.R b d1). +Proof. + move E : (PPair a b) => u h. move : a b E. + elim : n u c /h => //=. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + move : iha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. + split. + + move => p. + exists (PAbs (PApp (ren_PTm shift (if p is PL then d0 else d1)) (VarPTm var_zero))). + split. + * apply : relations.rtc_transitive. + ** apply RPars.ProjCong. apply RPars.AbsCong. eassumption. + ** apply : rtc_l. apply RPar.ProjAbs; eauto using RPar.refl. apply RPars.AbsCong. + apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. + hauto l:on. + * hauto lq:on use:EPar.AppEta'. + + exists d0, d1. + repeat split => //. + apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=. + by asimpl; renamify. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). + split => [p|]. + + move : iha => [/(_ p) [d [ih0 ih1]] _]. + exists d. split=>//. + apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. + set q := (X in rtc RPar.R X d). + by have -> : q = PProj p a1 by hauto lq:on. + + move :iha => [iha _]. + move : (iha PL) => [d0 [ih0 ih0']]. + move : (iha PR) => [d1 [ih1 ih1']] {iha}. + exists d0, d1. + apply RPars.weakening in ih0, ih1. + repeat split => //=. + apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl. + apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl. + - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst. + split. + + move => p. + exists (if p is PL then a1 else b1). + split. + * apply rtc_once. apply : RPar.ProjPair'; eauto using RPar.refl. + * hauto lq:on rew:off. + + exists a1, b1. + split. apply rtc_once. apply RPar.AppPair; eauto using RPar.refl. + split => //. +Qed. + +Lemma commutativity0 n (a b0 b1 : PTm n) : + EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. +Proof. + move => h. move : b1. + elim : n a b0 / h. + - move => n a b0 ha iha b1 hb. + move : iha (hb) => /[apply]. + move => [c [ih0 ih1]]. + exists (PAbs (PApp (ren_PTm shift c) (VarPTm var_zero))). + split. + + hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming. + + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. + - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. + move => [c [ih0 ih1]]. + exists (PPair (PProj PL c) (PProj PR c)). split. + + apply RPars.PairCong; + by apply RPars.ProjCong. + + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. + - hauto l:on ctrs:rtc inv:RPar.R. + - move => n a0 a1 h ih b1. + elim /RPar.inv => //= _. + move => a2 a3 ? [*]. subst. + hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong. + - move => n a0 a1 b0 b1 ha iha hb ihb b2. + elim /RPar.inv => //= _. + + move => a2 a3 b3 b4 h0 h1 [*]. subst. + move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]]. + have {}/iha : RPar.R (PAbs a2) (PAbs a3) by hauto lq:on ctrs:RPar.R. + move => [c [ih0 /Abs_EPar [[d [ih1 ih2]] _]]]. + exists (subst_PTm (scons b VarPTm) d). + split. + (* By substitution *) + * move /RPars.substing : ih2. + move /(_ b). + asimpl. + eauto using relations.rtc_transitive, RPars.AppCong. + (* By EPar morphing *) + * by apply EPar.substing. + + move => a2 a3 b3 b4 c0 c1 h0 h1 h2 [*]. subst. + move /(_ _ ltac:(by eauto using RPar.PairCong)) : iha + => [c [ihc0 ihc1]]. + move /(_ _ ltac:(by eauto)) : ihb => [d [ihd0 ihd1]]. + move /Pair_EPar : ihc1 => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. + move /RPars.substing : ih0. move /(_ d). + asimpl => h. + exists (PPair (PApp d0 d) (PApp d1 d)). + split. + hauto lq:on use:relations.rtc_transitive, RPars.AppCong. + apply EPar.PairCong; by apply EPar.AppCong. + + hauto lq:on ctrs:EPar.R use:RPars.AppCong. + - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. + - move => n p a b0 h0 ih0 b1. + elim /RPar.inv => //= _. + + move => ? a0 a1 h [*]. subst. + move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]]. + move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]]. + exists (PAbs (PProj p d)). + qauto l:on ctrs:EPar.R use:RPars.ProjCong, @relations.rtc_transitive. + + move => p0 a0 a1 b2 b3 h1 h2 [*]. subst. + move /(_ _ ltac:(by eauto using RPar.PairCong)) : ih0 => [c [ih0 ih1]]. + move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _]. + exists d. split => //. + hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. + - hauto l:on ctrs:EPar.R inv:RPar.R. + - hauto l:on ctrs:EPar.R inv:RPar.R. + - hauto l:on ctrs:EPar.R inv:RPar.R. +Qed. + +Lemma commutativity1 n (a b0 b1 : PTm n) : + EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. +Proof. + move => + h. move : b0. + elim : a b1 / h. + - sfirstorder. + - qauto l:on use:relations.rtc_transitive, commutativity0. +Qed. + +Lemma commutativity n (a b0 b1 : PTm n) : + rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c. + move => h. move : b1. elim : a b0 /h. + - sfirstorder. + - move => a0 a1 a2 + ha1 ih b1 +. + move : commutativity1; repeat move/[apply]. + hauto q:on ctrs:rtc. +Qed. + +Lemma Abs_EPar' n a (b : PTm n) : + EPar.R (PAbs a) b -> + (exists d, EPar.R a d /\ + rtc OExp.R (PAbs d) b). +Proof. + move E : (PAbs a) => u h. + move : a E. + elim : n u b /h => //=. + - move => n a0 a1 ha iha a ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 ha iha a ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Proj_EPar' n p a (b : PTm n) : + EPar.R (PProj p a) b -> + (exists d, EPar.R a d /\ + rtc OExp.R (PProj p d) b). +Proof. + move E : (PProj p a) => u h. + move : p a E. + elim : n u b /h => //=. + - move => n a0 a1 ha iha a p ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 ha iha a p ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma App_EPar' n (a b u : PTm n) : + EPar.R (PApp a b) u -> + (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PApp a0 b0) u). +Proof. + move E : (PApp a b) => t h. + move : a b E. elim : n t u /h => //=. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Pair_EPar' n (a b u : PTm n) : + EPar.R (PPair a b) u -> + exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PPair a0 b0) u. +Proof. + move E : (PPair a b) => t h. + move : a b E. elim : n t u /h => //=. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Const_EPar' n k (u : PTm n) : + EPar.R (PConst k) u -> + rtc OExp.R (PConst k) u. + move E : (PConst k) => t h. + move : k E. elim : n t u /h => //=. + - move => n a0 a1 h ih k ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih k ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Bot_EPar' n (u : PTm n) : + EPar.R (PBot) u -> + rtc OExp.R (PBot) u. + move E : (PBot) => t h. + move : E. elim : n t u /h => //=. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Univ_EPar' n i (u : PTm n) : + EPar.R (PUniv i) u -> + rtc OExp.R (PUniv i) u. + move E : (PUniv i) => t h. + move : E. elim : n t u /h => //=. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma EPar_diamond n (c a1 b1 : PTm n) : + EPar.R c a1 -> + EPar.R c b1 -> + exists d2, EPar.R a1 d2 /\ EPar.R b1 d2. +Proof. + move => h. move : b1. elim : n c a1 / h. + - move => n c a1 ha iha b1 /iha [d2 [hd0 hd1]]. + exists(PAbs (PApp (ren_PTm shift d2) (VarPTm var_zero))). + hauto lq:on ctrs:EPar.R use:EPar.renaming. + - hauto lq:on rew:off ctrs:EPar.R. + - hauto lq:on use:EPar.refl. + - move => n a0 a1 ha iha a2. + move /Abs_EPar' => [d [hd0 hd1]]. + move : iha hd0; repeat move/[apply]. + move => [d2 [h0 h1]]. + have : EPar.R (PAbs d) (PAbs d2) by eauto using EPar.AbsCong. + move : OExp.commutativity0 hd1; repeat move/[apply]. + move => [d1 [hd1 hd2]]. + exists d1. hauto lq:on ctrs:EPar.R use:OExp.merge. + - move => n a0 a1 b0 b1 ha iha hb ihb c. + move /App_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. + have : EPar.R (PApp a2 b2)(PApp a3 b3) + by hauto l:on use:EPar.AppCong. + move : OExp.commutativity0 h2; repeat move/[apply]. + move => [d h]. + exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. + - move => n a0 a1 b0 b1 ha iha hb ihb c. + move /Pair_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. + have : EPar.R (PPair a2 b2)(PPair a3 b3) + by hauto l:on use:EPar.PairCong. + move : OExp.commutativity0 h2; repeat move/[apply]. + move => [d h]. + exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. + - move => n p a0 a1 ha iha b. + move /Proj_EPar' => [d [/iha [d2 h] h1]] {iha}. + have : EPar.R (PProj p d) (PProj p d2) + by hauto l:on use:EPar.ProjCong. + move : OExp.commutativity0 h1; repeat move/[apply]. + move => [d1 h1]. + exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. + - qauto use:Const_EPar', EPar.refl. + - qauto use:Univ_EPar', EPar.refl. + - qauto use:Bot_EPar', EPar.refl. +Qed. + +Function tstar {n} (a : PTm n) := + match a with + | VarPTm i => a + | PAbs a => PAbs (tstar a) + | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a) + | PApp (PPair a b) c => + PPair (PApp (tstar a) (tstar c)) (PApp (tstar b) (tstar c)) + | PApp a b => PApp (tstar a) (tstar b) + | PPair a b => PPair (tstar a) (tstar b) + | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b) + | PProj p (PAbs a) => (PAbs (PProj p (tstar a))) + | PProj p a => PProj p (tstar a) + | PConst k => PConst k + | PUniv i => PUniv i + | PBot => PBot + end. + +Lemma RPar_triangle n (a : PTm n) : forall b, RPar.R a b -> RPar.R b (tstar a). +Proof. + apply tstar_ind => {n a}. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R. + - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R. + - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. + - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. + - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'. + - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. +Qed. + +Function tstar' {n} (a : PTm n) := + match a with + | VarPTm i => a + | PAbs a => PAbs (tstar' a) + | PApp (PAbs a) b => subst_PTm (scons (tstar' b) VarPTm) (tstar' a) + | PApp a b => PApp (tstar' a) (tstar' b) + | PPair a b => PPair (tstar' a) (tstar' b) + | PProj p (PPair a b) => if p is PL then (tstar' a) else (tstar' b) + | PProj p a => PProj p (tstar' a) + | PConst k => PConst k + | PUniv i => PUniv i + | PBot => PBot + end. + +Lemma RPar'_triangle n (a : PTm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). +Proof. + apply tstar'_ind => {n a}. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R. + - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R. + - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R. + - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. + - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. +Qed. + +Lemma RPar_diamond n (c a1 b1 : PTm n) : + RPar.R c a1 -> + RPar.R c b1 -> + exists d2, RPar.R a1 d2 /\ RPar.R b1 d2. +Proof. hauto l:on use:RPar_triangle. Qed. + +Lemma RPar'_diamond n (c a1 b1 : PTm n) : + RPar'.R c a1 -> + RPar'.R c b1 -> + exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2. +Proof. hauto l:on use:RPar'_triangle. Qed. + +Lemma RPar_confluent n (c a1 b1 : PTm n) : + rtc RPar.R c a1 -> + rtc RPar.R c b1 -> + exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2. +Proof. + sfirstorder use:relations.diamond_confluent, RPar_diamond. +Qed. + +Lemma RPar'_confluent n (c a1 b1 : PTm n) : + rtc RPar'.R c a1 -> + rtc RPar'.R c b1 -> + exists d2, rtc RPar'.R a1 d2 /\ rtc RPar'.R b1 d2. +Proof. + sfirstorder use:relations.diamond_confluent, RPar'_diamond. +Qed. + +Lemma EPar_confluent n (c a1 b1 : PTm n) : + rtc EPar.R c a1 -> + rtc EPar.R c b1 -> + exists d2, rtc EPar.R a1 d2 /\ rtc EPar.R b1 d2. +Proof. + sfirstorder use:relations.diamond_confluent, EPar_diamond. +Qed. + +Inductive prov {n} : PTm n -> PTm n -> Prop := +| P_Abs h a : + (forall b, prov h (subst_PTm (scons b VarPTm) a)) -> + prov h (PAbs a) +| P_App h a b : + prov h a -> + prov h (PApp a b) +| P_Pair h a b : + prov h a -> + prov h b -> + prov h (PPair a b) +| P_Proj h p a : + prov h a -> + prov h (PProj p a) +| P_Const k : + prov (PConst k) (PConst k) +| P_Var i : + prov (VarPTm i) (VarPTm i) +| P_Univ i : + prov (PUniv i) (PUniv i) +| P_Bot : + prov PBot PBot. + +Lemma ERed_EPar n (a b : PTm n) : ERed.R a b -> EPar.R a b. +Proof. + induction 1; hauto lq:on ctrs:EPar.R use:EPar.refl. +Qed. + +Lemma EPar_ERed n (a b : PTm n) : EPar.R a b -> rtc ERed.R a b. +Proof. + move => h. elim : n a b /h. + - eauto using rtc_r, ERed.AppEta. + - eauto using rtc_r, ERed.PairEta. + - auto using rtc_refl. + - eauto using EReds.AbsCong. + - eauto using EReds.AppCong. + - eauto using EReds.PairCong. + - eauto using EReds.ProjCong. + - auto using rtc_refl. + - auto using rtc_refl. + - auto using rtc_refl. +Qed. + +Lemma EPar_Par n (a b : PTm n) : EPar.R a b -> Par.R a b. +Proof. + move => h. elim : n a b /h; qauto ctrs:Par.R. +Qed. + +Lemma RPar_Par n (a b : PTm n) : RPar.R a b -> Par.R a b. +Proof. + move => h. elim : n a b /h; hauto lq:on ctrs:Par.R. +Qed. + +Lemma rtc_idem n (R : PTm n -> PTm n -> Prop) (a b : PTm n) : rtc (rtc R) a b -> rtc R a b. +Proof. + induction 1; hauto l:on use:@relations.rtc_transitive, @rtc_r. +Qed. + +Lemma EPars_EReds {n} (a b : PTm n) : rtc EPar.R a b <-> rtc ERed.R a b. +Proof. + sfirstorder use:@relations.rtc_subrel, EPar_ERed, rtc_idem, ERed_EPar. +Qed. + +Lemma prov_rpar n (u : PTm n) a b : prov u a -> RPar.R a b -> prov u b. +Proof. + move => h. + move : b. + elim : u a / h. + (* - qauto l:on ctrs:prov inv:RPar.R use:@rtc_r, RPar_Par. *) + - hauto lq:on ctrs:prov inv:RPar.R use:RPar.substing. + - move => h a b ha iha b0. + elim /RPar.inv => //= _. + + move => a0 a1 b1 b2 h0 h1 [*]. subst. + have {}iha : prov h (PAbs a1) by hauto lq:on ctrs:RPar.R. + hauto lq:on inv:prov use:RPar.substing. + + move => a0 a1 b1 b2 c0 c1. + move => h0 h1 h2 [*]. subst. + have {}iha : prov h (PPair a1 b2) by hauto lq:on ctrs:RPar.R. + hauto lq:on inv:prov ctrs:prov. + + hauto lq:on ctrs:prov. + - hauto lq:on ctrs:prov inv:RPar.R. + - move => h p a ha iha b. + elim /RPar.inv => //= _. + + move => p0 a0 a1 h0 [*]. subst. + have {iha} : prov h (PAbs a1) by hauto lq:on ctrs:RPar.R. + hauto lq:on ctrs:prov inv:prov use:RPar.substing. + + move => p0 a0 a1 b0 b1 h0 h1 [*]. subst. + have {iha} : prov h (PPair a1 b1) by hauto lq:on ctrs:RPar.R. + qauto l:on inv:prov. + + hauto lq:on ctrs:prov. + - hauto lq:on ctrs:prov inv:RPar.R. + - hauto l:on ctrs:RPar.R inv:RPar.R. + - hauto l:on ctrs:RPar.R inv:RPar.R. + - hauto l:on ctrs:RPar.R inv:RPar.R. +Qed. + + +Lemma prov_lam n (u : PTm n) a : prov u a <-> prov u (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))). +Proof. + split. + move => h. constructor. move => b. asimpl. by constructor. + inversion 1; subst. + specialize H2 with (b := PBot). + move : H2. asimpl. inversion 1; subst. done. +Qed. + +Lemma prov_pair n (u : PTm n) a : prov u a <-> prov u (PPair (PProj PL a) (PProj PR a)). +Proof. hauto lq:on inv:prov ctrs:prov. Qed. + +Lemma prov_ered n (u : PTm n) a b : prov u a -> ERed.R a b -> prov u b. +Proof. + move => h. + move : b. + elim : u a / h. + - move => h a ha iha b. + elim /ERed.inv => // _. + + move => a0 *. subst. + rewrite -prov_lam. + by constructor. + + move => a0 *. subst. + rewrite -prov_pair. + by constructor. + + hauto lq:on ctrs:prov use:ERed.substing. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - move => h a b ha iha hb ihb b0. + elim /ERed.inv => //_. + + move => a0 *. subst. + rewrite -prov_lam. + by constructor. + + move => a0 *. subst. + rewrite -prov_pair. + by constructor. + + hauto lq:on ctrs:prov. + + hauto lq:on ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. +Qed. + +Lemma prov_ereds n (u : PTm n) a b : prov u a -> rtc ERed.R a b -> prov u b. +Proof. + induction 2; sfirstorder use:prov_ered. +Qed. + +Fixpoint extract {n} (a : PTm n) : PTm n := + match a with + | PAbs a => subst_PTm (scons PBot VarPTm) (extract a) + | PApp a b => extract a + | PPair a b => extract a + | PProj p a => extract a + | PConst k => PConst k + | VarPTm i => VarPTm i + | PUniv i => PUniv i + | PBot => PBot + end. + +Lemma ren_extract n m (a : PTm n) (ξ : fin n -> fin m) : + extract (ren_PTm ξ a) = ren_PTm ξ (extract a). +Proof. + move : m ξ. elim : n/a. + - sfirstorder. + - move => n a ih m ξ /=. + rewrite ih. + by asimpl. + - hauto q:on. + - hauto q:on. + - hauto q:on. + - hauto q:on. + - sfirstorder. + - sfirstorder. +Qed. + +Lemma ren_morphing n m (a : PTm n) (ρ : fin n -> PTm m) : + (forall i, ρ i = extract (ρ i)) -> + extract (subst_PTm ρ a) = subst_PTm ρ (extract a). +Proof. + move : m ρ. + elim : n /a => n //=. + move => a ha m ρ hi. + rewrite ha. + - destruct i as [i|] => //. + rewrite ren_extract. + rewrite -hi. + by asimpl. + - by asimpl. +Qed. + +Lemma ren_subst_bot n (a : PTm (S n)) : + extract (subst_PTm (scons PBot VarPTm) a) = subst_PTm (scons PBot VarPTm) (extract a). +Proof. + apply ren_morphing. destruct i as [i|] => //=. +Qed. + +Definition prov_extract_spec {n} u (a : PTm n) := + match u with + | PUniv i => extract a = PUniv i + | VarPTm i => extract a = VarPTm i + | (PConst i) => extract a = (PConst i) + | PBot => extract a = PBot + | _ => True + end. + +Lemma prov_extract n u (a : PTm n) : + prov u a -> prov_extract_spec u a. +Proof. + move => h. + elim : u a /h. + - move => h a ha ih. + case : h ha ih => //=. + + move => i ha ih. + move /(_ PBot) in ih. + rewrite -ih. + by rewrite ren_subst_bot. + + move => p _ /(_ PBot). + by rewrite ren_subst_bot. + + move => i h /(_ PBot). + by rewrite ren_subst_bot => ->. + + move /(_ PBot). + move => h /(_ PBot). + by rewrite ren_subst_bot. + - hauto lq:on. + - hauto lq:on. + - hauto lq:on. + - case => //=. + - sfirstorder. + - sfirstorder. + - sfirstorder. +Qed. + +Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b := + R0 a b \/ R1 a b. + +Module ERPar. + Definition R {n} (a b : PTm n) := union RPar.R EPar.R a b. + Lemma RPar {n} (a b : PTm n) : RPar.R a b -> R a b. + Proof. sfirstorder. Qed. + + Lemma EPar {n} (a b : PTm n) : EPar.R a b -> R a b. + Proof. sfirstorder. Qed. + + Lemma refl {n} ( a : PTm n) : ERPar.R a a. + Proof. + sfirstorder use:RPar.refl, EPar.refl. + Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + R a0 a1 -> + rtc R (PProj p a0) (PProj p a1). + Proof. + move => []. + - move => h. + apply rtc_once. + left. + by apply RPar.ProjCong. + - move => h. + apply rtc_once. + right. + by apply EPar.ProjCong. + Qed. + + Lemma AbsCong n (a0 a1 : PTm (S n)) : + R a0 a1 -> + rtc R (PAbs a0) (PAbs a1). + Proof. + move => []. + - move => h. + apply rtc_once. + left. + by apply RPar.AbsCong. + - move => h. + apply rtc_once. + right. + by apply EPar.AbsCong. + Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + R a0 a1 -> + R b0 b1 -> + rtc R (PApp a0 b0) (PApp a1 b1). + Proof. + move => [] + []. + - sfirstorder use:RPar.AppCong, @rtc_once. + - move => h0 h1. + apply : rtc_l. + left. apply RPar.AppCong; eauto; apply RPar.refl. + apply rtc_once. + hauto l:on use:EPar.AppCong, EPar.refl. + - move => h0 h1. + apply : rtc_l. + left. apply RPar.AppCong; eauto; apply RPar.refl. + apply rtc_once. + hauto l:on use:EPar.AppCong, EPar.refl. + - sfirstorder use:EPar.AppCong, @rtc_once. + Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + R a0 a1 -> + R b0 b1 -> + rtc R (PPair a0 b0) (PPair a1 b1). + Proof. + move => [] + []. + - sfirstorder use:RPar.PairCong, @rtc_once. + - move => h0 h1. + apply : rtc_l. + left. apply RPar.PairCong; eauto; apply RPar.refl. + apply rtc_once. + hauto l:on use:EPar.PairCong, EPar.refl. + - move => h0 h1. + apply : rtc_l. + left. apply RPar.PairCong; eauto; apply RPar.refl. + apply rtc_once. + hauto l:on use:EPar.PairCong, EPar.refl. + - sfirstorder use:EPar.PairCong, @rtc_once. + Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + sfirstorder use:EPar.renaming, RPar.renaming. + Qed. + +End ERPar. + +Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong : erpar. + +Module ERPars. + #[local]Ltac solve_s_rec := + move => *; eapply relations.rtc_transitive; eauto; + hauto lq:on db:erpar. + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc ERPar.R a0 a1 -> + rtc ERPar.R b0 b1 -> + rtc ERPar.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma AbsCong n (a0 a1 : PTm (S n)) : + rtc ERPar.R a0 a1 -> + rtc ERPar.R (PAbs a0) (PAbs a1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc ERPar.R a0 a1 -> + rtc ERPar.R b0 b1 -> + rtc ERPar.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc ERPar.R a0 a1 -> + rtc ERPar.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. + + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : + rtc ERPar.R a0 a1 -> + rtc ERPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). + Proof. + induction 1. + - apply rtc_refl. + - eauto using ERPar.renaming, rtc_l. + Qed. + +End ERPars. + +Lemma ERPar_Par n (a b : PTm n) : ERPar.R a b -> Par.R a b. +Proof. + sfirstorder use:EPar_Par, RPar_Par. +Qed. + +Lemma Par_ERPar n (a b : PTm n) : Par.R a b -> rtc ERPar.R a b. +Proof. + move => h. elim : n a b /h. + - move => n a0 a1 b0 b1 ha iha hb ihb. + suff ? : rtc ERPar.R (PApp (PAbs a0) b0) (PApp (PAbs a1) b1). + apply : relations.rtc_transitive; eauto. + apply rtc_once. apply ERPar.RPar. + by apply RPar.AppAbs; eauto using RPar.refl. + eauto using ERPars.AppCong,ERPars.AbsCong. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc. + apply : rtc_l. apply ERPar.RPar. + apply RPar.AppPair; eauto using RPar.refl. + sfirstorder use:ERPars.AppCong, ERPars.PairCong. + - move => n p a0 a1 ha iha. + apply : rtc_l. apply ERPar.RPar. apply RPar.ProjAbs; eauto using RPar.refl. + sfirstorder use:ERPars.AbsCong, ERPars.ProjCong. + - move => n p a0 a1 b0 b1 ha iha hb ihb. + apply : rtc_l. apply ERPar.RPar. apply RPar.ProjPair; eauto using RPar.refl. + hauto lq:on. + - move => n a0 a1 ha iha. + apply : rtc_l. apply ERPar.EPar. apply EPar.AppEta; eauto using EPar.refl. + hauto lq:on ctrs:rtc + use:ERPars.AppCong, ERPars.AbsCong, ERPars.renaming. + - move => n a0 a1 ha iha. + apply : rtc_l. apply ERPar.EPar. apply EPar.PairEta; eauto using EPar.refl. + sfirstorder use:ERPars.PairCong, ERPars.ProjCong. + - sfirstorder. + - sfirstorder use:ERPars.AbsCong. + - sfirstorder use:ERPars.AppCong. + - sfirstorder use:ERPars.PairCong. + - sfirstorder use:ERPars.ProjCong. + - sfirstorder. + - sfirstorder. + - sfirstorder. +Qed. + +Lemma Pars_ERPar n (a b : PTm n) : rtc Par.R a b -> rtc ERPar.R a b. +Proof. + induction 1; hauto l:on use:Par_ERPar, @relations.rtc_transitive. +Qed. + +Lemma Par_ERPar_iff n (a b : PTm n) : rtc Par.R a b <-> rtc ERPar.R a b. +Proof. + split. + sfirstorder use:Pars_ERPar, @relations.rtc_subrel. + sfirstorder use:ERPar_Par, @relations.rtc_subrel. +Qed. + +Lemma RPar_ERPar n (a b : PTm n) : rtc RPar.R a b -> rtc ERPar.R a b. +Proof. + sfirstorder use:@relations.rtc_subrel. +Qed. + +Lemma EPar_ERPar n (a b : PTm n) : rtc EPar.R a b -> rtc ERPar.R a b. +Proof. + sfirstorder use:@relations.rtc_subrel. +Qed. + +Module Type HindleyRosen. + Parameter A : nat -> Type. + Parameter R0 R1 : forall n, A n -> A n -> Prop. + Axiom diamond_R0 : forall n, relations.diamond (R0 n). + Axiom diamond_R1 : forall n, relations.diamond (R1 n). + Axiom commutativity : forall n, + forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d. +End HindleyRosen. + +Module HindleyRosenFacts (M : HindleyRosen). + Import M. + Lemma R0_comm : + forall n a b c, R0 n a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ R0 n c d. + Proof. + move => n a + c + h. + elim : a c /h. + - sfirstorder. + - move => a0 a1 a2 ha ha0 ih b h. + case : ha. + + move : diamond_R0 h; repeat move/[apply]. + hauto lq:on ctrs:rtc. + + move : commutativity h; repeat move/[apply]. + hauto lq:on ctrs:rtc. + Qed. + + Lemma R1_comm : + forall n a b c, R1 n a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ R1 n c d. + Proof. + move => n a + c + h. + elim : a c /h. + - sfirstorder. + - move => a0 a1 a2 ha ha0 ih b h. + case : ha. + + move : commutativity h; repeat move/[apply]. + hauto lq:on ctrs:rtc. + + move : diamond_R1 h; repeat move/[apply]. + hauto lq:on ctrs:rtc. + Qed. + + Lemma U_comm : + forall n a b c, (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ (union (R0 n) (R1 n)) c d. + Proof. + hauto lq:on use:R0_comm, R1_comm. + Qed. + + Lemma U_comms : + forall n a b c, rtc (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ rtc (union (R0 n) (R1 n)) c d. + Proof. + move => n a b + h. + elim : a b /h. + - sfirstorder. + - hecrush ctrs:rtc use:U_comm. + Qed. + +End HindleyRosenFacts. + +Module HindleyRosenER <: HindleyRosen. + Definition A := PTm. + Definition R0 n := rtc (@RPar.R n). + Definition R1 n := rtc (@EPar.R n). + Lemma diamond_R0 : forall n, relations.diamond (R0 n). + sfirstorder use:RPar_confluent. + Qed. + Lemma diamond_R1 : forall n, relations.diamond (R1 n). + sfirstorder use:EPar_confluent. + Qed. + Lemma commutativity : forall n, + forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d. + Proof. + hauto l:on use:commutativity. + Qed. +End HindleyRosenER. + +Module ERFacts := HindleyRosenFacts HindleyRosenER. + +Lemma rtc_union n (a b : PTm n) : + rtc (union RPar.R EPar.R) a b <-> + rtc (union (rtc RPar.R) (rtc EPar.R)) a b. +Proof. + split; first by induction 1; hauto lq:on ctrs:rtc. + move => h. + elim :a b /h. + - sfirstorder. + - move => a0 a1 a2. + case. + + move => h0 h1 ih. + apply : relations.rtc_transitive; eauto. + move : h0. + apply relations.rtc_subrel. + sfirstorder. + + move => h0 h1 ih. + apply : relations.rtc_transitive; eauto. + move : h0. + apply relations.rtc_subrel. + sfirstorder. +Qed. + +Lemma prov_erpar n (u : PTm n) a b : prov u a -> ERPar.R a b -> prov u b. +Proof. + move => h []. + - sfirstorder use:prov_rpar. + - move /EPar_ERed. + sfirstorder use:prov_ereds. +Qed. + +Lemma prov_pars n (u : PTm n) a b : prov u a -> rtc Par.R a b -> prov u b. +Proof. + move => h /Pars_ERPar. + move => h0. + move : h. + elim : a b /h0. + - done. + - hauto lq:on use:prov_erpar. +Qed. + +Lemma Par_confluent n (a b c : PTm n) : + rtc Par.R a b -> + rtc Par.R a c -> + exists d, rtc Par.R b d /\ rtc Par.R c d. +Proof. + move : n a b c. + suff : forall (n : nat) (a b c : PTm n), + rtc ERPar.R a b -> + rtc ERPar.R a c -> exists d : PTm n, rtc ERPar.R b d /\ rtc ERPar.R c d. + move => h n a b c h0 h1. + apply Par_ERPar_iff in h0, h1. + move : h h0 h1; repeat move/[apply]. + hauto lq:on use:Par_ERPar_iff. + have h := ERFacts.U_comms. + move => n a b c. + rewrite /HindleyRosenER.R0 /HindleyRosenER.R1 in h. + specialize h with (n := n). + rewrite /HindleyRosenER.A in h. + rewrite /ERPar.R. + have eq : (fun a0 b0 : PTm n => union RPar.R EPar.R a0 b0) = union RPar.R EPar.R by reflexivity. + rewrite !{}eq. + move /rtc_union => + /rtc_union. + move : h; repeat move/[apply]. + hauto lq:on use:rtc_union. +Qed. + +Lemma pars_univ_inv n i (c : PTm n) : + rtc Par.R (PUniv i) c -> + extract c = PUniv i. +Proof. + have : prov (PUniv i) (PUniv i : PTm n) by sfirstorder. + move : prov_pars. repeat move/[apply]. + apply prov_extract. +Qed. + +Lemma pars_const_inv n i (c : PTm n) : + rtc Par.R (PConst i) c -> + extract c = PConst i. +Proof. + have : prov (PConst i) (PConst i : PTm n) by sfirstorder. + move : prov_pars. repeat move/[apply]. + apply prov_extract. +Qed. + +Lemma pars_var_inv n (i : fin n) C : + rtc Par.R (VarPTm i) C -> + extract C = VarPTm i. +Proof. + have : prov (VarPTm i) (VarPTm i) by hauto lq:on ctrs:prov, rtc. + move : prov_pars. repeat move/[apply]. + apply prov_extract. +Qed. + +Lemma pars_univ_inj n i j (C : PTm n) : + rtc Par.R (PUniv i) C -> + rtc Par.R (PUniv j) C -> + i = j. +Proof. + sauto l:on use:pars_univ_inv. +Qed. + +Lemma pars_const_inj n i j (C : PTm n) : + rtc Par.R (PConst i) C -> + rtc Par.R (PConst j) C -> + i = j. +Proof. + sauto l:on use:pars_const_inv. +Qed. + +Definition join {n} (a b : PTm n) := + exists c, rtc Par.R a c /\ rtc Par.R b c. + +Lemma join_transitive n (a b c : PTm n) : + join a b -> join b c -> join a c. +Proof. + rewrite /join. + move => [ab [h0 h1]] [bc [h2 h3]]. + move : Par_confluent h1 h2; repeat move/[apply]. + move => [abc [h4 h5]]. + eauto using relations.rtc_transitive. +Qed. + +Lemma join_symmetric n (a b : PTm n) : + join a b -> join b a. +Proof. sfirstorder unfold:join. Qed. + +Lemma join_refl n (a : PTm n) : join a a. +Proof. hauto lq:on ctrs:rtc unfold:join. Qed. + +Lemma join_univ_inj n i j : + join (PUniv i : PTm n) (PUniv j) -> i = j. +Proof. + sfirstorder use:pars_univ_inj. +Qed. + +Lemma join_const_inj n i j : + join (PConst i : PTm n) (PConst j) -> i = j. +Proof. + sfirstorder use:pars_const_inj. +Qed. + +Lemma join_substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + join a b -> + join (subst_PTm ρ a) (subst_PTm ρ b). +Proof. hauto lq:on unfold:join use:Pars.substing. Qed. + +Fixpoint ne {n} (a : PTm n) := + match a with + | VarPTm i => true + | PApp a b => ne a && nf b + | PAbs a => false + | PUniv _ => false + | PProj _ a => ne a + | PPair _ _ => false + | PConst _ => false + | PBot => true + end +with nf {n} (a : PTm n) := + match a with + | VarPTm i => true + | PApp a b => ne a && nf b + | PAbs a => nf a + | PUniv _ => true + | PProj _ a => ne a + | PPair a b => nf a && nf b + | PConst _ => true + | PBot => true +end. + +Lemma ne_nf n a : @ne n a -> nf a. +Proof. elim : a => //=. Qed. + +Definition wn {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ nf b. +Definition wne {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ ne b. + +(* Weakly neutral implies weakly normal *) +Lemma wne_wn n a : @wne n a -> wn a. +Proof. sfirstorder use:ne_nf. Qed. + +(* Normal implies weakly normal *) +Lemma nf_wn n v : @nf n v -> wn v. +Proof. sfirstorder ctrs:rtc. Qed. + +Lemma nf_refl n (a b : PTm n) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a). +Proof. + elim : a b /h => //=; solve [hauto b:on]. +Qed. + +Lemma nf_refls n (a b : PTm n) (h : rtc RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a). +Proof. + induction h; sauto lq:on rew:off ctrs:rtc use:nf_refl. +Qed. + +Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) : + (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)). +Proof. + move : m ξ. elim : n / a => //=; solve [hauto b:on]. +Qed. + +Lemma wne_app n (a b : PTm n) : + wne a -> wn b -> wne (PApp a b). +Proof. + move => [a0 [? ?]] [b0 [? ?]]. + exists (PApp a0 b0). hauto b:on drew:off use:RPars'.AppCong. +Qed. + +Lemma wn_abs n a (h : wn a) : @wn n (PAbs a). +Proof. + move : h => [v [? ?]]. + exists (PAbs v). + eauto using RPars'.AbsCong. +Qed. + +Require Import Coq.Program.Equality. + +Lemma wn_abs' n a (h : @wn n (PAbs a)) : wn a. +Proof. + move : h. move => [a0 [h0 h1]]. + dependent induction h0; sauto q:on. +Qed. + +Lemma wn_pair n (a b : PTm n) : wn a -> wn b -> wn (PPair a b). +Proof. + move => [a0 [? ?]] [b0 [? ?]]. + exists (PPair a0 b0). + hauto lqb:on use:RPars'.PairCong. +Qed. + +Lemma wne_proj n p (a : PTm n) : wne a -> wne (PProj p a). +Proof. + move => [a0 [? ?]]. + exists (PProj p a0). hauto lqb:on use:RPars'.ProjCong. +Qed. + +Create HintDb nfne. +#[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne. + +Lemma ne_nf_antiren n m (a : PTm n) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (ne (subst_PTm ρ a) -> ne a) /\ (nf (subst_PTm ρ a) -> nf a). +Proof. + move : m ρ. elim : n / a => //; + hauto b:on drew:off use:RPar.var_or_const_up. +Qed. + +Lemma wn_antirenaming n m a (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + wn (subst_PTm ρ a) -> wn a. +Proof. + rewrite /wn => hρ. + move => [v [rv nfv]]. + move /RPars'.antirenaming : rv. + move /(_ hρ) => [b [hb ?]]. subst. + exists b. split => //=. + move : nfv. + by eapply ne_nf_antiren. +Qed. + +Lemma ext_wn n (a : PTm n) : + wn (PApp a PBot) -> + wn a. +Proof. + move E : (PApp a (PBot)) => a0 [v [hr hv]]. + move : a E. + move : hv. + elim : a0 v / hr. + - hauto q:on inv:PTm ctrs:rtc b:on db: nfne. + - move => a0 a1 a2 hr0 hr1 ih hnfa2. + move /(_ hnfa2) in ih. + move => a. + case : a0 hr0=>// => b0 b1. + elim /RPar'.inv=>// _. + + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst. + have ? : b3 = (PBot) by hauto lq:on inv:RPar'.R. subst. + suff : wn (PAbs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn. + have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder. + move => h. apply wn_abs. + move : h. apply wn_antirenaming. + hauto lq:on rew:off inv:option. + + hauto q:on inv:RPar'.R ctrs:rtc b:on. +Qed. + +Module Join. + Lemma ProjCong p n (a0 a1 : PTm n) : + join a0 a1 -> + join (PProj p a0) (PProj p a1). + Proof. hauto lq:on use:Pars.ProjCong unfold:join. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + join a0 a1 -> + join b0 b1 -> + join (PPair a0 b0) (PPair a1 b1). + Proof. hauto lq:on use:Pars.PairCong unfold:join. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + join a0 a1 -> + join b0 b1 -> + join (PApp a0 b0) (PApp a1 b1). + Proof. hauto lq:on use:Pars.AppCong. Qed. + + Lemma AbsCong n (a b : PTm (S n)) : + join a b -> + join (PAbs a) (PAbs b). + Proof. hauto lq:on use:Pars.AbsCong. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + join a b -> join (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + induction 1; hauto lq:on use:Pars.renaming. + Qed. + + Lemma weakening n (a b : PTm n) : + join a b -> join (ren_PTm shift a) (ren_PTm shift b). + Proof. + apply renaming. + Qed. + + Lemma FromPar n (a b : PTm n) : + Par.R a b -> + join a b. + Proof. + hauto lq:on ctrs:rtc use:rtc_once. + Qed. +End Join. + +Lemma abs_eq n a (b : PTm n) : + join (PAbs a) b <-> join a (PApp (ren_PTm shift b) (VarPTm var_zero)). +Proof. + split. + - move => /Join.weakening h. + have {h} : join (PApp (ren_PTm shift (PAbs a)) (VarPTm var_zero)) (PApp (ren_PTm shift b) (VarPTm var_zero)) + by hauto l:on use:Join.AppCong, join_refl. + simpl. + move => ?. apply : join_transitive; eauto. + apply join_symmetric. apply Join.FromPar. + apply : Par.AppAbs'; eauto using Par.refl. by asimpl. + - move /Join.AbsCong. + move /join_transitive. apply. + apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl. +Qed. + +Lemma pair_eq n (a0 a1 b : PTm n) : + join (PPair a0 a1) b <-> join a0 (PProj PL b) /\ join a1 (PProj PR b). +Proof. + split. + - move => h. + have /Join.ProjCong {}h := h. + have h0 : forall p, join (if p is PL then a0 else a1) (PProj p (PPair a0 a1)) + by hauto lq:on use:join_symmetric, Join.FromPar, Par.ProjPair', Par.refl. + hauto lq:on rew:off use:join_transitive, join_symmetric. + - move => [h0 h1]. + move : h0 h1. + move : Join.PairCong; repeat move/[apply]. + move /join_transitive. apply. apply join_symmetric. + apply Join.FromPar. hauto lq:on ctrs:Par.R use:Par.refl. +Qed. + +Lemma join_pair_inj n (a0 a1 b0 b1 : PTm n) : + join (PPair a0 a1) (PPair b0 b1) <-> join a0 b0 /\ join a1 b1. +Proof. + split; last by hauto lq:on use:Join.PairCong. + move /pair_eq => [h0 h1]. + have : join (PProj PL (PPair b0 b1)) b0 by hauto lq:on use:Join.FromPar, Par.refl, Par.ProjPair'. + have : join (PProj PR (PPair b0 b1)) b1 by hauto lq:on use:Join.FromPar, Par.refl, Par.ProjPair'. + eauto using join_transitive. +Qed. + +Lemma rpars_wn n (a b : PTm n) : + rtc RPar'.R a b -> wn a -> wn b. +Proof. + move => h [b0 [h0 h1]]. + have : exists c, rtc RPar'.R b c /\ rtc RPar'.R b0 c by + eauto using RPar'_confluent. + move => [c [h2 h3]]. + have ? : c = b0 by sfirstorder use:nf_refls. subst. + sfirstorder use:@relations.rtc_transitive. +Qed. + +Lemma rpar_wn n (a b : PTm n) : + RPar'.R a b -> wn a -> wn b. +Proof. hauto lq:on use:rpars_wn ctrs:rtc. Qed. + +Definition norm {n} (a b : PTm n) := rtc RPar'.R a b /\ nf b. + + +Lemma epar_wn n (a b : PTm n) : + ERed.R b a -> wn a -> wn b. +Proof. + move => h. + move => [v [h0 h1]]. + move : b h1 h. + elim : a v /h0 . + - admit. + - move => a b v ha iha hb b0 hv hr. + specialize hb with (1 := hv). + + + - move => a h. + apply wn_abs' in h. + have {h} : wn (PApp a PBot) by admit. + apply ext_wn. + - move => a ha. + have [h0 h1] : wn (PProj PL a) /\ wn (PProj PR a) by admit. + admit. + - hauto q:on use:wn_abs, wn_abs'. + - move => a0 a1 b ha iha hb.