diff options
Diffstat (limited to 'backends/lean/Base')
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 13 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 17 |
2 files changed, 21 insertions, 9 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 523372bb..a09d6ac2 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -85,14 +85,19 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α := | none => fail .arrayOutOfBounds | some x => ret x +/- In the theorems below: we don't always need the `∃ ..`, but we use one + so that `progress` introduces an opaque variable and an equality. This + helps control the context. + -/ + @[pspec] theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - v.index α i = ret (v.val.index i.val) := by + ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by simp only [index] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) - simp only [*] + simp [*] -- This shouldn't be used def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit := @@ -109,11 +114,11 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α := @[pspec] theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - v.index_mut α i = ret (v.val.index i.val) := by + ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by simp only [index_mut] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) - simp only [*] + simp [*] instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where prop_ty := λ x => p x diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 9300edff..6a4729dc 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -162,6 +162,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) allGoals asmTac let newGoals ← getUnsolvedGoals setGoals (newGoals ++ curGoals) + trace[Progress] "progress: replaced the goals" -- pure .Ok @@ -281,12 +282,15 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs) | _ => throwError "Unexpected: invalid arguments" let keep : Option Name ← do + trace[Progress] "Keep arg: {keepArg}" let args := keepArg.getArgs - trace[Progress] "Keep args: {args}" - let arg := args.get! 1 - trace[Progress] "Keep arg: {arg}" - if arg.isIdent then pure (some arg.getId) - else do pure (some (← mkFreshAnonPropUserName)) + if args.size > 0 then do + trace[Progress] "Keep args: {args}" + let arg := args.get! 1 + trace[Progress] "Keep arg: {arg}" + if arg.isIdent then pure (some arg.getId) + else do pure (some (← mkFreshAnonPropUserName)) + else do pure none trace[Progress] "Keep: {keep}" let withArg ← do let withArg := withArg.getArgs @@ -328,7 +332,10 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do else throwError "Not a linear arithmetic goal" progressAsmsOrLookupTheorem keep withArg ids splitPost ( + withMainContext do + trace[Progress] "trying to solve assumption: {← getMainGoal}" firstTac [assumptionTac, scalarTac]) + trace[Diverge] "Progress done" elab "progress" args:progressArgs : tactic => evalProgress args |