folder.coq

Inductive Expr : Type :=
  | Const : nat -> Expr
  | Add : Expr -> Expr -> Expr 
  | Mul : Expr -> Expr -> Expr.

Fixpoint eval (e : Expr) : nat :=
  match e with
  | Const n => n
  | Add e1 e2 => eval e1 + eval e2
  | Mul e1 e2 => eval e1 * eval e2
  end.

Fixpoint optimize (e : Expr) : Expr :=
  match e with
  | Const n => Const n
  | Add e1 e2 =>
      match optimize e1, optimize e2 with
      | Const n1, Const n2 => Const (n1 + n2)
      | e1', e2' => Add e1' e2'
      end
  | Mul e1 e2 =>
      match optimize e1, optimize e2 with
      | Const n1, Const n2 => Const (n1 * n2)
      | e1', e2' => Mul e1' e2'
      end
  end.

Theorem optimize_correct : forall e,
  eval (optimize e) = eval e.
Proof.
  induction e; simpl; try reflexivity.
    destruct (optimize e1) eqn:H1, (optimize e2) eqn:H2; simpl in *;
    try rewrite IHe1; try rewrite IHe2; reflexivity.
    destruct (optimize e1) eqn:H1, (optimize e2) eqn:H2; simpl in *;
    try rewrite IHe1; try rewrite IHe2; reflexivity.
Qed.

Definition example_expr := Add (Const 2) (Mul (Const 4) (Const 3)).
Compute optimize example_expr.