# Optimizing

In this assignment you'll define your own optimizations and then prove them correct.
NOTE: Exercises 1 and 2, rough versions, are DUE BY EMAIL BEFORE CLASS ON MONDAY, FOR REVIEW.
 Due 2019-10-31 11:45AM Link https://github.ccs.neu.edu/verifcomp/19/asgn/7.v

Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
From Coq Require Import Strings.String.

Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c
.

Hint Constructors Rstar.

Lemma RTrans {T : Type} {P : T -> T -> Prop} {a b c : T} : Rstar P a b -> Rstar P b c -> Rstar P a c.
Proof.
elim; eauto.
Qed.

Inductive term : Set :=
| N : nat -> term
| B : bool -> term
| Plus : term -> term -> term
| Minus : term -> term -> term
| Times : term -> term -> term
| If : term -> term -> term -> term
| Eq : term -> term -> term
| Var : nat -> term
| Abs : term -> term
| App : term -> term -> term
.
Hint Constructors term.

Fixpoint shift (n : nat) (t : term) : term :=
match t with
| N n => N n
| B b => B b
| Plus t1 t2 => Plus (shift n t1) (shift n t2)
| Minus t1 t2 => Minus (shift n t1) (shift n t2)
| Times t1 t2 => Times (shift n t1) (shift n t2)
| If t t1 t2 => If (shift n t) (shift n t1) (shift n t2)
| Eq t1 t2 => Eq (shift n t1) (shift n t2)
| Var i => if i >= n then Var (i.+1) else Var i
| Abs body => Abs (shift (n.+1) body)
| App t1 t2 => App (shift n t1) (shift n t2)
end.

Fixpoint sub (n : nat) (e : term) (body : term) : term :=
match body with
| N n => N n
| B b => B b
| Plus t1 t2 => Plus (sub n e t1) (sub n e t2)
| Minus t1 t2 => Minus (sub n e t1) (sub n e t2)
| Times t1 t2 => Times (sub n e t1) (sub n e t2)
| If t t1 t2 => If (sub n e t) (sub n e t1) (sub n e t2)
| Eq t1 t2 => Eq (sub n e t1) (sub n e t2)
| Var i => if i < n then Var i
else if i == n then e
else Var (i - 1)
| Abs body => Abs (sub (n.+1) (shift 0 e) body)
| App t1 t2 => App (sub n e t1) (sub n e t2)
end.

Inductive step : term -> term -> Prop :=
| SPlus1 : forall e1 e1' e2, step e1 e1' -> step (Plus e1 e2) (Plus e1' e2)
| SPlus2 : forall n1 e2 e2', step e2 e2' -> step (Plus (N n1) e2) (Plus (N n1) e2')
| SPlus : forall n1 n2, step (Plus (N n1) (N n2)) (N (n1 + n2))
| SMinus1 : forall e1 e1' e2, step e1 e1' -> step (Minus e1 e2) (Minus e1' e2)
| SMinus2 : forall n1 e2 e2', step e2 e2' -> step (Minus (N n1) e2) (Minus (N n1) e2')
| SMinus : forall n1 n2, step (Minus (N n1) (N n2)) (N (n1 - n2))
| STimes1 : forall e1 e1' e2, step e1 e1' -> step (Times e1 e2) (Times e1' e2)
| STimes2 : forall n1 e2 e2', step e2 e2' -> step (Times (N n1) e2) (Times (N n1) e2')
| STimes : forall n1 n2, step (Times (N n1) (N n2)) (N (n1 * n2))

| SIf1 : forall e e' e1 e2, step e e' -> step (If e e1 e2) (If e' e1 e2)
| SIfTrue : forall e1 e2, step (If (B true) e1 e2) e1
| SIfFalse : forall e1 e2, step (If (B false) e1 e2) e2
| SEq1 : forall e1 e1' e2, step e1 e1' -> step (Eq e1 e2) (Eq e1' e2)
| SEqN2 : forall n1 e2 e2', step e2 e2' -> step (Eq (N n1) e2) (Eq (N n1) e2')
| SEqB2 : forall b1 e2 e2', step e2 e2' -> step (Eq (B b1) e2) (Eq (B b1) e2')
| SEqN : forall n1 n2, step (Eq (N n1) (N n2)) (B (n1 == n2))
| SEqB : forall b1 b2, step (Eq (B b1) (B b2)) (B (b1 == b2))

| SApp : forall e1 e1' e2, step e1 e1' -> step (App e1 e2) (App e1' e2)
| SBeta : forall body e, step (App (Abs body) e)
(sub 0 e body)
.
Hint Constructors step.

Ltac invert H := inversion H; subst.
MASTERS CREDIT ONLY Exercise 0. Prove the language is deterministic.
Theorem sdet : forall t t1 t2, step t t1 -> step t t2 -> t1 = t2.
Admitted.

Exercise 1. Define some optimization pass on the above language. You're welcome to define any pass, but keep in mind that local transformations will be much easier to prove correct.
DUE BY EMAIL BEFORE 10/28 CLASS.
Fixpoint compile (t : term) := t.

Exercise 2. Define a simulation relation for your compiler.
DUE BY EMAIL BEFORE 10/28 CLASS.
Inductive sim : term -> term -> Prop := .

Exercise 3. Prove your compiler correct for programs that terminate in numbers.
Theorem correct : forall t n, Rstar step t (N n) ->
Rstar step (compile t) (N n).
Admitted.