From dcd4465310d86d6de785f8cbff6a0e9d6cdf28c1 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 4 Mar 2025 21:47:57 -0500
Subject: [PATCH] Finish the proof of completeness for the algorithm

---
 theories/executable_correct.v | 74 +++++++++++++++++++++++++++++++++--
 1 file changed, 71 insertions(+), 3 deletions(-)

diff --git a/theories/executable_correct.v b/theories/executable_correct.v
index 54566c8..27092b1 100644
--- a/theories/executable_correct.v
+++ b/theories/executable_correct.v
@@ -62,6 +62,14 @@ Proof.
   sfirstorder use:hred_complete, hred_sound.
 Qed.
 
+Lemma coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b.
+Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed.
+
+Lemma coqeq_no_hred a b : a ↔ b -> HRed.nf a /\ HRed.nf b.
+Proof. induction 1;
+         qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf.
+Qed.
+
 Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom.
 Proof.
   have [h0 h1] : (ishf a \/ ishne a) /\ (ishf b \/ ishne b) by hauto l:on use:algo_dom_hf_hne.
@@ -178,6 +186,12 @@ Proof.
     sauto lq:on rew:off.
 Qed.
 
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. Qed.
+
 Lemma check_equal_complete :
   (forall a b (h : algo_dom a b), ~ check_equal a b h -> ~ a ↔ b) /\
   (forall a b (h : algo_dom_r a b), ~ check_equal_r a b h -> ~ a ⇔ b).
@@ -199,6 +213,60 @@ Proof.
     destruct x as [].
     sauto q:on.
     sfirstorder.
-  - admit.
-  - sfirstorder.
-  - best.
+  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1.
+    rewrite check_equal_bind_bind.
+    move /negP.
+    move /nandP.
+    case. move /nandP.
+    case. move => h. have : p0 <> p1  by sauto lqb:on.
+    clear. move => ?. hauto lq:on rew:off inv:CoqEq, CoqEq_Neu.
+    hauto qb:on inv:CoqEq,CoqEq_Neu.
+    hauto qb:on inv:CoqEq,CoqEq_Neu.
+  - simp check_equal. done.
+  - move => i j. simp check_equal.
+    case : nat_eqdec => //=. sauto lq:on.
+  - move => p0 p1 u0 u1 neu0 neu1 h ih.
+    rewrite check_equal_proj_proj.
+    move /negP /nandP. case.
+    case : PTag_eqdec => //=. sauto lq:on.
+    sauto lqb:on.
+  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
+    rewrite check_equal_app_app.
+    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
+  - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
+    rewrite check_equal_ind_ind.
+    move => + h.
+    inversion h; subst.
+    inversion H; subst.
+    move /negP /nandP.
+    case. move/nandP.
+    case. move/nandP.
+    case. qauto b:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+    sauto lqb:on inv:CoqEq, CoqEq_Neu.
+  - move => a b h ih.
+    rewrite check_equal_nfnf.
+    move : ih => /[apply].
+    move => + h0.
+    move /algo_dom_hf_hne in h.
+    inversion h0; subst.
+    have {h} [? ?] : HRed.nf a /\ HRed.nf b by sfirstorder use:hf_no_hred, hne_no_hred.
+    hauto l:on use:hreds_nf_refl.
+  - move => a a' b h dom.
+    simp ce_prop => /[apply].
+    move => + h1. inversion h1; subst.
+    inversion H; subst.
+    + sfirstorder use:coqeq_no_hred unfold:HRed.nf.
+    + have ? : y = a' by eauto using hred_deter. subst.
+      sauto lq:on.
+  - move => a b b' u hr dom ihdom.
+    rewrite check_equal_hredr.
+    move => + h. inversion h; subst.
+    have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred.
+    move => {}/ihdom.
+    inversion H0; subst.
+    + have ? : HRed.nf b'0 by hauto l:on use:coqeq_no_hred.
+      sfirstorder unfold:HRed.nf.
+    + sauto lq:on use:hred_deter.
+Qed.