The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Tue, Apr 24, 2012 at 07:54:17PM -0400, Adam Chlipala wrote:
> On 04/24/2012 07:47 PM, Bernard Hurley wrote:
>> In the following scenario, is it possible to prove the Lemma?
>>
>> +++++++++++++++++++++++++++
>> Section test.
>>    Variables A B : Set.
>>    Variables f g : A ->  B.
>>
>>    Hypothesis Hyp1: forall a, f a = g a.
>>
>>    Lemma test : f = g.
>>
>> End test.
>> +++++++++++++++++++++++++++
>>    
>
> Short answer: no.
>

So if I had code like:

Inductive nat_tree : Set :=
| NLeaf : nat -> nat_tree
| NNode : (nat -> nat_tree) -> nat_tree.

then [forall n, f n = g n] does not imply [NNode f = NNode g].

Thanks that is very helpful indeed.

Bernard.