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: Apr 20 2024 at 06:02 UTC