## Stream: math-comp devs

### Topic: size induction

#### Christian Doczkal (Sep 04 2020 at 09:17):

Every time I see this idiom:

``````move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *.
``````

I wonder whether it wouldn't be better to have a lemma for size induction that doesn't talk about the intermediate natural number. (i.e, the `#|P| < n.+1` and `IH : forall x, #|P| < n -> ...`assumptions)

``````(** usage: [elim/(size_ind f) : x] *)
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.
``````

For me, the most common size function is `fun x : <some type> => #|x|`, which is slightly annoying because one has to spell out the type. Unfortunately, I'm not aware of any "type of things one can put into `#|_|`". Hence, I ended up with the following tactic in term wrapper:

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

This way, induction on the size of a finite type (or graph) reduces to `elim/card_ind : G => G IH`. What do you think about this?

Last updated: Jun 01 2023 at 11:01 UTC