The Coq mailing list

[David Singh <david.singh45 AT googlemail.com>]

Dear Coq Club,

I am having trouble with the following proofs about binary trees and I hope someone can give some advice:

Give the following definitions about binary trees and means (TreeEq) of comparing them

---------------------------
 Variables (A : Set) ( Aeq : A -> A -> bool).

 Inductive Tree :     Set :=
   | Node :  A -> Tree
   | Leaf   :  A -> Tree -> Tree -> Tree.

  Fixpoint flatten_aux (a  : A) (x  y: Tree) {struct x} : Tree :=
    match x with 
    | Leaf a' px qx => flatten_aux a' px (flatten_aux a qx y)

    | k => Leaf a k y
    end.

  Fixpoint flatten ( t : Tree) : Tree :=
    match t with
    | Tree l p q => flatten_aux l (flatten p) (flatten q)
    | x => x
    end.

  Fixpoint TreeEq (i j : Tree) {struct i} : bool :=


     match i, j with
     | Node a, Node b => Aeq a b
     | Leaf  l p q , Leaf r x y => Aeq l r && TreeEq p x && TreeEq q y
     | _ , _  => false
     end.
------------

I would expect the following lemma to hold:

 Lemma flatten_aux_true : forall  (p1 p2 p3 p4 : Tree ) (a b : A),
  
TreeEq (flatten_aux a p1 p3) (flatten_aux b p2 p4) = true ->  Aeq a
b = true /\ TreeEq p1 p2 = true /\ TreeEq p3 p4 = true.

Yet I am struggling to prove it. Can anyone give some help?

Many Thanks,