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