550fa6994e
right now, the `induction` tactic accepts a custom eliminator using the `using <ident>` syntax, but is restricted to identifiers. This limitation becomes annoying when the elminator has explicit parameters that are not targets, and the user (naturally) wants to be able to write ``` induction a, b, c using foo (x := …) ``` This generalizes the syntax to expressions and changes the code accordingly. This can be used to instantiate a multi-motive induction: ``` example (a : A) : True := by induction a using A.rec (motive_2 := fun b => True) case mkA b IH => exact trivial case A => exact trivial case mkB b IH => exact trivial ``` For this to work the term elaborator learned the `heedElabAsElim` flag, `true` by default. But in the default setting, `A.rec (motive_2 := fun b => True)` would fail to elaborate, because there is no expected type. So the induction tactic will elaborate in a mode where that attribute is simply ignored. As a side effect, the “failed to infer implicit target” error message is improved and prints the name of the implicit target that could not be instantiated.
43 lines
1.2 KiB
Text
43 lines
1.2 KiB
Text
namespace Ex1
|
||
|
||
theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1 : ∀ m n, motive m n) (n : Nat) {m : Nat} : motive m n := case1 _ _
|
||
|
||
example (n m : Nat) : n ≤ m := by
|
||
induction n using elim_with_implicit_target
|
||
case case1 => sorry
|
||
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
|
||
theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1 : ∀ m n, motive m n) {n : Nat} (m : Nat) : motive m n := case1 _ _
|
||
|
||
example (n m : Nat) : n ≤ m := by
|
||
induction m using elim_with_implicit_target
|
||
case case1 => sorry
|
||
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
|
||
-- this one should work
|
||
theorem elim_with_implicit_target (motive : (n : Nat) → Fin n → Prop) (case1 : ∀ m n, motive m n) {n : Nat} (m : Fin n) : motive n m := case1 _ _
|
||
|
||
example (n : Nat) (m : Fin n) : n ≤ m := by
|
||
induction m using elim_with_implicit_target
|
||
case case1 => sorry
|
||
|
||
end Ex3
|
||
|
||
namespace Ex4
|
||
|
||
-- anonymous implicit target
|
||
|
||
theorem elim_with_implicit_target (motive : Bool → Nat → Prop)
|
||
(case1 : ∀ m k, motive m k) {_ : Bool} (m : Nat) : motive ‹Bool› m := case1 _ _
|
||
|
||
example (n m : Nat) : n ≤ m := by
|
||
induction m using elim_with_implicit_target
|
||
case case1 => sorry
|
||
|
||
end Ex4
|