From d7207c6532d6d55727172b202701b4003ce2b70c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 28 Apr 2025 17:33:12 -0400 Subject: [PATCH 1/5] Add ci --- .woodpecker.yaml | 13 +++++++++++++ README.org | 2 ++ 2 files changed, 15 insertions(+) create mode 100644 .woodpecker.yaml diff --git a/.woodpecker.yaml b/.woodpecker.yaml new file mode 100644 index 0000000..c121f1b --- /dev/null +++ b/.woodpecker.yaml @@ -0,0 +1,13 @@ +when: + - event: [push, pull_request] + branch: [main] + +steps: + - name: build + image: coqorg/coq:8.20.1-ocaml-4.14.2-flambda + commands: + - opam update + - opam install -y coq-hammer-tactics coq-equations coq-stdpp coq-autosubst-ocaml + - eval $(opam env) + - sudo chown -R 1000:1000 . + - make -j2 diff --git a/README.org b/README.org index 69c5993..8685d8b 100644 --- a/README.org +++ b/README.org @@ -1,4 +1,6 @@ * Church Rosser, surjective pairing, and strong normalization +[![status-badge](https://woodpecker.electriclam.com/api/badges/3/status.svg)](https://woodpecker.electriclam.com/repos/3) + This repository contains a mechanized proof that the lambda calculus with beta and eta rules for functions and pairs is in fact confluent for the subset of terms that are "strongly $\beta$-normalizing". From fe88b519a916da40a1b294d0e71ee228350dfa67 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 28 Apr 2025 17:33:53 -0400 Subject: [PATCH 2/5] Change woodpecker branch name --- .woodpecker.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.woodpecker.yaml b/.woodpecker.yaml index c121f1b..9726166 100644 --- a/.woodpecker.yaml +++ b/.woodpecker.yaml @@ -1,6 +1,6 @@ when: - event: [push, pull_request] - branch: [main] + branch: [master] steps: - name: build From 4c527c1b81de7ea01689832832161fc9ed4919bd Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 28 Apr 2025 17:41:07 -0400 Subject: [PATCH 3/5] Fix image --- README.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.org b/README.org index 8685d8b..94e83d9 100644 --- a/README.org +++ b/README.org @@ -1,5 +1,5 @@ * Church Rosser, surjective pairing, and strong normalization -[![status-badge](https://woodpecker.electriclam.com/api/badges/3/status.svg)](https://woodpecker.electriclam.com/repos/3) +[[https://woodpecker.electriclam.com/api/badges/3/status.svg]] This repository contains a mechanized proof that the lambda calculus with beta and eta rules for functions and pairs is in fact confluent From d2576f21fcb485fe058df2c7ad7b9f820536cba7 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 20 May 2025 14:41:09 -0400 Subject: [PATCH 4/5] Add back preservation lemma for ered Needed for justifying that the extended algorithm --- theories/fp_red.v | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 382f25b..507eb5a 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -719,6 +719,8 @@ Module RRed. move => */=; apply : IndSuc'; eauto. by asimpl. Qed. + Lemma abs_preservation a b : isabs a -> R a b -> isabs b. hauto q:on inv:R. Qed. + End RRed. Module RPar. @@ -1004,6 +1006,9 @@ Qed. Module RReds. + Lemma abs_preservation a b : isabs a -> rtc RRed.R a b -> isabs b. + induction 2; hauto lq:on use:RRed.abs_preservation. Qed. + #[local]Ltac solve_s_rec := move => *; eapply rtc_l; eauto; hauto lq:on ctrs:RRed.R. @@ -1755,6 +1760,15 @@ Module ERed. Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. + Lemma abs_back_preservation (a b : PTm) : + SN a -> R a b -> isabs b -> isabs a. + Proof. + move => + h. + elim : a b /h => //=. + case => //=. move => p. move /SN_NoForbid.P_PairInv. + sfirstorder use:SN_NoForbid.PProj_imp. + Qed. + Lemma ToEPar (a b : PTm) : ERed.R a b -> EPar.R a b. Proof. @@ -3292,7 +3306,6 @@ Module DJoin. Qed. End DJoin. - Module Sub1. Inductive R : PTm -> PTm -> Prop := | Refl a : From 8a719768588a047fd3f65261cc94e6cb50e8721a Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 4 Jun 2025 14:12:14 -0400 Subject: [PATCH 5/5] Simplify the completeness proof --- theories/algorithmic.v | 91 +++++++++--------------------------------- 1 file changed, 19 insertions(+), 72 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 4e4e6fd..fb660ec 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -1322,7 +1322,7 @@ Qed. Lemma ce_neu_neu_helper a b : ishne a -> ishne b -> - (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C). + (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b). Proof. sauto lq:on. Qed. Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 : @@ -1332,7 +1332,7 @@ Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 : Proof. hauto q:on use:REReds.hne_ind_inv. Qed. Lemma coqeq_complete' : - (forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\ + (forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b)) /\ (forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b). move => [:hConfNeuNf hhPairNeu hhAbsNeu]. apply algo_dom_mutual. @@ -1452,17 +1452,18 @@ Lemma coqeq_complete' : - move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B. move /Var_Inv => [h [A0 [h0 h1]]]. move /Var_Inv => [h' [A1 [h0' h1']]]. - split. by constructor. - suff : A0 = A1 by hauto lq:on db:wt. - eauto using lookup_deter. + by constructor. - move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja]. apply ce_neu_neu_helper => //= Γ A B. move /App_Inv => [A0][B0][hb0][ha0]hS0. move /App_Inv => [A1][B1][hb1][ha1]hS1. move /(_ hju) : ihu. move => [_ ihb]. - move : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply]. - move => [hb01][C][hT0][hT1][hT2]hT3. + move : ihb (neu0) (neu1) (hb0) (hb1). repeat move/[apply]. + move => ihb. + have : exists C, Γ ⊢ C ≲ PBind PPi A0 B0 /\ Γ ⊢ C ≲ PBind PPi A1 B1 + by hauto lq:on use:coqeq_sound_mutual. + move => [C][hT0]hT1. move /Sub_Bind_InvL : (hT0). move => [i][A2][B2]hE. have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by @@ -1477,26 +1478,7 @@ Lemma coqeq_complete' : move => iha. move : iha (ha0') (ha1'); repeat move/[apply]. move => iha. - split. sauto lq:on. - exists (subst_PTm (scons a0 VarPTm) B2). - split. - apply : Su_Transitive; eauto. - move /E_Refl in ha0. - hauto l:on use:Su_Pi_Proj2. - have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual. - split. - apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2). - move /regularity_sub0 : hSu10 => [i0]. - hauto l:on use:bind_inst. - hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl. - split. - by apply : T_App; eauto using T_Conv_E. - apply : T_Conv; eauto. - apply T_App with (A := A2) (B := B2); eauto. - apply : T_Conv_E; eauto. - move /E_Symmetric in h01. - move /regularity_sub0 : hSu20 => [i0]. - sfirstorder use:bind_inst. + hauto lq:on ctrs:CoqEq_Neu. - move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst. move : iha hja; repeat move/[apply]. move => [_ iha]. apply ce_neu_neu_helper => // Γ A B. @@ -1506,50 +1488,24 @@ Lemma coqeq_complete' : ** move => ha0 ha1. move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0. move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1. - move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply]. - move => [ha [C [hS0 [hS1 [wta0 wta1]]]]]. - split. sauto lq:on. + move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply]. + move => ih hnea0 hnea1. + have [C [hS0 hS1]] : exists C, Γ ⊢ C ≲ PBind PSig A0 B0 /\ Γ ⊢ C ≲ PBind PSig A1 B1 + by hauto lq:on use:coqeq_sound_mutual. move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2. have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 by eauto using Su_Transitive, Su_Eq. have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 by eauto using Su_Transitive, Su_Eq. - exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive. - repeat split => //=. - hauto l:on use:Su_Sig_Proj1, Su_Transitive. - apply T_Proj1 with (B := B2); eauto using T_Conv_E. - apply T_Proj1 with (B := B2); eauto using T_Conv_E. + hauto lq:on ctrs:CoqEq_Neu. ** move => ha0 ha1. move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0. move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1. - move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply]. - move => [ha [C [hS0 [hS1 [wta0 wta1]]]]]. - split. sauto lq:on. + move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply]. move => ih hnea0 hnea1. + have [C [hS0 hS1]] : exists C, Γ ⊢ C ≲ PBind PSig A0 B0 /\ Γ ⊢ C ≲ PBind PSig A1 B1 + by hauto lq:on use:coqeq_sound_mutual. move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2. - have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 - by eauto using Su_Transitive, Su_Eq. - have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 - by eauto using Su_Transitive, Su_Eq. - have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1. - have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1. - have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E. - have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E. - have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2 - by sauto lq:on use:coqeq_sound_mutual. - exists (subst_PTm (scons (PProj PL a0) VarPTm) B2). - repeat split. - *** apply : Su_Transitive; eauto. - have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2 - by qauto use:regularity, E_Refl. - sfirstorder use:Su_Sig_Proj2. - *** apply : Su_Transitive; eauto. - sfirstorder use:Su_Sig_Proj2. - *** eauto using T_Proj2. - *** apply : T_Conv. - apply : T_Proj2; eauto. - move /E_Symmetric in haE. - move /regularity_sub0 in hSu21. - sfirstorder use:bind_inst. + hauto lq:on ctrs:CoqEq_Neu. - move {hhPairNeu hhAbsNeu}. move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc /hne_ind_inj. move => /(_ neu0 neu1) [hjP][hju][hjb]hjc. @@ -1586,16 +1542,7 @@ Lemma coqeq_complete' : apply : morphing_ren; eauto using renaming_shift. by apply morphing_id. apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1. have {}ihc : c0 ⇔ c1 by qauto l:on. - move => [:ih]. - split. abstract : ih. move : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on. - have hEInd : Γ ⊢ PInd P0 u0 b0 c0 ≡ PInd P1 u1 b1 c1 ∈ subst_PTm (scons u0 VarPTm) P0 by hfcrush use:coqeq_sound_mutual. - exists (subst_PTm (scons u0 VarPTm) P0). - repeat split => //=; eauto with wt. - apply : Su_Transitive. - apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt. - apply : Su_Eq. apply E_Refl. by apply T_Nat'. - apply : Su_Eq. apply hPE. by eauto. - move : hEInd. clear. hauto l:on use:regularity. + hauto q:on ctrs:CoqEq_Neu. - move => a b ha hb. move {hhPairNeu hhAbsNeu}. case : hb; case : ha.