From 067ae89b1dd6e66baf654b0773c5c5162695fb85 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 17 Feb 2025 18:34:48 -0500 Subject: [PATCH 1/4] Finish soundness for subtyping --- theories/algorithmic.v | 48 ++++++++++++++++++++++++++++++++++++++++++ theories/fp_red.v | 4 ++++ 2 files changed, 52 insertions(+) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 96b7cb5..1576627 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -959,6 +959,16 @@ Lemma T_Univ_Raise n Γ (a : PTm n) i j : Γ ⊢ a ∈ PUniv j. Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed. +Lemma Bind_Univ_Inv n Γ p (A : PTm n) B i : + Γ ⊢ PBind p A B ∈ PUniv i -> + Γ ⊢ A ∈ PUniv i /\ funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i. +Proof. + move /Bind_Inv. + move => [i0][hA][hB]h. + move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]]. + sfirstorder use:T_Univ_Raise. +Qed. + Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B : Γ ⊢ PAbs a ∈ PBind PPi A B -> funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B. @@ -1378,3 +1388,41 @@ with CoqLEq_R {n} : PTm n -> PTm n -> Prop := (* ----------------------- *) a ≪ b where "a ≪ b" := (CoqLEq_R a b) and "a ⋖ b" := (CoqLEq a b). + +Scheme coqleq_ind := Induction for CoqLEq Sort Prop + with coqleq_r_ind := Induction for CoqLEq_R Sort Prop. + +Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind. + +Definition salgo_metric {n} k (a b : PTm n) := + exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ ESub.R va vb /\ size_PTm va + size_PTm vb + i + j <= k. + +Lemma coqleq_sound_mutual : forall n, + (forall (a b : PTm n), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\ + (forall (a b : PTm n), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ). +Proof. + apply coqleq_mutual. + - hauto lq:on use:wff_mutual ctrs:LEq. + - move => n A0 A1 B0 B1 hA ihA hB ihB Γ i. + move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1. + have hlA : Γ ⊢ A1 ≲ A0 by sfirstorder. + have hΓ : ⊢ Γ by sfirstorder use:wff_mutual. + apply Su_Transitive with (B := PBind PPi A1 B0). + by apply : Su_Pi; eauto using E_Refl, Su_Eq. + apply : Su_Pi; eauto using E_Refl, Su_Eq. + apply : ihB; eauto using ctx_eq_subst_one. + - move => n A0 A1 B0 B1 hA ihA hB ihB Γ i. + move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1. + have hlA : Γ ⊢ A0 ≲ A1 by sfirstorder. + have hΓ : ⊢ Γ by sfirstorder use:wff_mutual. + apply Su_Transitive with (B := PBind PSig A0 B1). + apply : Su_Sig; eauto using E_Refl, Su_Eq. + apply : ihB; by eauto using ctx_eq_subst_one. + apply : Su_Sig; eauto using E_Refl, Su_Eq. + - sauto lq:on use:coqeq_sound_mutual, Su_Eq. + - move => n a a' b b' ? ? ? ih Γ i ha hb. + have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq. + have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq. + suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive. + eauto using HReds.preservation. +Qed. diff --git a/theories/fp_red.v b/theories/fp_red.v index b8bcc41..0e597e2 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -2780,3 +2780,7 @@ Module Sub. hauto ctrs:rtc use:REReds.cong', Sub1.substing. Qed. End Sub. + +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. +End ESub. From 735c7f20469e8014c1ea6142672bee79e0d6e918 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 17 Feb 2025 21:43:21 -0500 Subject: [PATCH 2/4] Prove some simple soundness cases of subtyping --- theories/algorithmic.v | 138 +++++++++++++++++++++++++++++++++++++++++ theories/fp_red.v | 14 +++++ 2 files changed, 152 insertions(+) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 1576627..dc7f4b0 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -657,6 +657,18 @@ Proof. hauto lq:on use:Sub.bind_univ_noconf. Qed. +Lemma T_AbsUniv_Imp' n Γ (a : PTm (S n)) i : + Γ ⊢ PAbs a ∈ PUniv i -> False. +Proof. + hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv. +Qed. + +Lemma T_PairUniv_Imp' n Γ (a b : PTm n) i : + Γ ⊢ PPair a b ∈ PUniv i -> False. +Proof. + hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Pair_Inv. +Qed. + Lemma T_AbsBind_Imp n Γ a p A0 B0 (U : PTm n) : Γ ⊢ PAbs a ∈ U -> Γ ⊢ PBind p A0 B0 ∈ U -> @@ -1397,6 +1409,24 @@ Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind. Definition salgo_metric {n} k (a b : PTm n) := exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ ESub.R va vb /\ size_PTm va + size_PTm vb + i + j <= k. +Lemma salgo_metric_algo_metric n k (a b : PTm n) : + ishne a \/ ishne b -> + salgo_metric k a b -> + algo_metric k a b. +Proof. + move => h. + move => [i][j][va][vb][hva][hvb][nva][nvb][hS]sz. + rewrite/ESub.R in hS. + move : hS => [va'][vb'][h0][h1]h2. + suff : va' = vb' by sauto lq:on. + have {}hva : rtc RERed.R a va by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds. + have {}hvb : rtc RERed.R b vb by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds. + apply REReds.FromEReds in h0, h1. + have : ishne va' \/ ishne vb' by + hauto lq:on rew:off use:@relations.rtc_transitive, REReds.hne_preservation. + hauto lq:on use:Sub1.hne_refl. +Qed. + Lemma coqleq_sound_mutual : forall n, (forall (a b : PTm n), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\ (forall (a b : PTm n), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ). @@ -1426,3 +1456,111 @@ Proof. suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive. eauto using HReds.preservation. Qed. + +Lemma salgo_metric_case n k (a b : PTm n) : + salgo_metric k a b -> + (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ salgo_metric k' a' b /\ k' < k. +Proof. + move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. + case : a h0 => //=; try firstorder. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder qb:on use:ne_hne. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. +Qed. + +Lemma CLE_HRedL n (a a' b : PTm n) : + HRed.R a a' -> + a' ≪ b -> + a ≪ b. +Proof. + hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R. +Qed. + +Lemma CLE_HRedR n (a a' b : PTm n) : + HRed.R a a' -> + b ≪ a' -> + b ≪ a. +Proof. + hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R. +Qed. + + +Lemma algo_metric_caseR n k (a b : PTm n) : + salgo_metric k a b -> + (ishf b \/ ishne b) \/ exists k' b', HRed.R b b' /\ salgo_metric k' a b' /\ k' < k. +Proof. + move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. + case : b h1 => //=; try by firstorder. + - inversion 1 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto q:on use:HRed.AppAbs unfold:salgo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:salgo_metric solve+:lia. + + sfirstorder qb:on use:ne_hne. + - inversion 1 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. +Qed. + +Lemma salgo_metric_sub n k (a b : PTm n) : + salgo_metric k a b -> + Sub.R a b. +Proof. + rewrite /algo_metric. + move => [i][j][va][vb][h0][h1][h2][h3][[va' [vb' [hva [hvb hS]]]]]h5. + have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps. + have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps. + apply REReds.FromEReds in hva,hvb. + apply LoReds.ToRReds in h0,h1. + apply REReds.FromRReds in h0,h1. + rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive. +Qed. + +Lemma coqleq_complete' n k (a b : PTm n) : + salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b). +Proof. + move : k n a b. + elim /Wf_nat.lt_wf_ind. + move => n ih. + move => k a b /[dup] h /salgo_metric_case. + (* Cases where a and b can take steps *) + case; cycle 1. + move : k a b h. + qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne. + case /algo_metric_caseR : (h); cycle 1. + qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne. + (* Cases where neither a nor b can take steps *) + case => fb; case => fa. + - case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + * move => p0 A0 B0 _ p1 A1 B1 _. + move => h. + have ? : p1 = p0 by + hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj. + subst. + case : p0 h => //=; admit. + * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf. + + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf. + * move => *. econstructor; eauto using rtc_refl. + hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong. + (* Both cases are impossible *) + - admit. + - admit. + - move => Γ i ha hb. + econstructor; eauto using rtc_refl. + apply CLE_NeuNeu. move {ih}. + have {}h : algo_metric n a b by + hauto lq:on use:salgo_metric_algo_metric. + eapply coqeq_complete'; eauto. +Admitted. diff --git a/theories/fp_red.v b/theories/fp_red.v index 0e597e2..3a40f2e 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -2620,6 +2620,10 @@ Module Sub1. 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) : + ishne a \/ ishne b -> R a b -> a = b. + Proof. hauto q:on inv:R. Qed. + End Sub1. Module Sub. @@ -2628,6 +2632,16 @@ Module Sub. Lemma refl n (a : PTm n) : R a a. Proof. sfirstorder use:@rtc_refl unfold:R. Qed. + Lemma ToJoin n (a b : PTm n) : + ishne a \/ ishne b -> + R a b -> + DJoin.R a b. + Proof. + move => h [c][d][h0][h1]h2. + have : ishne c \/ ishne d by hauto q:on use:REReds.hne_preservation. + 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. Proof. rewrite /R. From 9c5eb31edfdba5e289cf8ac5a7e1e609b9f3728f Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 17 Feb 2025 22:50:25 -0500 Subject: [PATCH 3/4] Finish all cases of subtyping --- theories/algorithmic.v | 61 +++++++++++++++++++++++++++++++++++++++--- theories/fp_red.v | 32 ++++++++++++++++++++++ 2 files changed, 89 insertions(+), 4 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index dc7f4b0..2ea3f78 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -946,6 +946,7 @@ Proof. repeat split => //=; sfirstorder b:on use:ne_nf. Qed. + Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1 : algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) -> p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1. @@ -1526,6 +1527,32 @@ Proof. rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive. Qed. +Lemma salgo_metric_pi n k (A0 : PTm n) B0 A1 B1 : + salgo_metric k (PBind PPi A0 B0) (PBind PPi A1 B1) -> + exists j, j < k /\ salgo_metric j A1 A0 /\ salgo_metric j B0 B1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_bind_inv h0 => /[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_bind_inv h1 => /[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + move /ESub.pi_inj : h4 => [? ?]. + hauto qb:on solve+:lia. +Qed. + +Lemma salgo_metric_sig n k (A0 : PTm n) B0 A1 B1 : + salgo_metric k (PBind PSig A0 B0) (PBind PSig A1 B1) -> + exists j, j < k /\ salgo_metric j A0 A1 /\ salgo_metric j B0 B1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_bind_inv h0 => /[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_bind_inv h1 => /[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + move /ESub.sig_inj : h4 => [? ?]. + hauto qb:on solve+:lia. +Qed. + Lemma coqleq_complete' n k (a b : PTm n) : salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b). Proof. @@ -1548,19 +1575,45 @@ Proof. have ? : p1 = p0 by hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj. subst. - case : p0 h => //=; admit. + case : p0 h => //=. + ** move /salgo_metric_pi. + move => [j [hj [hA hB]]] Γ i. + move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. + have ihA : A0 ≪ A1 by hauto l:on. + econstructor; eauto using E_Refl; constructor=> //. + have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual. + suff : funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B1 ∈ PUniv i + by hauto l:on. + eauto using ctx_eq_subst_one. + ** move /salgo_metric_sig. + move => [j [hj [hA hB]]] Γ i. + move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. + have ihA : A1 ≪ A0 by hauto l:on. + econstructor; eauto using E_Refl; constructor=> //. + have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual. + suff : funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ∈ PUniv i + by hauto l:on. + eauto using ctx_eq_subst_one. * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf. + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf. * move => *. econstructor; eauto using rtc_refl. hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong. (* Both cases are impossible *) - - admit. - - admit. + - have {}h : DJoin.R a b by + hauto lq:on use:salgo_metric_algo_metric, algo_metric_join. + case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + hauto lq:on use:DJoin.hne_bind_noconf. + + hauto lq:on use:DJoin.hne_univ_noconf. + - have {}h : DJoin.R b a by + hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric. + case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + hauto lq:on use:DJoin.hne_bind_noconf. + + hauto lq:on use:DJoin.hne_univ_noconf. - move => Γ i ha hb. econstructor; eauto using rtc_refl. apply CLE_NeuNeu. move {ih}. have {}h : algo_metric n a b by hauto lq:on use:salgo_metric_algo_metric. eapply coqeq_complete'; eauto. -Admitted. +Qed. diff --git a/theories/fp_red.v b/theories/fp_red.v index 3a40f2e..d1702fe 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -2337,6 +2337,17 @@ Module DJoin. case : c => //=. Qed. + Lemma hne_bind_noconf n (a b : PTm n) : + R a b -> ishne a -> isbind b -> False. + Proof. + move => [c [h0 h1]] h2 h3. + have {h0 h1 h2 h3} : ishne c /\ isbind c by + hauto l:on use:REReds.hne_preservation, + REReds.bind_preservation. + move => []. + case : c => //=. + Qed. + Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 : DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) -> p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1. @@ -2797,4 +2808,25 @@ End Sub. 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. + + Lemma pi_inj n (A0 A1 : PTm n) B0 B1 : + R (PBind PPi A0 B0) (PBind PPi A1 B1) -> + R A1 A0 /\ R B0 B1. + Proof. + move => [u0 [u1 [h0 [h1 h2]]]]. + move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. + move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. + sauto lq:on rew:off inv:Sub1.R. + Qed. + + Lemma sig_inj n (A0 A1 : PTm n) B0 B1 : + R (PBind PSig A0 B0) (PBind PSig A1 B1) -> + R A0 A1 /\ R B0 B1. + Proof. + move => [u0 [u1 [h0 [h1 h2]]]]. + move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. + move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. + sauto lq:on rew:off inv:Sub1.R. + Qed. + End ESub. From d48d9db1b74cbd044ac89d36ec29904c2d755fd0 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 17 Feb 2025 23:31:12 -0500 Subject: [PATCH 4/4] Finish the conversion proof completely --- theories/algorithmic.v | 29 ++++++++++++++ theories/fp_red.v | 87 ++++++++++++++++++++++++++++++------------ 2 files changed, 91 insertions(+), 25 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 2ea3f78..6fe5fad 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -1617,3 +1617,32 @@ Proof. hauto lq:on use:salgo_metric_algo_metric. eapply coqeq_complete'; eauto. Qed. + +Lemma coqleq_complete n Γ (a b : PTm n) : + Γ ⊢ a ≲ b -> a ≪ b. +Proof. + move => h. + suff : exists k, salgo_metric k a b by hauto lq:on use:coqleq_complete', regularity. + eapply fundamental_theorem in h. + move /logrel.SemLEq_SN_Sub : h. + move => h. + have : exists va vb : PTm n, + rtc LoRed.R a va /\ + rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb + by hauto l:on use:Sub.standardization_lo. + move => [va][vb][hva][hvb][nva][nvb]hj. + move /relations.rtc_nsteps : hva => [i hva]. + move /relations.rtc_nsteps : hvb => [j hvb]. + exists (i + j + size_PTm va + size_PTm vb). + hauto lq:on solve+:lia. +Qed. + +Lemma coqleq_sound : forall n Γ (a b : PTm n) i j, + Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv j -> a ≪ b -> Γ ⊢ a ≲ b. +Proof. + move => n Γ a b i j. + have [*] : i <= i + j /\ j <= i + j by lia. + have : Γ ⊢ a ∈ PUniv (i + j) /\ Γ ⊢ b ∈ PUniv (i + j) + by sfirstorder use:T_Univ_Raise. + sfirstorder use:coqleq_sound_mutual. +Qed. diff --git a/theories/fp_red.v b/theories/fp_red.v index d1702fe..e89c191 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -2637,6 +2637,31 @@ Module Sub1. 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. + + Lemma pi_inj n (A0 A1 : PTm n) B0 B1 : + R (PBind PPi A0 B0) (PBind PPi A1 B1) -> + R A1 A0 /\ R B0 B1. + Proof. + move => [u0 [u1 [h0 [h1 h2]]]]. + move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. + move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. + sauto lq:on rew:off inv:Sub1.R. + Qed. + + Lemma sig_inj n (A0 A1 : PTm n) B0 B1 : + R (PBind PSig A0 B0) (PBind PSig A1 B1) -> + R A0 A1 /\ R B0 B1. + Proof. + move => [u0 [u1 [h0 [h1 h2]]]]. + move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. + move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. + sauto lq:on rew:off inv:Sub1.R. + Qed. + +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. @@ -2804,29 +2829,41 @@ Module Sub. 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. + Proof. hauto q:on use:REReds.ToEReds. Qed. + + Lemma standardization n (a b : PTm n) : + 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. + move => h0 h1 hS. + have : exists v, rtc RRed.R a v /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds. + move => [v [hv2 hv3]]. + have : exists v, rtc RRed.R b v /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds. + move => [v' [hv2' hv3']]. + move : (hv2) (hv2') => *. + apply DJoin.FromRReds in hv2, hv2'. + move/DJoin.symmetric in hv2'. + apply FromJoin in hv2, hv2'. + have hv : R v v' by eauto using transitive. + have {}hv : ESub.R v v' by hauto l:on use:ToESub. + hauto lq:on. + Qed. + + Lemma standardization_lo n (a b : PTm n) : + 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. + move => /[dup] sna + /[dup] snb. + move : standardization; repeat move/[apply]. + move => [va][vb][hva][hvb][nfva][nfvb]hj. + move /LoReds.FromSN : sna => [va' [hva' hva'0]]. + move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]]. + exists va', vb'. + repeat split => //=. + have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds. + case; congruence. + Qed. + End Sub. - -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. - - Lemma pi_inj n (A0 A1 : PTm n) B0 B1 : - R (PBind PPi A0 B0) (PBind PPi A1 B1) -> - R A1 A0 /\ R B0 B1. - Proof. - move => [u0 [u1 [h0 [h1 h2]]]]. - move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. - move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. - sauto lq:on rew:off inv:Sub1.R. - Qed. - - Lemma sig_inj n (A0 A1 : PTm n) B0 B1 : - R (PBind PSig A0 B0) (PBind PSig A1 B1) -> - R A0 A1 /\ R B0 B1. - Proof. - move => [u0 [u1 [h0 [h1 h2]]]]. - move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst. - move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst. - sauto lq:on rew:off inv:Sub1.R. - Qed. - -End ESub.