killing a few admits

project-everest · Nov 29, 2023 · 7381972 · 7381972
1 parent 563c2b5
commit 7381972
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 17 deletions.
diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst
@@ -53,6 +53,24 @@ let disjoint l1 l2 = eloc_disjoint l1 l2
 let conj_disjointness p1 p2 = p1 /\ p2
 let imp_disjointness p1 p2 = p1 ==> p2
 
+let conj_disjointess_trivial_unit_left (d:disjointness_pre)
+  : Lemma 
+    (ensures (disjointness_trivial `conj_disjointness` d) == d)
+    [SMTPat (disjointness_trivial `conj_disjointness` d)]
+  = FStar.PropositionalExtensionality.apply (disjointness_trivial `conj_disjointness` d) d
+
+let conj_disjointess_trivial_unit_right (d:disjointness_pre)
+  : Lemma 
+    (ensures (d `conj_disjointness` disjointness_trivial == d))
+    [SMTPat (d `conj_disjointness` disjointness_trivial)]
+  = FStar.PropositionalExtensionality.apply (d `conj_disjointness` disjointness_trivial) d
+
+let imp_disjointess_idem (d:disjointness_pre)
+  : Lemma 
+    (ensures (imp_disjointness d d))
+    [SMTPat (imp_disjointness d d)]
+  = ()
+
 let bpointer a = B.pointer a
 let ptr_loc #a (x:B.pointer a) : Tot eloc = B.loc_buffer x
 let ptr_inv #a (x:B.pointer a) : slice_inv = F.on HS.mem #prop (fun h -> B.live h x /\ True)

diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti
@@ -62,6 +62,21 @@ val disjoint (l1 l2:eloc) : disjointness_pre
 val conj_disjointness (d0 d1:disjointness_pre) : disjointness_pre
 val imp_disjointness (d1 d2:disjointness_pre) : prop
 
+val conj_disjointess_trivial_unit_left (d:disjointness_pre)
+  : Lemma 
+    (ensures (disjointness_trivial `conj_disjointness` d) == d)
+    [SMTPat (disjointness_trivial `conj_disjointness` d)]
+
+val conj_disjointess_trivial_unit_right (d:disjointness_pre)
+  : Lemma 
+    (ensures (d `conj_disjointness` disjointness_trivial == d))
+    [SMTPat (d `conj_disjointness` disjointness_trivial)]
+
+val imp_disjointess_idem (d:disjointness_pre)
+  : Lemma 
+    (ensures (imp_disjointness d d))
+    [SMTPat (imp_disjointness d d)]
+
 inline_for_extraction
 noextract
 val bpointer (a: Type0) : Tot Type0

diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst
@@ -616,23 +616,6 @@ let _eloc_includes_refl (l: A.eloc) : Lemma
   [SMTPat (l `A.eloc_includes` l)]
 = A.eloc_includes_refl l
 
-let conj_disjointess_trivial_unit_left (d:A.disjointness_pre)
-  : Lemma 
-    (ensures (A.disjointness_trivial `A.conj_disjointness` d) == d)
-    [SMTPat (A.disjointness_trivial `A.conj_disjointness` d)]
-  = admit()
-
-let conj_disjointess_trivial_unit_right (d:A.disjointness_pre)
-  : Lemma 
-    (ensures (d `A.conj_disjointness` A.disjointness_trivial == d))
-    [SMTPat (d `A.conj_disjointness` A.disjointness_trivial)]
-  = admit()
-
-let imp_disjointess_idem (d:A.disjointness_pre)
-  : Lemma 
-    (ensures (A.imp_disjointness d d))
-    [SMTPat (A.imp_disjointness d d)]
-  = admit()
 
 (* Denotation of action as A.action *)
 [@@specialize]