From 9ab338c9e1f3c9b1b783651e5a41bb9b1fe5412a Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 8 Jan 2025 15:31:40 -0500 Subject: [PATCH] Add wn --- theories/fp_red.v | 131 +++++++++++++++++++++++++++++++++++++++++++++- theories/logrel.v | 99 ++++++++++++++++++----------------- 2 files changed, 180 insertions(+), 50 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 0c207be..26a2309 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -373,6 +373,73 @@ Module RPar. move => h0 h1. apply morphing => //=. qauto l:on ctrs:R inv:option. Qed. + + Lemma antirenaming n m (a : Tm n) (b : Tm m) (ξ : fin n -> fin m) : + R (ren_Tm ξ a) b -> exists b0, R a b0 /\ ren_Tm ξ b0 = b. + Proof. + move E : (ren_Tm ξ a) => u h. + move : n ξ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=. + move => c c0 [+ ?]. subst. + case : c => //=. + move => c [?]. subst. + spec_refl. + move : iha => [c1][ih0]?. subst. + move : ihb => [c2][ih1]?. subst. + eexists. split. + apply AppAbs; eauto. + by asimpl. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//=. + move => []//= t t0 t1 [*]. subst. + spec_refl. + move : iha => [? [*]]. + move : ihb => [? [*]]. + move : ihc => [? [*]]. + eexists. split. + apply AppPair; hauto. subst. + by asimpl. + - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst. + spec_refl. move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjAbs; eauto. by asimpl. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ξ []//= p0 []//= t t0[*]. + subst. spec_refl. + move : iha => [b0 [? ?]]. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by eauto using ProjPair. + hauto q:on. + - move => n i m ξ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ξ []//= t [*]. subst. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + by asimpl. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0[*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply PairCong; eauto. + by asimpl. + - move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. by apply ProjCong; eauto. + by asimpl. + - move => n p A0 A1 B0 B1 ha iha hB ihB m ξ []//= ? t t0 [*]. subst. + spec_refl. + move : iha => [b0 [? ?]]. + move : ihB => [c0 [? ?]]. subst. + eexists. split. by apply BindCong; eauto. + by asimpl. + - move => n n0 ξ []//=. hauto l:on. + - move => n i n0 ξ []//=. hauto l:on. + Qed. End RPar. Module ERed. @@ -1863,8 +1930,70 @@ Proof. hauto l:on. Qed. - Lemma join_substing n m (a b : Tm n) (ρ : fin n -> Tm m) : join a b -> join (subst_Tm ρ a) (subst_Tm ρ b). Proof. hauto lq:on unfold:join use:Pars.substing. Qed. + + +Fixpoint ne {n} (a : Tm n) := + match a with + | VarTm i => true + | TBind _ A B => nf A && nf B + | Bot => false + | App a b => ne a && nf b + | Abs a => false + | Univ _ => false + | Proj _ a => ne a + | Pair _ _ => false + end +with nf {n} (a : Tm n) := + match a with + | VarTm i => true + | TBind _ A B => nf A && nf B + | Bot => true + | App a b => ne a && nf b + | Abs a => nf a + | Univ _ => true + | Proj _ a => ne a + | Pair a b => nf a && nf b +end. + +Lemma ne_nf n a : @ne n a -> nf a. +Proof. elim : a => //=. Qed. + +Definition wn {n} (a : Tm n) := exists b, rtc RPar.R a b /\ nf b. +Definition wne {n} (a : Tm n) := exists b, rtc RPar.R a b /\ ne b. + +(* Weakly neutral implies weakly normal *) +Lemma wne_wn n a : @wne n a -> wn a. +Proof. sfirstorder use:ne_nf. Qed. + +(* Normal implies weakly normal *) +Lemma nf_wn n v : @nf n v -> wn v. +Proof. sfirstorder ctrs:rtc. Qed. + +Lemma nf_refl n (a b : Tm n) (h : RPar.R a b) : (nf a -> b = a) /\ (ne a -> b = a). +Proof. + elim : a b /h => //=; solve [hauto b:on]. +Qed. + +Lemma ne_nf_ren n m (a : Tm n) (ξ : fin n -> fin m) : + (ne a <-> ne (ren_Tm ξ a)) /\ (nf a <-> nf (ren_Tm ξ a)). +Proof. + move : m ξ. elim : n / a => //=; solve [hauto b:on]. +Qed. + +Lemma wne_app n (a b : Tm n) : + wne a -> wn b -> wne (App a b). +Proof. + move => [a0 [? ?]] [b0 [? ?]]. + exists (App a0 b0). hauto b:on use:RPars.AppCong. +Qed. + +Lemma wn_abs (a : tm) (h : wn a) : wn (tAbs a). +Proof. + move : h => [v [? ?]]. + exists (tAbs v). + eauto using S_Abs. +Qed. diff --git a/theories/logrel.v b/theories/logrel.v index 9a8f1af..9a5c1ac 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -6,18 +6,19 @@ Require Import ssreflect ssrbool. Require Import Logic.PropExtensionality (propositional_extensionality). From stdpp Require Import relations (rtc(..), rtc_subrel). Import Psatz. -Definition ProdSpace (PA : Tm 0 -> Prop) - (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) b : Prop := + +Definition ProdSpace {n} (PA : Tm n -> Prop) + (PF : Tm n -> (Tm n -> Prop) -> Prop) b : Prop := forall a PB, PA a -> PF a PB -> PB (App b a). -Definition SumSpace (PA : Tm 0 -> Prop) - (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) t : Prop := +Definition SumSpace {n} (PA : Tm n -> Prop) + (PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop := exists a b, rtc RPar.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b). -Definition BindSpace p := if p is TPi then ProdSpace else SumSpace. +Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace. Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70). -Inductive InterpExt i (I : nat -> Tm 0 -> Prop) : Tm 0 -> (Tm 0 -> Prop) -> Prop := +Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop := | InterpExt_Bind p A B PA PF : ⟦ A ⟧ i ;; I ↘ PA -> (forall a, PA a -> exists PB, PF a PB) -> @@ -34,7 +35,7 @@ Inductive InterpExt i (I : nat -> Tm 0 -> Prop) : Tm 0 -> (Tm 0 -> Prop) -> Prop ⟦ A ⟧ i ;; I ↘ PA where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S). -Lemma InterpExt_Univ' i I j (PF : Tm 0 -> Prop) : +Lemma InterpExt_Univ' n i I j (PF : Tm n -> Prop) : PF = I j -> j < i -> ⟦ Univ j ⟧ i ;; I ↘ PF. @@ -42,16 +43,16 @@ Proof. hauto lq:on ctrs:InterpExt. Qed. Infix " (Tm 0 -> Prop) -> Prop by wf i lt := - InterpUnivN i := @InterpExt i +Equations InterpUnivN n (i : nat) : Tm n -> (Tm n -> Prop) -> Prop by wf i lt := + InterpUnivN n i := @InterpExt n i (fun j A => match j exists PA, InterpUnivN j A PA + | left _ => exists PA, InterpUnivN n j A PA | right _ => False end). -Arguments InterpUnivN . +Arguments InterpUnivN {n}. -Lemma InterpExt_lt_impl i I I' A (PA : Tm 0 -> Prop) : +Lemma InterpExt_lt_impl n i I I' A (PA : Tm n -> Prop) : (forall j, j < i -> I j = I' j) -> ⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I' ↘ PA. @@ -63,7 +64,7 @@ Proof. - hauto lq:on ctrs:InterpExt. Qed. -Lemma InterpExt_lt_eq i I I' A (PA : Tm 0 -> Prop) : +Lemma InterpExt_lt_eq n i I I' A (PA : Tm n -> Prop) : (forall j, j < i -> I j = I' j) -> ⟦ A ⟧ i ;; I ↘ PA = ⟦ A ⟧ i ;; I' ↘ PA. @@ -75,8 +76,8 @@ Qed. Notation "⟦ A ⟧ i ↘ S" := (InterpUnivN i A S) (at level 70). -Lemma InterpUnivN_nolt i : - InterpUnivN i = InterpExt i (fun j (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA). +Lemma InterpUnivN_nolt n i : + @InterpUnivN n i = @InterpExt n i (fun j (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA). Proof. simp InterpUnivN. extensionality A. extensionality PA. @@ -92,9 +93,9 @@ Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n): RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed. -Lemma InterpExt_Bind_inv p i I (A : Tm 0) B P +Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P (h : ⟦ TBind p A B ⟧ i ;; I ↘ P) : - exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop), + exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop), ⟦ A ⟧ i ;; I ↘ PA /\ (forall a, PA a -> exists PB, PF a PB) /\ (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\ @@ -109,8 +110,8 @@ Proof. hauto lq:on ctrs:InterpExt use:RPar_substone. Qed. -Lemma InterpExt_Univ_inv i I j P - (h : ⟦ Univ j ⟧ i ;; I ↘ P) : +Lemma InterpExt_Univ_inv n i I j P + (h : ⟦ Univ j : Tm n ⟧ i ;; I ↘ P) : P = I j /\ j < i. Proof. move : h. @@ -120,7 +121,7 @@ Proof. - hauto lq:on rew:off inv:RPar.R. Qed. -Lemma InterpExt_Bind_nopf p i I (A : Tm 0) B PA : +Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA : ⟦ A ⟧ i ;; I ↘ PA -> (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) -> ⟦ TBind p A B ⟧ i ;; I ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB)). @@ -128,7 +129,7 @@ Proof. move => h0 h1. apply InterpExt_Bind =>//. Qed. -Lemma InterpUnivN_Fun_nopf p i (A : Tm 0) B PA : +Lemma InterpUnivN_Fun_nopf n p i (A : Tm n) B PA : ⟦ A ⟧ i ↘ PA -> (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) -> ⟦ TBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB)). @@ -136,7 +137,7 @@ Proof. hauto l:on use:InterpExt_Bind_nopf rew:db:InterpUniv. Qed. -Lemma InterpExt_cumulative i j I (A : Tm 0) PA : +Lemma InterpExt_cumulative n i j I (A : Tm n) PA : i <= j -> ⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ j ;; I ↘ PA. @@ -146,14 +147,14 @@ Proof. hauto l:on ctrs:InterpExt solve+:(by lia). Qed. -Lemma InterpUnivN_cumulative i (A : Tm 0) PA : +Lemma InterpUnivN_cumulative n i (A : Tm n) PA : ⟦ A ⟧ i ↘ PA -> forall j, i <= j -> ⟦ A ⟧ j ↘ PA. Proof. hauto l:on rew:db:InterpUniv use:InterpExt_cumulative. Qed. -Lemma InterpExt_preservation i I (A : Tm 0) B P (h : InterpExt i I A P) : +Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) : RPar.R A B -> ⟦ B ⟧ i ;; I ↘ P. Proof. @@ -171,32 +172,32 @@ Proof. hauto lq:on ctrs:InterpExt. Qed. -Lemma InterpUnivN_preservation i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) : +Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : RPar.R A B -> ⟦ B ⟧ i ↘ P. Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed. -Lemma InterpExt_back_preservation_star i I (A : Tm 0) B P (h : ⟦ B ⟧ i ;; I ↘ P) : +Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) : rtc RPar.R A B -> ⟦ A ⟧ i ;; I ↘ P. Proof. induction 1; hauto l:on ctrs:InterpExt. Qed. -Lemma InterpExt_preservation_star i I (A : Tm 0) B P (h : ⟦ A ⟧ i ;; I ↘ P) : +Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) : rtc RPar.R A B -> ⟦ B ⟧ i ;; I ↘ P. Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed. -Lemma InterpUnivN_preservation_star i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) : +Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : rtc RPar.R A B -> ⟦ B ⟧ i ↘ P. Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed. -Lemma InterpUnivN_back_preservation_star i (A : Tm 0) B P (h : ⟦ B ⟧ i ↘ P) : +Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) : rtc RPar.R A B -> ⟦ A ⟧ i ↘ P. Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed. -Lemma InterpExtInv i I (A : Tm 0) PA : +Lemma InterpExtInv n i I (A : Tm n) PA : ⟦ A ⟧ i ;; I ↘ PA -> exists B, hfb B /\ rtc RPar.R A B /\ ⟦ B ⟧ i ;; I ↘ PA. Proof. @@ -210,17 +211,17 @@ Proof. - hauto lq:on ctrs:rtc. Qed. -Lemma RPars_Pars (A B : Tm 0) : +Lemma RPars_Pars (A B : Tm n) : rtc RPar.R A B -> rtc Par.R A B. Proof. hauto lq:on use:RPar_Par, rtc_subrel. Qed. -Lemma RPars_join (A B : Tm 0) : +Lemma RPars_join (A B : Tm n) : rtc RPar.R A B -> join A B. Proof. hauto lq:on ctrs:rtc use:RPars_Pars. Qed. -Lemma bindspace_iff p (PA : Tm 0 -> Prop) PF PF0 b : - (forall (a : Tm 0) (PB PB0 : Tm 0 -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) -> +Lemma bindspace_iff p (PA : Tm n -> Prop) PF PF0 b : + (forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) -> (forall a, PA a -> exists PB, PF a PB) -> (forall a, PA a -> exists PB0, PF0 a PB0) -> (BindSpace p PA PF b <-> BindSpace p PA PF0 b). @@ -241,7 +242,7 @@ Proof. hauto lq:on rew:off. Qed. -Lemma InterpExt_Join i I (A B : Tm 0) PA PB : +Lemma InterpExt_Join i I (A B : Tm n) PA PB : ⟦ A ⟧ i ;; I ↘ PA -> ⟦ B ⟧ i ;; I ↘ PB -> join A B -> @@ -281,7 +282,7 @@ Proof. exfalso. eauto using join_univ_pi_contra. + move => m _ [/RPars_join h0 + h1]. - have /join_univ_inj {h0 h1} ? : join (Univ j : Tm 0) (Univ m) by eauto using join_transitive. + have /join_univ_inj {h0 h1} ? : join (Univ j : Tm n) (Univ m) by eauto using join_transitive. subst. move /InterpExt_Univ_inv. firstorder. - move => A A0 PA h. @@ -289,16 +290,16 @@ Proof. eauto using join_transitive. Qed. -Lemma InterpUniv_Join i (A B : Tm 0) PA PB : +Lemma InterpUniv_Join i (A B : Tm n) PA PB : ⟦ A ⟧ i ↘ PA -> ⟦ B ⟧ i ↘ PB -> join A B -> PA = PB. Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed. -Lemma InterpUniv_Bind_inv p i (A : Tm 0) B P +Lemma InterpUniv_Bind_inv p i (A : Tm n) B P (h : ⟦ TBind p A B ⟧ i ↘ P) : - exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop), + exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop), ⟦ A ⟧ i ↘ PA /\ (forall a, PA a -> exists PB, PF a PB) /\ (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\ @@ -307,22 +308,22 @@ Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed. Lemma InterpUniv_Univ_inv i j P (h : ⟦ Univ j ⟧ i ↘ P) : - P = (fun (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i. + P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i. Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed. -Lemma InterpExt_Functional i I (A B : Tm 0) PA PB : +Lemma InterpExt_Functional i I (A B : Tm n) PA PB : ⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PB -> PA = PB. Proof. hauto use:InterpExt_Join, join_refl. Qed. -Lemma InterpUniv_Functional i (A : Tm 0) PA PB : +Lemma InterpUniv_Functional i (A : Tm n) PA PB : ⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PB -> PA = PB. Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed. -Lemma InterpUniv_Join' i j (A B : Tm 0) PA PB : +Lemma InterpUniv_Join' i j (A B : Tm n) PA PB : ⟦ A ⟧ i ↘ PA -> ⟦ B ⟧ j ↘ PB -> join A B -> @@ -344,7 +345,7 @@ Proof. Qed. Lemma InterpExt_Bind_inv_nopf i I p A B P (h : ⟦TBind p A B ⟧ i ;; I ↘ P) : - exists (PA : Tm 0 -> Prop), + exists (PA : Tm n -> Prop), ⟦ A ⟧ i ;; I ↘ PA /\ (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\ P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB). @@ -366,13 +367,13 @@ Proof. Qed. Lemma InterpUniv_Bind_inv_nopf i p A B P (h : ⟦TBind p A B ⟧ i ↘ P) : - exists (PA : Tm 0 -> Prop), + exists (PA : Tm n -> Prop), ⟦ A ⟧ i ↘ PA /\ (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\ P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB). Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed. -Lemma InterpExt_back_clos i I (A : Tm 0) PA : +Lemma InterpExt_back_clos i I (A : Tm n) PA : (forall j, forall a b, (RPar.R a b) -> I j b -> I j a) -> ⟦ A ⟧ i ;; I ↘ PA -> forall a b, (RPar.R a b) -> @@ -390,7 +391,7 @@ Proof. - eauto. Qed. -Lemma InterpUniv_back_clos i (A : Tm 0) PA : +Lemma InterpUniv_back_clos i (A : Tm n) PA : ⟦ A ⟧ i ↘ PA -> forall a b, (RPar.R a b) -> PA b -> PA a. @@ -400,7 +401,7 @@ Proof. hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star. Qed. -Lemma InterpUniv_back_clos_star i (A : Tm 0) PA : +Lemma InterpUniv_back_clos_star i (A : Tm n) PA : ⟦ A ⟧ i ↘ PA -> forall a b, rtc RPar.R a b -> PA b -> PA a. @@ -410,7 +411,7 @@ Proof. hauto lq:on use:InterpUniv_back_clos. Qed. -Definition ρ_ok {n} Γ (ρ : fin n -> Tm 0) := forall i m PA, +Definition ρ_ok {n} Γ (ρ : fin n -> Tm n) := forall i m PA, ⟦ subst_Tm ρ (Γ i) ⟧ m ↘ PA -> PA (ρ i). Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists m PA, ⟦ subst_Tm ρ A ⟧ m ↘ PA /\ PA (subst_Tm ρ a).