The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

D. Pucci wrote:
> I am stuck with an apparently very simple prove:
>
> =================================================
> 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?
>
> Can anybody help me?
>
> Thank you in advance.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

Hello,
  In order to prove p1=p2, you have to assume some extentionality, at 
least on functions from bool to bool. Quoting Florent Kirchner, we
can say that extensionality is an axiom in set theory, but from a 
programming point of view, cannot be accepted, since it would identify
any pair of functions which are pointwise equal like, for instance
bubble-sort and quick-sort.
 It is often useful to reason with function equivalence instead of
equiality and to use setoids (see the reference manual)



 In the following lines, I first define equivalence between functions,
and show your functions p1 and p2 are equivalent, inside a section, 
assuming extensionallity for functions from bool to bool, you prove
p1=p2.


 In

http://www.labri.fr/Perso/~casteran/CoqArt/structinduct/tree_bij.html

we (Yves Bertot and me) wrote an exercise to illustrate functional 
extensionality : representing binary trees with functions is possible,
but proving two trees are equal requires extensionality.

Pierre

Here's your example, slighty modified:

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).

Definition fun_equiv (A B:Set)(f g : A->B): Prop := forall a, f a =g a.

Theorem p1_p2_equiv : fun_equiv  _ _ p1 p2.
 unfold p1, p2; intro a ; case a ; simpl; trivial.
 Qed.

 Section bool_ext.
 Hypothesis bool_extensionality : forall (f g: bool -> bool),
                             (fun_equiv _ _ f g)-> f =g.

 Theorem p1_p2_eq : p1=p2.
   apply bool_extensionality.
   apply p1_p2_equiv.
 Qed.

 End bool_ext.




--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran