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)

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: Jul 15 2024 at 21:02 UTC