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: Oct 13 2024 at 01:02 UTC