## Stream: math-comp users

### Topic: induction lemmas

#### Christian Doczkal (May 08 2020 at 08:22):

Hi, I was toying around with induction lemmas (i.e., lemmas to be used with `elim/`). I created one for size induction (I'm not a fan of the `have [m] := ubnP ... ; elim: m ...` idiom):

``````Lemma size_ind (X : Type) (f : X -> nat) (P : X -> Type) :
(forall x, (forall y, (f y < f x) -> P y) -> P x) -> forall x, P x.
Arguments size_ind [X] f [P].
``````

This I can use as `elim/(size_ind f)`. However, in more than half of my instances f is `fun x : T => #|x|` for some `T`. I even introduced a notation for this `Notation card_ind T := (size_ind (fun x : T => #|x|))`. However, this still forces me to give the type `T`, which is always the type of the variable one is doing induction on. Is there a lemma that can be used as `elim/card_ind`. I tried:

``````Lemma card_ind' (T : finType) (pT : predType T) (P : pT -> Type) :
(forall x : pT, (forall y : pT, (#|y| < #|x|) -> P y) -> P x) -> forall x : pT, P x.
``````

this works when the goal is of the form `forall A : pred T, ...` for some finite type `T`, but it fails for `forall T : finType, ...` and forall `A : {set T}, .... `. (This message was posted to the math-comp/Lobby after the export)

#### Christian Doczkal (May 11 2020 at 10:48):

I realized that one can use tactics in terms to obtain the behavior I want. That is, one can do the following:

``````Notation card_ind :=
(size_ind (fun x : (ltac:(match goal with  [ _ : ?X |- _ ] => exact X end)) => #|x|))
(only parsing).
``````

this allows `elim/card_ind` on anything for which `#|_|` is defined (at least on anything I have tried), because `?X` gets instantiated to the type of `_top_assumption_` during the execution of elim/card_ind. Still, I am curious whether this Ltac trickery can be avoided by a suitably typed lemma.

Last updated: Feb 08 2023 at 07:02 UTC