Christian Doczkal (May 08 2020 at 08:22): 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)
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