projection example

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

Hide file tree

Showing 4 changed files with 25 additions and 10 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -246,3 +246,11 @@ nr_def structProjection<>(x : Field, y : Field) -> Field {
   let s = @Pair { x : Field, y : Field };
   @Pair s[a]
 }
+
+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
+  aesop
diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
@@ -39,8 +39,9 @@ example : ((tupleNth p nameOpt (List.replicate 7 $ .u 16) (0, 1, 2, 3, 4, 5, 6,
 
 inductive projectTupleOmni : Omni where
 | mk {p st} {n : Fin fieldTps.length} {tpl Q} :
-  Q (some (st, tupleNth p _ fieldTps tpl n)) →
-  projectTupleOmni p st [.tuple _ fieldTps] (fieldTps.get n) h![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
 
 def projectTuple : Builtin := {
   omni := projectTupleOmni
@@ -56,6 +57,7 @@ def projectTuple : Builtin := {
     constructor
     simp only
     repeat apply Exists.intro <;> tauto
+    assumption
 }
 
 -- abbrev FieldProjector (fieldTps : List Tp) := Finmap fun _ : String => Fin fieldTps.length

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 :
-  STHoare p Γ ⟦⟧ (.call h![] [.tuple nameOpt fieldTps] (fieldTps.get n) (.builtin .projectTuple) h![tpl])
-  (fun v => v = Lampe.Builtin.tupleNth p nameOpt fieldTps tpl n) := by
+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
   unfold STHoare THoare
   intros
   constructor
@@ -457,7 +457,10 @@ theorem projectTuple_intro :
   simp_all only [SLP.true_star, List.get_eq_getElem, Option.map_some']
   rename_i h
   apply SLP.ent_star_top at h
-  assumption
+  rotate_left 1
+  exact n
+  exact ho
+  simp_all
 
 -- Misc
 

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 _ _] (List.get _ $accessor) (.builtin .projectTuple) h![$ref])
+  `(.call h![] [.tuple _ _] _ (.builtin .projectTuple) h![$ref])
 | _ => throwUnsupportedSyntax
 
 end
@@ -316,24 +316,26 @@ def mkTraitImpl [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE
 
 def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `ident) : Syntax → m (TSyntax `term)
 | `(nr_struct_def| < $generics,* > { $params,* }) => do
-  let genericKinds ← mkListLit (← generics.getElems.toList.mapM fun _ => `(Kind.type))
+  let genericKinds ← mkListLit (←generics.getElems.toList.mapM fun _ => `(Kind.type))
   let generics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString)
   let fieldTypes ← params.getElems.toList.mapM fun paramSyn => match paramSyn with
     | `(nr_param_decl| $_:ident : $ty:nr_type) => mkNrType ty
     | _ => throwUnsupportedSyntax
-  let fieldTypes ← `(fun gs => match gs with | $(← mkHListLit generics) => $(← mkListLit fieldTypes))
+  let fieldTypes ← `(fun gs => match gs with | $(←mkHListLit generics) => $(←mkListLit fieldTypes))
   let structNameStrLit := Syntax.mkStrLit structName.getId.toString
   let syn ← `(Struct.mk $structNameStrLit $genericKinds $fieldTypes)
   pure syn
 | _ => 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| < $_,* > { $params,* }) => do
+| `(nr_struct_def| < $generics,* > { $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