Require Arith.
Import nat_scope.
Open Scope nat_scope.
Require ZArith.
Require PolyList.

Inductive aexpr : Set := 
    Var : nat -> aexpr 
  | Plus : aexpr -> aexpr -> aexpr 
  | Num : nat -> aexpr.

Fixpoint interp [v:nat->nat; e:aexpr] : nat := 
   Cases e of (Var x) => (v x)
           | (Plus e1 e2) => (interp v e1)+(interp v e2)
           | (Num n) => n
    end.

Fixpoint flat [e:aexpr] : nat * (list nat) := 
   Cases e of (Var x) => (O,(cons x (nil nat)))
           | (Plus e1 e2) => let (n1,l1) = (flat e1) in 
                             let (n2,l2) = (flat e2) in 
                             ((n1+n2),(app l1 l2) )
           | (Num n) => (n,(nil nat))
    end.

Fixpoint  exprlv [n:nat; l: (list nat)] : aexpr := 
   Cases l of nil => (Num n)
           | (cons x m) => (Plus (Var x) (exprlv n m))
    end.

Definition norm [e:aexpr] : aexpr := 
    let (n,lv)=(flat e) in (exprlv n lv).


Lemma flat_correct : (v:nat->nat)(e:aexpr)
    (interp v e)=(interp v (norm e)).
    
Induction e; Unfold norm; Simpl; Auto.
Intros a1; Case (flat a1); Intros n1 lv1 H1.
Intros a2; Case (flat a2); Intros n2 lv2 H2.
Rewrite H1; Rewrite H2; Clear H1 H2 a1 a2 e.
Induction lv1; Simpl; Auto with zarith.
Induction lv2; Simpl; Auto with zarith.
Save.

Variables x,y,z:nat.
Definition v:= [n]Cases n of 
    0 => x | 1 => y | 2 => z 
   | 3 => (x*y) | _ => O end.

Lemma test :5+x+1+(y+2+(x*y+z))=0.
Change (interp v 
        (Plus (Plus (Plus (Num 5) (Var 0)) (Num 1))
        (Plus (Plus (Var 1) (Num 2)) 
              (Plus (Var 3) (Var 2)))))=O.
Rewrite flat_correct.
Simpl.
Show Proof.