The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

On Fri, Sep 4, 2009 at 4:58 AM, David 
Singh<david.singh45 AT googlemail.com>
 wrote:
> ---------------------------
>  Variables (A : Set) ( Aeq : A -> A -> bool).
>
>  Inductive Tree :     Set :=
>    | Node :  A -> Tree
>    | Leaf   :  A -> Tree -> Tree -> Tree.

Your terminology is strange, and threw me off for a while.  Usually a
"leaf" is a tree with no subtrees.  The more conventional naming would
be:

Inductive Tree : Set :=
  | Leaf : A -> Tree
  | Branch : 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.

You are matching against Tree here?  That doesn't make any sense, and
oughtn't type check.  You will find we spend more time trying to help
you if we can see you have spent time yourself...

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

I don't think this lemma is true.  flatten_aux essentially destroys
the structure of a tree and turns it into an in-order list of
elements.  What you are asking from the lemma is that if two trees'
lists of elements are equal, then the trees themselves are equal,
which is false.

flatten_aux_true isn't a terribly descriptive name.  What intuitive
property are you trying to prove?

Luke