The Coq mailing list

[Matthieu Sozeau <mattam AT altern.org>]

Hello coqers (?),
        I'm learning Coq using the Coq'Art book and found exercise 5.28 (page 
172) 
particularly difficult. We define f1 : Z_btree -> Z_fbtree and f2 : Z_fbtree 
-> Z_btree to be conversion functions between two binary tree 
representations. Then one must prove (t:Z_btree) (f2 (f1 t)) = t which is 
quite doable and (t:Z_fbtree) (f1 (f2 t)) = t. 
This one requires two things: 
        First, to prove (1) z0=([b0:bool](z0 b0)), you need an h-reduction(/ 
contraction) axiom as it isn't included in Coq's reduction rules. A "Remark" 
in the ref. manual state exactly that, but with no explanation, so I ask you, 
why not include it or make it easily accessible ? also, is (1) provable in 
Coq without it ? 
        Second, i ended up with a term of the form : 
 [b0:bool](z0 b0) = [b0:bool](if b0 then (z0 true) else (z0 false)) which, as 
I understand it now (after searching a few hours(!)), requires an 
extensionality axiom like: (b:A)((f b) = (g b)) -> ([b:A](f b)) = ([b:A](g 
b)) or (b:A)((f b) = (g b)) -> (f b) = (g b) to be proven. The extensionality 
problem is not discussed before this exercice so I found it quite mean not to 
give any hint, although I may have taken the wrong path in the proof. Anyway, 
I'd like to know how experienced users would have solved it. 

My solution is attached.
--
Matthieu Sozeau
Require ZArith.

Inductive Z_btree : Set :=
 | Z_leaf : Z_btree
 | Z_node : Z -> Z_btree -> Z_btree -> Z_btree.

Inductive Z_fbtree : Set :=
 | Z_fbleaf : Z_fbtree
 | Z_fbnode : Z -> (bool -> Z_fbtree) -> Z_fbtree.

Section Exercice5'28.

Fixpoint f1 [t:Z_btree] : Z_fbtree :=
 Cases t of 
 | Z_leaf => Z_fbleaf
 | (Z_node v l r) =>
  let (l',r') = (f1 l, f1 r) in
   (Z_fbnode v [b:bool](if b then l' else r'))
 end.

Fixpoint f2 [t:Z_fbtree] : Z_btree :=
  Cases t of
  | Z_fbleaf => Z_leaf
  | (Z_fbnode v f) => 
   let (l,r) = (f2 (f true), f2 (f false)) in
    (Z_node v l r)
  end.

Theorem f2f1_eq_id : (t:Z_btree)(f2 (f1 t)) = t.
Proof.
  Intros t.
  Induction t.
  Auto.
  Replace (f2 (f1 (Z_node z t1 t0))) with (Z_node z (f2 (f1 t1)) (f2 (f1 
t0))).
  Rewrite Hrect1.
  Rewrite Hrect0.
  Trivial.
  Unfold f1 ; Unfold f2 ; Trivial.
Qed.

(* FIXME: Where is it defined ? h-reduction is not included in Coq's conv 
rules *)
Axiom hreduction : (A,B:Set; f:A -> B) f = [x:A](f x).

Lemma if_app_unused : (A:Set; f:bool -> A)
 (b:bool) ((f b) = (if b then (f true) else (f false))).
Proof.
  Intros A f b.
  Case b ; Reflexivity.
Qed.

Require Classical_Pred_Set.

(* FIXME: How-to prove that ? : seems impossible: 
http://www.irit.fr/zeno/sujets/sujets-2003-2004.html *)
Axiom for_all_difficult : (A,B:Set; f,g:A -> B)
 (b:A)((f b) = (g b)) -> ([b:A](f b)) = ([b:A](g b)).

Hypothesis b : bool.

Theorem f1f2_eq_id : (t:Z_fbtree)(f1 (f2 t)) = t.
Proof.
  Induction t.
  Trivial.
  Intros z z0 H.
  Unfold f1 ; Unfold f2.
  Rewrite H ; Rewrite H.
  Replace [b:bool](if b then (z0 true) else (z0 false)) with z0.
  Reflexivity.
  Transitivity [b:bool](z0 b).
  Apply hreduction.
  Apply (for_all_difficult ? ? z0 ([b:bool](if b then (z0 true) else (z0 
false))) b).
  Apply if_app_unused.
Qed.

End Exercice5'28.