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.

Theorem sdet : forall t t1 t2, step t t1 -> step t t2 -> t1 = t2.
Admitted.

Fixpoint compile (t : term) := t.

Inductive sim : term -> term -> Prop := .

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