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.

Fixpoint compile (t : source) : target. Admitted.

Theorem correct : forall t b, Rstar sstep t (B b) ->
                         Rstar tstep (compile t) (compile (B b)).
Admitted.

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