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: Feb 09 2023 at 01:03 UTC