The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Joachim,

I like this trick. Crafting induction principles is an efficient way to
ease proofs. I think ikdc is right: Derive is what you want.

I have several questions:
1) do you use functional induction in the proof of foo_ind_aux? It seems to
be a good idea.
2) I would expect (P x (foo x)) for the conclusion of foo_ind_aux instead
of (P (foo x)). Did you just simplify your example or do you manage to use
it like that?
3) the shape of this "functional scheme" is probably not accepted by
"induction ... using foo_ind". Does it? Or do you have to apply the
principle by hand?
Best regards
P.



Le mer. 16 mai 2018 à 17:55, ikdc 
<ikdc AT mit.edu>
 a écrit :

> The Derive extension does what you want.

> https://coq.inria.fr/refman/addendum/miscellaneous-extensions.html



> On May 16, 2018 11:38, Joachim Breitner 
> <mail AT joachim-breitner.de>
>  wrote:

> Hi,

> I am experimenting right now with something like this:

>    Lemma foo_ind_aux:
>      forall (P : _ -> Prop),
>      { IHs : Prop |
>        IHs -> forall x, WellFormed x -> P (foo x)
>      }.
>    Proof. intros P. eexists. intro IHs. … Defined.

>    Definition foo_ind P := proj2_sig (foo_ind_aux P).

> The context is that I have a complex function `foo` with a few cases,
> and a predicate `WellFormed` on its domain. Previously, I had multiple
> proofs about `foo`, with different conclusions, but all of them
> duplicated a lot of structure; in particular every invocation of the
> inductive hypothesis would repeat the same proofs to satisfy the
> WellFormed-obligation of the inductive hypothesis.

> With the above trick, I can do this once and for all and essentially
> define a “functional induction scheme with built-in invariant
> handling”. The neat thing is that I don't have to spell out the (rather
> big) preconditions, but rather leave them as existential. When I then
> use them in foo_ind_aux, Coq learns their actual type.
> At the end, IHs is the conjunction of all the proof obligations that
> you would expect in such an induction lemma.


> But what I’d really like to do is to write directly

>    Lemma foo_ind:
>      forall (P : _ -> Prop) (IH1 : ?_) (IH2 : ?_),
>      forall x, WellFormed x -> P (foo x)
>    Proof. intros P IH1 IH2. … Qed.

> where ?_ introduces an existential variable for the type of these
> hypotheses that will become concrete during the proof.


> Is a way of doing that?

> Thanks,
> Joachim

> --
> Joachim Breitner
>    
> mail AT joachim-breitner.de
>    http://www.joachim-breitner.de/