Stream: math-comp users

Topic: induction lemmas

view this post on Zulip Christian Doczkal (May 08 2020 at 08:22):

Hi, I was toying around with induction lemmas (i.e., lemmas to be used with elim/). I created one for size induction (I'm not a fan of the have [m] := ubnP ... ; elim: m ... idiom):

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.
Arguments size_ind [X] f [P].

This I can use as elim/(size_ind f). However, in more than half of my instances f is fun x : T => #|x| for some T. I even introduced a notation for this Notation card_ind T := (size_ind (fun x : T => #|x|)). However, this still forces me to give the type T, which is always the type of the variable one is doing induction on. Is there a lemma that can be used as elim/card_ind. I tried:

Lemma card_ind' (T : finType) (pT : predType T) (P : pT -> Type) :
  (forall x : pT, (forall y : pT, (#|y| < #|x|) -> P y) -> P x) -> forall x : pT, P x.

this works when the goal is of the form forall A : pred T, ... for some finite type T, but it fails for forall T : finType, ... and forall A : {set T}, .... . (This message was posted to the math-comp/Lobby after the export)

view this post on Zulip Christian Doczkal (May 11 2020 at 10:48):

I realized that one can use tactics in terms to obtain the behavior I want. That is, one can do the following:

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

this allows elim/card_ind on anything for which #|_| is defined (at least on anything I have tried), because ?X gets instantiated to the type of _top_assumption_ during the execution of elim/card_ind. Still, I am curious whether this Ltac trickery can be avoided by a suitably typed lemma.

Last updated: Feb 08 2023 at 07:02 UTC