Merge branch 'us/tuple-support' of https://github.com/reilabs/lampe i…

…nto us/lens-support
reilabs · Dec 28, 2024 · 34c6f1f · 34c6f1f
2 parents c8fb45c + cd05bac
commit 34c6f1f
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 19 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -269,12 +269,18 @@ example {x y : Tp.denote p .field} :
   STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
     ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [call_decl, struct_construct]
-  steps <;> tauto
-  . simp_all [exists_const, SLP.true_star]
+  apply STHoare.letIn_intro
+  on_goal 3 => exact (fun (v : Tp.denote p $ .tuple _ [.field, .field]) => v = (x, y, ()))
+  apply STHoare.callDecl_intro <;> tauto
+  . apply STHoare.letIn_intro
+    . steps
+    . intros
+      steps
+      aesop
+  . intros
     steps
-    simp only [exists_const, SLP.true_star]
-    simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall']
-  . sorry
+    aesop
+
 
 nr_def simple_tuple<>() -> Field {
   let t = `(1 : Field, true, 3 : Field);
@@ -303,12 +309,7 @@ nr_def simple_array<>() -> Field {
 example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 2) := by
   simp only [simple_array, Expr.mkArray]
   steps <;> tauto
-  on_goal 3 => exact fun v => v = 2
-  rotate_left
-  steps; aesop
-  simp_all
-  simp only [Expr.readArray]
-  sorry
+  aesop
 
 nr_def tuple_lens<>() -> Field {
   let mut p = `(`(1 : Field, 2 : Field), 3 : Field);

diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
@@ -131,20 +131,20 @@ theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps}
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
 -- BigInt