# File 5

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.

Axiom string_eqP : Equality.axiom (fun x1 x2 => String.eqb x1 x2).
Definition string_eqMixin := EqMixin string_eqP.
Canonical string_eqType := Eval hnf in EqType string string_eqMixin.

Inductive sty : Set :=
| Bool : sty
| Arr : sty -> sty -> sty
.

Hint Constructors sty.

Inductive source : Set :=
| B : bool -> source
| And : source -> source -> source
| Var : string -> source
| Abs : string -> sty -> source -> source
| App : source -> source -> source
.

Hint Constructors source.

Fixpoint ssub (e : source) (x : string) (body : source) :=
match body with
| B b => body
| And t1 t2 => And (ssub e x t1) (ssub e x t2)
| Var x' => if x == x' then e else body
| App t1 t2 => App (ssub e x t1) (ssub e x t2)
| Abs x' t body' => if x == x' then body
else Abs x' t (ssub e x body')
end.

Inductive sstep : source -> source -> Prop :=
| SApp : forall e e' a, sstep e e' ->
sstep (App e a) (App e' a)
| SBeta : forall x1 t1 body e,
sstep (App (Abs x1 t1 body) e)
(ssub e x1 body)
| SAnd1 : forall e1 e1' e2, sstep e1 e1' ->
sstep (And e1 e2) (And e1' e2)
| SAnd2 : forall b e2 e2', sstep e2 e2' ->
sstep (And (B b) e2) (And (B b) e2')
| SAnd : forall b1 b2, sstep (And (B b1) (B b2))
(B (b1 && b2))
.

Hint Constructors sstep.

Inductive tty : Set :=
| Nat : tty
| Tarr : tty -> tty -> tty
.

Hint Constructors tty.

Inductive target : Set :=
| N : nat -> target
| Plus : target -> target -> target
| Minus : target -> target -> target
| TVar : string -> target
| TAbs : string -> tty -> target -> target
| TApp : target -> target -> target
.

Hint Constructors target.

Fixpoint tsub (e : target) (x : string) (body : target) :=
match body with
| N n => body
| Plus t1 t2 => Plus (tsub e x t1) (tsub e x t2)
| Minus t1 t2 => Minus (tsub e x t1) (tsub e x t2)
| TVar x' => if x == x' then e else body
| TApp t1 t2 => TApp (tsub e x t1) (tsub e x t2)
| TAbs x' t body' => if x == x' then body
else TAbs x' t (tsub e x body')
end.

Inductive tstep : target -> target -> Prop :=
| STApp : forall e e' a, tstep e e' ->
tstep (TApp e a) (TApp e' a)
| STBeta : forall x1 t1 body e,
tstep (TApp (TAbs x1 t1 body) e)
(tsub e x1 body)
| SPlus1 : forall e1 e1' e2, tstep e1 e1' ->
tstep (Plus e1 e2) (Plus e1' e2)
| SPlus2 : forall e1 e2 e2', tstep e2 e2' ->
tstep (Plus e1 e2) (Plus e1 e2')
| SPlus : forall n1 n2, tstep (Plus (N n1) (N n2))
(N (n1 + n2))
| SMinus1 : forall e1 e1' e2, tstep e1 e1' ->
tstep (Minus e1 e2) (Minus e1' e2)
| SMinus2 : forall e1 e2 e2', tstep e2 e2' ->
tstep (Minus e1 e2) (Minus e1 e2')
| SMinus : forall n1 n2, tstep (Minus (N n1) (N n2))
(N (n1 - n2))
.

Hint Constructors tstep.

Exercise 1. Define a compiler from source to target.
Fixpoint compile (t : source) : target. Admitted.

Exercise 2. Prove that your compiler is correct for programs that terminate in boolean values, by showing that the compiled program terminates in the translated value.
Theorem correct : forall t b, Rstar sstep t (B b) ->
Rstar tstep (compile t) (compile (B b)).