summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base.lean2
-rw-r--r--backends/lean/Base/Arith/Arith.lean (renamed from backends/lean/Base/Arith.lean)61
-rw-r--r--backends/lean/Base/Arith/Base.lean (renamed from backends/lean/Base/ArithBase.lean)0
-rw-r--r--backends/lean/Base/Diverge/Elab.lean17
-rw-r--r--backends/lean/Base/Utils.lean95
5 files changed, 101 insertions, 74 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 1f8cbc8e..51211704 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -1,3 +1,5 @@
+import Base.Utils
import Base.Primitives
import Base.Diverge
import Base.Arith
+import Base.Progress
diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 364447ed..0ba73d18 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -8,7 +8,8 @@ import Mathlib.Tactic.Linarith
-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
--import Mathlib.Tactic.Omega
import Base.Primitives
-import Base.ArithBase
+import Base.Utils
+import Base.Arith.Base
/-
Mathlib tactics:
@@ -222,62 +223,6 @@ example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
display_prop_has_imp_instances
simp
-def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
- -- I don't think we need that
- Lean.Elab.Tactic.withMainContext do
- -- Insert the new declaration
- let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
- withDecl fun nval => do
- -- For debugging
- let lctx ← Lean.MonadLCtx.getLCtx
- let fid := nval.fvarId!
- let decl := lctx.get! fid
- trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
- --
- -- Tranform the main goal `?m0` to `let x = nval in ?m1`
- let mvarId ← Tactic.getMainGoal
- let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
- let newVal ← mkLetFVars #[nval] newMVar
- -- There are two cases:
- -- - asLet is true: newVal is `let $name := $val in $newMVar`
- -- - asLet is false: ewVal is `λ $name => $newMVar`
- -- We need to apply it to `val`
- let newVal := if asLet then newVal else mkAppN newVal #[val]
- -- Assign the main goal and update the current goal
- mvarId.assign newVal
- let goals ← Tactic.getUnsolvedGoals
- Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
- -- Return the new value - note: we are in the *new* context, created
- -- after the declaration was added, so it will persist
- pure nval
-
-def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
- -- I don't think we need that
- Lean.Elab.Tactic.withMainContext do
- --
- let val ← elabTerm val .none
- let type ← inferType val
- -- In some situations, the type will be left as a metavariable (for instance,
- -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
- -- not choose): we force the instantiation of the meta-variable
- synthesizeSyntheticMVarsUsingDefault
- --
- let _ ← addDecl name val type asLet
-
-elab "custom_let " n:ident " := " v:term : tactic => do
- addDeclSyntax n.getId v (asLet := true)
-
-elab "custom_have " n:ident " := " v:term : tactic =>
- addDeclSyntax n.getId v (asLet := false)
-
-example : Nat := by
- custom_let x := 4
- custom_have y := 4
- apply y
-
-example (x : Bool) : Nat := by
- cases x <;> custom_let x := 3 <;> apply x
-
-- Lookup instances in a context and introduce them with additional declarations.
def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do
let hs ← collectInstancesFromMainCtx lookup
@@ -285,7 +230,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
let type ← inferType e
let name ← mkFreshUserName `h
-- Add a declaration
- let nval ← addDecl name e type (asLet := false)
+ let nval ← Utils.addDecl name e type (asLet := false)
-- Simplify to unfold the declaration to unfold (i.e., the projector)
let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
-- Add the equational theorem for the decl to unfold
diff --git a/backends/lean/Base/ArithBase.lean b/backends/lean/Base/Arith/Base.lean
index ddd2dc24..ddd2dc24 100644
--- a/backends/lean/Base/ArithBase.lean
+++ b/backends/lean/Base/Arith/Base.lean
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 96f7abc0..f109e847 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -14,8 +14,8 @@ namespace Diverge
syntax (name := divergentDef)
declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command
-open Utils
open Lean Elab Term Meta Primitives Lean.Meta
+open Utils
/- The following was copied from the `wfRecursion` function. -/
@@ -47,21 +47,6 @@ def getSigmaTypes (ty : Expr) : MetaM (Expr × Expr) := do
else
pure (args.get! 0, args.get! 1)
-/- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/
-def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
- lambdaTelescope e fun xs body => do
- if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas";
- let xs := xs.extract 0 n
- let ys := xs.extract n xs.size
- let body ← mkLambdaFVars ys body
- k xs body
-
-/- Like `lambdaTelescope`, but only destructs one lambda
- TODO: is there an equivalent of this function somewhere in the
- standard library? -/
-def lambdaOne (e : Expr) (k : Expr → Expr → MetaM α) : MetaM α :=
- lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b
-
/- Generate a Sigma type from a list of *variables* (all the expressions
must be variables).
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 161b9ddb..2ce63620 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -116,4 +116,99 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr :
| .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
visit 0 e
+section Methods
+ variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m]
+ variable {a : Type}
+
+ /- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/
+ def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → m a) : m a :=
+ lambdaTelescope e fun xs body => do
+ if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas"
+ let xs := xs.extract 0 n
+ let ys := xs.extract n xs.size
+ let body ← liftMetaM (mkLambdaFVars ys body)
+ k xs body
+
+ /- Like `lambdaTelescope`, but only destructs one lambda
+ TODO: is there an equivalent of this function somewhere in the
+ standard library? -/
+ def lambdaOne (e : Expr) (k : Expr → Expr → m a) : m a :=
+ lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b
+
+ def isExists (e : Expr) : Bool := e.getAppFn.isConstOf ``Exists ∧ e.getAppNumArgs = 2
+
+ -- Remark: Lean doesn't find the inhabited and nonempty instances if we don'
+ -- put them explicitely in the signature
+ partial def existsTelescopeProcess [Inhabited (m a)] [Nonempty (m a)]
+ (fvars : Array Expr) (e : Expr) (k : Array Expr → Expr → m a) : m a := do
+ -- Attempt to deconstruct an existential
+ if isExists e then do
+ let p := e.appArg!
+ lambdaOne p fun x ne =>
+ existsTelescopeProcess (fvars.push x) ne k
+ else
+ -- No existential: call the continuation
+ k fvars e
+
+ def existsTelescope [Inhabited (m a)] [Nonempty (m a)] (e : Expr) (k : Array Expr → Expr → m a) : m a := do
+ existsTelescopeProcess #[] e k
+
+end Methods
+
+def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
+ -- I don't think we need that
+ Lean.Elab.Tactic.withMainContext do
+ -- Insert the new declaration
+ let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
+ withDecl fun nval => do
+ -- For debugging
+ let lctx ← Lean.MonadLCtx.getLCtx
+ let fid := nval.fvarId!
+ let decl := lctx.get! fid
+ trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+ --
+ -- Tranform the main goal `?m0` to `let x = nval in ?m1`
+ let mvarId ← Tactic.getMainGoal
+ let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
+ let newVal ← mkLetFVars #[nval] newMVar
+ -- There are two cases:
+ -- - asLet is true: newVal is `let $name := $val in $newMVar`
+ -- - asLet is false: ewVal is `λ $name => $newMVar`
+ -- We need to apply it to `val`
+ let newVal := if asLet then newVal else mkAppN newVal #[val]
+ -- Assign the main goal and update the current goal
+ mvarId.assign newVal
+ let goals ← Tactic.getUnsolvedGoals
+ Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
+ -- Return the new value - note: we are in the *new* context, created
+ -- after the declaration was added, so it will persist
+ pure nval
+
+def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
+ -- I don't think we need that
+ Lean.Elab.Tactic.withMainContext do
+ --
+ let val ← elabTerm val .none
+ let type ← inferType val
+ -- In some situations, the type will be left as a metavariable (for instance,
+ -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
+ -- not choose): we force the instantiation of the meta-variable
+ synthesizeSyntheticMVarsUsingDefault
+ --
+ let _ ← addDecl name val type asLet
+
+elab "custom_let " n:ident " := " v:term : tactic => do
+ addDeclSyntax n.getId v (asLet := true)
+
+elab "custom_have " n:ident " := " v:term : tactic =>
+ addDeclSyntax n.getId v (asLet := false)
+
+example : Nat := by
+ custom_let x := 4
+ custom_have y := 4
+ apply y
+
+example (x : Bool) : Nat := by
+ cases x <;> custom_let x := 3 <;> apply x
+
end Utils