intro rule. updated the steps tactic. example in main

reilabs · Nov 9, 2024 · 3d103e1 · 3d103e1
1 parent 4dfcd8b
commit 3d103e1
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 0 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -58,3 +58,27 @@ example {self that : Tp.denote P (.slice tp)} : STHoare P Γ ⟦⟧ (sliceAppend
   · simp_all
   steps
   simp_all [Nat.mod_eq_of_lt]
+
+nr_def simple_if<>(x : Field, y : Field) -> u32 {
+  let z = if #eq(x, y) : bool { 0 : u32 } else { 1 : u32 };
+  3 : u32
+}
+
+example : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] h![x, y])
+  fun v => v =  BitVec.ofNat _ 3 := by
+  simp only [simple_if]
+  steps
+  simp_all
+  rename_i cnd
+  cases cnd <;> simp_all
+  . steps
+    simp only [Nat.cast_zero, BitVec.ofNat_eq_ofNat, SLP.true_star]
+    tauto
+  . simp only [beq_false, Bool.not_eq_true', eq_iff_iff]
+    intros
+    steps
+    . simp only [Bool.false_eq_true, false_iff, SLP.true_star]
+      tauto
+    . simp only [Nat.cast_one, BitVec.ofNat_eq_ofNat, SLP.true_star]
+      tauto
+  . aesop
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -336,4 +336,26 @@ theorem loop_inv_intro (Inv : (i : U s) → (lo ≤ i) → (i ≤ hi) → SLP p)
           apply h
           simp [*]
 
+theorem iteTrue_intro :
+    STHoare p Γ P mainBody Q →
+    STHoare p Γ P (.ite true mainBody elseBody) Q := by
+  tauto
+
+theorem iteFalse_intro :
+    STHoare p Γ P elseBody Q →
+    STHoare p Γ P (.ite false mainBody elseBody) Q := by
+  tauto
+
+theorem ite_intro :
+  (cnd == true → STHoare p Γ P mainBody Q) →
+  (cnd == false → STHoare p Γ P elseBody Q) →
+  STHoare p Γ P (.ite cnd mainBody elseBody) Q := by
+  unfold STHoare
+  intros
+  cases cnd
+  . apply iteFalse_intro
+    tauto
+  . apply iteTrue_intro
+    tauto
+
 end Lampe.STHoare
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -187,6 +187,11 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
   mkExpr e none fun eVal => do
     wrapSimple (←`(Lampe.Expr.writeRef $v $eVal)) vname k
 | `(nr_expr| ( $e )) => mkExpr e vname k
+| `(nr_expr| if $cond $mainBody else $elseBody) => do
+    mkExpr cond none fun cond => do
+      let mainBody ← mkExpr mainBody none fun x => ``(Lampe.Expr.var $x)
+      let elseBody ← mkExpr elseBody none fun x => ``(Lampe.Expr.var $x)
+      wrapSimple (←`(Lampe.Expr.ite $cond $mainBody $elseBody)) vname k
 | _ => throwUnsupportedSyntax
 
 end

diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -455,6 +455,7 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply sliceLen_intro
     | apply sliceIndex_intro
     | apply slicePushBack_intro
+    | apply ite_intro
   )
 ))
 
@@ -471,6 +472,7 @@ macro "stephelper2" : tactic => `(tactic|(
     | apply consequence_frame_left sliceLen_intro
     | apply consequence_frame_left sliceIndex_intro
     | apply consequence_frame_left slicePushBack_intro
+    | apply consequence_frame_left ite_intro
   )
   repeat sl
 ))
@@ -488,6 +490,7 @@ macro "stephelper3" : tactic => `(tactic|(
     | apply ramified_frame_top sliceLen_intro
     | apply ramified_frame_top sliceIndex_intro
     | apply ramified_frame_top slicePushBack_intro
+    | apply ramified_frame_top ite_intro
   )
   repeat sl
 ))