The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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/

Attachment: signature.asc
Description: This is a digitally signed message part