feat: decide +revert and improvements to native_decide (#5999)
This PR adds configuration options for `decide`/`decide!`/`native_decide` and refactors the tactics to be frontends to the same backend. Adds a `+revert` option that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makes `native_decide` fail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once). Now `native_decide` supports universe polymorphism. Closes #2072
This commit is contained in:
Kyle Miller
GitHub
parent
4f7aa8c3c8
commit
e3420c08f1
10 changed files with 571 additions and 867 deletions
|
|
@ -1951,7 +1951,7 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
|
|||
instance : DecidableEq UInt8 := UInt8.decEq
|
||||
|
||||
instance : Inhabited UInt8 where
|
||||
default := UInt8.ofNatCore 0 (by decide)
|
||||
default := UInt8.ofNatCore 0 (of_decide_eq_true rfl)
|
||||
|
||||
/-- The size of type `UInt16`, that is, `2^16 = 65536`. -/
|
||||
abbrev UInt16.size : Nat := 65536
|
||||
|
|
@ -1992,7 +1992,7 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
|
|||
instance : DecidableEq UInt16 := UInt16.decEq
|
||||
|
||||
instance : Inhabited UInt16 where
|
||||
default := UInt16.ofNatCore 0 (by decide)
|
||||
default := UInt16.ofNatCore 0 (of_decide_eq_true rfl)
|
||||
|
||||
/-- The size of type `UInt32`, that is, `2^32 = 4294967296`. -/
|
||||
abbrev UInt32.size : Nat := 4294967296
|
||||
|
|
@ -2038,7 +2038,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
|
|||
instance : DecidableEq UInt32 := UInt32.decEq
|
||||
|
||||
instance : Inhabited UInt32 where
|
||||
default := UInt32.ofNatCore 0 (by decide)
|
||||
default := UInt32.ofNatCore 0 (of_decide_eq_true rfl)
|
||||
|
||||
instance : LT UInt32 where
|
||||
lt a b := LT.lt a.toBitVec b.toBitVec
|
||||
|
|
@ -2105,7 +2105,7 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
|
|||
instance : DecidableEq UInt64 := UInt64.decEq
|
||||
|
||||
instance : Inhabited UInt64 where
|
||||
default := UInt64.ofNatCore 0 (by decide)
|
||||
default := UInt64.ofNatCore 0 (of_decide_eq_true rfl)
|
||||
|
||||
/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
|
||||
abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
|
||||
|
|
@ -2113,8 +2113,8 @@ abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
|
|||
theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
|
||||
show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
|
||||
match System.Platform.numBits, System.Platform.numBits_eq with
|
||||
| _, Or.inl rfl => Or.inl (by decide)
|
||||
| _, Or.inr rfl => Or.inr (by decide)
|
||||
| _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
|
||||
| _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
|
||||
|
||||
/--
|
||||
A `USize` is an unsigned integer with the size of a word
|
||||
|
|
@ -2156,8 +2156,8 @@ instance : DecidableEq USize := USize.decEq
|
|||
|
||||
instance : Inhabited USize where
|
||||
default := USize.ofNatCore 0 (match USize.size, usize_size_eq with
|
||||
| _, Or.inl rfl => by decide
|
||||
| _, Or.inr rfl => by decide)
|
||||
| _, Or.inl rfl => of_decide_eq_true rfl
|
||||
| _, Or.inr rfl => of_decide_eq_true rfl)
|
||||
|
||||
/--
|
||||
Upcast a `Nat` less than `2^32` to a `USize`.
|
||||
|
|
@ -2170,7 +2170,7 @@ def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
|
|||
BitVec.ofNatLt n (
|
||||
match System.Platform.numBits, System.Platform.numBits_eq with
|
||||
| _, Or.inl rfl => h
|
||||
| _, Or.inr rfl => Nat.lt_trans h (by decide)
|
||||
| _, Or.inr rfl => Nat.lt_trans h (of_decide_eq_true rfl)
|
||||
)
|
||||
|
||||
/--
|
||||
|
|
@ -2197,8 +2197,8 @@ structure Char where
|
|||
|
||||
private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
|
||||
match h with
|
||||
| Or.inl h => Nat.lt_trans h (by decide)
|
||||
| Or.inr ⟨_, h⟩ => Nat.lt_trans h (by decide)
|
||||
| Or.inl h => Nat.lt_trans h (of_decide_eq_true rfl)
|
||||
| Or.inr ⟨_, h⟩ => Nat.lt_trans h (of_decide_eq_true rfl)
|
||||
|
||||
/--
|
||||
Pack a `Nat` encoding a valid codepoint into a `Char`.
|
||||
|
|
@ -2216,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
|
|||
def Char.ofNat (n : Nat) : Char :=
|
||||
dite (n.isValidChar)
|
||||
(fun h => Char.ofNatAux n h)
|
||||
(fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
|
||||
(fun _ => { val := ⟨BitVec.ofNatLt 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
|
||||
|
||||
theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
|
||||
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
|
||||
|
|
@ -2239,9 +2239,9 @@ instance : DecidableEq Char :=
|
|||
/-- Returns the number of bytes required to encode this `Char` in UTF-8. -/
|
||||
def Char.utf8Size (c : Char) : Nat :=
|
||||
let v := c.val
|
||||
ite (LE.le v (UInt32.ofNatCore 0x7F (by decide))) 1
|
||||
(ite (LE.le v (UInt32.ofNatCore 0x7FF (by decide))) 2
|
||||
(ite (LE.le v (UInt32.ofNatCore 0xFFFF (by decide))) 3 4))
|
||||
ite (LE.le v (UInt32.ofNatCore 0x7F (of_decide_eq_true rfl))) 1
|
||||
(ite (LE.le v (UInt32.ofNatCore 0x7FF (of_decide_eq_true rfl))) 2
|
||||
(ite (LE.le v (UInt32.ofNatCore 0xFFFF (of_decide_eq_true rfl))) 3 4))
|
||||
|
||||
/--
|
||||
`Option α` is the type of values which are either `some a` for some `a : α`,
|
||||
|
|
@ -3480,7 +3480,7 @@ def USize.toUInt64 (u : USize) : UInt64 where
|
|||
let ⟨⟨n, h⟩⟩ := u
|
||||
show LT.lt n _ from
|
||||
match System.Platform.numBits, System.Platform.numBits_eq, h with
|
||||
| _, Or.inl rfl, h => Nat.lt_trans h (by decide)
|
||||
| _, Or.inl rfl, h => Nat.lt_trans h (of_decide_eq_true rfl)
|
||||
| _, Or.inr rfl, h => h
|
||||
)
|
||||
|
||||
|
|
@ -3549,9 +3549,9 @@ with
|
|||
/-- A hash function for names, which is stored inside the name itself as a
|
||||
computed field. -/
|
||||
@[computed_field] hash : Name → UInt64
|
||||
| .anonymous => .ofNatCore 1723 (by decide)
|
||||
| .anonymous => .ofNatCore 1723 (of_decide_eq_true rfl)
|
||||
| .str p s => mixHash p.hash s.hash
|
||||
| .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
|
||||
| .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (of_decide_eq_true rfl)))
|
||||
|
||||
instance : Inhabited Name where
|
||||
default := Name.anonymous
|
||||
|
|
|
|||
|
|
@ -990,13 +990,6 @@ and tries to clear the previous one.
|
|||
-/
|
||||
syntax (name := specialize) "specialize " term : tactic
|
||||
|
||||
macro_rules | `(tactic| trivial) => `(tactic| assumption)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| rfl)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| contradiction)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| decide)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
|
||||
|
||||
/--
|
||||
`unhygienic tacs` runs `tacs` with name hygiene disabled.
|
||||
This means that tactics that would normally create inaccessible names will instead
|
||||
|
|
@ -1156,6 +1149,132 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
|
|||
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
|
||||
macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
|
||||
|
||||
/--
|
||||
Configuration for the `decide` tactic family.
|
||||
-/
|
||||
structure DecideConfig where
|
||||
/-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
|
||||
This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
|
||||
however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
|
||||
kernel : Bool := false
|
||||
/-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
|
||||
admitting the result via the axiom `Lean.ofReduceBool`. This can be significantly more efficient,
|
||||
but it is at the cost of increasing the trusted code base, namely the Lean compiler
|
||||
and all definitions with an `@[implemented_by]` attribute.
|
||||
The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/
|
||||
native : Bool := false
|
||||
/-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
|
||||
zetaReduce : Bool := true
|
||||
/-- If true (default: false), then when preprocessing reverts free variables. -/
|
||||
revert : Bool := false
|
||||
|
||||
/--
|
||||
`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
|
||||
and then reducing that instance to evaluate the truth value of `p`.
|
||||
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
|
||||
|
||||
The target is not allowed to contain local variables or metavariables.
|
||||
If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target,
|
||||
or you can use the `+revert` option, described below.
|
||||
|
||||
Options:
|
||||
- `decide +revert` begins by reverting local variables that the target depends on,
|
||||
after cleaning up the local context of irrelevant variables.
|
||||
A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
|
||||
or if it is a proposition that refers to a relevant variable.
|
||||
- `decide +kernel` uses kernel for reduction instead of the elaborator.
|
||||
It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
|
||||
and (2) it reduces the `Decidable` instance only once instead of twice.
|
||||
- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
|
||||
admitting the result via the `Lean.ofReduceBool` axiom.
|
||||
This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
|
||||
of the trusted code base.
|
||||
Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
|
||||
Like with `+kernel`, the `Decidable` instance is evaluated only once.
|
||||
|
||||
Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term,
|
||||
`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
|
||||
Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms.
|
||||
These can appear in instances defined using tactics (such as `rw` and `simp`).
|
||||
To avoid this, create such instances using definitions such as `decidable_of_iff` instead.
|
||||
|
||||
## Examples
|
||||
|
||||
Proving inequalities:
|
||||
```lean
|
||||
example : 2 + 2 ≠ 5 := by decide
|
||||
```
|
||||
|
||||
Trying to prove a false proposition:
|
||||
```lean
|
||||
example : 1 ≠ 1 := by decide
|
||||
/-
|
||||
tactic 'decide' proved that the proposition
|
||||
1 ≠ 1
|
||||
is false
|
||||
-/
|
||||
```
|
||||
|
||||
Trying to prove a proposition whose `Decidable` instance fails to reduce
|
||||
```lean
|
||||
opaque unknownProp : Prop
|
||||
|
||||
open scoped Classical in
|
||||
example : unknownProp := by decide
|
||||
/-
|
||||
tactic 'decide' failed for proposition
|
||||
unknownProp
|
||||
since its 'Decidable' instance reduced to
|
||||
Classical.choice ⋯
|
||||
rather than to the 'isTrue' constructor.
|
||||
-/
|
||||
```
|
||||
|
||||
## Properties and relations
|
||||
|
||||
For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
|
||||
```lean
|
||||
example : 1 + 1 = 2 := by decide
|
||||
example : 1 + 1 = 2 := by rfl
|
||||
```
|
||||
-/
|
||||
syntax (name := decide) "decide" optConfig : tactic
|
||||
|
||||
/--
|
||||
`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
|
||||
It has the following properties:
|
||||
- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
|
||||
- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
|
||||
and once during kernel type checking), the `decide!` tactic reduces it exactly once.
|
||||
|
||||
The `decide!` syntax is short for `decide +kernel`.
|
||||
-/
|
||||
syntax (name := decideBang) "decide!" optConfig : tactic
|
||||
|
||||
/--
|
||||
`native_decide` is a synonym for `decide +native`.
|
||||
It will attempt to prove a goal of type `p` by synthesizing an instance
|
||||
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
|
||||
uses `#eval` to evaluate the decidability instance.
|
||||
|
||||
This should be used with care because it adds the entire lean compiler to the trusted
|
||||
part, and the axiom `Lean.ofReduceBool` will show up in `#print axioms` for theorems using
|
||||
this method or anything that transitively depends on them. Nevertheless, because it is
|
||||
compiled, this can be significantly more efficient than using `decide`, and for very
|
||||
large computations this is one way to run external programs and trust the result.
|
||||
```lean
|
||||
example : (List.range 1000).length = 1000 := by native_decide
|
||||
```
|
||||
-/
|
||||
syntax (name := nativeDecide) "native_decide" optConfig : tactic
|
||||
|
||||
macro_rules | `(tactic| trivial) => `(tactic| assumption)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| rfl)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| contradiction)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| decide)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
|
||||
macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
|
||||
|
||||
/--
|
||||
The `omega` tactic, for resolving integer and natural linear arithmetic problems.
|
||||
|
||||
|
|
|
|||
|
|
@ -7,9 +7,11 @@ prelude
|
|||
import Lean.Meta.Tactic.Constructor
|
||||
import Lean.Meta.Tactic.Assert
|
||||
import Lean.Meta.Tactic.AuxLemma
|
||||
import Lean.Meta.Tactic.Cleanup
|
||||
import Lean.Meta.Tactic.Clear
|
||||
import Lean.Meta.Tactic.Rename
|
||||
import Lean.Elab.Tactic.Basic
|
||||
import Lean.Elab.Tactic.Config
|
||||
import Lean.Elab.SyntheticMVars
|
||||
|
||||
namespace Lean.Elab.Tactic
|
||||
|
|
@ -347,6 +349,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
|
|||
replaceMainGoal [← (← getMainGoal).rename fvarId h.getId]
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
|
||||
/--
|
||||
Make sure `expectedType` does not contain free and metavariables.
|
||||
It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
|
||||
|
|
@ -355,8 +358,11 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
|
|||
let mut expectedType ← instantiateMVars expectedType
|
||||
if expectedType.hasFVar then
|
||||
expectedType ← zetaReduce expectedType
|
||||
if expectedType.hasFVar || expectedType.hasMVar then
|
||||
throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
|
||||
if expectedType.hasMVar then
|
||||
throwError "expected type must not contain meta variables{indentExpr expectedType}"
|
||||
if expectedType.hasFVar then
|
||||
throwError "expected type must not contain free variables{indentExpr expectedType}\n\
|
||||
Use the '+revert' option to automatically cleanup and revert free variables."
|
||||
return expectedType
|
||||
|
||||
/--
|
||||
|
|
@ -381,36 +387,96 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
|
|||
return ← blameDecideReductionFailure inst''
|
||||
return inst
|
||||
|
||||
def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
|
||||
private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
|
||||
let d ← mkDecide expectedType
|
||||
let levels := (collectLevelParams {} expectedType).params.toList
|
||||
let auxDeclName ← Term.mkAuxName `_nativeDecide
|
||||
let decl := Declaration.defnDecl {
|
||||
name := auxDeclName
|
||||
levelParams := levels
|
||||
type := mkConst ``Bool
|
||||
value := d
|
||||
hints := .abbrev
|
||||
safety := .safe
|
||||
}
|
||||
addAndCompile decl
|
||||
-- get instance from `d`
|
||||
let s := d.appArg!
|
||||
let rflPrf ← mkEqRefl (toExpr true)
|
||||
let levelParams := levels.map .param
|
||||
let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
|
||||
mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
|
||||
try
|
||||
let lemmaName ← mkAuxLemma levels expectedType pf
|
||||
return .const lemmaName levelParams
|
||||
catch ex =>
|
||||
-- Diagnose error
|
||||
throwError MessageData.ofLazyM (es := #[expectedType]) do
|
||||
let r ←
|
||||
try
|
||||
evalConst Bool auxDeclName
|
||||
catch ex =>
|
||||
return m!"\
|
||||
tactic '{tacticName}' failed, could not evaluate decidable instance. \
|
||||
Error: {ex.toMessageData}"
|
||||
if !r then
|
||||
return m!"\
|
||||
tactic '{tacticName}' evaluated that the proposition\
|
||||
{indentExpr expectedType}\n\
|
||||
is false"
|
||||
else
|
||||
return m!"tactic '{tacticName}' failed. Error: {ex.toMessageData}"
|
||||
|
||||
@[implemented_by elabNativeDecideCoreUnsafe]
|
||||
private opaque elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr
|
||||
|
||||
def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
|
||||
if cfg.revert then
|
||||
-- In revert mode: clean up the local context and then revert everything that is left.
|
||||
liftMetaTactic1 fun g => do
|
||||
let g ← g.cleanup
|
||||
let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
|
||||
return g
|
||||
closeMainGoalUsing tacticName fun expectedType _ => do
|
||||
if cfg.kernel && cfg.native then
|
||||
throwError "tactic '{tacticName}' failed, cannot simultaneously set both '+kernel' and '+native'"
|
||||
let expectedType ← preprocessPropToDecide expectedType
|
||||
if cfg.native then
|
||||
elabNativeDecideCore tacticName expectedType
|
||||
else if cfg.kernel then
|
||||
doKernel expectedType
|
||||
else
|
||||
doElab expectedType
|
||||
where
|
||||
doElab (expectedType : Expr) : TacticM Expr := do
|
||||
let pf ← mkDecideProof expectedType
|
||||
-- Get instance from `pf`
|
||||
let s := pf.appFn!.appArg!
|
||||
if kernelOnly then
|
||||
-- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
|
||||
-- The `mkAuxLemma` function caches the result in two ways:
|
||||
-- 1. First, the function makes use of a `type`-indexed cache per module.
|
||||
-- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
|
||||
let levelsInType := (collectLevelParams {} expectedType).params
|
||||
-- Level variables occurring in `expectedType`, in ambient order
|
||||
let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
|
||||
try
|
||||
let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
|
||||
return mkConst lemmaName (lemmaLevels.map .param)
|
||||
catch _ =>
|
||||
diagnose expectedType s none
|
||||
let r ← withAtLeastTransparency .default <| whnf s
|
||||
if r.isAppOf ``isTrue then
|
||||
-- Success!
|
||||
-- While we have a proof from reduction, we do not embed it in the proof term,
|
||||
-- and instead we let the kernel recompute it during type checking from the following more
|
||||
-- efficient term. The kernel handles the unification `e =?= true` specially.
|
||||
return pf
|
||||
else
|
||||
let r ← withAtLeastTransparency .default <| whnf s
|
||||
if r.isAppOf ``isTrue then
|
||||
-- Success!
|
||||
-- While we have a proof from reduction, we do not embed it in the proof term,
|
||||
-- and instead we let the kernel recompute it during type checking from the following more
|
||||
-- efficient term. The kernel handles the unification `e =?= true` specially.
|
||||
return pf
|
||||
else
|
||||
diagnose expectedType s r
|
||||
where
|
||||
diagnose expectedType s r
|
||||
doKernel (expectedType : Expr) : TacticM Expr := do
|
||||
let pf ← mkDecideProof expectedType
|
||||
-- Get instance from `pf`
|
||||
let s := pf.appFn!.appArg!
|
||||
-- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
|
||||
-- The `mkAuxLemma` function caches the result in two ways:
|
||||
-- 1. First, the function makes use of a `type`-indexed cache per module.
|
||||
-- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
|
||||
let levelsInType := (collectLevelParams {} expectedType).params
|
||||
-- Level variables occurring in `expectedType`, in ambient order
|
||||
let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
|
||||
try
|
||||
let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
|
||||
return mkConst lemmaName (lemmaLevels.map .param)
|
||||
catch _ =>
|
||||
diagnose expectedType s none
|
||||
diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α :=
|
||||
-- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
|
||||
throwError MessageData.ofLazyM (es := #[expectedType]) do
|
||||
|
|
@ -470,30 +536,20 @@ where
|
|||
did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``isFalse}'.\n\n\
|
||||
{stuckMsg}{hint}"
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
|
||||
evalDecideCore `decide false
|
||||
declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
|
||||
evalDecideCore `decide! true
|
||||
@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
|
||||
let cfg ← elabDecideConfig stx[1]
|
||||
evalDecideCore `decide cfg
|
||||
|
||||
private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
|
||||
let auxName ← Term.mkAuxName baseName
|
||||
let decl := Declaration.defnDecl {
|
||||
name := auxName, levelParams := [], type, value
|
||||
hints := .abbrev
|
||||
safety := .safe
|
||||
}
|
||||
addDecl decl
|
||||
compileDecl decl
|
||||
pure auxName
|
||||
@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
|
||||
let cfg ← elabDecideConfig stx[1]
|
||||
let cfg := { cfg with kernel := true }
|
||||
evalDecideCore `decide! cfg
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
|
||||
closeMainGoalUsing `nativeDecide fun expectedType _ => do
|
||||
let expectedType ← preprocessPropToDecide expectedType
|
||||
let d ← mkDecide expectedType
|
||||
let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d
|
||||
let rflPrf ← mkEqRefl (toExpr true)
|
||||
let s := d.appArg! -- get instance from `d`
|
||||
return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf
|
||||
@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
|
||||
let cfg ← elabDecideConfig stx[1]
|
||||
let cfg := { cfg with native := true }
|
||||
evalDecideCore `native_decide cfg
|
||||
|
||||
end Lean.Elab.Tactic
|
||||
|
|
|
|||
|
|
@ -67,90 +67,6 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode.
|
|||
@[builtin_tactic_parser] def introMatch := leading_parser
|
||||
nonReservedSymbol "intro" >> matchAlts
|
||||
|
||||
/--
|
||||
`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
|
||||
and then reducing that instance to evaluate the truth value of `p`.
|
||||
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
|
||||
|
||||
Limitations:
|
||||
- The target is not allowed to contain local variables or metavariables.
|
||||
If there are local variables, you can try first using the `revert` tactic with these local variables
|
||||
to move them into the target, which may allow `decide` to succeed.
|
||||
- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
|
||||
by well-founded recursion might not work, because evaluating them requires reducing proofs.
|
||||
The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
|
||||
These can appear for instances defined using tactics (such as `rw` and `simp`).
|
||||
To avoid this, use definitions such as `decidable_of_iff` instead.
|
||||
|
||||
## Examples
|
||||
|
||||
Proving inequalities:
|
||||
```lean
|
||||
example : 2 + 2 ≠ 5 := by decide
|
||||
```
|
||||
|
||||
Trying to prove a false proposition:
|
||||
```lean
|
||||
example : 1 ≠ 1 := by decide
|
||||
/-
|
||||
tactic 'decide' proved that the proposition
|
||||
1 ≠ 1
|
||||
is false
|
||||
-/
|
||||
```
|
||||
|
||||
Trying to prove a proposition whose `Decidable` instance fails to reduce
|
||||
```lean
|
||||
opaque unknownProp : Prop
|
||||
|
||||
open scoped Classical in
|
||||
example : unknownProp := by decide
|
||||
/-
|
||||
tactic 'decide' failed for proposition
|
||||
unknownProp
|
||||
since its 'Decidable' instance reduced to
|
||||
Classical.choice ⋯
|
||||
rather than to the 'isTrue' constructor.
|
||||
-/
|
||||
```
|
||||
|
||||
## Properties and relations
|
||||
|
||||
For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
|
||||
```lean
|
||||
example : 1 + 1 = 2 := by decide
|
||||
example : 1 + 1 = 2 := by rfl
|
||||
```
|
||||
-/
|
||||
@[builtin_tactic_parser] def decide := leading_parser
|
||||
nonReservedSymbol "decide"
|
||||
|
||||
/--
|
||||
`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
|
||||
It has the following properties:
|
||||
- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
|
||||
- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
|
||||
and once during kernel type checking), the `decide!` tactic reduces it exactly once.
|
||||
-/
|
||||
@[builtin_tactic_parser] def decideBang := leading_parser
|
||||
nonReservedSymbol "decide!"
|
||||
|
||||
/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
|
||||
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
|
||||
uses `#eval` to evaluate the decidability instance.
|
||||
|
||||
This should be used with care because it adds the entire lean compiler to the trusted
|
||||
part, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using
|
||||
this method or anything that transitively depends on them. Nevertheless, because it is
|
||||
compiled, this can be significantly more efficient than using `decide`, and for very
|
||||
large computations this is one way to run external programs and trust the result.
|
||||
```
|
||||
example : (List.range 1000).length = 1000 := by native_decide
|
||||
```
|
||||
-/
|
||||
@[builtin_tactic_parser] def nativeDecide := leading_parser
|
||||
nonReservedSymbol "native_decide"
|
||||
|
||||
builtin_initialize
|
||||
register_parser_alias "matchRhsTacticSeq" matchRhs
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,3 @@
|
|||
1825.lean:2:8-2:13: error: application type mismatch
|
||||
Lean.ofReduceBool boom'._nativeDecide_1 true (Eq.refl true)
|
||||
argument has type
|
||||
true = true
|
||||
but function has type
|
||||
Lean.reduceBool boom'._nativeDecide_1 = true → boom'._nativeDecide_1 = true
|
||||
1825.lean:2:71-2:84: error: tactic 'native_decide' evaluated that the proposition
|
||||
-2147483648 + 2147483648 = -18446744069414584320
|
||||
is false
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -11,12 +11,9 @@ info: 12776324570088369205
|
|||
#eval (123456789012345678901).toUInt64.toNat
|
||||
|
||||
/--
|
||||
error: application type mismatch
|
||||
Lean.ofReduceBool false._nativeDecide_1 true (Eq.refl true)
|
||||
argument has type
|
||||
true = true
|
||||
but function has type
|
||||
Lean.reduceBool false._nativeDecide_1 = true → false._nativeDecide_1 = true
|
||||
error: tactic 'native_decide' evaluated that the proposition
|
||||
(Nat.toUInt64 123456789012345678901).toNat = 123456789012345678901
|
||||
is false
|
||||
-/
|
||||
#guard_msgs in
|
||||
theorem false : False := by
|
||||
|
|
|
|||
|
|
@ -69,3 +69,28 @@ info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
|
|||
decideBang._auxLemma.3
|
||||
-/
|
||||
#guard_msgs in #print thm1'
|
||||
|
||||
|
||||
/-!
|
||||
Reverting free variables.
|
||||
-/
|
||||
|
||||
/--
|
||||
error: expected type must not contain free variables
|
||||
x + 1 ≤ 5
|
||||
Use the '+revert' option to automatically cleanup and revert free variables.
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide!
|
||||
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide! +revert
|
||||
|
||||
|
||||
/--
|
||||
Can handle universe levels.
|
||||
-/
|
||||
|
||||
instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) :=
|
||||
decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h)
|
||||
|
||||
example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide!
|
||||
|
|
|
|||
130
tests/lean/run/decideNative.lean
Normal file
130
tests/lean/run/decideNative.lean
Normal file
|
|
@ -0,0 +1,130 @@
|
|||
import Lean
|
||||
/-!
|
||||
# `native_decide`
|
||||
-/
|
||||
|
||||
/-!
|
||||
Simplest example.
|
||||
-/
|
||||
theorem ex1 : True := by native_decide
|
||||
/-- info: 'ex1' depends on axioms: [Lean.ofReduceBool] -/
|
||||
#guard_msgs in #print axioms ex1
|
||||
|
||||
|
||||
/-!
|
||||
The decidable instance is only evaluated once.
|
||||
It is evaluated at elaboration time, hence stdout can be collected by `collect_stdout`.
|
||||
-/
|
||||
|
||||
elab "collect_stdout " t:tactic : tactic => do
|
||||
let (out, _) ← IO.FS.withIsolatedStreams <| Lean.Elab.Tactic.evalTactic t
|
||||
Lean.logInfo m!"output: {out}"
|
||||
|
||||
def P (n : Nat) := ∃ k, n = 2 * k
|
||||
|
||||
instance instP : DecidablePred P :=
|
||||
fun
|
||||
| 0 => isTrue ⟨0, rfl⟩
|
||||
| 1 => isFalse (by intro ⟨k, h⟩; omega)
|
||||
| n + 2 =>
|
||||
dbg_trace "step";
|
||||
match instP n with
|
||||
| isTrue h => isTrue (by have ⟨k, h⟩ := h; exact ⟨k + 1, by omega⟩)
|
||||
| isFalse h => isFalse (by intro ⟨k, h'⟩; apply h; exists k - 1; omega)
|
||||
|
||||
/-- info: output: step -/
|
||||
#guard_msgs in example : P 2 := by collect_stdout native_decide
|
||||
|
||||
|
||||
/-!
|
||||
The `native_decide` tactic can fail at elaboration time, rather than waiting until kernel checking.
|
||||
-/
|
||||
|
||||
-- Check the error message
|
||||
/--
|
||||
error: tactic 'native_decide' evaluated that the proposition
|
||||
False
|
||||
is false
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : False := by native_decide
|
||||
|
||||
/--
|
||||
error: second case
|
||||
⊢ False
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : False := by first | native_decide | fail "second case"
|
||||
|
||||
|
||||
/-!
|
||||
Reverting free variables.
|
||||
-/
|
||||
|
||||
/--
|
||||
error: expected type must not contain free variables
|
||||
x + 1 ≤ 5
|
||||
Use the '+revert' option to automatically cleanup and revert free variables.
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by native_decide
|
||||
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by native_decide +revert
|
||||
|
||||
|
||||
/-!
|
||||
Make sure `native_decide` fails at elaboration time.
|
||||
https://github.com/leanprover/lean4/issues/2072
|
||||
-/
|
||||
|
||||
/--
|
||||
error: tactic 'native_decide' evaluated that the proposition
|
||||
False
|
||||
is false
|
||||
---
|
||||
info: let_fun this := sorry;
|
||||
this : False
|
||||
-/
|
||||
#guard_msgs in #check show False by native_decide
|
||||
|
||||
|
||||
/--
|
||||
Can handle universe levels.
|
||||
-/
|
||||
|
||||
instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) :=
|
||||
decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h)
|
||||
|
||||
example : ∀ (x : PUnit.{u}), x = PUnit.unit := by native_decide
|
||||
|
||||
|
||||
/-!
|
||||
Can't evaluate
|
||||
-/
|
||||
|
||||
inductive ItsTrue : Prop
|
||||
| mk
|
||||
|
||||
instance : Decidable ItsTrue := sorry
|
||||
|
||||
/--
|
||||
error: tactic 'native_decide' failed, could not evaluate decidable instance.
|
||||
Error: cannot evaluate code because 'instDecidableItsTrue' uses 'sorry' and/or contains errors
|
||||
-/
|
||||
#guard_msgs in example : ItsTrue := by native_decide
|
||||
|
||||
|
||||
/-!
|
||||
Panic during evaluation
|
||||
-/
|
||||
|
||||
inductive ItsTrue2 : Prop
|
||||
| mk
|
||||
|
||||
instance : Decidable ItsTrue2 :=
|
||||
have : Inhabited (Decidable ItsTrue2) := ⟨isTrue .mk⟩
|
||||
panic! "oh no"
|
||||
|
||||
-- Note: this test fails within VS Code
|
||||
/-- info: output: PANIC at instDecidableItsTrue2 decideNative:126:2: oh no -/
|
||||
#guard_msgs in example : ItsTrue2 := by collect_stdout native_decide
|
||||
|
|
@ -52,7 +52,7 @@ example : unknownProp := by decide
|
|||
Reporting unfolded instances and give hint about Eq.rec.
|
||||
From discussion with Heather Macbeth on Zulip
|
||||
-/
|
||||
structure Nice (n : Nat) : Prop :=
|
||||
structure Nice (n : Nat) : Prop where
|
||||
(large : 100 ≤ n)
|
||||
|
||||
theorem nice_iff (n : Nat) : Nice n ↔ 100 ≤ n := ⟨Nice.rec id, Nice.mk⟩
|
||||
|
|
@ -102,3 +102,28 @@ defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of func
|
|||
-/
|
||||
#guard_msgs in
|
||||
example : ¬ Nice 102 := by decide
|
||||
|
||||
|
||||
/-!
|
||||
Reverting free variables.
|
||||
-/
|
||||
|
||||
/--
|
||||
error: expected type must not contain free variables
|
||||
x + 1 ≤ 5
|
||||
Use the '+revert' option to automatically cleanup and revert free variables.
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide
|
||||
|
||||
example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +revert
|
||||
|
||||
|
||||
/--
|
||||
Can handle universe levels.
|
||||
-/
|
||||
|
||||
instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) :=
|
||||
decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h)
|
||||
|
||||
example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue