445c8f2ee0
A round of clean-up for the context of the functional induction principle cases. * Already previously, with `match e with | p => …`, functional induction would ensure that `h : e = p` is in scope, but it wouldn’t work in dependent cases. Now it introduces heterogeneous equality where needed (fixes #4146) * These equalities are now added always (previously we omitted them when the discriminant was a variable that occurred in the goal, on the grounds that the goal gets refined through the match, but it’s more consistent to introduce the equality in any case) * We no longer use `MVarId.cleanup` to clean up the goal; it was sometimes too aggressive (fixes #5347) * Instead, we clean up more carefully and with a custom strategy: * First, we substitute all variables without a user-accessible name, if we can. * Then, we substitute all variable, if we can, outside in. * As we do that, we look for `HEq`s that we can turn into `Eq`s to substitute some more * We substitute unused `let`s. **Breaking change**: In some cases leads to a different functional induction principle (different names and order of assumptions, for example).
49 lines
1.4 KiB
Text
49 lines
1.4 KiB
Text
set_option linter.unusedVariables false
|
|
|
|
def bar (n : Nat) : Bool :=
|
|
if h : n = 0 then
|
|
true
|
|
else
|
|
match n with -- NB: the elaborator adds `h` as an discriminant
|
|
| m+1 => bar m
|
|
termination_by n
|
|
|
|
-- set_option pp.match false
|
|
-- #print bar
|
|
-- #check bar.match_1
|
|
-- #print bar.induct
|
|
|
|
-- NB: The induction theorem has both `h` in scope, as its original type mentioning `x`,
|
|
-- and a refined `h` mentioning `m+1`.
|
|
-- The former is redundant here, but will we always know that?
|
|
-- No HEq betwen the two `h`s due to proof irrelevance
|
|
|
|
/--
|
|
info: bar.induct (motive : Nat → Prop) (case1 : motive 0)
|
|
(case2 : ∀ (m : Nat), ¬m + 1 = 0 → ¬m.succ = 0 → motive m → motive m.succ) (n : Nat) : motive n
|
|
-/
|
|
#guard_msgs in
|
|
#check bar.induct
|
|
|
|
def baz (n : Nat) (i : Fin (n+1)) : Bool :=
|
|
if h : n = 0 then
|
|
true
|
|
else
|
|
match n, i + 1 with
|
|
| 1, _ => true
|
|
| m+2, j => baz (m+1) ⟨j.1-1, by omega⟩
|
|
termination_by n
|
|
|
|
-- #print baz._unary
|
|
|
|
/--
|
|
info: baz.induct (motive : (n : Nat) → Fin (n + 1) → Prop) (case1 : ∀ (i : Fin (0 + 1)), motive 0 i)
|
|
(case2 : ¬1 = 0 → ∀ (i : Fin (1 + 1)), ¬1 = 0 → motive 1 i)
|
|
(case3 :
|
|
∀ (m : Nat),
|
|
¬m + 2 = 0 →
|
|
∀ (i : Fin (m.succ.succ + 1)), ¬m.succ.succ = 0 → motive (m + 1) ⟨↑(i + 1) - 1, ⋯⟩ → motive m.succ.succ i)
|
|
(n : Nat) (i : Fin (n + 1)) : motive n i
|
|
-/
|
|
#guard_msgs in
|
|
#check baz.induct
|