STLC

stlc.v

Set Implicit Arguments.

Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import FunInd.

Require Import Arith.Wf_nat.
Require Import Recdef.
Require Import Omega.

Notation "f $ x" := ((f) (x)) (at level 68, right associativity, only parsing).

Inductive typ : Set :=
| bol : typ
| arr : typ -> typ -> typ.

Definition env := list typ.

Fixpoint lookup {T : Type} (l : list T) (n : nat) : option T :=
  match l with
  | nil => None
  | cons x l' => if Nat.eq_dec (length l) n then Some x else lookup l' n
  end.

Inductive trm : Set :=
| var : nat -> trm
| tru : trm
| fals : trm
| lam : typ -> trm -> trm
| app : trm -> trm -> trm.

Inductive typing : env -> trm -> typ -> Set :=
| ty_var : forall G n T, lookup G n = Some T -> typing G (var n) T
| ty_tru : forall G, typing G tru bol
| ty_fals : forall G, typing G fals bol
| ty_lam : forall G T U t, typing (T :: G) t U ->
                      typing G (lam T t) (arr T U)
| ty_app : forall G T U x y, typing G x (arr T U) ->
                        typing G y T ->
                        typing G (app x y) U.

Definition type_eq (T U : typ) : {T = U} + {T <> U}.
Proof. decide equality. Defined.

Definition calc_typ (G : env) (t : trm) : option {T : typ & typing G t T}.
Proof.
  revert G. induction t; intros.
  - destruct (lookup G n) eqn:?.
    + refine (Some $ existT _ _ _).
      constructor. eassumption.
    + exact None.
  - apply Some. repeat econstructor.
  - apply Some. repeat econstructor.
  - rename t into T.
    specialize (IHt $ T :: G).
    destruct IHt.
    + destruct s.
      refine (Some $ existT _ _ _).
      constructor. eassumption.
    + exact None.
  - destruct (IHt1 G).
    + destruct s. destruct x.
      * exact None.
      * destruct (IHt2 G).
        -- destruct s. destruct (type_eq x x1).
           ++ subst. refine (Some $ existT _ _ _).
              econstructor; eassumption.
           ++ exact None.
        -- exact None.
    + exact None.
Defined.

Inductive val : Set :=
| t_val : val
| f_val : val
| lam_val : list val -> typ -> trm -> val.

Definition venv := list val.

Inductive valty : val -> typ -> Set :=
| t_vty : valty t_val bol
| f_vty : valty f_val bol
| lam_vty : forall G ve T t U,
    typing G (lam T t) (arr T U) ->
    econ ve G ->
    valty (lam_val ve T t) (arr T U)
with
econ : venv -> env -> Set :=
| econ_nil : econ nil nil
| econ_cons : forall ve G v T,
    valty v T -> econ ve G -> econ (v :: ve) (T :: G).

Inductive eval : venv -> trm -> val -> Set :=
| ev_t : forall e, eval e tru t_val
| ev_f : forall e, eval e fals f_val
| ev_lam : forall e T t, eval e (lam T t) (lam_val e T t)
| ev_var : forall e n v, lookup e n = Some v ->
                    eval e (var n) v
| ev_app : forall e x y e' Tx tx vy v,
    eval e x (lam_val e' Tx tx) -> eval e y vy ->
    eval (vy :: e') tx v ->
    eval e (app x y ) v.


Lemma econ_length : forall e G, econ e G -> length e = length G.
Proof.
  induction 1; intros; simpl in *; trivial.
  rewrite IHecon. trivial.
Defined.

Definition econ_lookup : forall e G n T,
    econ e G ->
    lookup G n = Some T ->
    { v : val & @sig (valty v T) $ fun _ => lookup e n = Some v }.
Proof.
  induction 1; intros.
  - simpl in H. inversion H.
  - cbn [lookup] in *.
    destruct (Nat.eq_dec $ length (T0 :: G));
      destruct (Nat.eq_dec $ length (v :: ve)).
    + inversion H0. subst. econstructor. constructor.
      eassumption. trivial.
    + apply econ_length in H. simpl in *. rewrite H in n0.
      congruence.
    + apply econ_length in H. simpl in *. rewrite H in e.
      congruence.
    + apply IHecon. eassumption.
Defined.

Require Import Coq.Program.Equality.

Definition trm_measure (t : trm): nat := 0.

Require Coq.Program.Wf.

Program Fixpoint run
        G e (t : trm) T (ty : typing G t T) (con : econ e G)
        {measure (trm_measure t)}
  : option { v : val & prod (valty v T) $ eval e t v } :=
  match ty in typing G0 t0 T0
        return G = G0 -> t = t0 -> T = T0 -> option { v : val & prod (valty v T0) $ eval e t0 v } with
  | @ty_var G0 n T T_found =>
    fun eqG eqt eqT =>
      let con' : econ e G0 := eq_rec G _ con G0 eqG
      in match econ_lookup n con T_found with
         | existT _ v (exist _ vT v_found) =>
           Some $ existT _ _ $ pair vT $ ev_var e n v_found
         end
             
  | @ty_tru G => fun _ _ _ => Some $ existT _ _ $ pair t_vty (ev_t e)
  | @ty_fals G => fun _ _ _ => Some $ existT _ _ $ pair f_vty (ev_f e)
  | @ty_lam G T U t tU =>
    fun _ _ _ =>
      Some $ existT _ _ $ pair (lam_vty (@ty_lam G T U t tU) con) $ (ev_lam e T t)
  | @ty_app G0 T U x y x_TU yT =>
    fun eqG eqt eqT =>
      let con' : econ e G0 := eq_rec G _ con G0 eqG
      in match run x_TU con' with
         | Some (existT _ vx (pair vx_TU xsteps)) =>
           
           match vx_TU in valty vx0 TU0
                 return arr T U = TU0 -> option { v : val & prod (valty v U) $ eval e (app x y) v } with
           | @lam_vty G2 e2 T t U ty_lam con_lam =>

             match ty_lam in typing G1 t1 T1
                   return  with
             | ty_lam G T U t x => _
             | _ => 
             end
             
             fun _ =>
               match run yT con' with
               | Some (existT _ vy (pair vy_T ysteps)) =>
                 
                 None
               | None =>
                 None
               end
               
           | _ => fun eq => ltac:(congruence)
           end eq_refl

         | _ => None
         end
           
  end eq_refl eq_refl eq_refl.
Next Obligation.