The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Yes, extensionality helps. Just rely on the following lemma:

<<<
Require Import FunctionalExtensionality.

Lemma eqfun_refl : forall X Y Z f g, eqfun X (Y->Z) f g -> f = g.
Proof.
intros. induction H.
  reflexivity.
  apply functional_extensionality. assumption.
Qed.
>>>

Hugo Herbelin

On Sat, Nov 05, 2011 at 06:40:11AM -0700, Kenneth Roe wrote:
> 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].