AE Interpreter

I’ve posted the interpreter from yesterday’s class at AE with a few updates. First, I’ve renamed expDenote to eval. No functionality changes or changes to proofs, I just think that eval is clearer. Second, I fixed the first proof we attempted to use auto. We’ve not covered that in class yet, but will in the next couple of days.

Following is a source listing for convenience.

From Stdlib Require Bool Arith List.
From Stdlib Require Lia.
Set Implicit Arguments.

Module AE.

(** Simple abstract syntax for an expression language, [exp], with a
  constant value constructed with [Num] and binary operations [Plus] and
  [Mult].
 *)

Inductive exp : Type := 
| Num : nat -> exp
| Plus : exp -> exp -> exp
| Mult : exp -> exp -> exp.

Check exp_ind.

Check (Num 3).
Check (Plus (Num 2) (Num 3)).
Check (Mult (Num 2) (Num 3)).

(** Recursive function that evaluates an [exp] to a [nat]. [Num n] evaluates
 to [n].  [Plus e1 e2] evaluates to the operation [plus] applied
 to the evaluation of [e1] and [e2].
 *)

Fixpoint eval (e:exp) : nat :=
  match e with
  | Num n => n
  | Plus e1 e2 => (plus (eval e1) (eval e2))
  | Mult e1 e2 => (mult (eval e1) (eval e2))
  end.

(** An experiment to show [eval] working as an interpreter *)

Compute eval (Mult (Plus (Num 2) (Num 4)) (Num 5)).
Check eval (Mult (Plus (Num 2) (Num 4)) (Num 5)).

(* 5*(2+4) *)

(** A theorem over addition of natural numbers *)
Theorem ex0: forall x, (eval (Plus (Num x) (Num 4))) >= 4.
Proof.
  simpl. induction x.
  - simpl. auto.
  - simpl. auto.
Qed.

(* * Verifying a simple optimization that replaces [0+x] with [x].  In [expOpt]
  we replace [0+x] by [x] using pattern matching and leave everything else
  alone. *)
Fixpoint expOpt (e:exp) : exp :=
  match e with
  | Num n => Num n
  | Plus (Num 0) e2 => (expOpt e2)
  | Plus e1 e2 => (Plus (expOpt e1) (expOpt e2))
  | Mult e1 e2 => (Mult (expOpt e1) (expOpt e2))
  end.

(* * The correctness theorem simply says that evaluating an expression has the
  same value as evaluating its optimization.  Note that in the proof we're only
  using commands learned so far.  Heavy use of induction hypotheses and a nested
  [destruct] structure the verification. *)
Theorem optimize_correct: forall e,
  (eval e) = ((eval (expOpt e))).
Proof.
  intros e. induction e.
  - reflexivity.
  - simpl. rewrite IHe1. rewrite IHe2. destruct e1.
    destruct n.
    + reflexivity.
    + reflexivity.
    + reflexivity.
    + reflexivity.
  - simpl. rewrite <- IHe1. rewrite <- IHe2. reflexivity.
Qed.

End AE.

EECS 755

Software Modeling and Analysis

AE Interpreter