2907df22ec
This PR implements RFC #12216: native computation (`native_decide`, `bv_decide`) is represented in the logic as one axiom per computation, asserting the equality that was obtained from the native computation. `#print axiom` will no longer show `Lean.trustCompiler`, but rather the auto-generated names of these axioms (with, for example, `._native.bv_decide.` in the name). See the RFC for more information. This PR introduces a common MetaM helper (`nativeEqTrue`) used by `native_decide` and `bv_decide` alike that runs the computation and then asserts the result using an axiom. It also deprecated the `ofReduceBool` axioms etc. Not included in this PR is infrastructure for enumerating these axioms, prettier `#print axioms` (should we want his) and tactic concurrency. Fixes #12216.
117 lines
2.6 KiB
Text
117 lines
2.6 KiB
Text
import Lean
|
|
/-!
|
|
# `native_decide`
|
|
-/
|
|
|
|
/-!
|
|
Simplest example.
|
|
-/
|
|
theorem ex1 : True := by
|
|
skip
|
|
native_decide
|
|
skip
|
|
/-- info: 'ex1' depends on axioms: [ex1._native.native_decide.ax_1_1] -/
|
|
#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
|
|
|
|
Hint: Use the `+revert` option to automatically clean up 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: have 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
|