File 6

Extending / modifying compilers

In this assignment you'll take compilers you have already proved correct, make changes to them, and re-prove them correct.
Due2019-10-24 11:45AM
Reading (OPTIONAL)static/vouillon2012.pdf (a modern explanation of de Bruijn indices, among other things), static/debruijn1972.pdf (the original paper, which may be dense, due to old notation, etc)
Linkhttps://github.ccs.neu.edu/verifcomp/19/asgn/6.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.

Exercise 1. Full constant folding.
Before, you proved a compiler that just folded constants at the leaves. Here we've modified it to do this recursively, so the largest constant subexpression will be folded. Prove that this, too, is correct.

Module Exercise1.
  Inductive ty : Set :=
  | Nat : ty
  | Arr : ty -> ty -> ty
  .
  Hint Constructors ty.

  Inductive term : Set :=
  | N : nat -> term
  | Plus : term -> term -> term
  | Var : string -> term
  | Abs : string -> ty -> term -> term
  | App : term -> term -> term
  .
  Hint Constructors term.

  Fixpoint sub (e : term) (x : string) (body : term) :=
    match body with
    | N n => body
    | Plus t1 t2 => Plus (sub e x t1) (sub e x t2)
    | Var x' => if String.eqb x x' then e else body
    | App t1 t2 => App (sub e x t1) (sub e x t2)
    | Abs x' t body' => if String.eqb x x' then body
                       else Abs x' t (sub e x body')
    end.

  Inductive step : term -> term -> Prop :=
  | SApp : forall e1 e1' e2, step e1 e1' -> step (App e1 e2) (App e1' e2)
  | SBeta : forall x1 t1 body e, step (App (Abs x1 t1 body) e)
                                 (sub e x1 body)
  | SPlus1 : forall e1 e1' e2, step e1 e1' -> step (Plus e1 e2) (Plus e1' e2)
  | SPlus2 : forall e1 e2 e2', step e2 e2' -> step (Plus e1 e2) (Plus e1 e2')
  | SPlus : forall n1 n2, step (Plus (N n1) (N n2))
                          (N (n1 + n2)).
  Hint Constructors step.

  Fixpoint compile (t : term) : term :=
    match t with
    | Plus t1 t2 => match compile t1 with
                   | N n1 => match compile t2 with
                            | N n2 => N (n1 + n2)
                            | t2' => Plus (N n1) t2'
                            end
                   | t1' => Plus t1' (compile t2)
                   end
    | N n1 => t
    | Var x => t
    | App t1 t2 => App (compile t1) (compile t2)
    | Abs x t b => Abs x t (compile b)
    end.

  Theorem correct : forall t n, Rstar step t (N n) ->
                           Rstar step (compile t) (N n).
  Admitted.

End Exercise1.

Exercise 2. De Bruijn indices and +1-1.
This is a modified version of the +1-1 compiler presented in class, changed to use nats (and have a Minus instruction added) to avoid the dependency on ssr-algebra, and to use De Bruijn indices and evaluation contexts. Prove that like the previous compiler, this too is correct.

Module Exercise2.

  Inductive term : Set :=
  | N : nat -> term
  | Nn : nat -> term
  | Plus : term -> term -> term
  | Minus : 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
    | Nn n => Nn n
    | Plus t1 t2 => Plus (shift n t1) (shift n t2)
    | Minus t1 t2 => Minus (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
    | Nn n => Nn n
    | Plus t1 t2 => Plus (sub n e t1) (sub n e t2)
    | Minus t1 t2 => Minus (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 context : Set :=
  | Hole : context
  | Plus1 : context -> term -> context
  | Plus2 : term -> context -> context
  | Minus1 : context -> term -> context
  | Minus2 : term -> context -> context
  | App1 : context -> term -> context
  .

  Hint Constructors context.

  Inductive prim : term -> term -> Prop :=
  | PrimBeta : forall body t, prim (App (Abs body) t)
                              (sub 0 t body)
  | PrimN : forall n, prim (N n) (Nn n)
  | PrimPlus : forall n1 n2, prim (Plus (Nn n1) (Nn n2))
                             (Nn (n1 + n2))
  | PrimMinus : forall n1 n2, prim (Minus (Nn n1) (Nn n2))
                              (Nn (n1 - n2)).

  Hint Constructors prim.

  Inductive decomp : term -> term * context -> Prop :=
  | DN : forall n, decomp (N n) (N n, Hole)
  | DNn : forall n, decomp (Nn n) (Nn n, Hole)
  | DPlusConst : forall n1 n2,
      decomp (Plus (Nn n1) (Nn n2)) (Plus (Nn n1) (Nn n2), Hole)
  | DPlus2 : forall n1 t2 t2' c,
      decomp t2 (t2', c) ->
      decomp (Plus (Nn n1) t2) (t2', (Plus2 (Nn n1) c))
  | DPlus1 : forall t1 t1' t2 c,
      decomp t1 (t1', c) ->
      decomp (Plus t1 t2) (t1', (Plus1 c t2))
  | DMinusConst : forall n1 n2,
      decomp (Minus (Nn n1) (Nn n2)) (Minus (Nn n1) (Nn n2), Hole)
  | DMinus2 : forall n1 t2 t2' c,
      decomp t2 (t2', c) ->
      decomp (Minus (Nn n1) t2) (t2', (Minus2 (Nn n1) c))
  | DMinus1 : forall t1 t1' t2 c,
      decomp t1 (t1', c) ->
      decomp (Minus t1 t2) (t1', (Minus1 c t2))
  | DVar : forall k, decomp (Var k) (Var k, Hole)
  | DAbs : forall body, decomp (Abs body) (Abs body, Hole)
  | DApp1 : forall body t2, decomp (App (Abs body) t2) (App (Abs body) t2, Hole)
  | DApp2 : forall t1 t1' c t2,
      decomp t1 (t1', c) ->
      decomp (App t1 t2) (t1', App1 c t2)
  .

  Inductive plug : term -> context -> term -> Prop :=
  | PHole : forall t, plug t Hole t
  | PPlus1 : forall c t t' t2, plug t c t' -> plug t (Plus1 c t2) (Plus t' t2)
  | PPlus2 : forall c t t' t1, plug t c t' -> plug t (Plus2 t1 c) (Plus t1 t')
  | PMinus1 : forall c t t' t2, plug t c t' -> plug t (Minus1 c t2) (Minus t' t2)
  | PMinus2 : forall c t t' t1, plug t c t' -> plug t (Minus2 t1 c) (Minus t1 t')
  | PApp1 : forall c t t' t2, plug t c t' -> plug t (App1 c t2) (App t' t2)
  .

  Inductive step : term -> term -> Prop :=
  | S : forall e e' t c t', decomp e (t,c) ->
                       prim t t' ->
                       plug t' c e' ->
                       step e e'.

  Hint Constructors step.

  Fixpoint compile (t : term) : term :=
    match t with
    | Plus t1 t2 => Plus (compile t1) (compile t2)
    | Minus t1 t2 => Minus (compile t1) (compile t2)
    | N _ => Minus (Plus t (N 1)) (N 1)
    | Nn _ => t
    | Var _ => t
    | App t1 t2 => App (compile t1) (compile t2)
    | Abs b => Abs (compile b)
    end.

  Theorem correct : forall t n, Rstar step t (Nn n) ->
                           Rstar step (compile t) (Nn n).
  Admitted.

End Exercise2.