Fix the miniML type soundness proof for =

HOL-Theorem-Prover · Feb 28, 2012 · eefe62f · eefe62f
1 parent 4cf17fb
commit eefe62f
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 3 deletions.
diff --git a/examples/miniML/MiniMLScript.sml b/examples/miniML/MiniMLScript.sml
@@ -1103,7 +1103,7 @@ val _ = Define `
       (Opapp, Tfn t2' t3', _) => (t2 = t2') /\ (t3 = t3')
     | (Opn _, Tnum, Tnum) => (t3 = Tnum)
     | (Opb _, Tnum, Tnum) => (t3 = Tbool)
-    | (Equality, t1, t2) => (t1 = t2)
+    | (Equality, t1, t2) => (t1 = t2) /\ (t3 = Tbool)
     | _ => F
   ))`;
 

diff --git a/examples/miniML/miniML.lem b/examples/miniML/miniML.lem
@@ -1005,7 +1005,7 @@ let type_op op t1 t2 t3 =
     | (Opapp, Tfn t2' t3', _) -> (t2 = t2') && (t3 = t3')
     | (Opn _, Tnum, Tnum) -> (t3 = Tnum)
     | (Opb _, Tnum, Tnum) -> (t3 = Tbool)
-    | (Equality, t1, t2) -> (t1 = t2)
+    | (Equality, t1, t2) -> (t1 = t2) && (t3 = Tbool)
     | _ -> false
   end
 

diff --git a/examples/miniML/typeSoundScript.sml b/examples/miniML/typeSoundScript.sml
@@ -365,7 +365,8 @@ val type_op_cases = Q.prove (
   type_op op t1 t2 t3 =
   ((∃op'. op = Opn op') ∧ (t1 = Tnum) ∧ (t2 = Tnum) ∧ (t3 = Tnum)) ∨
   ((∃op'. op = Opb op') ∧ (t1 = Tnum) ∧ (t2 = Tnum) ∧ (t3 = Tbool)) ∨
-  ((op = Opapp) ∧ (t1 = Tfn t2 t3))`,
+  ((op = Opapp) ∧ (t1 = Tfn t2 t3)) ∨
+  ((op = Equality) ∧ (t1 = t2) ∧ (t3 = Tbool))`,
 rw [type_op_def] >>
 every_case_tac >>
 fs [] >>
@@ -731,6 +732,14 @@ rw [] >|
                fs [type_op_cases] >>
                rw [] >>
                metis_tac [],
+           every_case_tac >>
+               fs [] >>
+               rw [type_e_val] >>
+               fs [hd (CONJUNCTS type_v_cases)] >>
+               rw [] >>
+               fs [type_op_cases] >>
+               rw [] >>
+               metis_tac [],
            every_case_tac >>
                fs [] >>
                rw [type_e_val] >|