Skip to content

Instantly share code, notes, and snippets.

@HuStmpHrrr
Last active September 10, 2018 16:55
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save HuStmpHrrr/0d92e646916ae9ec7ced3ff21724ba2d to your computer and use it in GitHub Desktop.
STLC
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment