The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Hey Bernard!
No, it does not. Due to injectivity of constructors, that statement is
equivalent to f = g.

2012/4/25 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.