projectTuple fixed

reilabs · Dec 10, 2024 · feae9b8 · feae9b8
1 parent 1c408ad
commit feae9b8
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 18 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -250,7 +250,5 @@ nr_def structProjection<>(x : Field, y : Field) -> Field {
 example {p} {x y : Tp.denote p .field} :
   STHoare p Γ ⟦⟧ (structProjection.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [structProjection]
-  steps
-  on_goal 2 => exact Pair_a
-  on_goal 2 => rfl
+  steps <;> try rfl
   aesop
diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
@@ -37,14 +37,15 @@ def tupleNth (p : Prime) (nameOpt : Option String) (fieldTps : List Tp)  (tpl :
 
 example : ((tupleNth p nameOpt (List.replicate 7 $ .u 16) (0, 1, 2, 3, 4, 5, 6, ())) $ Fin.mk 4 (by simp_all)) = BitVec.ofNat _ 4 := by rfl
 
-inductive projectTupleOmni : Omni where
-| mk {p st} {n : Fin fieldTps.length} {tpl Q} :
-  (ho : outTp = fieldTps.get n) →
-  Q (some (st, ho ▸ tupleNth p nameOpt fieldTps tpl n)) →
-  projectTupleOmni p st [.tuple nameOpt fieldTps] outTp h![tpl] Q
+inductive projectTupleOmni (n : Fin l) : Omni where
+| mk {p st} {tpl Q} :
+  (hl : l = fieldTps.length) →
+  (ho : outTp = fieldTps.get (hl ▸ n)) →
+  Q (some (st, ho ▸ tupleNth p nameOpt fieldTps tpl (hl ▸ n))) →
+  projectTupleOmni n p st [.tuple nameOpt fieldTps] outTp h![tpl] Q
 
-def projectTuple : Builtin := {
-  omni := projectTupleOmni
+def projectTuple (n : Fin l) : Builtin := {
+  omni := projectTupleOmni n
   conseq := by
     unfold omni_conseq
     intros

diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
@@ -446,9 +446,9 @@ theorem mkStruct_intro : STHoarePureBuiltin p Γ Builtin.mkStruct (by tauto) fie
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem projectTuple_intro {n : Fin fieldTps.length} {ho : outTp = (fieldTps.get n)} :
-  STHoare p Γ ⟦⟧ (.call h![] [.tuple nameOpt fieldTps] outTp (.builtin .projectTuple) h![tpl])
-    (fun v => v = ho ▸ Lampe.Builtin.tupleNth p nameOpt fieldTps tpl n) := by
+theorem projectTuple_intro {n : Fin l} {fieldTps : List Tp} {tpl} {hl : l = fieldTps.length} {ho : outTp = (fieldTps.get (hl ▸ n))} :
+  STHoare p Γ ⟦⟧ (.call h![] [.tuple nameOpt fieldTps] outTp (.builtin $ .projectTuple n) h![tpl])
+    (fun v => v = ho ▸ Lampe.Builtin.tupleNth p nameOpt fieldTps tpl (hl ▸ n)) := by
   unfold STHoare THoare
   intros
   constructor
@@ -458,7 +458,7 @@ theorem projectTuple_intro {n : Fin fieldTps.length} {ho : outTp = (fieldTps.get
   rename_i h
   apply SLP.ent_star_top at h
   rotate_left 1
-  exact n
+  exact hl
   exact ho
   simp_all
 

diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -263,7 +263,7 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
     wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $(←mkListLit argTps)) (.builtin Builtin.mkStruct) $(←mkHListLit argVals))) vname k
 | `(nr_expr| @ $structName:nr_ident $ref:ident [ $structField:ident ]) => do
   let accessor := mkFieldName (←mkNrIdent structName) (structField.getId.toString)
-  `(.call h![] [.tuple _ _] _ (.builtin .projectTuple) h![$ref])
+  `(.call h![] [.tuple _ _] _ (.builtin (.projectTuple $accessor)) h![$ref])
 | _ => throwUnsupportedSyntax
 
 end
@@ -328,14 +328,12 @@ def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE
 | _ => throwUnsupportedSyntax
 
 def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `ident) : Syntax → m (List (Lean.Ident × TSyntax `term))
-| `(nr_struct_def| < $generics,* > { $params,* }) => do
+| `(nr_struct_def| < $_,* > { $params,* }) => do
   let numFields := params.getElems.toList.length
   params.getElems.toList.enum.mapM fun (idx, paramSyn) => match paramSyn with
     | `(nr_param_decl| $paramName:ident : $_:nr_type) => do
       let numFields := Syntax.mkNumLit (toString numFields)
       let fieldIdx := Syntax.mkNumLit (toString idx)
-      -- let generics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString)
-      -- let fieldTypes ← `(fun gs => match gs with | $(←mkHListLit generics) => $(←mkListLit fieldTypes))
       let paramIdxSyn ← `(@Fin.mk $numFields $fieldIdx (by tauto))
       pure (mkFieldName structName.getId.toString paramName.getId.toString, paramIdxSyn)
     | _ => throwUnsupportedSyntax