From 226b196d159bb45dd1e04a7ebaeadc46472669f7 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 2 Mar 2025 17:35:51 -0500 Subject: [PATCH] Refactor half of fp_red --- theories/Autosubst2/fintype.v | 419 -------------- theories/fp_red.v | 988 +++++++++++++++++----------------- 2 files changed, 486 insertions(+), 921 deletions(-) delete mode 100644 theories/Autosubst2/fintype.v diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v deleted file mode 100644 index 99508b6..0000000 --- a/theories/Autosubst2/fintype.v +++ /dev/null @@ -1,419 +0,0 @@ -(** * Autosubst Header for Scoped Syntax - Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact. - -Version: December 11, 2019. -*) -Require Import core. -Require Import Setoid Morphisms Relation_Definitions. - -Set Implicit Arguments. -Unset Strict Implicit. - -Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := - match p with eq_refl => eq_refl end. - -Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := - match q with eq_refl => match p with eq_refl => eq_refl end end. - -(** ** Primitives of the Sigma Calculus - We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type. -*) - -Fixpoint fin (n : nat) : Type := - match n with - | 0 => False - | S m => option (fin m) - end. - -(** Renamings and Injective Renamings - _Renamings_ are mappings between finite types. -*) -Definition ren (m n : nat) : Type := fin m -> fin n. - -Definition id {X} := @Datatypes.id X. - -Definition idren {k: nat} : ren k k := @Datatypes.id (fin k). - -(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *) -Definition var_zero {n : nat} : fin (S n) := None. - -Definition null {T} (i : fin 0) : T := match i with end. - -Definition shift {n : nat} : ren n (S n) := - Some. - -(** Extension of Finite Mappings - Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows: -*) -Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X := - match m with - | None => x - | Some i => f i - end. - -#[ export ] -Hint Opaque scons : rewrite. - -(** ** Type Class Instances for Notation *) - -(** *** Type classes for renamings. *) - -Class Ren1 (X1 : Type) (Y Z : Type) := - ren1 : X1 -> Y -> Z. - -Class Ren2 (X1 X2 : Type) (Y Z : Type) := - ren2 : X1 -> X2 -> Y -> Z. - -Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := - ren3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := - ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := - ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module RenNotations. - Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. - - Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. - - Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. -End RenNotations. - -(** *** Type Classes for Substiution *) - -Class Subst1 (X1 : Type) (Y Z: Type) := - subst1 : X1 -> Y -> Z. - -Class Subst2 (X1 X2 : Type) (Y Z: Type) := - subst2 : X1 -> X2 -> Y -> Z. - -Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := - subst3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := - subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := - subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module SubstNotations. - Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. - - Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. -End SubstNotations. - -(** ** Type Class for Variables *) -Class Var X Y := - ids : X -> Y. - - -(** ** Proofs for substitution primitives *) - -(** Forward Function Composition - Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour. - That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *) - -Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. - -Module CombineNotations. - Notation "f >> g" := (funcomp g f) (at level 50) : fscope. - - Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. - - #[ global ] - Open Scope fscope. - #[ global ] - Open Scope subst_scope. -End CombineNotations. - -Import CombineNotations. - - -(** Generic lifting operation for renamings *) -Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) := - var_zero .: xi >> shift. - -(** Generic proof that lifting of renamings composes. *) -Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. -Proof. - intros [x|]. - - cbn. unfold funcomp. now rewrite <- E. - - reflexivity. -Qed. - -Arguments up_ren_ren {k l m} xi zeta rho E. - -Lemma fin_eta {X} (f g : fin 0 -> X) : - pointwise_relation _ eq f g. -Proof. intros []. Qed. - -(** Eta laws *) -Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) : - pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_eta_id' {n : nat} : - pointwise_relation (fin (S n)) eq (var_zero .: shift) id. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) : - pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). -Proof. intros x. destruct x; reflexivity. Qed. - -(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *) -(* pointwise_relation _ eq (funcomp (scons s f) shift) f. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *) -(* (scons s f (shift x)) = f x. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) -#[export] Instance scons_morphism {X: Type} {n:nat} : - Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n). -Proof. - intros t t' -> sigma tau H. - intros [x|]. - cbn. apply H. - reflexivity. -Qed. - -#[export] Instance scons_morphism2 {X: Type} {n: nat} : - Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n). -Proof. - intros ? t -> sigma tau H ? x ->. - destruct x as [x|]. - cbn. apply H. - reflexivity. -Qed. - -(** ** Variadic Substitution Primitives *) - -Fixpoint shift_p (p : nat) {n} : ren n (p + n) := - fun n => match p with - | 0 => n - | S p => Some (shift_p p n) - end. - -Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n) -> X. -Proof. - destruct m. - - intros n f g. exact g. - - intros n f g. cbn. apply scons. - + exact (f var_zero). - + apply scons_p. - * intros z. exact (f (Some z)). - * exact g. -Defined. - -#[export] Hint Opaque scons_p : rewrite. - -#[export] Instance scons_p_morphism {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau. - intros x. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau ? x ->. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -Definition zero_p {m : nat} {n} : fin m -> fin (m + n). -Proof. - induction m. - - intros []. - - intros [x|]. - + exact (shift_p 1 (IHm x)). - + exact var_zero. -Defined. - -Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z: - (scons_p f g) (zero_p z) = f z. -Proof. - induction m. - - inversion z. - - destruct z. - + simpl. simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f. -Proof. - intros z. - unfold funcomp. - induction m. - - inversion z. - - destruct z. - + simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_tail' X m n (f : fin m -> X) (g : fin n -> X) z : - scons_p f g (shift_p m z) = g z. -Proof. induction m; cbn; eauto. Qed. - -Lemma scons_p_tail_pointwise X m n (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g. -Proof. intros z. induction m; cbn; eauto. Qed. - -Lemma destruct_fin {m n} (x : fin (m + n)): - (exists x', x = zero_p x') \/ exists x', x = shift_p m x'. -Proof. - induction m; simpl in *. - - right. eauto. - - destruct x as [x|]. - + destruct (IHm x) as [[x' ->] |[x' ->]]. - * left. now exists (Some x'). - * right. eauto. - + left. exists None. eauto. -Qed. - -Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) : - pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)). -Proof. - intros x. - destruct (destruct_fin x) as [[x' ->]|[x' ->]]. - (* TODO better way to solve this? *) - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h). - now setoid_rewrite scons_p_head_pointwise. - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h). - change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)). - now rewrite !scons_p_tail_pointwise. -Qed. - - -Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z: - (forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z. -Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed. - -(** Generic n-ary lifting operation. *) -Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n) := - scons_p (zero_p ) (xi >> shift_p _). - -Arguments upRen_p p {m n} xi. - -(** Generic proof for composition of n-ary lifting. *) -Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x. -Proof. - intros x. destruct (destruct_fin x) as [[? ->]|[? ->]]. - - unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'. - - unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'. - now rewrite <- E. -Qed. - - -Arguments zero_p m {n}. -Arguments scons_p {X} m {n} f g. - -Lemma scons_p_eta {X} {m n} {f : fin m -> X} - {g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}: - (forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z. -Proof. - intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]]. - - rewrite scons_p_head'. eauto. - - rewrite scons_p_tail'. eauto. -Qed. - -Arguments scons_p_eta {X} {m n} {f g} h {z}. -Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}. - -(** ** Notations for Scoped Syntax *) - -Module ScopedNotations. - Include RenNotations. - Include SubstNotations. - Include CombineNotations. - -(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) - - Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. - - Notation "↑" := (shift) : subst_scope. - - #[global] - Open Scope fscope. - #[global] - Open Scope subst_scope. -End ScopedNotations. - - -(** ** Tactics for Scoped Syntax *) - -Tactic Notation "auto_case" tactic(t) := (match goal with - | [|- forall (i : fin 0), _] => intros []; t - | [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t - | [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t - | [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t - | [|- forall (i : fin (S _)), _] => intros [?|]; t - end). - -#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances. - -(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) -Ltac fsimpl := - repeat match goal with - | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) - | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) - | [|- context [id ?s]] => change (id s) with s - | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *) - (* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *) - | [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s - | [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m) - (* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *) - | [|- context[idren >> ?f]] => change (idren >> f) with f - | [|- context[?f >> idren]] => change (f >> idren) with f - | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) - | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce - | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce - | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) - | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) - | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce - | [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce - | [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce - (* | _ => progress autorewrite with FunctorInstances *) - | [|- context[funcomp (scons_p _ _ _) (zero_p _)]] => - first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ] - | [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head' - | [|- context[funcomp (scons_p _ _ _) (shift_p _)]] => - first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ] - | [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail' - | _ => first [progress minimize | progress cbn [shift scons scons_p] ] - end. diff --git a/theories/fp_red.v b/theories/fp_red.v index bffe1a7..5f7ea0d 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -8,7 +8,7 @@ Require Import Arith.Wf_nat (well_founded_lt_compat). Require Import Psatz. From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn). From Hammer Require Import Tactics. -Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common. +Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common. Require Import Btauto. Require Import Cdcl.Itauto. @@ -23,7 +23,7 @@ Ltac2 spec_refl () := Ltac spec_refl := ltac2:(Control.enter spec_refl). Module EPar. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> @@ -54,8 +54,6 @@ Module EPar. R A0 A1 -> R B0 B1 -> R (PBind p A0 B0) (PBind p A1 B1) - | BotCong : - R PBot PBot | NatCong : R PNat PNat | IndCong P0 P1 a0 a1 b0 b1 c0 c1 : @@ -72,64 +70,64 @@ Module EPar. (* ------------ *) R (PSuc a0) (PSuc a1). - Lemma refl n (a : PTm n) : R a a. + Lemma refl (a : PTm) : R a a. Proof. - elim : n / a; hauto lq:on ctrs:R. + elim : a; hauto lq:on ctrs:R. Qed. - Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop. - Lemma AppEta' n a0 a1 (u : PTm n) : + Lemma AppEta' a0 a1 (u : PTm) : u = (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) -> R a0 a1 -> R u a1. Proof. move => ->. apply AppEta. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. - elim : n a b /h. + move => h. move : ξ. + elim : a b /h. all : try qauto ctrs:R. - move => n a0 a1 ha iha m ξ /=. + move => a0 a1 ha iha ξ /=. eapply AppEta'; eauto. by asimpl. Qed. - Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) : (forall i, R (ρ0 i) (ρ1 i)) -> - (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ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 : + Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) 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. + Proof. hauto q:on inv:nat. Qed. - Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : + Lemma morphing_up (ρ0 ρ1 : nat -> PTm) : (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) : + Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : (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 => n. - move => a0 a1 ha iha m ρ0 ρ1 hρ /=. + move => + h. move : ρ0 ρ1. elim : a b / h. + move => a0 a1 ha iha ρ0 ρ1 hρ /=. eapply AppEta'; eauto. by asimpl. all : hauto lq:on ctrs:R use:morphing_up. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + Lemma substing (a b : PTm) (ρ : nat -> PTm) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. End EPar. -Inductive SNe {n} : PTm n -> Prop := +Inductive SNe : PTm -> Prop := | N_Var i : SNe (VarPTm i) | N_App a b : @@ -139,15 +137,13 @@ Inductive SNe {n} : PTm n -> Prop := | N_Proj p a : SNe a -> SNe (PProj p a) -| N_Bot : - SNe PBot | N_Ind P a b c : SN P -> SNe a -> SN b -> SN c -> SNe (PInd P a b c) -with SN {n} : PTm n -> Prop := +with SN : PTm -> Prop := | N_Pair a b : SN a -> SN b -> @@ -175,7 +171,7 @@ with SN {n} : PTm n -> Prop := | N_Suc a : SN a -> SN (PSuc a) -with TRedSN {n} : PTm n -> PTm n -> Prop := +with TRedSN : PTm -> PTm -> Prop := | N_β a b : SN b -> TRedSN (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) @@ -210,38 +206,38 @@ with TRedSN {n} : PTm n -> PTm n -> Prop := TRedSN a0 a1 -> TRedSN (PInd P a0 b c) (PInd P a1 b c). -Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop. +Derive Inversion tred_inv with (forall (a b : PTm), TRedSN a b) Sort Prop. -Inductive SNat {n} : PTm n -> Prop := +Inductive SNat : PTm -> Prop := | S_Zero : SNat PZero | S_Neu a : SNe a -> SNat a | S_Suc a : SNat a -> SNat (PSuc a) | S_Red a b : TRedSN a b -> SNat b -> SNat a. -Lemma PProj_imp n p a : - @ishf n a -> +Lemma PProj_imp p a : + ishf a -> ~~ ispair a -> ~ SN (PProj p a). Proof. move => + + h. move E : (PProj p a) h => u h. move : p a E. - elim : n u / h => //=. + elim : u / h => //=. hauto lq:on inv:SNe,PTm. hauto lq:on inv:TRedSN. Qed. -Lemma PApp_imp n a b : - @ishf n a -> +Lemma PApp_imp a b : + ishf a -> ~~ isabs a -> ~ SN (PApp a b). Proof. move => + + h. move E : (PApp a b) h => u h. - move : a b E. elim : n u /h=>//=. + move : a b E. elim : u /h=>//=. hauto lq:on inv:SNe,PTm. hauto lq:on inv:TRedSN. Qed. -Lemma PInd_imp n P (a : PTm n) b c : +Lemma PInd_imp P (a : PTm) b c : ishf a -> ~~ iszero a -> ~~ issuc a -> @@ -249,35 +245,35 @@ Lemma PInd_imp n P (a : PTm n) b c : Proof. move => + + + h. move E : (PInd P a b c) h => u h. move : P a b c E. - elim : n u /h => //=. + elim : u /h => //=. hauto lq:on inv:SNe,PTm. hauto lq:on inv:TRedSN. Qed. -Lemma PProjAbs_imp n p (a : PTm (S n)) : +Lemma PProjAbs_imp p (a : PTm) : ~ SN (PProj p (PAbs a)). Proof. sfirstorder use:PProj_imp. Qed. -Lemma PAppPair_imp n (a b0 b1 : PTm n ) : +Lemma PAppPair_imp (a b0 b1 : PTm ) : ~ SN (PApp (PPair b0 b1) a). Proof. sfirstorder use:PApp_imp. Qed. -Lemma PAppBind_imp n p (A : PTm n) B b : +Lemma PAppBind_imp p (A : PTm) B b : ~ SN (PApp (PBind p A B) b). Proof. sfirstorder use:PApp_imp. Qed. -Lemma PProjBind_imp n p p' (A : PTm n) B : +Lemma PProjBind_imp p p' (A : PTm) B : ~ SN (PProj p (PBind p' A B)). Proof. move E :(PProj p (PBind p' A B)) => u hu. move : p p' A B E. - elim : n u /hu=>//=. + elim : u /hu=>//=. hauto lq:on inv:SNe. hauto lq:on inv:TRedSN. Qed. @@ -288,7 +284,7 @@ Scheme sne_ind := Induction for SNe Sort Prop Combined Scheme sn_mutual from sne_ind, sn_ind, sred_ind. -Fixpoint ne {n} (a : PTm n) := +Fixpoint ne (a : PTm) := match a with | VarPTm i => true | PApp a b => ne a && nf b @@ -297,13 +293,12 @@ Fixpoint ne {n} (a : PTm n) := | PProj _ a => ne a | PUniv _ => false | PBind _ _ _ => false - | PBot => true | PInd P a b c => nf P && ne a && nf b && nf c | PNat => false | PSuc a => false | PZero => false end -with nf {n} (a : PTm n) := +with nf (a : PTm) := match a with | VarPTm i => true | PApp a b => ne a && nf b @@ -312,69 +307,66 @@ with nf {n} (a : PTm n) := | PProj _ a => ne a | PUniv _ => true | PBind _ A B => nf A && nf B - | PBot => true | PInd P a b c => nf P && ne a && nf b && nf c | PNat => true | PSuc a => nf a | PZero => true end. -Lemma ne_nf n a : @ne n a -> nf a. +Lemma ne_nf a : ne a -> nf a. Proof. elim : a => //=. Qed. -Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) : +Lemma ne_nf_ren (a : PTm) (ξ : nat -> nat) : (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)). Proof. - move : m ξ. elim : n / a => //=; solve [hauto b:on]. + move : ξ. elim : a => //=; solve [hauto b:on]. Qed. -Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop := +Inductive TRedSN' (a : PTm) : PTm -> Prop := | T_Refl : TRedSN' a a | T_Once b : TRedSN a b -> TRedSN' a b. -Lemma SN_Proj n p (a : PTm n) : +Lemma SN_Proj p (a : PTm) : SN (PProj p a) -> SN a. Proof. move E : (PProj p a) => u h. move : a E. - elim : n u / h => n //=; sauto. + elim : u / h => n //=; sauto. Qed. -Lemma N_β' n a (b : PTm n) u : +Lemma N_β' a (b : PTm) u : u = (subst_PTm (scons b VarPTm) a) -> SN b -> TRedSN (PApp (PAbs a) b) u. Proof. move => ->. apply N_β. Qed. -Lemma N_IndSuc' n P a b c u : +Lemma N_IndSuc' P a b c u : u = (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) -> SN P -> - @SN n a -> + SN a -> SN b -> SN c -> TRedSN (PInd P (PSuc a) b c) u. Proof. move => ->. apply N_IndSuc. Qed. -Lemma sn_renaming n : - (forall (a : PTm n) (s : SNe a), forall m (ξ : fin n -> fin m), SNe (ren_PTm ξ a)) /\ - (forall (a : PTm n) (s : SN a), forall m (ξ : fin n -> fin m), SN (ren_PTm ξ a)) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall m (ξ : fin n -> fin m), TRedSN (ren_PTm ξ a) (ren_PTm ξ b)). +Lemma sn_renaming : + (forall (a : PTm) (s : SNe a), forall (ξ : nat -> nat), SNe (ren_PTm ξ a)) /\ + (forall (a : PTm) (s : SN a), forall (ξ : nat -> nat), SN (ren_PTm ξ a)) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall (ξ : nat -> nat), TRedSN (ren_PTm ξ a) (ren_PTm ξ b)). Proof. - move : n. apply sn_mutual => n; try qauto ctrs:SN, SNe, TRedSN depth:1. - move => a b ha iha m ξ /=. - apply N_β'. by asimpl. eauto. + apply sn_mutual => n; try qauto ctrs:SN, SNe, TRedSN depth:1. + move => */=. apply N_β';eauto. by asimpl. - move => * /=. - apply N_IndSuc';eauto. by asimpl. + move => */=. apply N_IndSuc'; eauto. by asimpl. Qed. -Lemma ne_nf_embed n (a : PTm n) : +Lemma ne_nf_embed (a : PTm) : (ne a -> SNe a) /\ (nf a -> SN a). Proof. - elim : n / a => //=; hauto qb:on ctrs:SNe, SN. + elim : a => //=; hauto qb:on ctrs:SNe, SN. Qed. #[export]Hint Constructors SN SNe TRedSN : sn. @@ -383,49 +375,53 @@ Ltac2 rec solve_anti_ren () := let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in intro $x; lazy_match! Constr.type (Control.hyp x) with - | fin _ -> _ _ => (ltac1:(case;qauto depth:2 db:sn)) + | nat -> nat => (ltac1:(case;qauto depth:2 db:sn)) + | nat -> PTm => (ltac1:(case;qauto depth:2 db:sn)) | _ => solve_anti_ren () end. Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). -Lemma sn_antirenaming n : - (forall (a : PTm n) (s : SNe a), forall m (ξ : fin m -> fin n) b, a = ren_PTm ξ b -> SNe b) /\ - (forall (a : PTm n) (s : SN a), forall m (ξ : fin m -> fin n) b, a = ren_PTm ξ b -> SN b) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall m (ξ : fin m -> fin n) a0, +Lemma sn_antirenaming : + (forall (a : PTm) (s : SNe a), forall (ξ : nat -> nat) b, a = ren_PTm ξ b -> SNe b) /\ + (forall (a : PTm) (s : SN a), forall (ξ : nat -> nat) b, a = ren_PTm ξ b -> SN b) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall (ξ : nat -> nat) a0, a = ren_PTm ξ a0 -> exists b0, TRedSN a0 b0 /\ b = ren_PTm ξ b0). Proof. - move : n. apply sn_mutual => n; try solve_anti_ren. + apply sn_mutual; try solve_anti_ren. + move => *. subst. spec_refl. hauto lq:on ctrs:TRedSN, SN. - move => a b ha iha m ξ []//= u u0 [+ ?]. subst. + move => a b ha iha ξ []//= u u0 [+ ?]. subst. case : u => //= => u [*]. subst. spec_refl. eexists. split. apply N_β=>//. by asimpl. - move => a b hb ihb m ξ[]//= p p0 [? +]. subst. + move => a b hb ihb ξ[]//= p p0 [? +]. subst. case : p0 => //= p p0 [*]. subst. spec_refl. by eauto with sn. - move => a b ha iha m ξ[]//= u u0 [? ]. subst. + move => a b ha iha ξ[]//= u u0 [? ]. subst. case : u0 => //=. move => p p0 [*]. subst. spec_refl. by eauto with sn. - move => P b c ha iha hb ihb hc ihc m ξ []//= P0 a0 b0 c0 [?]. subst. + move => P b c ha iha hb ihb hc ihc ξ []//= P0 a0 b0 c0 [?]. subst. case : a0 => //= _ *. subst. spec_refl. by eauto with sn. - move => P a b c hP ihP ha iha hb ihb hc ihc m ξ []//= P0 a0 b0 c0 [?]. subst. + move => P a b c hP ihP ha iha hb ihb hc ihc ξ []//= P0 a0 b0 c0 [?]. subst. case : a0 => //= a0 [*]. subst. spec_refl. eexists; repeat split; eauto with sn. - by asimpl. Qed. + by asimpl. +Qed. -Lemma sn_unmorphing n : - (forall (a : PTm n) (s : SNe a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SNe b) /\ - (forall (a : PTm n) (s : SN a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SN b) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall m (ρ : fin m -> PTm n) a0, +Lemma sn_unmorphing : + (forall (a : PTm) (s : SNe a), forall (ρ : nat -> PTm) b, a = subst_PTm ρ b -> SNe b) /\ + (forall (a : PTm) (s : SN a), forall (ρ : nat -> PTm) b, a = subst_PTm ρ b -> SN b) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall (ρ : nat -> PTm) a0, a = subst_PTm ρ a0 -> (exists b0, b = subst_PTm ρ b0 /\ TRedSN a0 b0) \/ SNe a0). Proof. - move : n. apply sn_mutual => n; try solve_anti_ren. - - move => a b ha iha m ξ b0. + apply sn_mutual; try solve_anti_ren. + - hauto q:on db:sn. + - move => a b ha iha ξ b0. case : b0 => //=. + hauto lq:on rew:off db:sn. + move => p p0 [+ ?]. subst. @@ -436,7 +432,7 @@ Proof. spec_refl. eexists. split; last by eauto using N_β. by asimpl. - - move => a0 a1 b hb ihb ha iha m ρ []//=. + - move => a0 a1 b hb ihb ha iha ρ []//=. + hauto lq:on rew:off db:sn. + move => t0 t1 [*]. subst. spec_refl. @@ -447,18 +443,18 @@ Proof. * move => h. right. apply N_App => //. - - move => a b hb ihb m ρ []//=. + - move => a b hb ihb ρ []//=. + hauto l:on ctrs:TRedSN. + move => p p0 [?]. subst. case : p0 => //=. * hauto lq:on rew:off db:sn. * move => p p0 [*]. subst. hauto lq:on db:sn. - - move => a b ha iha m ρ []//=; first by hauto l:on db:sn. + - move => a b ha iha ρ []//=; first by hauto l:on db:sn. case => //=. move => []//=. + hauto lq:on db:sn. + hauto lq:on db:sn. - - move => p a b ha iha m ρ []//=; first by hauto l:on db:sn. + - move => p a b ha iha ρ []//=; first by hauto l:on db:sn. move => t0 t1 [*]. subst. spec_refl. case : iha. @@ -466,12 +462,12 @@ Proof. left. eexists. split; last by eauto with sn. reflexivity. + hauto lq:on db:sn. - - move => P b c hP ihP hb ihb hc ihc m ρ []//=. + - move => P b c hP ihP hb ihb hc ihc ρ []//=. + hauto lq:on db:sn. + move => p []//=. * hauto lq:on db:sn. * hauto q:on db:sn. - - move => P a b c hP ihP ha iha hb ihb hc ihc m ρ []//=. + - move => P a b c hP ihP ha iha hb ihb hc ihc ρ []//=. + hauto lq:on db:sn. + move => P0 a0 b0 c0 [?]. subst. case : a0 => //=. @@ -480,7 +476,7 @@ Proof. spec_refl. left. eexists. split; last by eauto with sn. by asimpl. - - move => P a0 a1 b c hP ihP hb ihb hc ihc ha iha m ρ[]//=. + - move => P a0 a1 b c hP ihP hb ihb hc ihc ha iha ρ[]//=. + hauto lq:on db:sn. + move => P1 a2 b2 c2 [*]. subst. spec_refl. @@ -491,42 +487,41 @@ Proof. * hauto lq:on db:sn. Qed. -Lemma SN_AppInv : forall n (a b : PTm n), SN (PApp a b) -> SN a /\ SN b. +Lemma SN_AppInv : forall (a b : PTm), SN (PApp a b) -> SN a /\ SN b. Proof. - move => n a b. move E : (PApp a b) => u hu. move : a b E. - elim : n u /hu=>//=. + move => a b. move E : (PApp a b) => u hu. move : a b E. + elim : u /hu=>//=. hauto lq:on rew:off inv:SNe db:sn. - move => n a b ha hb ihb a0 b0 ?. subst. + move => a b ha hb ihb a0 b0 ?. subst. inversion ha; subst. move {ihb}. hecrush use:sn_unmorphing. hauto lq:on db:sn. Qed. -Lemma SN_ProjInv : forall n p (a : PTm n), SN (PProj p a) -> SN a. +Lemma SN_ProjInv : forall p (a : PTm), SN (PProj p a) -> SN a. Proof. - move => n p a. move E : (PProj p a) => u hu. + move => p a. move E : (PProj p a) => u hu. move : p a E. - elim : n u / hu => //=. + elim : u / hu => //=. hauto lq:on rew:off inv:SNe db:sn. hauto lq:on rew:off inv:TRedSN db:sn. Qed. -Lemma SN_IndInv : forall n P (a : PTm n) b c, SN (PInd P a b c) -> SN P /\ SN a /\ SN b /\ SN c. +Lemma SN_IndInv : forall P (a : PTm) b c, SN (PInd P a b c) -> SN P /\ SN a /\ SN b /\ SN c. Proof. - move => n P a b c. move E : (PInd P a b c) => u hu. move : P a b c E. - elim : n u / hu => //=. + move => P a b c. move E : (PInd P a b c) => u hu. move : P a b c E. + elim : u / hu => //=. hauto lq:on rew:off inv:SNe db:sn. hauto lq:on rew:off inv:TRedSN db:sn. Qed. -Lemma epar_sn_preservation n : - (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\ - (forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall c, EPar.R a c -> exists d, TRedSN' c d /\ EPar.R b d). +Lemma epar_sn_preservation : + (forall (a : PTm) (s : SNe a), forall b, EPar.R a b -> SNe b) /\ + (forall (a : PTm) (s : SN a), forall b, EPar.R a b -> SN b) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall c, EPar.R a c -> exists d, TRedSN' c d /\ EPar.R b d). Proof. - move : n. apply sn_mutual => n. - - sauto lq:on. + apply sn_mutual. - sauto lq:on. - sauto lq:on. - sauto lq:on. @@ -562,7 +557,7 @@ Proof. exists (subst_PTm (scons b1 VarPTm) a2). split. sauto lq:on. - hauto lq:on use:EPar.morphing, EPar.refl inv:option. + hauto lq:on use:EPar.morphing, EPar.refl inv:nat. - sauto. - move => a b hb ihb c. elim /EPar.inv => //= _. @@ -590,12 +585,12 @@ Proof. elim /EPar.inv : ha0 => //=_. move => a0 a2 ha0 [*]. subst. eexists. split. apply T_Once. apply N_IndSuc; eauto. - hauto q:on ctrs:EPar.R use:EPar.morphing, EPar.refl inv:option. + hauto q:on ctrs:EPar.R use:EPar.morphing, EPar.refl inv:nat. - sauto q:on. Qed. Module RRed. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Beta ***********************) | AppAbs a b : R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) @@ -649,27 +644,27 @@ Module RRed. R a0 a1 -> R (PSuc a0) (PSuc a1). - Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. - Lemma AppAbs' n a (b : PTm n) u : + Lemma AppAbs' a (b : PTm) u : u = (subst_PTm (scons b VarPTm) a) -> R (PApp (PAbs a) b) u. Proof. move => ->. by apply AppAbs. Qed. - Lemma IndSuc' n P a b c u : + Lemma IndSuc' P a b c u : u = (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) -> - R (@PInd n P (PSuc a) b c) u. + R (PInd P (PSuc a) b c) u. Proof. move => ->. apply IndSuc. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. - elim : n a b /h. + move => h. move : ξ. + elim : a b /h. all : try qauto ctrs:R. - move => n a b m ξ /=. + move => a b ξ /=. apply AppAbs'. by asimpl. move => */=; apply IndSuc'; eauto. by asimpl. Qed. @@ -678,56 +673,56 @@ Module RRed. let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in intro $x; lazy_match! Constr.type (Control.hyp x) with - | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:RRed.R)) + | nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:RRed.R)) + | nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:RRed.R)) | _ => solve_anti_ren () end. Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). - Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) : 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; try solve_anti_ren. - - move => n a b m ξ []//=. move => []//= t t0 [*]. subst. + move : ξ a E. elim : u b/h; try solve_anti_ren. + - move => a b ξ []//=. move => []//= t t0 [*]. subst. eexists. split. apply AppAbs. by asimpl. - - move => n p a b m ξ []//=. + - move => p a b ξ []//=. move => p0 []//=. hauto q:on ctrs:R. - - move => n p b c m ξ []//= P a0 b0 c0 [*]. subst. + - move => p b c ξ []//= P a0 b0 c0 [*]. subst. destruct a0 => //=. hauto lq:on ctrs:R. - - move => n P a b c m ξ []//=. + - move => P a b c ξ []//=. move => p p0 p1 p2 [?]. subst. case : p0 => //=. move => p0 [?] *. subst. eexists. split; eauto using IndSuc. by asimpl. Qed. - Lemma nf_imp n (a b : PTm n) : + Lemma nf_imp (a b : PTm) : nf a -> R a b -> False. Proof. move/[swap]. induction 1; hauto qb:on inv:PTm. Qed. - Lemma FromRedSN n (a b : PTm n) : + Lemma FromRedSN (a b : PTm) : TRedSN a b -> RRed.R a b. Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + Lemma substing (a b : PTm) (ρ : nat -> PTm) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. - move => h. move : m ρ. elim : n a b / h => n. + move => h. move : ρ. elim : a b / h => n. all : try hauto lq:on ctrs:R. - move => a b m ρ /=. - eapply AppAbs'; eauto; cycle 1. by asimpl. + move => */=. eapply AppAbs'; eauto; cycle 1. by asimpl. move => */=; apply : IndSuc'; eauto. by asimpl. Qed. End RRed. Module RPar. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> @@ -774,8 +769,6 @@ Module RPar. R A0 A1 -> R B0 B1 -> R (PBind p A0 B0) (PBind p A1 B1) - | BotCong : - R PBot PBot | NatCong : R PNat PNat | IndCong P0 P1 a0 a1 b0 b1 c0 c1 : @@ -792,28 +785,28 @@ Module RPar. (* ------------ *) R (PSuc a0) (PSuc a1). - Lemma refl n (a : PTm n) : R a a. + Lemma refl (a : PTm) : R a a. Proof. - elim : n / a; hauto lq:on ctrs:R. + elim : a; hauto lq:on ctrs:R. Qed. - Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop. - Lemma AppAbs' n a0 a1 (b0 b1 : PTm n) u : + Lemma AppAbs' a0 a1 (b0 b1 : PTm) u : u = (subst_PTm (scons b1 VarPTm) a1) -> R a0 a1 -> R b0 b1 -> R (PApp (PAbs a0) b0) u. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' n p u (a0 a1 b0 b1 : PTm n) : + Lemma ProjPair' p u (a0 a1 b0 b1 : PTm) : u = (if p is PL then a1 else b1) -> R a0 a1 -> R b0 b1 -> R (PProj p (PPair a0 b0)) u. Proof. move => ->. apply ProjPair. Qed. - Lemma IndSuc' n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 u : + Lemma IndSuc' P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 u : u = (subst_PTm (scons (PInd P1 a1 b1 c1) (scons a1 VarPTm)) c1) -> R P0 P1 -> R a0 a1 -> @@ -823,43 +816,43 @@ Module RPar. R (PInd P0 (PSuc a0) b0 c0) u. Proof. move => ->. apply IndSuc. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. - elim : n a b /h. + move => h. move : ξ. + elim : a b /h. all : try qauto ctrs:R use:ProjPair'. - move => n a0 a1 b0 b1 ha iha hb ihb m ξ /=. + move => a0 a1 b0 b1 ha iha hb ihb ξ /=. eapply AppAbs'; eauto. by asimpl. move => * /=. apply : IndSuc'; eauto. by asimpl. Qed. - Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) : (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 : + Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) 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. + Proof. hauto q:on inv:nat. Qed. - Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : + Lemma morphing_up (ρ0 ρ1 : nat -> PTm) : (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) : + Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : (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 => n. + move => + h. move : ρ0 ρ1. elim : a b / h. all : try hauto lq:on ctrs:R use:morphing_up, ProjPair'. - move => a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=. + move => a0 a1 b0 b1 ha iha hb ihb ρ0 ρ1 hρ /=. eapply AppAbs'; eauto; cycle 1. sfirstorder use:morphing_up. by asimpl. move => */=; eapply IndSuc'; eauto; cycle 1. sfirstorder use:morphing_up. @@ -867,29 +860,29 @@ Module RPar. by asimpl. Qed. - Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : + Lemma substing (a : PTm) b (ρ : nat -> PTm) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma cong n (a0 a1 : PTm (S n)) b0 b1 : + Lemma cong (a0 a1 : PTm) b0 b1 : 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 q:on inv:option ctrs:R. + hauto q:on inv:nat ctrs:R. Qed. - Lemma FromRRed n (a b : PTm n) : + Lemma FromRRed (a b : PTm) : RRed.R a b -> RPar.R a b. Proof. induction 1; qauto l:on use:RPar.refl ctrs:RPar.R. Qed. - Function tstar {n} (a : PTm n) := + Function tstar (a : PTm) := match a with | VarPTm i => a | PAbs a => PAbs (tstar a) @@ -900,7 +893,6 @@ Module RPar. | PProj p a => PProj p (tstar a) | PUniv i => PUniv i | PBind p A B => PBind p (tstar A) (tstar B) - | PBot => PBot | PNat => PNat | PZero => PZero | PSuc a => PSuc (tstar a) @@ -910,11 +902,11 @@ Module RPar. | PInd P a b c => PInd (tstar P) (tstar a) (tstar b) (tstar c) end. - Lemma triangle n (a b : PTm n) : + Lemma triangle (a b : PTm) : RPar.R a b -> RPar.R b (tstar a). Proof. move : b. - apply tstar_ind => {}n{}a. + apply tstar_ind => {}a. - hauto lq:on ctrs:R inv:R. - hauto lq:on ctrs:R inv:R. - hauto lq:on rew:off inv:R use:cong ctrs:R. @@ -942,33 +934,31 @@ Module RPar. - hauto lq:on ctrs:R inv:R. - hauto lq:on ctrs:R inv:R. - hauto lq:on ctrs:R inv:R. - - move => P b c ?. subst. - move => h0. inversion 1; subst. hauto lq:on ctrs:R. qauto l:on inv:R ctrs:R. - move => P a0 b c ? hP ihP ha iha hb ihb u. subst. elim /inv => //= _. + move => P0 P1 a1 a2 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst. - apply morphing. hauto lq:on ctrs:R inv:option. + apply morphing. hauto lq:on ctrs:R inv:nat. eauto. + sauto q:on ctrs:R. - sauto lq:on. Qed. - Lemma diamond n (a b c : PTm n) : + Lemma diamond (a b c : PTm) : R a b -> R a c -> exists d, R b d /\ R c d. Proof. eauto using triangle. Qed. End RPar. -Lemma red_sn_preservation n : - (forall (a : PTm n) (s : SNe a), forall b, RPar.R a b -> SNe b) /\ - (forall (a : PTm n) (s : SN a), forall b, RPar.R a b -> SN b) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall c, RPar.R a c -> exists d, TRedSN' c d /\ RPar.R b d). +Lemma red_sn_preservation : + (forall (a : PTm) (s : SNe a), forall b, RPar.R a b -> SNe b) /\ + (forall (a : PTm) (s : SN a), forall b, RPar.R a b -> SN b) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall c, RPar.R a c -> exists d, TRedSN' c d /\ RPar.R b d). Proof. - move : n. apply sn_mutual => n. + apply sn_mutual. - hauto l:on inv:RPar.R. - qauto l:on inv:RPar.R,SNe,SN ctrs:SNe. - hauto lq:on inv:RPar.R, SNe ctrs:SNe. - hauto lq:on inv:RPar.R, SNe ctrs:SNe. - - qauto l:on inv:RPar.R, SN,SNe ctrs:SNe. + (* - qauto l:on inv:RPar.R, SN,SNe ctrs:SNe. *) - qauto l:on ctrs:SN inv:RPar.R. - hauto lq:on ctrs:SN inv:RPar.R. - hauto lq:on ctrs:SN. @@ -1002,13 +992,13 @@ Proof. elim /RPar.inv => //=_. + move => P0 P1 a0 a1 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst. eexists. split; first by apply T_Refl. - apply RPar.morphing=>//. hauto lq:on ctrs:RPar.R inv:option. + apply RPar.morphing=>//. hauto lq:on ctrs:RPar.R inv:nat. + move => P0 P1 a0 a1 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst. elim /RPar.inv : ha' => //=_. move => a0 a2 ha' [*]. subst. eexists. split. apply T_Once. apply N_IndSuc; eauto. - hauto q:on use:RPar.morphing ctrs:RPar.R inv:option. + hauto q:on use:RPar.morphing ctrs:RPar.R inv:nat. - sauto q:on. Qed. @@ -1021,34 +1011,34 @@ Module RReds. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong n (a b : PTm (S n)) : + Lemma AbsCong (a b : PTm) : rtc RRed.R a b -> rtc RRed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + Lemma AppCong (a0 a1 b0 b1 : PTm) : rtc RRed.R a0 a1 -> rtc RRed.R b0 b1 -> rtc RRed.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + Lemma PairCong (a0 a1 b0 b1 : PTm) : rtc RRed.R a0 a1 -> rtc RRed.R b0 b1 -> rtc RRed.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : PTm n) : + Lemma ProjCong p (a0 a1 : PTm) : rtc RRed.R a0 a1 -> rtc RRed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma SucCong n (a0 a1 : PTm n) : + Lemma SucCong (a0 a1 : PTm) : rtc RRed.R a0 a1 -> rtc RRed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. - Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma IndCong P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : rtc RRed.R P0 P1 -> rtc RRed.R a0 a1 -> rtc RRed.R b0 b1 -> @@ -1056,27 +1046,27 @@ Module RReds. rtc RRed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1). Proof. solve_s. Qed. - Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : + Lemma BindCong p (A0 A1 : PTm) B0 B1 : rtc RRed.R A0 A1 -> rtc RRed.R B0 B1 -> rtc RRed.R (PBind p A0 B0) (PBind p A1 B1). Proof. solve_s. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : rtc RRed.R a b -> rtc RRed.R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. elim : a b /h; hauto lq:on ctrs:rtc use:RRed.renaming. + move => h. move : ξ. elim : a b /h; hauto lq:on ctrs:rtc use:RRed.renaming. Qed. - Lemma FromRPar n (a b : PTm n) (h : RPar.R a b) : + Lemma FromRPar (a b : PTm) (h : RPar.R a b) : rtc RRed.R a b. Proof. - elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong. - move => n a0 a1 b0 b1 ha iha hb ihb. + elim : a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong. + move => a0 a1 b0 b1 ha iha hb ihb. apply : rtc_r; last by apply RRed.AppAbs. by eauto using AppCong, AbsCong. - move => n p a0 a1 b0 b1 ha iha hb ihb. + move => p a0 a1 b0 b1 ha iha hb ihb. apply : rtc_r; last by apply RRed.ProjPair. by eauto using PairCong, ProjCong. @@ -1087,7 +1077,7 @@ Module RReds. by eauto using SucCong, IndCong. Qed. - Lemma RParIff n (a b : PTm n) : + Lemma RParIff (a b : PTm) : rtc RRed.R a b <-> rtc RPar.R a b. Proof. split. @@ -1095,11 +1085,11 @@ Module RReds. induction 1; hauto l:on ctrs:rtc use:FromRPar, @relations.rtc_transitive. Qed. - Lemma nf_refl n (a b : PTm n) : + Lemma nf_refl (a b : PTm) : rtc RRed.R a b -> nf a -> a = b. Proof. induction 1; sfirstorder use:RRed.nf_imp. Qed. - Lemma FromRedSNs n (a b : PTm n) : + Lemma FromRedSNs (a b : PTm) : rtc TRedSN a b -> rtc RRed.R a b. Proof. induction 1; hauto lq:on ctrs:rtc use:RRed.FromRedSN. Qed. @@ -1108,7 +1098,7 @@ End RReds. Module NeEPar. - Inductive R_nonelim {n} : PTm n -> PTm n -> Prop := + Inductive R_nonelim : PTm -> PTm -> Prop := (****************** Eta ***********************) | AppEta a0 a1 : ~~ ishf a0 -> @@ -1141,8 +1131,6 @@ Module NeEPar. R_nonelim A0 A1 -> R_nonelim B0 B1 -> R_nonelim (PBind p A0 B0) (PBind p A1 B1) - | BotCong : - R_nonelim PBot PBot | NatCong : R_nonelim PNat PNat | IndCong P0 P1 a0 a1 b0 b1 c0 c1 : @@ -1158,7 +1146,7 @@ Module NeEPar. R_nonelim a0 a1 -> (* ------------ *) R_nonelim (PSuc a0) (PSuc a1) - with R_elim {n} : PTm n -> PTm n -> Prop := + with R_elim : PTm -> PTm -> Prop := | NAbsCong a0 a1 : R_nonelim a0 a1 -> R_elim (PAbs a0) (PAbs a1) @@ -1181,8 +1169,6 @@ Module NeEPar. R_nonelim A0 A1 -> R_nonelim B0 B1 -> R_elim (PBind p A0 B0) (PBind p A1 B1) - | NBotCong : - R_elim PBot PBot | NNatCong : R_elim PNat PNat | NIndCong P0 P1 a0 a1 b0 b1 c0 c1 : @@ -1204,11 +1190,11 @@ Module NeEPar. Combined Scheme epar_mutual from epar_elim_ind, epar_nonelim_ind. - Lemma R_elim_nf n : - (forall (a b : PTm n), R_elim a b -> nf b -> nf a) /\ - (forall (a b : PTm n), R_nonelim a b -> nf b -> nf a). + Lemma R_elim_nf : + (forall (a b : PTm), R_elim a b -> nf b -> nf a) /\ + (forall (a b : PTm), R_nonelim a b -> nf b -> nf a). Proof. - move : n. apply epar_mutual => n //=. + apply epar_mutual => //=. - move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1]. have hb0 : nf b0 by eauto. suff : ne a0 by qauto b:on. @@ -1237,22 +1223,22 @@ Module NeEPar. - hauto lqb:on inv:R_elim. Qed. - Lemma R_nonelim_nothf n (a b : PTm n) : + Lemma R_nonelim_nothf (a b : PTm) : R_nonelim a b -> ~~ ishf a -> R_elim a b. Proof. - move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_elim. + move => h. elim : a b /h=>//=; hauto lq:on ctrs:R_elim. Qed. - Lemma R_elim_nonelim n (a b : PTm n) : + Lemma R_elim_nonelim (a b : PTm) : R_elim a b -> R_nonelim a b. - move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim. + move => h. elim : a b /h=>//=; hauto lq:on ctrs:R_nonelim. Qed. - Lemma ToEPar : forall n, (forall (a b : PTm n), R_elim a b -> EPar.R a b) /\ - (forall (a b : PTm n), R_nonelim a b -> EPar.R a b). + Lemma ToEPar : (forall (a b : PTm), R_elim a b -> EPar.R a b) /\ + (forall (a b : PTm), R_nonelim a b -> EPar.R a b). Proof. apply epar_mutual; qauto l:on ctrs:EPar.R. Qed. @@ -1260,51 +1246,45 @@ Module NeEPar. End NeEPar. Module Type NoForbid. - Parameter P : forall n, PTm n -> Prop. - Arguments P {n}. + Parameter P : PTm -> Prop. - Axiom P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b. - Axiom P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. - (* Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). *) - (* Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). *) - (* Axiom P_ProjBind : forall n p p' (A : PTm n) B, ~ P (PProj p (PBind p' A B)). *) - (* Axiom P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b). *) - Axiom PApp_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b). - Axiom PProj_imp : forall n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a). - Axiom PInd_imp : forall n Q (a : PTm n) b c, + Axiom P_EPar : forall (a b : PTm), EPar.R a b -> P a -> P b. + Axiom P_RRed : forall (a b : PTm), RRed.R a b -> P a -> P b. + Axiom PApp_imp : forall a b, ishf a -> ~~ isabs a -> ~ P (PApp a b). + Axiom PProj_imp : forall p a, ishf a -> ~~ ispair a -> ~ P (PProj p a). + Axiom PInd_imp : forall Q (a : PTm) b c, ishf a -> ~~ iszero a -> ~~ issuc a -> ~ P (PInd Q a b c). - Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. - Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. - Axiom P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a. - Axiom P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B. - Axiom P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c. - - Axiom P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b. - Axiom P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a. - Axiom P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. + Axiom P_AppInv : forall (a b : PTm), P (PApp a b) -> P a /\ P b. + Axiom P_AbsInv : forall (a : PTm), P (PAbs a) -> P a. + Axiom P_SucInv : forall (a : PTm), P (PSuc a) -> P a. + Axiom P_BindInv : forall p (A : PTm) B, P (PBind p A B) -> P A /\ P B. + Axiom P_IndInv : forall Q (a : PTm) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c. + Axiom P_PairInv : forall (a b : PTm), P (PPair a b) -> P a /\ P b. + Axiom P_ProjInv : forall p (a : PTm), P (PProj p a) -> P a. + Axiom P_renaming : forall (ξ : nat -> nat) a , P (ren_PTm ξ a) <-> P a. End NoForbid. Module Type NoForbid_FactSig (M : NoForbid). - Axiom P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> M.P a -> M.P b. + Axiom P_EPars : forall (a b : PTm), rtc EPar.R a b -> M.P a -> M.P b. - Axiom P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> M.P a -> M.P b. + Axiom P_RReds : forall (a b : PTm), rtc RRed.R a b -> M.P a -> M.P b. End NoForbid_FactSig. Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M. Import M. - Lemma P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> P a -> P b. + Lemma P_EPars : forall (a b : PTm), rtc EPar.R a b -> P a -> P b. Proof. induction 1; eauto using P_EPar, rtc_l, rtc_refl. Qed. - Lemma P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> P a -> P b. + Lemma P_RReds : forall (a b : PTm), rtc RRed.R a b -> P a -> P b. Proof. induction 1; eauto using P_RRed, rtc_l, rtc_refl. Qed. @@ -1312,62 +1292,61 @@ End NoForbid_Fact. Module SN_NoForbid <: NoForbid. Definition P := @SN. - Arguments P {n}. - Lemma P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b. + Lemma P_EPar : forall (a b : PTm), EPar.R a b -> P a -> P b. Proof. sfirstorder use:epar_sn_preservation. Qed. - Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. + Lemma P_RRed : forall (a b : PTm), RRed.R a b -> P a -> P b. Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed. - Lemma PApp_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b). + Lemma PApp_imp : forall a b, ishf a -> ~~ isabs a -> ~ P (PApp a b). sfirstorder use:fp_red.PApp_imp. Qed. - Lemma PProj_imp : forall n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a). + Lemma PProj_imp : forall p a, ishf a -> ~~ ispair a -> ~ P (PProj p a). sfirstorder use:fp_red.PProj_imp. Qed. - Lemma PInd_imp : forall n Q (a : PTm n) b c, + Lemma PInd_imp : forall Q (a : PTm) b c, ishf a -> ~~ iszero a -> ~~ issuc a -> ~ P (PInd Q a b c). Proof. sfirstorder use: fp_red.PInd_imp. Qed. - Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. + Lemma P_AppInv : forall (a b : PTm), P (PApp a b) -> P a /\ P b. Proof. sfirstorder use:SN_AppInv. Qed. - Lemma P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b. - move => n a b. move E : (PPair a b) => u h. - move : a b E. elim : n u / h; sauto lq:on rew:off. Qed. + Lemma P_PairInv : forall (a b : PTm), P (PPair a b) -> P a /\ P b. + move => a b. move E : (PPair a b) => u h. + move : a b E. elim : u / h; sauto lq:on rew:off. Qed. - Lemma P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a. + Lemma P_ProjInv : forall p (a : PTm), P (PProj p a) -> P a. Proof. sfirstorder use:SN_ProjInv. Qed. - Lemma P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B. + Lemma P_BindInv : forall p (A : PTm) B, P (PBind p A B) -> P A /\ P B. Proof. - move => n p A B. + move => p A B. move E : (PBind p A B) => u hu. - move : p A B E. elim : n u /hu=>//=;sauto lq:on rew:off. + move : p A B E. elim : u /hu=>//=;sauto lq:on rew:off. Qed. - Lemma P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a. + Lemma P_SucInv : forall (a : PTm), P (PSuc a) -> P a. Proof. sauto lq:on. Qed. - Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. + Lemma P_AbsInv : forall (a : PTm), P (PAbs a) -> P a. Proof. - move => n a. move E : (PAbs a) => u h. + move => a. move E : (PAbs a) => u h. move : E. move : a. induction h; sauto lq:on rew:off. Qed. - Lemma P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. + Lemma P_renaming : forall (ξ : nat -> nat) a , P (ren_PTm ξ a) <-> P a. Proof. hauto lq:on use:sn_antirenaming, sn_renaming. Qed. - Lemma P_ProjBind : forall n p p' (A : PTm n) B, ~ P (PProj p (PBind p' A B)). + Lemma P_ProjBind : forall p p' (A : PTm) B, ~ P (PProj p (PBind p' A B)). Proof. sfirstorder use:PProjBind_imp. Qed. - Lemma P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b). + Lemma P_AppBind : forall p (A : PTm) B b, ~ P (PApp (PBind p A B) b). Proof. sfirstorder use:PAppBind_imp. Qed. - Lemma P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c. + Lemma P_IndInv : forall Q (a : PTm) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c. Proof. sfirstorder use:SN_IndInv. Qed. End SN_NoForbid. @@ -1378,13 +1357,13 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). Import M MFacts. #[local]Hint Resolve P_EPar P_RRed PApp_imp PProj_imp : forbid. - Lemma η_split n (a0 a1 : PTm n) : + Lemma η_split (a0 a1 : PTm) : EPar.R a0 a1 -> P a0 -> exists b, rtc RRed.R a0 b /\ NeEPar.R_nonelim b a1. Proof. - move => h. elim : n a0 a1 /h . - - move => n a0 a1 ha ih /[dup] hP. + move => h. elim : a0 a1 /h . + - move => a0 a1 ha ih /[dup] hP. move /P_AbsInv /P_AppInv => [/P_renaming ha0 _]. have {ih} := ih ha0. move => [b [ih0 ih1]]. @@ -1404,7 +1383,13 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). by eauto using RReds.renaming. apply rtc_refl. apply : RRed.AbsCong => /=. - apply RRed.AppAbs'. by asimpl. + apply RRed.AppAbs'. asimpl. + set y := subst_PTm _ _. + suff : ren_PTm id p = y. by asimpl. + subst y. + substify. + apply ext_PTm. + case => //=. (* violates SN *) + move /P_AbsInv in hP. have {}hP : P (PApp (ren_PTm shift b) (VarPTm var_zero)) @@ -1414,7 +1399,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). have ? : ishf (ren_PTm shift b) by scongruence use:ishf_ren. exfalso. sfirstorder use:PApp_imp. - - move => n a0 a1 h ih /[dup] hP. + - move => a0 a1 h ih /[dup] hP. move /P_PairInv => [/P_ProjInv + _]. move : ih => /[apply]. move => [b [ih0 ih1]]. @@ -1439,7 +1424,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). move : P_RReds hP. repeat move/[apply] => /=. sfirstorder use:PProj_imp. - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.AbsCong, P_AbsInv. - - move => n a0 a1 b0 b1 ha iha hb ihb. + - move => a0 a1 b0 b1 ha iha hb ihb. move => /[dup] hP /P_AppInv [hP0 hP1]. have {iha} [a2 [iha0 iha1]] := iha hP0. have {ihb} [b2 [ihb0 ihb1]] := ihb hP1. @@ -1462,7 +1447,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). have : P (PApp a2 b0) by sfirstorder use:RReds.AppCong, @rtc_refl, P_RReds. sfirstorder use:PApp_imp. - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.PairCong, P_PairInv. - - move => n p a0 a1 ha ih /[dup] hP /P_ProjInv. + - move => p a0 a1 ha ih /[dup] hP /P_ProjInv. move : ih => /[apply]. move => [a2 [iha0 iha1]]. case /orP : (orNb (ishf a2)) => [h|]. exists (PProj p a2). @@ -1487,8 +1472,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). - hauto l:on. - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv. - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv. - - hauto l:on ctrs:NeEPar.R_nonelim. - - move => n P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc /[dup] hInd /P_IndInv. + - move => P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc /[dup] hInd /P_IndInv. move => []. move : ihP => /[apply]. move => [P01][ihP0]ihP1. move => []. move : iha => /[apply]. @@ -1514,32 +1498,32 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.SucCong, P_SucInv. Qed. - Lemma eta_postponement n a b c : - @P n a -> + Lemma eta_postponement a b c : + P a -> EPar.R a b -> RRed.R b c -> exists d, rtc RRed.R a d /\ EPar.R d c. Proof. move => + h. move : c. - elim : n a b /h => //=. - - move => n a0 a1 ha iha c /[dup] hP /P_AbsInv /P_AppInv [/P_renaming hP' _] hc. + elim : a b /h => //=. + - move => a0 a1 ha iha c /[dup] hP /P_AbsInv /P_AppInv [/P_renaming hP' _] hc. move : iha (hP') (hc); repeat move/[apply]. move => [d [h0 h1]]. exists (PAbs (PApp (ren_PTm shift d) (VarPTm var_zero))). split. hauto lq:on rew:off ctrs:rtc use:RReds.AbsCong, RReds.AppCong, RReds.renaming. hauto lq:on ctrs:EPar.R. - - move => n a0 a1 ha iha c /P_PairInv [/P_ProjInv + _]. + - move => a0 a1 ha iha c /P_PairInv [/P_ProjInv + _]. move /iha => /[apply]. move => [d [h0 h1]]. exists (PPair (PProj PL d) (PProj PR d)). hauto lq:on ctrs:EPar.R use:RReds.PairCong, RReds.ProjCong. - - move => n a0 a1 ha iha c /P_AbsInv /[swap]. + - move => a0 a1 ha iha c /P_AbsInv /[swap]. elim /RRed.inv => //=_. move => a2 a3 + [? ?]. subst. move : iha; repeat move/[apply]. hauto lq:on use:RReds.AbsCong ctrs:EPar.R. - - move => n a0 a1 b0 b1 ha iha hb ihb c hP. + - move => a0 a1 b0 b1 ha iha hb ihb c hP. elim /RRed.inv => //= _. + move => a2 b2 [*]. subst. have [hP' hP''] : P a0 /\ P b0 by sfirstorder use:P_AppInv. @@ -1558,7 +1542,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). apply RRed.AppCong0. apply RRed.AbsCong. simpl. apply RRed.AppAbs. asimpl. apply rtc_once. - apply RRed.AppAbs. + apply RRed.AppAbs'. by asimpl. * exfalso. move : hP h0. clear => hP h0. have : rtc RRed.R (PApp a0 b0) (PApp (PPair (PProj PL a1) (PProj PR a1)) b0) @@ -1569,7 +1553,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). split. apply : rtc_r; last by apply RRed.AppAbs. hauto lq:on ctrs:rtc use:RReds.AppCong. - hauto l:on inv:option use:EPar.morphing,NeEPar.ToEPar. + hauto l:on inv:nat use:EPar.morphing,NeEPar.ToEPar. + move => a2 a3 b2 ha2 [*]. subst. move : iha (ha2) {ihb} => /[apply]. have : P a0 by sfirstorder use:P_AppInv. @@ -1582,10 +1566,10 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). have : P b0 by sfirstorder use:P_AppInv. move : ihb hb2; repeat move /[apply]. hauto lq:on rew:off ctrs:EPar.R, rtc use:RReds.AppCong. - - move => n a0 a1 b0 b1 ha iha hb ihb c /P_PairInv [hP hP']. + - move => a0 a1 b0 b1 ha iha hb ihb c /P_PairInv [hP hP']. elim /RRed.inv => //=_; hauto lq:on rew:off ctrs:EPar.R, rtc use:RReds.PairCong. - - move => n p a0 a1 ha iha c /[dup] hP /P_ProjInv hP'. + - move => p a0 a1 ha iha c /[dup] hP /P_ProjInv hP'. elim / RRed.inv => //= _. + move => p0 a2 b0 [*]. subst. move : η_split hP' ha; repeat move/[apply]. @@ -1619,8 +1603,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). - hauto lq:on inv:RRed.R ctrs:rtc. - sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive. - hauto lq:on inv:RRed.R ctrs:rtc. - - hauto q:on ctrs:rtc inv:RRed.R. - - move => n P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc u. + - move => P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc u. move => /[dup] hInd. move /P_IndInv. move => [pP0][pa0][pb0]pc0. @@ -1650,7 +1633,12 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). apply : rtc_r. apply RReds.IndCong; eauto; eauto using rtc_refl. apply RRed.IndSuc. - apply EPar.morphing;eauto. hauto lq:on ctrs:EPar.R inv:option use:NeEPar.ToEPar. + apply EPar.morphing;eauto. + case => [|]. + hauto lq:on rew:off ctrs:EPar.R use:NeEPar.ToEPar. + case => [|i]. + hauto lq:on rew:off ctrs:EPar.R use:NeEPar.ToEPar. + asimpl. apply EPar.VarTm. + move => P2 P3 a2 b2 c hP0 [*]. subst. move : ihP hP0 pP0. repeat move/[apply]. move => [P2][h0]h1. @@ -1672,7 +1660,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). exists (PInd P0 a0 b0 c2). sfirstorder use:RReds.IndCong, @rtc_refl, EPar.IndCong. - hauto lq:on inv:RRed.R ctrs:rtc, EPar.R. - - move => n a0 a1 ha iha u /P_SucInv ha0. + - move => a0 a1 ha iha u /P_SucInv ha0. elim /RRed.inv => //= _ a2 a3 h [*]. subst. move : iha (ha0) (h); repeat move/[apply]. move => [a2 [ih0 ih1]]. @@ -1681,8 +1669,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). by apply EPar.SucCong. Qed. - Lemma η_postponement_star n a b c : - @P n a -> + Lemma η_postponement_star a b c : + P a -> EPar.R a b -> rtc RRed.R b c -> exists d, rtc RRed.R a d /\ EPar.R d c. @@ -1698,8 +1686,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). sfirstorder use:@relations.rtc_transitive. Qed. - Lemma η_postponement_star' n a b c : - @P n a -> + Lemma η_postponement_star' a b c : + P a -> EPar.R a b -> rtc RRed.R b c -> exists d, rtc RRed.R a d /\ NeEPar.R_nonelim d c. @@ -1716,7 +1704,7 @@ End UniqueNF. Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN. Module ERed. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Eta ***********************) | AppEta a : @@ -1765,9 +1753,9 @@ Module ERed. R a0 a1 -> R (PSuc a0) (PSuc a1). - Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. - Lemma ToEPar n (a b : PTm n) : + Lemma ToEPar (a b : PTm) : ERed.R a b -> EPar.R a b. Proof. induction 1; hauto lq:on use:EPar.refl ctrs:EPar.R. @@ -1777,38 +1765,34 @@ Module ERed. let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in intro $x; lazy_match! Constr.type (Control.hyp x) with - | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:ERed.R)) + | nat -> _ => (ltac1:(case;hauto q:on depth:2 ctrs:ERed.R)) | _ => solve_anti_ren () end. Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). - (* Definition down n m (ξ : fin n -> fin m) (a : fin (S n)) : fin m. *) - (* destruct a. *) - (* exact (ξ f). *) - - Lemma AppEta' n a u : - u = (@PApp (S n) (ren_PTm shift a) (VarPTm var_zero)) -> + Lemma AppEta' a u : + u = (PApp (ren_PTm shift a) (VarPTm var_zero)) -> R (PAbs u) a. Proof. move => ->. apply AppEta. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. - elim : n a b /h. + move => h. move : ξ. + elim : a b /h. - move => n a m ξ /=. + move => a ξ /=. apply AppEta'; eauto. by asimpl. all : qauto ctrs:R. Qed. (* Characterization of variable freeness conditions *) - Definition tm_i_free {n} a (i : fin n) := exists m (ξ ξ0 : fin n -> fin m), ξ i <> ξ0 i /\ ren_PTm ξ a = ren_PTm ξ0 a. + Definition tm_i_free a (i : fin n) := exists m (ξ ξ0 : fin n -> fin m), ξ i <> ξ0 i /\ ren_PTm a = ren_PTm0 a. Lemma subst_differ_one_ren_up n m i (ξ0 ξ1 : fin n -> fin m) : (forall j, i <> j -> ξ0 j = ξ1 j) -> - (forall j, shift i <> j -> upRen_PTm_PTm ξ0 j = upRen_PTm_PTm ξ1 j). + (forall j, shift i <> j -> upRen_PTm_PTm0 j = upRen_PTm_PTm1 j). Proof. move => hξ. destruct j. asimpl. @@ -1820,7 +1804,7 @@ Module ERed. Lemma tm_free_ren_any n a i : tm_i_free a i -> forall m (ξ0 ξ1 : fin n -> fin m), (forall j, i <> j -> ξ0 j = ξ1 j) -> - ren_PTm ξ0 a = ren_PTm ξ1 a. + ren_PTm0 a = ren_PTm1 a. Proof. rewrite /tm_i_free. move => [+ [+ [+ +]]]. @@ -1841,7 +1825,7 @@ Module ERed. move /subst_differ_one_ren_up in hξ. move /(_ (shift i)) in iha. move : iha hξ. repeat move/[apply]. - move /(_ _ (upRen_PTm_PTm ρ0) (upRen_PTm_PTm ρ1)). + move /(_ _ (upRen_PTm_PTm0) (upRen_PTm_PTm1)). apply. hauto l:on. - hauto lq:on rew:off. - hauto lq:on rew:off. @@ -1851,12 +1835,12 @@ Module ERed. - admit. Admitted. - Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + Lemma antirenaming n m (a : PTm) (b : PTm) (ξ : fin n -> fin m) : (forall i j, ξ i = ξ j -> i = j) -> - R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. + R (ren_PTm a) b -> exists b0, R a b0 /\ ren_PTm b0 = b. Proof. move => hξ. - move E : (ren_PTm ξ a) => u hu. + move E : (ren_PTm a) => u hu. move : n ξ a hξ E. elim : m u b / hu; try solve_anti_ren. - move => n a m ξ []//=. @@ -1870,7 +1854,7 @@ Module ERed. move => [p ?]. subst. move : h. asimpl. replace (ren_PTm (funcomp shift ξ) p) with - (ren_PTm shift (ren_PTm ξ p)); last by asimpl. + (ren_PTm shift (ren_PTm p)); last by asimpl. move /ren_injective. move /(_ ltac:(hauto l:on)). move => ?. subst. @@ -1886,14 +1870,14 @@ Module ERed. sauto lq:on use:up_injective. - move => n p A B0 B1 hB ihB m ξ + hξ. case => //= p' A2 B2 [*]. subst. - have : (forall i j, (upRen_PTm_PTm ξ) i = (upRen_PTm_PTm ξ) j -> i = j) by sauto. + have : (forall i j, (upRen_PTm_PTm) i = (upRen_PTm_PTm) j -> i = j) by sauto. move => {}/ihB => ihB. spec_refl. sauto lq:on. Admitted. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + R a b -> R (subst_PTm a) (subst_PTm b). Proof. move => h. move : m ρ. elim : n a b /h => n. move => a m ρ /=. @@ -1901,7 +1885,7 @@ Module ERed. all : hauto lq:on ctrs:R. Qed. - Lemma nf_preservation n (a b : PTm n) : + Lemma nf_preservation n (a b : PTm) : ERed.R a b -> (nf a -> nf b) /\ (ne a -> ne b). Proof. move => h. @@ -1925,36 +1909,36 @@ Module EReds. rtc ERed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm) : 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) : + Lemma PairCong n (a0 a1 b0 b1 : PTm) : 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) : + Lemma ProjCong n p (a0 a1 : PTm) : rtc ERed.R a0 a1 -> rtc ERed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : + Lemma BindCong n p (A0 A1 : PTm) B0 B1 : rtc ERed.R A0 A1 -> rtc ERed.R B0 B1 -> rtc ERed.R (PBind p A0 B0) (PBind p A1 B1). Proof. solve_s. Qed. - Lemma SucCong n (a0 a1 : PTm n) : + Lemma SucCong n (a0 a1 : PTm) : rtc ERed.R a0 a1 -> rtc ERed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. - Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma IndCong n P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : rtc ERed.R P0 P1 -> rtc ERed.R a0 a1 -> rtc ERed.R b0 b1 -> @@ -1962,11 +1946,11 @@ Module EReds. rtc ERed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1). Proof. solve_s. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : - rtc ERed.R a b -> rtc ERed.R (ren_PTm ξ a) (ren_PTm ξ b). + Lemma renaming n m (a b : PTm) (ξ : fin n -> fin m) : + rtc ERed.R a b -> rtc ERed.R (ren_PTm a) (ren_PTm b). Proof. induction 1; hauto l:on use:ERed.renaming ctrs:rtc. Qed. - Lemma FromEPar n (a b : PTm n) : + Lemma FromEPar n (a b : PTm) : EPar.R a b -> rtc ERed.R a b. Proof. @@ -1981,18 +1965,18 @@ Module EReds. apply ERed.PairEta. Qed. - Lemma FromEPars n (a b : PTm n) : + Lemma FromEPars n (a b : PTm) : rtc EPar.R a b -> rtc ERed.R a b. Proof. induction 1; hauto l:on use:FromEPar, @relations.rtc_transitive. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - rtc ERed.R a b -> rtc ERed.R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + rtc ERed.R a b -> rtc ERed.R (subst_PTm a) (subst_PTm b). Proof. induction 1; hauto lq:on ctrs:rtc use:ERed.substing. Qed. - Lemma app_inv n (a0 b0 C : PTm n) : + Lemma app_inv n (a0 b0 C : PTm) : rtc ERed.R (PApp a0 b0) C -> exists a1 b1, C = PApp a1 b1 /\ rtc ERed.R a0 a1 /\ @@ -2006,7 +1990,7 @@ Module EReds. hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R. Qed. - Lemma proj_inv n p (a C : PTm n) : + Lemma proj_inv n p (a C : PTm) : rtc ERed.R (PProj p a) C -> exists c, C = PProj p c /\ rtc ERed.R a c. Proof. @@ -2016,7 +2000,7 @@ Module EReds. scrush ctrs:rtc,ERed.R inv:ERed.R. Qed. - Lemma bind_inv n p (A : PTm n) B C : + Lemma bind_inv n p (A : PTm) B C : rtc ERed.R (PBind p A B) C -> exists A0 B0, C = PBind p A0 B0 /\ rtc ERed.R A A0 /\ rtc ERed.R B B0. Proof. @@ -2027,7 +2011,7 @@ Module EReds. hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc. Qed. - Lemma suc_inv n (a : PTm n) C : + Lemma suc_inv n (a : PTm) C : rtc ERed.R (PSuc a) C -> exists b, rtc ERed.R a b /\ C = PSuc b. Proof. @@ -2038,14 +2022,14 @@ Module EReds. - hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc. Qed. - Lemma zero_inv n (C : PTm n) : + Lemma zero_inv n (C : PTm) : rtc ERed.R PZero C -> C = PZero. move E : PZero => u hu. move : E. elim : u C /hu=>//=. - hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc. Qed. - Lemma ind_inv n P (a : PTm n) b c C : + Lemma ind_inv n P (a : PTm) b c C : rtc ERed.R (PInd P a b c) C -> exists P0 a0 b0 c0, rtc ERed.R P P0 /\ rtc ERed.R a a0 /\ rtc ERed.R b b0 /\ rtc ERed.R c c0 /\ @@ -2063,37 +2047,37 @@ End EReds. #[export]Hint Constructors ERed.R RRed.R EPar.R : red. Module EJoin. - Definition R {n} (a b : PTm n) := exists c, rtc ERed.R a c /\ rtc ERed.R b c. + Definition R (a b : PTm) := exists c, rtc ERed.R a c /\ rtc ERed.R b c. - Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) : + Lemma hne_app_inj n (a0 b0 a1 b1 : PTm) : R (PApp a0 b0) (PApp a1 b1) -> R a0 a1 /\ R b0 b1. Proof. hauto lq:on use:EReds.app_inv. Qed. - Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) : + Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm) : R (PProj p0 a0) (PProj p1 a1) -> p0 = p1 /\ R a0 a1. Proof. hauto lq:on rew:off use:EReds.proj_inv. Qed. - Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 : + Lemma bind_inj n p0 p1 (A0 A1 : PTm) B0 B1 : R (PBind p0 A0 B0) (PBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1. Proof. hauto lq:on rew:off use:EReds.bind_inv. Qed. - Lemma suc_inj n (A0 A1 : PTm n) : + Lemma suc_inj n (A0 A1 : PTm) : R (PSuc A0) (PSuc A1) -> R A0 A1. Proof. hauto lq:on rew:off use:EReds.suc_inv. Qed. - Lemma ind_inj n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma ind_inj n P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) -> R P0 P1 /\ R a0 a1 /\ R b0 b1 /\ R c0 c1. Proof. hauto q:on use:EReds.ind_inv. Qed. @@ -2101,7 +2085,7 @@ Module EJoin. End EJoin. Module RERed. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Beta ***********************) | AppAbs a b : R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) @@ -2162,79 +2146,79 @@ Module RERed. R a0 a1 -> R (PSuc a0) (PSuc a1). - Lemma ToBetaEta n (a b : PTm n) : + Lemma ToBetaEta n (a b : PTm) : R a b -> ERed.R a b \/ RRed.R a b. Proof. induction 1; hauto lq:on db:red. Qed. - Lemma FromBeta n (a b : PTm n) : + Lemma FromBeta n (a b : PTm) : RRed.R a b -> RERed.R a b. Proof. induction 1; qauto l:on ctrs:R. Qed. - Lemma FromEta n (a b : PTm n) : + Lemma FromEta n (a b : PTm) : ERed.R a b -> RERed.R a b. Proof. induction 1; qauto l:on ctrs:R. Qed. - Lemma ToBetaEtaPar n (a b : PTm n) : + Lemma ToBetaEtaPar n (a b : PTm) : R a b -> EPar.R a b \/ RRed.R a b. Proof. hauto q:on use:ERed.ToEPar, ToBetaEta. Qed. - Lemma sn_preservation n (a b : PTm n) : + Lemma sn_preservation n (a b : PTm) : R a b -> SN a -> SN b. Proof. hauto q:on use:ToBetaEtaPar, epar_sn_preservation, red_sn_preservation, RPar.FromRRed. Qed. - Lemma bind_preservation n (a b : PTm n) : + Lemma bind_preservation n (a b : PTm) : R a b -> isbind a -> isbind b. Proof. hauto q:on inv:R. Qed. - Lemma univ_preservation n (a b : PTm n) : + Lemma univ_preservation n (a b : PTm) : R a b -> isuniv a -> isuniv b. Proof. hauto q:on inv:R. Qed. - Lemma nat_preservation n (a b : PTm n) : + Lemma nat_preservation n (a b : PTm) : R a b -> isnat a -> isnat b. Proof. hauto q:on inv:R. Qed. - Lemma sne_preservation n (a b : PTm n) : + Lemma sne_preservation n (a b : PTm) : R a b -> SNe a -> SNe b. Proof. hauto q:on use:ToBetaEtaPar, RPar.FromRRed use:red_sn_preservation, epar_sn_preservation. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - RERed.R a b -> RERed.R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + RERed.R a b -> RERed.R (subst_PTm a) (subst_PTm b). Proof. hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing. Qed. - Lemma hne_preservation n (a b : PTm n) : + Lemma hne_preservation n (a b : PTm) : RERed.R a b -> ishne a -> ishne b. Proof. induction 1; sfirstorder. Qed. End RERed. Module REReds. - Lemma hne_preservation n (a b : PTm n) : + Lemma hne_preservation n (a b : PTm) : rtc RERed.R a b -> ishne a -> ishne b. Proof. induction 1; eauto using RERed.hne_preservation, rtc_refl, rtc. Qed. - Lemma sn_preservation n (a b : PTm n) : + Lemma sn_preservation n (a b : PTm) : rtc RERed.R a b -> SN a -> SN b. Proof. induction 1; eauto using RERed.sn_preservation. Qed. - Lemma FromRReds n (a b : PTm n) : + Lemma FromRReds n (a b : PTm) : rtc RRed.R a b -> rtc RERed.R a b. Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromBeta. Qed. - Lemma FromEReds n (a b : PTm n) : + Lemma FromEReds n (a b : PTm) : rtc ERed.R a b -> rtc RERed.R a b. Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromEta. Qed. @@ -2251,29 +2235,29 @@ Module REReds. rtc RERed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm) : rtc RERed.R a0 a1 -> rtc RERed.R b0 b1 -> rtc RERed.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm) : rtc RERed.R a0 a1 -> rtc RERed.R b0 b1 -> rtc RERed.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : PTm n) : + Lemma ProjCong n p (a0 a1 : PTm) : rtc RERed.R a0 a1 -> rtc RERed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma SucCong n (a0 a1 : PTm n) : + Lemma SucCong n (a0 a1 : PTm) : rtc RERed.R a0 a1 -> rtc RERed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. - Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma IndCong n P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : rtc RERed.R P0 P1 -> rtc RERed.R a0 a1 -> rtc RERed.R b0 b1 -> @@ -2281,25 +2265,25 @@ Module REReds. rtc RERed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1). Proof. solve_s. Qed. - Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : + Lemma BindCong n p (A0 A1 : PTm) B0 B1 : rtc RERed.R A0 A1 -> rtc RERed.R B0 B1 -> rtc RERed.R (PBind p A0 B0) (PBind p A1 B1). Proof. solve_s. Qed. - Lemma bind_preservation n (a b : PTm n) : + Lemma bind_preservation n (a b : PTm) : rtc RERed.R a b -> isbind a -> isbind b. Proof. induction 1; qauto l:on ctrs:rtc use:RERed.bind_preservation. Qed. - Lemma univ_preservation n (a b : PTm n) : + Lemma univ_preservation n (a b : PTm) : rtc RERed.R a b -> isuniv a -> isuniv b. Proof. induction 1; qauto l:on ctrs:rtc use:RERed.univ_preservation. Qed. - Lemma nat_preservation n (a b : PTm n) : + Lemma nat_preservation n (a b : PTm) : rtc RERed.R a b -> isnat a -> isnat b. Proof. induction 1; qauto l:on ctrs:rtc use:RERed.nat_preservation. Qed. - Lemma sne_preservation n (a b : PTm n) : + Lemma sne_preservation n (a b : PTm) : rtc RERed.R a b -> SNe a -> SNe b. Proof. induction 1; qauto l:on ctrs:rtc use:RERed.sne_preservation. Qed. @@ -2329,7 +2313,7 @@ Module REReds. move : i E. elim : u C /hu; hauto lq:on rew:off inv:RERed.R. Qed. - Lemma hne_app_inv n (a0 b0 C : PTm n) : + Lemma hne_app_inv n (a0 b0 C : PTm) : rtc RERed.R (PApp a0 b0) C -> ishne a0 -> exists a1 b1, C = PApp a1 b1 /\ @@ -2344,7 +2328,7 @@ Module REReds. hauto lq:on rew:off ctrs:rtc, RERed.R use:RERed.hne_preservation inv:RERed.R. Qed. - Lemma hne_proj_inv n p (a C : PTm n) : + Lemma hne_proj_inv n p (a C : PTm) : rtc RERed.R (PProj p a) C -> ishne a -> exists c, C = PProj p c /\ rtc RERed.R a c. @@ -2355,7 +2339,7 @@ Module REReds. scrush ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R. Qed. - Lemma hne_ind_inv n P a b c (C : PTm n) : + Lemma hne_ind_inv n P a b c (C : PTm) : rtc RERed.R (PInd P a b c) C -> ishne a -> exists P0 a0 b0 c0, C = PInd P0 a0 b0 c0 /\ rtc RERed.R P P0 /\ @@ -2369,47 +2353,47 @@ Module REReds. scrush ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + rtc RERed.R a b -> rtc RERed.R (subst_PTm a) (subst_PTm b). Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.substing. Qed. - Lemma cong_up n m (ρ0 ρ1 : fin n -> PTm m) : + Lemma cong_up n m (ρ0 ρ1 : fin n -> PTm) : (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) -> - (forall i, rtc RERed.R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). + (forall i, rtc RERed.R (up_PTm_PTm0 i) (up_PTm_PTm1 i)). Proof. move => h i. destruct i as [i|]. simpl. rewrite /funcomp. substify. by apply substing. apply rtc_refl. Qed. - Lemma cong_up2 n m (ρ0 ρ1 : fin n -> PTm m) : + Lemma cong_up2 n m (ρ0 ρ1 : fin n -> PTm) : (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) -> - (forall i, rtc RERed.R (up_PTm_PTm (up_PTm_PTm ρ0) i) (up_PTm_PTm (up_PTm_PTm ρ1) i)). + (forall i, rtc RERed.R (up_PTm_PTm (up_PTm_PTm0) i) (up_PTm_PTm (up_PTm_PTm1) i)). Proof. hauto l:on use:cong_up. Qed. - Lemma cong n m (a : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + Lemma cong n m (a : PTm) (ρ0 ρ1 : fin n -> PTm) : (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) -> - rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 a). + rtc RERed.R (subst_PTm0 a) (subst_PTm1 a). Proof. move : m ρ0 ρ1. elim : n / a => /=; eauto 20 using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl, IndCong, SucCong, cong_up2. Qed. - Lemma cong' n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + Lemma cong' n m (a b : PTm) (ρ0 ρ1 : fin n -> PTm) : rtc RERed.R a b -> (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) -> - rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + rtc RERed.R (subst_PTm0 a) (subst_PTm1 b). Proof. move => h0 h1. - have : rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 a) by eauto using cong. + have : rtc RERed.R (subst_PTm0 a) (subst_PTm1 a) by eauto using cong. move => ?. apply : relations.rtc_transitive; eauto. hauto l:on use:substing. Qed. - Lemma ToEReds n (a b : PTm n) : + Lemma ToEReds n (a b : PTm) : nf a -> rtc RERed.R a b -> rtc ERed.R a b. Proof. @@ -2417,14 +2401,14 @@ Module REReds. induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation. Qed. - Lemma zero_inv n (C : PTm n) : + Lemma zero_inv n (C : PTm) : rtc RERed.R PZero C -> C = PZero. move E : PZero => u hu. move : E. elim : u C /hu=>//=. - hauto lq:on rew:off ctrs:rtc, RERed.R inv:RERed.R, rtc. Qed. - Lemma suc_inv n (a : PTm n) C : + Lemma suc_inv n (a : PTm) C : rtc RERed.R (PSuc a) C -> exists b, rtc RERed.R a b /\ C = PSuc b. Proof. @@ -2447,7 +2431,7 @@ Module REReds. End REReds. Module LoRed. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (****************** Beta ***********************) | AppAbs a b : R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) @@ -2515,7 +2499,7 @@ Module LoRed. R a0 a1 -> R (PSuc a0) (PSuc a1). - Lemma hf_preservation n (a b : PTm n) : + Lemma hf_preservation n (a b : PTm) : LoRed.R a b -> ishf a -> ishf b. @@ -2523,12 +2507,12 @@ Module LoRed. move => h. elim : n a b /h=>//=. Qed. - Lemma ToRRed n (a b : PTm n) : + Lemma ToRRed n (a b : PTm) : LoRed.R a b -> RRed.R a b. Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed. - Lemma AppAbs' n a (b : PTm n) u : + Lemma AppAbs' n a (b : PTm) u : u = (subst_PTm (scons b VarPTm) a) -> R (PApp (PAbs a) b) u. Proof. move => ->. apply AppAbs. Qed. @@ -2538,8 +2522,8 @@ Module LoRed. R (@PInd n P (PSuc a) b c) u. Proof. move => ->. apply IndSuc. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : - R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Lemma renaming n m (a b : PTm) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm a) (ren_PTm b). Proof. move => h. move : m ξ. elim : n a b /h. @@ -2553,7 +2537,7 @@ Module LoRed. End LoRed. Module LoReds. - Lemma hf_preservation n (a b : PTm n) : + Lemma hf_preservation n (a b : PTm) : rtc LoRed.R a b -> ishf a -> ishf b. @@ -2561,7 +2545,7 @@ Module LoReds. induction 1; eauto using LoRed.hf_preservation. Qed. - Lemma hf_ne_imp n (a b : PTm n) : + Lemma hf_ne_imp n (a b : PTm) : rtc LoRed.R a b -> ne b -> ~~ ishf a. @@ -2582,34 +2566,34 @@ Module LoReds. rtc LoRed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm) : rtc LoRed.R a0 a1 -> rtc LoRed.R b0 b1 -> ne a1 -> rtc LoRed.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm) : rtc LoRed.R a0 a1 -> rtc LoRed.R b0 b1 -> nf a1 -> rtc LoRed.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : PTm n) : + Lemma ProjCong n p (a0 a1 : PTm) : rtc LoRed.R a0 a1 -> ne a1 -> rtc LoRed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : + Lemma BindCong n p (A0 A1 : PTm) B0 B1 : rtc LoRed.R A0 A1 -> rtc LoRed.R B0 B1 -> nf A1 -> rtc LoRed.R (PBind p A0 B0) (PBind p A1 B1). Proof. solve_s. Qed. - Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma IndCong n P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : rtc LoRed.R a0 a1 -> rtc LoRed.R P0 P1 -> rtc LoRed.R b0 b1 -> @@ -2620,7 +2604,7 @@ Module LoReds. rtc LoRed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1). Proof. solve_s. Qed. - Lemma SucCong n (a0 a1 : PTm n) : + Lemma SucCong n (a0 a1 : PTm) : rtc LoRed.R a0 a1 -> rtc LoRed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. @@ -2628,9 +2612,9 @@ Module LoReds. Local Ltac triv := simpl in *; itauto. Lemma FromSN_mutual : forall n, - (forall (a : PTm n) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\ - (forall (a : PTm n) (_ : SN a), exists v, rtc LoRed.R a v /\ nf v) /\ - (forall (a b : PTm n) (_ : TRedSN a b), LoRed.R a b). + (forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\ + (forall (a : PTm) (_ : SN a), exists v, rtc LoRed.R a v /\ nf v) /\ + (forall (a b : PTm) (_ : TRedSN a b), LoRed.R a b). Proof. apply sn_mutual. - hauto lq:on ctrs:rtc. @@ -2666,49 +2650,49 @@ Module LoReds. Lemma FromSN : forall n a, @SN n a -> exists v, rtc LoRed.R a v /\ nf v. Proof. firstorder using FromSN_mutual. Qed. - Lemma ToRReds : forall n (a b : PTm n), rtc LoRed.R a b -> rtc RRed.R a b. + Lemma ToRReds : forall n (a b : PTm), rtc LoRed.R a b -> rtc RRed.R a b. Proof. induction 1; hauto lq:on ctrs:rtc use:LoRed.ToRRed. Qed. End LoReds. -Fixpoint size_PTm {n} (a : PTm n) := +Fixpoint size_PTm (a : PTm) := match a with | VarPTm _ => 1 - | PAbs a => 3 + size_PTm a - | PApp a b => 1 + Nat.add (size_PTm a) (size_PTm b) - | PProj p a => 1 + size_PTm a - | PPair a b => 3 + Nat.add (size_PTm a) (size_PTm b) + | PAbs a => 3 + size_PTm + | PApp a b => 1 + Nat.add (size_PTm) (size_PTm) + | PProj p a => 1 + size_PTm + | PPair a b => 3 + Nat.add (size_PTm) (size_PTm) | PUniv _ => 3 - | PBind p A B => 3 + Nat.add (size_PTm A) (size_PTm B) - | PInd P a b c => 3 + size_PTm P + size_PTm a + size_PTm b + size_PTm c + | PBind p A B => 3 + Nat.add (size_PTm) (size_PTm) + | PInd P a b c => 3 + size_PTm + size_PTm + size_PTm + size_PTm | PNat => 3 - | PSuc a => 3 + size_PTm a + | PSuc a => 3 + size_PTm | PZero => 3 | PBot => 1 end. -Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm ξ a) = size_PTm a. +Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm a) = size_PTm. Proof. move : m ξ. elim : n / a => //=; scongruence. Qed. #[export]Hint Rewrite size_PTm_ren : sizetm. -Lemma ered_size {n} (a b : PTm n) : +Lemma ered_size (a b : PTm) : ERed.R a b -> - size_PTm b < size_PTm a. + size_PTm < size_PTm. Proof. move => h. elim : n a b /h; hauto l:on rew:db:sizetm. Qed. -Lemma ered_sn n (a : PTm n) : sn ERed.R a. +Lemma ered_sn n (a : PTm) : sn ERed.R a. Proof. hauto lq:on rew:off use:size_PTm_ren, ered_size, well_founded_lt_compat unfold:well_founded. Qed. -Lemma ered_local_confluence n (a b c : PTm n) : +Lemma ered_local_confluence n (a b c : PTm) : ERed.R a b -> ERed.R a c -> exists d, rtc ERed.R b d /\ rtc ERed.R c d. @@ -2814,7 +2798,7 @@ Proof. - qauto l:on inv:ERed.R ctrs:rtc use:EReds.SucCong. Qed. -Lemma ered_confluence n (a b c : PTm n) : +Lemma ered_confluence n (a b c : PTm) : rtc ERed.R a b -> rtc ERed.R a c -> exists d, rtc ERed.R b d /\ rtc ERed.R c d. @@ -2822,18 +2806,18 @@ Proof. sfirstorder use:relations.locally_confluent_confluent, ered_sn, ered_local_confluence. Qed. -Lemma red_confluence n (a b c : PTm n) : +Lemma red_confluence n (a b c : PTm) : rtc RRed.R a b -> rtc RRed.R a c -> exists d, rtc RRed.R b d /\ rtc RRed.R c d. - suff : rtc RPar.R a b -> rtc RPar.R a c -> exists d : PTm n, rtc RPar.R b d /\ rtc RPar.R c d + suff : rtc RPar.R a b -> rtc RPar.R a c -> exists d : PTm, rtc RPar.R b d /\ rtc RPar.R c d by hauto lq:on use:RReds.RParIff. apply relations.diamond_confluent. rewrite /relations.diamond. eauto using RPar.diamond. Qed. -Lemma red_uniquenf n (a b c : PTm n) : +Lemma red_uniquenf n (a b c : PTm) : rtc RRed.R a b -> rtc RRed.R a c -> nf b -> @@ -2848,20 +2832,20 @@ Proof. Qed. Module NeEPars. - Lemma R_nonelim_nf n (a b : PTm n) : + Lemma R_nonelim_nf n (a b : PTm) : rtc NeEPar.R_nonelim a b -> nf b -> nf a. Proof. induction 1; sfirstorder use:NeEPar.R_elim_nf. Qed. - Lemma ToEReds : forall n, (forall (a b : PTm n), rtc NeEPar.R_nonelim a b -> rtc ERed.R a b). + Lemma ToEReds : forall n, (forall (a b : PTm), rtc NeEPar.R_nonelim a b -> rtc ERed.R a b). Proof. induction 1; hauto l:on use:NeEPar.ToEPar, EReds.FromEPar, @relations.rtc_transitive. Qed. End NeEPars. -Lemma rered_standardization n (a c : PTm n) : +Lemma rered_standardization n (a c : PTm) : SN a -> rtc RERed.R a c -> exists b, rtc RRed.R a b /\ rtc NeEPar.R_nonelim b c. @@ -2878,7 +2862,7 @@ Proof. - hauto lq:on ctrs:rtc use:red_sn_preservation, RPar.FromRRed. Qed. -Lemma rered_confluence n (a b c : PTm n) : +Lemma rered_confluence n (a b c : PTm) : SN a -> rtc RERed.R a b -> rtc RERed.R a c -> @@ -2912,14 +2896,14 @@ Qed. (* Beta joinability *) Module BJoin. - Definition R {n} (a b : PTm n) := exists c, rtc RRed.R a c /\ rtc RRed.R b c. - Lemma refl n (a : PTm n) : R a a. + Definition R (a b : PTm) := exists c, rtc RRed.R a c /\ rtc RRed.R b c. + Lemma refl n (a : PTm) : R a a. Proof. sfirstorder use:@rtc_refl unfold:R. Qed. - Lemma symmetric n (a b : PTm n) : R a b -> R b a. + Lemma symmetric n (a b : PTm) : R a b -> R b a. Proof. sfirstorder unfold:R. Qed. - Lemma transitive n (a b c : PTm n) : R a b -> R b c -> R a c. + Lemma transitive n (a b c : PTm) : R a b -> R b c -> R a c. Proof. rewrite /R. move => [ab [ha +]] [bc [+ hc]]. @@ -2933,7 +2917,7 @@ Module BJoin. (* R (PAbs a) (PAbs b). *) (* Proof. hauto lq:on use:RReds.AbsCong unfold:R. Qed. *) - (* Lemma AppCong n (a0 a1 b0 b1 : PTm n) : *) + (* Lemma AppCong n (a0 a1 b0 b1 : PTm) : *) (* R a0 a1 -> *) (* R b0 b1 -> *) (* R (PApp a0 b0) (PApp a1 b1). *) @@ -2941,21 +2925,21 @@ Module BJoin. End BJoin. Module DJoin. - Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c. + Definition R (a b : PTm) := exists c, rtc RERed.R a c /\ rtc RERed.R b c. - Lemma refl n (a : PTm n) : R a a. + Lemma refl n (a : PTm) : R a a. Proof. sfirstorder use:@rtc_refl unfold:R. Qed. - Lemma FromEJoin n (a b : PTm n) : EJoin.R a b -> DJoin.R a b. + Lemma FromEJoin n (a b : PTm) : EJoin.R a b -> DJoin.R a b. Proof. hauto q:on use:REReds.FromEReds. Qed. - Lemma ToEJoin n (a b : PTm n) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b. + Lemma ToEJoin n (a b : PTm) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b. Proof. hauto q:on use:REReds.ToEReds. Qed. - Lemma symmetric n (a b : PTm n) : R a b -> R b a. + Lemma symmetric n (a b : PTm) : R a b -> R b a. Proof. sfirstorder unfold:R. Qed. - Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c. + Lemma transitive n (a b c : PTm) : SN b -> R a b -> R b c -> R a c. Proof. rewrite /R. move => + [ab [ha +]] [bc [+ hc]]. @@ -2969,30 +2953,30 @@ Module DJoin. R (PAbs a) (PAbs b). Proof. hauto lq:on use:REReds.AbsCong unfold:R. Qed. - Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm) : R a0 a1 -> R b0 b1 -> R (PApp a0 b0) (PApp a1 b1). Proof. hauto lq:on use:REReds.AppCong unfold:R. Qed. - Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm) : R a0 a1 -> R b0 b1 -> R (PPair a0 b0) (PPair a1 b1). Proof. hauto q:on use:REReds.PairCong. Qed. - Lemma ProjCong n p (a0 a1 : PTm n) : + Lemma ProjCong n p (a0 a1 : PTm) : R a0 a1 -> R (PProj p a0) (PProj p a1). Proof. hauto q:on use:REReds.ProjCong. Qed. - Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : + Lemma BindCong n p (A0 A1 : PTm) B0 B1 : R A0 A1 -> R B0 B1 -> R (PBind p A0 B0) (PBind p A1 B1). Proof. hauto q:on use:REReds.BindCong. Qed. - Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 : + Lemma IndCong n P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 : R P0 P1 -> R a0 a1 -> R b0 b1 -> @@ -3000,12 +2984,12 @@ Module DJoin. R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1). Proof. hauto q:on use:REReds.IndCong. Qed. - Lemma SucCong n (a0 a1 : PTm n) : + Lemma SucCong n (a0 a1 : PTm) : R a0 a1 -> R (PSuc a0) (PSuc a1). Proof. qauto l:on use:REReds.SucCong. Qed. - Lemma FromRedSNs n (a b : PTm n) : + Lemma FromRedSNs n (a b : PTm) : rtc TRedSN a b -> R a b. Proof. @@ -3013,7 +2997,7 @@ Module DJoin. sfirstorder use:@rtc_refl unfold:R. Qed. - Lemma sne_nat_noconf n (a b : PTm n) : + Lemma sne_nat_noconf n (a b : PTm) : R a b -> SNe a -> isnat b -> False. Proof. move => [c [? ?]] *. @@ -3021,7 +3005,7 @@ Module DJoin. qauto l:on inv:SNe. Qed. - Lemma sne_bind_noconf n (a b : PTm n) : + Lemma sne_bind_noconf n (a b : PTm) : R a b -> SNe a -> isbind b -> False. Proof. move => [c [? ?]] *. @@ -3029,14 +3013,14 @@ Module DJoin. qauto l:on inv:SNe. Qed. - Lemma sne_univ_noconf n (a b : PTm n) : + Lemma sne_univ_noconf n (a b : PTm) : R a b -> SNe a -> isuniv b -> False. Proof. hauto q:on use:REReds.sne_preservation, REReds.univ_preservation inv:SNe. Qed. - Lemma bind_univ_noconf n (a b : PTm n) : + Lemma bind_univ_noconf n (a b : PTm) : R a b -> isbind a -> isuniv b -> False. Proof. move => [c [h0 h1]] h2 h3. @@ -3046,7 +3030,7 @@ Module DJoin. case : c => //=; itauto. Qed. - Lemma hne_univ_noconf n (a b : PTm n) : + Lemma hne_univ_noconf n (a b : PTm) : R a b -> ishne a -> isuniv b -> False. Proof. move => [c [h0 h1]] h2 h3. @@ -3057,7 +3041,7 @@ Module DJoin. case : c => //=. Qed. - Lemma hne_bind_noconf n (a b : PTm n) : + Lemma hne_bind_noconf n (a b : PTm) : R a b -> ishne a -> isbind b -> False. Proof. move => [c [h0 h1]] h2 h3. @@ -3068,7 +3052,7 @@ Module DJoin. case : c => //=. Qed. - Lemma hne_nat_noconf n (a b : PTm n) : + Lemma hne_nat_noconf n (a b : PTm) : R a b -> ishne a -> isnat b -> False. Proof. move => [c [h0 h1]] h2 h3. @@ -3076,7 +3060,7 @@ Module DJoin. clear. case : c => //=; itauto. Qed. - Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 : + Lemma bind_inj n p0 p1 (A0 A1 : PTm) B0 B1 : DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) -> p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1. Proof. @@ -3094,14 +3078,14 @@ Module DJoin. sauto lq:on rew:off use:REReds.univ_inv. Qed. - Lemma suc_inj n (A0 A1 : PTm n) : + Lemma suc_inj n (A0 A1 : PTm) : R (PSuc A0) (PSuc A1) -> R A0 A1. Proof. hauto lq:on rew:off use:REReds.suc_inv. Qed. - Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) : + Lemma hne_app_inj n (a0 b0 a1 b1 : PTm) : R (PApp a0 b0) (PApp a1 b1) -> ishne a0 -> ishne a1 -> @@ -3110,7 +3094,7 @@ Module DJoin. hauto lq:on use:REReds.hne_app_inv. Qed. - Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) : + Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm) : R (PProj p0 a0) (PProj p1 a1) -> ishne a0 -> ishne a1 -> @@ -3119,45 +3103,45 @@ Module DJoin. sauto lq:on use:REReds.hne_proj_inv. Qed. - Lemma FromRRed0 n (a b : PTm n) : + Lemma FromRRed0 n (a b : PTm) : RRed.R a b -> R a b. Proof. hauto lq:on ctrs:rtc use:RERed.FromBeta unfold:R. Qed. - Lemma FromRRed1 n (a b : PTm n) : + Lemma FromRRed1 n (a b : PTm) : RRed.R b a -> R a b. Proof. hauto lq:on ctrs:rtc use:RERed.FromBeta unfold:R. Qed. - Lemma FromRReds n (a b : PTm n) : + Lemma FromRReds n (a b : PTm) : rtc RRed.R b a -> R a b. Proof. hauto lq:on ctrs:rtc use:REReds.FromRReds unfold:R. Qed. - Lemma FromBJoin n (a b : PTm n) : + Lemma FromBJoin n (a b : PTm) : BJoin.R a b -> R a b. Proof. hauto lq:on ctrs:rtc use:REReds.FromRReds unfold:R. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + R a b -> R (subst_PTm a) (subst_PTm b). Proof. hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing. Qed. - Lemma renaming n m (a b : PTm n) (ρ : fin n -> fin m) : - R a b -> R (ren_PTm ρ a) (ren_PTm ρ b). + Lemma renaming n m (a b : PTm) (ρ : fin n -> fin m) : + R a b -> R (ren_PTm a) (ren_PTm b). Proof. substify. apply substing. Qed. - Lemma weakening n (a b : PTm n) : + Lemma weakening n (a b : PTm) : R a b -> R (ren_PTm shift a) (ren_PTm shift b). Proof. apply renaming. Qed. - Lemma cong n m (a : PTm (S n)) c d (ρ : fin n -> PTm m) : + Lemma cong n m (a : PTm (S n)) c d (ρ : fin n -> PTm) : R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) a). Proof. rewrite /R. move => [cd [h0 h1]]. @@ -3165,7 +3149,7 @@ Module DJoin. hauto q:on ctrs:rtc inv:option use:REReds.cong. Qed. - Lemma cong' n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) : + Lemma cong' n m (a b : PTm (S n)) c d (ρ : fin n -> PTm) : R a b -> R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b). Proof. @@ -3174,7 +3158,7 @@ Module DJoin. hauto q:on ctrs:rtc inv:option use:REReds.cong'. Qed. - Lemma pair_inj n (a0 a1 b0 b1 : PTm n) : + Lemma pair_inj n (a0 a1 b0 b1 : PTm) : SN (PPair a0 b0) -> SN (PPair a1 b1) -> R (PPair a0 b0) (PPair a1 b1) -> @@ -3201,7 +3185,7 @@ Module DJoin. split; eauto using transitive. Qed. - Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm n) : + Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm) : nf a0 -> nf b0 -> nf a1 -> nf b1 -> EJoin.R (PPair a0 b0) (PPair a1 b1) -> EJoin.R a0 a1 /\ EJoin.R b0 b1. @@ -3250,7 +3234,7 @@ Module DJoin. hauto l:on use:ToEJoin. Qed. - Lemma standardization n (a b : PTm n) : + Lemma standardization n (a b : PTm) : SN a -> SN b -> R a b -> exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb. Proof. @@ -3270,7 +3254,7 @@ Module DJoin. hauto q:on use:NeEPars.ToEReds unfold:EJoin.R. Qed. - Lemma standardization_lo n (a b : PTm n) : + Lemma standardization_lo n (a b : PTm) : SN a -> SN b -> R a b -> exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb. Proof. @@ -3288,7 +3272,7 @@ End DJoin. Module Sub1. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := | Refl a : R a a | Univ i j : @@ -3303,21 +3287,21 @@ Module Sub1. R B0 B1 -> R (PBind PSig A0 B0) (PBind PSig A1 B1). - Lemma transitive0 n (A B C : PTm n) : + Lemma transitive0 n (A B C : PTm) : R A B -> (R B C -> R A C) /\ (R C A -> R C B). Proof. move => h. move : C. elim : n A B /h; hauto lq:on ctrs:R inv:R solve+:lia. Qed. - Lemma transitive n (A B C : PTm n) : + Lemma transitive n (A B C : PTm) : R A B -> R B C -> R A C. Proof. hauto q:on use:transitive0. Qed. - Lemma refl n (A : PTm n) : R A A. + Lemma refl n (A : PTm) : R A A. Proof. sfirstorder. Qed. - Lemma commutativity0 n (A B C : PTm n) : + Lemma commutativity0 n (A B C : PTm) : R A B -> (RERed.R A C -> exists D, RERed.R B D /\ R C D) /\ @@ -3328,7 +3312,7 @@ Module Sub1. elim : n A B / h; hauto lq:on ctrs:RERed.R, R inv:RERed.R. Qed. - Lemma commutativity_Ls n (A B C : PTm n) : + Lemma commutativity_Ls n (A B C : PTm) : R A B -> rtc RERed.R A C -> exists D, rtc RERed.R B D /\ R C D. @@ -3336,7 +3320,7 @@ Module Sub1. move => + h. move : B. induction h; sauto lq:on use:commutativity0. Qed. - Lemma commutativity_Rs n (A B C : PTm n) : + Lemma commutativity_Rs n (A B C : PTm) : R A B -> rtc RERed.R B C -> exists D, rtc RERed.R A D /\ R D C. @@ -3345,46 +3329,46 @@ Module Sub1. Qed. Lemma sn_preservation : forall n, - (forall (a : PTm n) (s : SNe a), forall b, R a b \/ R b a -> a = b) /\ - (forall (a : PTm n) (s : SN a), forall b, R a b \/ R b a -> SN b) /\ - (forall (a b : PTm n) (_ : TRedSN a b), forall c, R a c \/ R c a -> a = c). + (forall (a : PTm) (s : SNe a), forall b, R a b \/ R b a -> a = b) /\ + (forall (a : PTm) (s : SN a), forall b, R a b \/ R b a -> SN b) /\ + (forall (a b : PTm) (_ : TRedSN a b), forall c, R a c \/ R c a -> a = c). Proof. apply sn_mutual; hauto lq:on inv:R ctrs:SN. Qed. - Lemma bind_preservation n (a b : PTm n) : + Lemma bind_preservation n (a b : PTm) : R a b -> isbind a = isbind b. Proof. hauto q:on inv:R. Qed. - Lemma univ_preservation n (a b : PTm n) : + Lemma univ_preservation n (a b : PTm) : R a b -> isuniv a = isuniv b. Proof. hauto q:on inv:R. Qed. - Lemma sne_preservation n (a b : PTm n) : + Lemma sne_preservation n (a b : PTm) : R a b -> SNe a <-> SNe b. Proof. hfcrush use:sn_preservation. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : - R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Lemma renaming n m (a b : PTm) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm a) (ren_PTm b). Proof. move => h. move : m ξ. elim : n a b /h; 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). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + R a b -> R (subst_PTm a) (subst_PTm b). Proof. move => h. move : m ρ. elim : n a b /h; hauto lq:on ctrs:R. Qed. - Lemma hne_refl n (a b : PTm n) : + Lemma hne_refl n (a b : PTm) : ishne a \/ ishne b -> R a b -> a = b. Proof. hauto q:on inv:R. Qed. End Sub1. Module ESub. - Definition R {n} (a b : PTm n) := exists c0 c1, rtc ERed.R a c0 /\ rtc ERed.R b c1 /\ Sub1.R c0 c1. + Definition R (a b : PTm) := exists c0 c1, rtc ERed.R a c0 /\ rtc ERed.R b c1 /\ Sub1.R c0 c1. - Lemma pi_inj n (A0 A1 : PTm n) B0 B1 : + Lemma pi_inj n (A0 A1 : PTm) B0 B1 : R (PBind PPi A0 B0) (PBind PPi A1 B1) -> R A1 A0 /\ R B0 B1. Proof. @@ -3394,7 +3378,7 @@ Module ESub. sauto lq:on rew:off inv:Sub1.R. Qed. - Lemma sig_inj n (A0 A1 : PTm n) B0 B1 : + Lemma sig_inj n (A0 A1 : PTm) B0 B1 : R (PBind PSig A0 B0) (PBind PSig A1 B1) -> R A0 A1 /\ R B0 B1. Proof. @@ -3404,7 +3388,7 @@ Module ESub. sauto lq:on rew:off inv:Sub1.R. Qed. - Lemma suc_inj n (a b : PTm n) : + Lemma suc_inj n (a b : PTm) : R (PSuc a) (PSuc b) -> R a b. Proof. @@ -3414,12 +3398,12 @@ Module ESub. End ESub. Module Sub. - Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d. + Definition R (a b : PTm) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d. - Lemma refl n (a : PTm n) : R a a. + Lemma refl n (a : PTm) : R a a. Proof. sfirstorder use:@rtc_refl unfold:R. Qed. - Lemma ToJoin n (a b : PTm n) : + Lemma ToJoin n (a b : PTm) : ishne a \/ ishne b -> R a b -> DJoin.R a b. @@ -3429,7 +3413,7 @@ Module Sub. hauto lq:on rew:off use:Sub1.hne_refl. Qed. - Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c. + Lemma transitive n (a b c : PTm) : SN b -> R a b -> R b c -> R a c. Proof. rewrite /R. move => h [a0][b0][ha][hb]ha0b0 [b1][c0][hb'][hc]hb1c0. @@ -3441,10 +3425,10 @@ Module Sub. exists a',c'; hauto l:on use:Sub1.transitive, @relations.rtc_transitive. Qed. - Lemma FromJoin n (a b : PTm n) : DJoin.R a b -> R a b. + Lemma FromJoin n (a b : PTm) : DJoin.R a b -> R a b. Proof. sfirstorder. Qed. - Lemma PiCong n (A0 A1 : PTm n) B0 B1 : + Lemma PiCong n (A0 A1 : PTm) B0 B1 : R A1 A0 -> R B0 B1 -> R (PBind PPi A0 B0) (PBind PPi A1 B1). @@ -3456,7 +3440,7 @@ Module Sub. repeat split; eauto using REReds.BindCong, Sub1.PiCong. Qed. - Lemma SigCong n (A0 A1 : PTm n) B0 B1 : + Lemma SigCong n (A0 A1 : PTm) B0 B1 : R A0 A1 -> R B0 B1 -> R (PBind PSig A0 B0) (PBind PSig A1 B1). @@ -3473,7 +3457,7 @@ Module Sub. @R n (PUniv i) (PUniv j). Proof. hauto lq:on ctrs:Sub1.R, rtc. Qed. - Lemma sne_nat_noconf n (a b : PTm n) : + Lemma sne_nat_noconf n (a b : PTm) : R a b -> SNe a -> isnat b -> False. Proof. move => [c [d [h0 [h1 h2]]]] *. @@ -3481,7 +3465,7 @@ Module Sub. move : h2. clear. hauto q:on inv:Sub1.R, SNe. Qed. - Lemma nat_sne_noconf n (a b : PTm n) : + Lemma nat_sne_noconf n (a b : PTm) : R a b -> isnat a -> SNe b -> False. Proof. move => [c [d [h0 [h1 h2]]]] *. @@ -3489,7 +3473,7 @@ Module Sub. move : h2. clear. hauto q:on inv:Sub1.R, SNe. Qed. - Lemma sne_bind_noconf n (a b : PTm n) : + Lemma sne_bind_noconf n (a b : PTm) : R a b -> SNe a -> isbind b -> False. Proof. rewrite /R. @@ -3499,7 +3483,7 @@ Module Sub. qauto l:on inv:SNe. Qed. - Lemma hne_bind_noconf n (a b : PTm n) : + Lemma hne_bind_noconf n (a b : PTm) : R a b -> ishne a -> isbind b -> False. Proof. rewrite /R. @@ -3510,7 +3494,7 @@ Module Sub. clear. case : d => //=. Qed. - Lemma bind_sne_noconf n (a b : PTm n) : + Lemma bind_sne_noconf n (a b : PTm) : R a b -> SNe b -> isbind a -> False. Proof. rewrite /R. @@ -3520,14 +3504,14 @@ Module Sub. qauto l:on inv:SNe. Qed. - Lemma sne_univ_noconf n (a b : PTm n) : + Lemma sne_univ_noconf n (a b : PTm) : R a b -> SNe a -> isuniv b -> False. Proof. hauto l:on use:REReds.sne_preservation, REReds.univ_preservation, Sub1.sne_preservation, Sub1.univ_preservation inv:SNe. Qed. - Lemma univ_sne_noconf n (a b : PTm n) : + Lemma univ_sne_noconf n (a b : PTm) : R a b -> SNe b -> isuniv a -> False. Proof. move => [c[d] [? []]] *. @@ -3537,7 +3521,7 @@ Module Sub. clear. case : c => //=. inversion 2. Qed. - Lemma univ_nat_noconf n (a b : PTm n) : + Lemma univ_nat_noconf n (a b : PTm) : R a b -> isuniv b -> isnat a -> False. Proof. move => [c[d] [? []]] h0 h1 h2 h3. @@ -3547,7 +3531,7 @@ Module Sub. clear. case : d => //=. Qed. - Lemma nat_univ_noconf n (a b : PTm n) : + Lemma nat_univ_noconf n (a b : PTm) : R a b -> isnat b -> isuniv a -> False. Proof. move => [c[d] [? []]] h0 h1 h2 h3. @@ -3557,7 +3541,7 @@ Module Sub. clear. case : d => //=. Qed. - Lemma bind_nat_noconf n (a b : PTm n) : + Lemma bind_nat_noconf n (a b : PTm) : R a b -> isbind b -> isnat a -> False. Proof. move => [c[d] [? []]] h0 h1 h2 h3. @@ -3568,7 +3552,7 @@ Module Sub. case : d h1 => //=. Qed. - Lemma nat_bind_noconf n (a b : PTm n) : + Lemma nat_bind_noconf n (a b : PTm) : R a b -> isnat b -> isbind a -> False. Proof. move => [c[d] [? []]] h0 h1 h2 h3. @@ -3579,7 +3563,7 @@ Module Sub. case : d h1 => //=. Qed. - Lemma bind_univ_noconf n (a b : PTm n) : + Lemma bind_univ_noconf n (a b : PTm) : R a b -> isbind a -> isuniv b -> False. Proof. move => [c[d] [h0 [h1 h1']]] h2 h3. @@ -3590,7 +3574,7 @@ Module Sub. case : c => //=; itauto. Qed. - Lemma univ_bind_noconf n (a b : PTm n) : + Lemma univ_bind_noconf n (a b : PTm) : R a b -> isbind b -> isuniv a -> False. Proof. move => [c[d] [h0 [h1 h1']]] h2 h3. @@ -3601,7 +3585,7 @@ Module Sub. case : c => //=; itauto. Qed. - Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 : + Lemma bind_inj n p0 p1 (A0 A1 : PTm) B0 B1 : R (PBind p0 A0 B0) (PBind p1 A1 B1) -> p0 = p1 /\ (if p0 is PPi then R A1 A0 else R A0 A1) /\ R B0 B1. Proof. @@ -3618,7 +3602,7 @@ Module Sub. sauto lq:on rew:off use:REReds.univ_inv. Qed. - Lemma suc_inj n (A0 A1 : PTm n) : + Lemma suc_inj n (A0 A1 : PTm) : R (PSuc A0) (PSuc A1) -> R A0 A1. Proof. @@ -3626,7 +3610,7 @@ Module Sub. Qed. - Lemma cong n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) : + Lemma cong n m (a b : PTm (S n)) c d (ρ : fin n -> PTm) : R a b -> DJoin.R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b). Proof. rewrite /R. @@ -3639,18 +3623,18 @@ Module Sub. eauto using Sub1.substing. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : - R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). + Lemma substing n m (a b : PTm) (ρ : fin n -> PTm) : + R a b -> R (subst_PTm a) (subst_PTm b). Proof. rewrite /R. move => [a0][b0][h0][h1]h2. hauto ctrs:rtc use:REReds.cong', Sub1.substing. Qed. - Lemma ToESub n (a b : PTm n) : nf a -> nf b -> R a b -> ESub.R a b. + Lemma ToESub n (a b : PTm) : nf a -> nf b -> R a b -> ESub.R a b. Proof. hauto q:on use:REReds.ToEReds. Qed. - Lemma standardization n (a b : PTm n) : + Lemma standardization n (a b : PTm) : SN a -> SN b -> R a b -> exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb. Proof. @@ -3668,7 +3652,7 @@ Module Sub. hauto lq:on. Qed. - Lemma standardization_lo n (a b : PTm n) : + Lemma standardization_lo n (a b : PTm) : SN a -> SN b -> R a b -> exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb. Proof.