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.
225 lines
6 KiB
Text
225 lines
6 KiB
Text
namespace Ex0
|
||
|
||
-- NB: no parameter
|
||
theorem elim_without_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n :=
|
||
case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_without_param
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_without_param
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using (elim_without_param) -- Error: unexpected eliminator resulting type
|
||
case case1 n => rfl
|
||
|
||
end Ex0
|
||
|
||
namespace Ex1
|
||
|
||
-- NB: p before motive
|
||
theorem elim_with_param (p : Bool) {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n :=
|
||
if p then case1 _ else case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param
|
||
case p => exact true -- uninstantiated parameters becomes goal
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param
|
||
case p => exact true -- uninstantiated parameters becomes goal
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- not really a useful idiom, but it better works:
|
||
induction n using fun motive case1 n => @elim_with_param true motive case1 n
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- NB: no renaming of cases this way?
|
||
induction n using fun motive the_case n => @elim_with_param true motive the_case n
|
||
case case1 n => rfl
|
||
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
|
||
-- NB: p after motive
|
||
theorem elim_with_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) (p : Bool) : motive n :=
|
||
if p then case1 _ else case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param
|
||
case p => exact true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param
|
||
case p => exact true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- This renames the cases with unhelpful names
|
||
induction n using elim_with_param _ _ true
|
||
case x_1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- We can put in custom names
|
||
induction n using elim_with_param ?case2 _ true
|
||
case case2 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- not really a useful idiom, but it works:
|
||
induction n using fun motive case1 n => @elim_with_param motive case1 n true
|
||
case case1 n => rfl
|
||
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
|
||
-- Mutual induction, multiple motives
|
||
|
||
mutual
|
||
inductive A : Type u where | mkA : B → A | A : A
|
||
inductive B : Type u where | mkB : A → B
|
||
end
|
||
|
||
-- NB: A.rec is configured as elab_as_elim,
|
||
-- but in `using` it should not matter
|
||
|
||
-- For comparision, a copy without that attribute
|
||
noncomputable def A_rec := @A.rec
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using A.rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using A_rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial -- Error: type mismatch
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using @A.rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using @A_rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using fun motive_1 => @A.rec motive_1 (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using fun motive_1 => @A_rec motive_1 (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
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
|
||
|
||
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
|
||
|
||
example (a : A) : True := by
|
||
-- A.rec is marked elab_as_elim, and normally elaborating
|
||
-- #check A.rec (motive_2 := fun b => True)
|
||
-- fails with
|
||
-- > failed to elaborate eliminator, expected type is not available
|
||
-- so we elaborate with heedElabAsElim := false
|
||
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
|
||
|
||
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
|
||
|
||
end Ex3
|
||
|
||
namespace Ex4
|
||
|
||
-- We can use parameters as elaborators
|
||
|
||
set_option linter.unusedVariables false in
|
||
example
|
||
(α : Type u)
|
||
(ela : ∀ {motive : α → Prop} (case1 : ∀ (x : α), motive x) (x : α), motive x)
|
||
(x : α)
|
||
: x = x := by
|
||
induction x using ela
|
||
case case1 x => rfl
|
||
|
||
end Ex4
|
||
|
||
namespace Ex5
|
||
|
||
-- Multiple motives, different number of extra assumptions
|
||
|
||
mutual
|
||
inductive A : Type u where | mkA : B → A | A : A
|
||
inductive B : Type u where | mkB : A → B
|
||
end
|
||
|
||
set_option linter.unusedVariables false in
|
||
example (a : A) : True := by
|
||
induction a using A.rec (motive_2 := fun b => (heq : b = b) -> True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH h => exact trivial
|
||
|
||
end Ex5
|