Fix some broken proofs

CakeML · Dec 18, 2021 · cc205ef · cc205ef
1 parent a04d609
commit cc205ef
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 10 deletions.
diff --git a/candle/overloading/semantics/holExtensionScript.sml b/candle/overloading/semantics/holExtensionScript.sml
@@ -199,7 +199,7 @@ End
 Triviality LIST_LENGTH_2:
   LENGTH l = 2 ⇔ ∃e1 e2. l = [e1; e2]
 Proof
-  fs [LENGTH_EQ_NM_compute]
+  Cases_on ‘l’ \\ fs [] \\ Cases_on ‘t’ \\ fs []
 QED
 
 Theorem allTypes'_subst_clos_dependency:

diff --git a/candle/overloading/semantics/holModelConservativityScript.sml b/candle/overloading/semantics/holModelConservativityScript.sml
@@ -7239,7 +7239,7 @@ Proof
                (drule models_ConstSpec_witnesses_model_ext >>
                 disch_then(fn thm => first_x_assum(mp_then (Pos last) mp_tac thm)) >>
                 disch_then(qspec_then ‘HD ctxt’ mp_tac) >>
-                simp[quantHeuristicsTheory.HD_TL_EQ_THMS] >>
+                (*simp[quantHeuristicsTheory.HD_TL_EQ_THMS] >>*)
                 simp[Q.prove(‘∀l. l ≠ [] ⇒ HD l :: TL l = l’,Cases>>simp[])] >>
                 rpt(disch_then(fn thm => first_x_assum(mp_then Any mp_tac thm))) >>
                 impl_tac >-
@@ -7497,7 +7497,7 @@ Proof
               (drule models_ConstSpec_witnesses_model_ext >>
                disch_then(fn thm => first_x_assum(mp_then (Pos last) mp_tac thm)) >>
                disch_then(qspec_then ‘HD ctxt’ mp_tac) >>
-               simp[quantHeuristicsTheory.HD_TL_EQ_THMS] >>
+               (*simp[quantHeuristicsTheory.HD_TL_EQ_THMS] >>*)
                simp[Q.prove(‘∀l. l ≠ [] ⇒ HD l :: TL l = l’,Cases>>simp[])] >>
                rpt(disch_then(fn thm => first_x_assum(mp_then Any mp_tac thm))) >>
                impl_tac >-

diff --git a/candle/overloading/semantics/holSemanticsExtraScript.sml b/candle/overloading/semantics/holSemanticsExtraScript.sml
@@ -437,7 +437,7 @@ Proof
   >> ho_match_mp_tac allTypes'_defn_ind >> rpt strip_tac
   >> fs[allTypes'_defn,nonbuiltin_types_def,is_builtin_type_def]
   >> every_case_tac >> fs[is_builtin_type_def,EVERY_MEM,MEM_FLAT,MEM_MAP,PULL_EXISTS]
-  >> fs[LENGTH_EQ_NUM_compute,is_builtin_name_def]
+  >> fs[listTheory.LENGTH_EQ_NUM_compute,is_builtin_name_def]
   >- metis_tac[]
 QED
 
@@ -539,7 +539,7 @@ QED
 Triviality LIST_LENGTH_2:
   LENGTH l = 2 ⇔ ∃e1 e2. l = [e1; e2]
 Proof
-  fs [LENGTH_EQ_NM_compute]
+  Cases_on ‘l’ \\ fs [] \\ Cases_on ‘t’ \\ fs []
 QED
 
 Theorem allTypes'_no_tyvars:

diff --git a/candle/overloading/semantics/holSemanticsScript.sml b/candle/overloading/semantics/holSemanticsScript.sml
@@ -132,7 +132,7 @@ val allTypes_no_tyvars_and_ok = Q.prove(
   \\ BasicProvers.PURE_FULL_CASE_TAC >- fs[type_ok_def,is_std_sig_def]
   \\ qpat_x_assum `!x. _` mp_tac >> simp[] >> strip_tac
   >> BasicProvers.PURE_FULL_CASE_TAC
-  >- (fs[LENGTH_EQ_NUM_compute,is_std_sig_def,type_ok_def]
+  >- (fs[listTheory.LENGTH_EQ_NUM_compute,is_std_sig_def,type_ok_def]
       \\ fs[])
   \\ fs[type_ok_def]);
 
@@ -199,11 +199,27 @@ Proof
   >- (fs[boolTheory.IN_DEF,builtin_closure_rules])
   >> qpat_x_assum `!x. _` mp_tac >> simp[]
   >> BasicProvers.PURE_FULL_CASE_TAC >> simp[builtin_closure_rules,boolTheory.IN_DEF]
-  >> fs[LENGTH_EQ_NUM_compute]
+  >> fs []
+  >> gvs[listTheory.LENGTH_EQ_NUM_compute]
   >> rpt(BasicProvers.VAR_EQ_TAC)
   >> fs[allTypes'_defn] >> strip_tac
-  >> rfs[LENGTH_EQ_NUM_compute]
-  >> metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+  >- metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+  >- metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+  >-
+   (Cases_on ‘l’ \\ fs []
+    >- metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+    >> Cases_on ‘t’ \\ fs []
+    >- metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+    >> rfs[listTheory.LENGTH_EQ_NUM_compute,PULL_EXISTS]
+    >> metis_tac[builtin_closure_rules,boolTheory.IN_DEF])
+  >- (rfs[listTheory.LENGTH_EQ_NUM_compute,PULL_EXISTS]
+    >> metis_tac[builtin_closure_rules,boolTheory.IN_DEF])
+  >-
+   (Cases_on ‘l’ \\ fs []
+    >> Cases_on ‘t’ \\ fs []
+    >- metis_tac[builtin_closure_rules,boolTheory.IN_DEF]
+    >> rfs[listTheory.LENGTH_EQ_NUM_compute,PULL_EXISTS]
+    >> metis_tac[builtin_closure_rules,boolTheory.IN_DEF])
 QED
 
 val allTypes'_builtin_closure = Q.prove(
@@ -1096,7 +1112,7 @@ Proof
   >- (fs[boolTheory.IN_DEF] \\ match_mp_tac (builtin_closure_inj) \\
       simp[boolTheory.IN_DEF])
   \\ fs[nonbuiltin_types_def,builtin_types_def,is_builtin_type_def,is_builtin_name_def,
-        LENGTH_EQ_NUM_compute,boolTheory.IN_DEF]
+        listTheory.LENGTH_EQ_NUM_compute,boolTheory.IN_DEF]
   \\ fs[tyvars_def,ground_types_def,LIST_UNION_EQ_NIL,type_ok_def]
   \\ metis_tac[builtin_closure_rules]
 QED

diff --git a/candle/overloading/syntax/holSyntaxExtraScript.sml b/candle/overloading/syntax/holSyntaxExtraScript.sml
@@ -9284,6 +9284,7 @@ Proof
       >> Cases_on `HD r`
       >> fs[subtype_at_def]
       >> fs[]
+      >> ‘r ≠ []’ by (Cases_on ‘r’ \\ fs [])
       >> fs[MEM_ZIP]
       >> DISJ1_TAC
       >> asm_exists_tac