summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith/Int.lean2
-rw-r--r--backends/lean/Base/Arith/Scalar.lean2
-rw-r--r--backends/lean/Base/Progress/Progress.lean41
-rw-r--r--backends/lean/Base/Utils.lean12
4 files changed, 32 insertions, 25 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 48a30a49..7a5bbe98 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
let hs ← collectInstancesFromMainCtx lookup
hs.toArray.mapM fun e => do
let type ← inferType e
- let name ← mkFreshUserName `h
+ let name ← mkFreshAnonPropUserName
-- Add a declaration
let nval ← Utils.addDeclTac name e type (asLet := false)
-- Simplify to unfold the declaration to unfold (i.e., the projector)
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 6f4a8eba..b792ff21 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
-- Inroduce the bounds for the isize/usize types
let add (e : Expr) : Tactic.TacticM Unit := do
let ty ← inferType e
- let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false)
+ let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 4a406bdf..9300edff 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -79,7 +79,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
match th with
| .Theorem thName => mkAppOptM thName (mvars.map some)
| .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
- let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n
+ let asmName ← do match keep with | none => mkFreshAnonPropUserName | some n => do pure n
let thTy ← inferType th
let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
@@ -101,8 +101,8 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
let hName := (← h.fvarId!.getDecl).userName
let (optIds, ids) ← do
match ids with
- | [] => do pure (some (hName, ← mkFreshUserName `h), [])
- | none :: ids => do pure (some (hName, ← mkFreshUserName `h), ids)
+ | [] => do pure (some (hName, ← mkFreshAnonPropUserName), [])
+ | none :: ids => do pure (some (hName, ← mkFreshAnonPropUserName), ids)
| some id :: ids => do pure (some (hName, id), ids)
splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids)
else k h none ids
@@ -142,7 +142,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
-- Split
let nid ← do
match nid with
- | none => mkFreshUserName `h
+ | none => mkFreshAnonPropUserName
| some nid => pure nid
trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
if ← isConj (← inferType hPost) then
@@ -270,23 +270,26 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
-- Nothing worked: failed
throwError "Progress failed"
-syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
+syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
let args := args.raw
-- Process the arguments to retrieve the identifiers to use
trace[Progress] "Progress arguments: {args}"
- let args := args.getArgs
+ let (keepArg, withArg, asArgs) ←
+ match args.getArgs.toList with
+ | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
+ | _ => throwError "Unexpected: invalid arguments"
let keep : Option Name ← do
- let args := (args.get! 0).getArgs
- if args.size > 0 then do
- let args := (args.get! 1).getArgs
- if args.size > 0 then pure (some (args.get! 1).getId)
- else do pure (some (← mkFreshUserName `h))
- else pure none
+ 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))
trace[Progress] "Keep: {keep}"
let withArg ← do
- let withArg := (args.get! 1).getArgs
+ let withArg := withArg.getArgs
if withArg.size > 0 then
let id := withArg.get! 1
trace[Progress] "With arg: {id}"
@@ -306,12 +309,12 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
pure (some (.Theorem id))
else pure none
let ids :=
- let args := (args.get! 2).getArgs
+ let args := asArgs.getArgs
let args := (args.get! 2).getSepArgs
args.map (λ s => if s.isIdent then some s.getId else none)
trace[Progress] "User-provided ids: {ids}"
let splitPost : Bool :=
- let args := (args.get! 2).getArgs
+ let args := asArgs.getArgs
(args.get! 3).getArgs.size > 0
trace[Progress] "Split post: {splitPost}"
/- For scalarTac we have a fast track: if the goal is not a linear
@@ -343,15 +346,15 @@ namespace Test
(hmin : Scalar.min ty ≤ x.val + y.val)
(hmax : x.val + y.val ≤ Scalar.max ty) :
∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
- progress keep as h as ⟨ x, h1 .. ⟩
- simp [*]
+ progress keep _ as ⟨ z, h1 .. ⟩
+ simp [*, h1]
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
(hmax : x.val + y.val ≤ Scalar.max ty) :
∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
- progress keep as h with Scalar.add_spec as ⟨ z ⟩
- simp [*]
+ progress keep h with Scalar.add_spec as ⟨ z ⟩
+ simp [*, h]
/- Checking that universe instantiation works: the original spec uses
`α : Type u` where u is quantified, while here we use `α : Type 0` -/
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index f6dc45c7..1f8f1455 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -201,6 +201,10 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr :
| .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
visit 0 e
+-- Generate a fresh user name for an anonymous proposition to introduce in the
+-- assumptions
+def mkFreshAnonPropUserName := mkFreshUserName `_
+
section Methods
variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m]
variable {a : Type}
@@ -411,7 +415,7 @@ def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do
trace[Arith] "left: {inl}: {mleft}"
trace[Arith] "right: {inr}: {mright}"
-- Create the match expression
- withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
+ withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do
let motive ← mkLambdaFVars #[hVar] goalType
let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
let mgoal ← getMainGoal
@@ -505,8 +509,8 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
let altVarNames ←
match optIds with
| none => do
- let id0 ← mkFreshUserName `h
- let id1 ← mkFreshUserName `h
+ let id0 ← mkFreshAnonPropUserName
+ let id1 ← mkFreshAnonPropUserName
pure #[{ varNames := [id0, id1] }]
| some (id0, id1) => do
pure #[{ varNames := [id0, id1] }]
@@ -532,7 +536,7 @@ partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName :
let ids ← do
if keepCurrentName then do
let cur := (← h.fvarId!.getDecl).userName
- let nid ← mkFreshUserName `h
+ let nid ← mkFreshAnonPropUserName
pure (some (cur, nid))
else
pure none
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:14:19 +0000