tree.v

Require Import Coq.Arith.Mult.

Inductive tree
          (a:  Type)
  : Type :=
| Leaf (x:  a)
  : tree a
| Node (x:  a)
       (l:  tree a)
       (r:  tree a)
  : tree a.

Arguments Leaf [a] (x).
Arguments Node [a] (x l r).

Inductive has_zero
  : tree nat -> Prop :=
| leaf_0
  : has_zero (Leaf 0)
| node_0 (l r:  tree nat)
  : has_zero (Node 0 l r)
| right_0 (x:  nat)
          (l r:  tree nat)
          (H:    has_zero r)
  : has_zero (Node x l r)
| left_0 (x:  nat)
         (l r:  tree nat)
         (H:    has_zero l)
  : has_zero (Node x l r).

Fixpoint mult
         (t:  tree nat)
  : nat :=
  match t with
  | Leaf x
    => x
  | Node x l r
    => x * mult l * mult r
  end.

Lemma has_zero_mult_zero
      (t:  tree nat)
  : has_zero t -> mult t = 0.
Proof.
  intros H.
  induction H.
  + reflexivity.
  + reflexivity.
  + cbn.
    rewrite IHhas_zero.
    rewrite <- mult_n_O.
    reflexivity.
  + cbn.
    rewrite IHhas_zero.
    rewrite <- mult_n_O.
    reflexivity.
Qed.

Lemma mult_zero_has_zero
      (t:  tree nat)
  : mult t = 0 -> has_zero t.
Proof.
  induction t.
  + intro H.
    cbn in H.
    rewrite H.
    constructor.
  + intros Heq.
    cbn in Heq.
    apply mult_is_O in Heq.
    destruct Heq as [Heq|Heq].
    ++ apply mult_is_O in Heq.
       destruct Heq as [Heq|Heq].
       +++ rewrite Heq.
           constructor.
       +++ apply left_0.
           apply IHt1.
           exact Heq.
    ++ apply right_0.
       apply IHt2.
       exact Heq.
Qed.