e575736cae
This PR makes `fun_induction` and `fun_cases` (try to) unfold the function application of interest in the goal. The old behavior can be enabled with `set_option tactic.fun_induction.unfolding false`. For `fun_cases` this does not work yet when the function’s result type depends on one of the arguments, see issue #8296.
57 lines
1.9 KiB
Text
57 lines
1.9 KiB
Text
set_option linter.unusedVariables false
|
||
|
||
inductive MyVec (α : Type u) : Nat → Type u where
|
||
| nil : MyVec α 0
|
||
| cons : α → MyVec α n → MyVec α (n + 1)
|
||
|
||
def test (f : Unit → MyVec α n) : Nat :=
|
||
match f () with
|
||
| .nil => 52
|
||
| .cons _ _ => 421
|
||
|
||
/--
|
||
info: test.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||
(case1 :
|
||
∀ {α : Type u_1} (f : Unit → MyVec α 0),
|
||
f () = MyVec.nil →
|
||
motive f
|
||
(match 0, f (), f with
|
||
| .(0), MyVec.nil, f => 52
|
||
| .(n + 1), MyVec.cons a a_1, f => 421))
|
||
(case2 :
|
||
∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||
f () = MyVec.cons a a_1 →
|
||
motive f
|
||
(match n + 1, f (), f with
|
||
| .(0), MyVec.nil, f => 52
|
||
| .(n + 1), MyVec.cons a a_2, f => 421))
|
||
{α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#check test.fun_cases_unfolding
|
||
|
||
def alsoTest (f : Unit → MyVec α n) : Nat :=
|
||
match h : f () with
|
||
| .nil => 52
|
||
| .cons _ _ => 421
|
||
|
||
/--
|
||
info: alsoTest.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||
(case1 :
|
||
∀ {α : Type u_1} (f : Unit → MyVec α 0),
|
||
f () = MyVec.nil →
|
||
motive f
|
||
(match h : 0, h : f (), f with
|
||
| .(0), MyVec.nil, f_1 => 52
|
||
| .(n + 1), MyVec.cons a a_1, f_1 => 421))
|
||
(case2 :
|
||
∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||
f () = MyVec.cons a a_1 →
|
||
motive f
|
||
(match h : n + 1, h : f (), f with
|
||
| .(0), MyVec.nil, f_1 => 52
|
||
| .(n_1 + 1), MyVec.cons a a_2, f_1 => 421))
|
||
{α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#check alsoTest.fun_cases_unfolding
|