The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

You might want to check out FunctionalExtensionality and Classical in the set of standard Coq libraries.  They extend the Coq logic with classical axioms.  If you are not doing function extraction, I would recommend putting in these libraries.  Check out the following URL for more information: http://coq.inria.fr/stdlib/.

                  - Ken

> Date: Sat, 5 Nov 2011 09:31:17 -0400
> From: adamc AT csail.mit.edu
> To: david.leduc6 AT googlemail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] The tactic induction fails :-(
>
> David Leduc wrote:
> > How can I prove the lemma cnuf below?
> >
> > Inductive eqfun : forall X Y, (X->Y) -> (X->Y) -> Prop :=
> > | refl : forall X Y (f:X->Y), eqfun X Y f f
> > | func : forall X Y Z (f g:X->Y->Z), (forall x, eqfun Y Z (f x) (g x))
> > -> eqfun X (Y->Z) f g.
> >
> > Lemma cnuf : forall X Y Z f g, eqfun X (Y->Z) f g -> (forall x, eqfun
> > Y Z (f x) (g x)).
> >
>
> It's not obvious to me that your lemma is provable, even given the full
> set of axioms commonly assumed in Coq developments. You must
> fundamentally do inversion on [eqfun] with a particular function type as
> a parameter, which seems to call for a proof step going from [(D1 -> R1)
> = (D2 -> R2)] to [D1 = D2] and [R1 = R2], but I don't think such a rule
> is provable in CIC, and I don't think any of the common axioms imply the
> soundness of this step. It may be validated by the usual Boolean model
> in ZF, so perhaps it would be consistent to assert this as an axiom.
>
> Or perhaps you could tell us more about the larger context of your
> development, and we could suggest ways to avoid depending on lemma [cnuf].