The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

Hello,


> =================================================
> Parameter f: bool -> bool -> bool.
> 
> Definition p1 := fun a: bool => (if a then (f false) else (f true)) a.
> 
> Definition p2 := fun a: bool => if a then (f false a) else (f true a).
> 
> Theorem abc: p1 = p2.
> =================================================
> 
> Shouldn't this be provable by reducing p1 and p2 to the same normal form?

One could imagine that the corresponding reduction would be added to Coq's 
type theory (actually it is a form of what is called "commutative cut" in 
the proof theory literature, see eg.  "Proofs and Types"). If this were 
the case, you could indeed prove the equality by reflexivity.

Since it is not the case for the moment, you cannot prove your equality as 
stated. p1 and p2 are extentionaly equal, that is:

forall b : bool, (p1 b) = (p2 b)

which is proved by case analysis  over b.

See many previous posts on extentionaly equal functions vs. intentionaly 
equal functions.


Good luck,


Benjamin Werner