4 changed files with 73 additions and 48 deletions
--- a/.woodpecker.yaml
+++ b/.woodpecker.yaml
@ -1,13 +0,0 @@
-when:
-  - event: [push, pull_request]
-    branch: [master]
-
-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
--- a/README.org
+++ b/README.org
@ -1,6 +1,4 @@
 * Church Rosser, surjective pairing, and strong normalization
-[[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
 for the subset of terms that are "strongly $\beta$-normalizing".
--- 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) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ 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).
 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)) /\
+  (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_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
  move => [:hConfNeuNf hhPairNeu hhAbsNeu].
  apply algo_dom_mutual.
@ -1452,18 +1452,17 @@ 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']]].
-    by constructor.
+    split. by constructor.
+    suff : A0 = A1 by hauto lq:on db:wt.
+    eauto using lookup_deter.
  - 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 => 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 : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply].
+    move => [hb01][C][hT0][hT1][hT2]hT3.
    move /Sub_Bind_InvL : (hT0).
    move => [i][A2][B2]hE.
    have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
@ -1478,7 +1477,26 @@ Lemma coqeq_complete' :
    move => iha.
    move : iha (ha0') (ha1'); repeat move/[apply].
    move => iha.
-    hauto lq:on ctrs:CoqEq_Neu.
+    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.
  - 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.
@ -1488,24 +1506,50 @@ 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 => 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 : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
       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.
-       hauto lq:on ctrs:CoqEq_Neu.
+       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.
    ** 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 => 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 : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
       move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
-       hauto lq:on ctrs:CoqEq_Neu.
+       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.
  - 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.
@ -1542,7 +1586,16 @@ 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.
-    hauto q:on ctrs:CoqEq_Neu.
+    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.
  - move => a b ha hb.
    move {hhPairNeu hhAbsNeu}.
    case : hb; case : ha.
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@ -719,8 +719,6 @@ 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.
@ -1006,9 +1004,6 @@ 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.
@ -1760,15 +1755,6 @@ 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.
@ -3306,6 +3292,7 @@ Module DJoin.
  Qed.
 End DJoin.

+
 Module Sub1.
  Inductive R : PTm -> PTm -> Prop :=
  | Refl a :