Fix final bugs to make evaluation work again

coq/Expressions.v

@@ -777,7 +777,30 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
     - apply expCompare_eq_trans.
   Defined.
 
-  Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Ltac solve_tac :=
+      try (left; auto; fail"" );
+      try (right; hnf; intros; congruence).
+
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+    unfold eq.
+    induction x; destruct y; cbn;
+      solve_tac.
+    - destruct (n ?= n0)%nat eqn:?; firstorder.
+    - destruct m, m0; cbn; solve_tac;
+        destruct (V_ordered.eq_dec v v0) as [eq_case | eq_case];
+        rewrite <- V_orderedFacts.compare_eq_iff in eq_case; firstorder.
+    - destruct u, u0; cbn; solve_tac; apply IHx.
+    - destruct b, b0; cbn; solve_tac; destruct (IHx1 y1) as [eq_case | eq_case];
+        try rewrite eq_case; try apply IHx2;
+          destruct (expCompare x1 y1) eqn:? ; firstorder.
+    - destruct (IHx1 y1) as [eq_case | eq_case];
+        try rewrite eq_case; destruct (IHx2 y2) as [eq_case2 | eq_case2];
+          try rewrite eq_case2; try apply IHx3;
+            destruct (expCompare x1 y1) eqn:?; try auto;
+            destruct (expCompare x2 y2) eqn:?; auto.
+    - destruct m, m0; cbn; solve_tac; apply IHx.
+  Defined.
 
   Definition eq_refl : forall x, eq x x.
   Proof.

coq/binary/Makefile

@@ -2,6 +2,7 @@
 #	ocamlc -c CoqChecker.ml
 #	ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
 native:
+	ocamlc -c big.ml
 	ocamlc -c CoqChecker.ml
 	ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
 

hol4/Infra/DaisyTactics.sml

@@ -102,14 +102,14 @@ fun impl_subgoal_tac th =
       SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
   end
 
-fun daisy_eval_tac t :tactic=
-  let
-    val result_thm = computeLib.EVAL_CONV t
-  in
-    rewrite_tac [result_thm]
+val daisy_eval_tac :tactic=
+  let val _ =  computeLib.del_funs([sptreeTheory.lookup_def])
+      val _ = computeLib.add_funs([sptreeTheory.lookup_compute]) in
+    computeLib.EVAL_TAC
     \\ fs[sptreeTheory.lookup_def]
     \\ rpt strip_tac
     \\ fs[sptreeTheory.lookup_def]
+    \\ EVAL_TAC
 end;
 
 (* Daisy Compute Tactic as in Coq dev to simplify goals involving computations *)

hol4/TypingScript.sml

@@ -68,7 +68,7 @@ val typeMap_def = Define `
             | _, _, _  => DaisyMapTree_empty)
         | Downcast m e1 =>
           let tMap_new = typeMap Gamma e1 tMap in
-          let m1 = DaisyMapTree_find e1 tMap in
+          let m1 = DaisyMapTree_find e1 tMap_new in
           (case m1 of
              | SOME t1 =>
                (if morePrecise t1 m

src/main/scala/daisy/backend/CertificatePhase.scala

@@ -744,7 +744,7 @@ object CertificatePhase extends DaisyPhase {
       "Proof.\n  vm_compute; auto.\nQed.\n"
     } else if (prover == "hol4"){
       "val _ = store_thm (\""+s"ErrorBound_${fName}_Sound"+"\",\n" +
-      s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n daisy_eval_tac \\\\ fs[]);\n"
+      s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n daisy_eval_tac \\\\ fs[REAL_INV_1OVER]);\n"
     } else
       ""