61186629d6
This PR implements the option `revert`, which is set to `false` by default. To recover the old `grind` behavior, you should use `grind +revert`. Previously, `grind` used the `RevSimpIntro` idiom, i.e., it would revert all hypotheses and then re-introduce them while simplifying and applying eager `cases`. This idiom created several problems: * Users reported that `grind` would include unnecessary parameters. See [here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20aggressively.20includes.20local.20hypotheses.2E/near/554887715). * Unnecessary section variables were also being introduced. See the new test contributed by Sebastian Graf. * Finally, it prevented us from supporting arbitrary parameters as we do in `simp`. In `simp`, I implemented a mechanism that simulates local universe-polymorphic theorems, but this approach could not be used in `grind` because there is no mechanism for reverting (and re-introducing) local universe-polymorphic theorems. Adding such a mechanism would require substantial work: I would need to modify the local context object. I considered maintaining a substitution from the original variables to the new ones, but this is also tricky, because the mapping would have to be stored in the `grind` goal objects, and it is not just a simple mapping. After reverting everything, I would need to keep a sequence of original variables that must be added to the mapping as we re-introduce them, but eager case splits complicate this quite a bit. The whole approach felt overly messy. The new behavior `grind -revert` addresses all these issues. None of the `grind` proofs in our test suite broke after we fixed the bugs exposed by the new feature. That said, the traces and counterexamples produced by `grind` are different. The new proof terms are also different.
76 lines
2.6 KiB
Text
76 lines
2.6 KiB
Text
inductive L (α : Type u) : Type u where
|
||
| nil : L α
|
||
| cons (x : α) (xs : L α) : L α
|
||
|
||
-- Check that L.cons.inj uses the per-ctor noConfusion principle
|
||
/--
|
||
info: theorem L.cons.inj.{u} : ∀ {α : Type u} {x : α} {xs : L α} {x_1 : α} {xs_1 : L α},
|
||
L.cons x xs = L.cons x_1 xs_1 → x = x_1 ∧ xs = xs_1 :=
|
||
fun {α} {x} {xs} {x_1} {xs_1} x_2 =>
|
||
L.cons.noConfusion (x = x_1 ∧ xs = xs_1) x xs x_1 xs_1 x_2 fun x_eq xs_eq => ⟨x_eq, xs_eq⟩
|
||
-/
|
||
#guard_msgs in
|
||
#print L.cons.inj
|
||
|
||
-- Check that injection uses the per-ctor noConfusion principle
|
||
|
||
theorem ex1 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
|
||
injection h
|
||
repeat constructor <;> assumption
|
||
|
||
/--
|
||
info: theorem ex1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
|
||
L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
|
||
fun {α} {x} {xs} {y} {ys} h => L.cons.noConfusion (x = y ∧ xs = ys) x xs y ys h fun x_eq xs_eq => ⟨x_eq, xs_eq⟩
|
||
-/
|
||
#guard_msgs in #print ex1
|
||
|
||
-- Check that injection does not intro more than it should
|
||
theorem ex2 (h : L.cons x xs = L.cons y ys) : Unit → x = y ∧ xs = ys := by
|
||
injection h
|
||
intro u
|
||
repeat constructor <;> assumption
|
||
|
||
-- Check that grind uses `L.cons.noConfusion`
|
||
|
||
theorem ex3 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
|
||
grind
|
||
/--
|
||
info: theorem ex3._proof_1_1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
|
||
L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
|
||
fun {α} {x} {xs} {y} {ys} h =>
|
||
Classical.byContradiction
|
||
(Lean.Grind.intro_with_eq (¬(x = y ∧ xs = ys)) (¬x = y ∨ ¬xs = ys) False (Lean.Grind.not_and (x = y) (xs = ys))
|
||
fun h_1 =>
|
||
id
|
||
(Eq.mp
|
||
(Eq.trans (Eq.symm (eq_true (L.cons.inj (id h)).1))
|
||
(Lean.Grind.eq_false_of_not_eq_true
|
||
(Eq.trans
|
||
(Eq.symm
|
||
(Lean.Grind.or_eq_of_eq_false_right (Lean.Grind.not_eq_of_eq_true (eq_true (L.cons.inj (id h)).2))))
|
||
(eq_true h_1))))
|
||
True.intro))
|
||
-/
|
||
#guard_msgs in #print ex3._proof_1_1
|
||
|
||
|
||
-- Check that for numary constructors, we get a trivial inlined “no confusion” principle
|
||
|
||
inductive AlmostEnum where | a | b | mk (b : Bool)
|
||
|
||
-- No explicit noConfusion principle for `AlmostEnum.a`:
|
||
/-- error: Unknown constant `AlmostEnum.a.noConfusion` -/
|
||
#guard_msgs in #print sig AlmostEnum.a.noConfusion
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
theorem ex4 (h : AlmostEnum.a = AlmostEnum.a) : True := by
|
||
injection h
|
||
trivial
|
||
|
||
/--
|
||
info: theorem ex4 : AlmostEnum.a = AlmostEnum.a → True :=
|
||
fun h => (fun P => P) True.intro
|
||
-/
|
||
#guard_msgs in #print ex4
|