Skip to content

Commit

Permalink
Progress on progress: only missing T_Var and canonical forms lemmas
Browse files Browse the repository at this point in the history
  • Loading branch information
Lasse Overgaard Møldrup committed Nov 16, 2020
1 parent 7791c9f commit d58dbb8
Showing 1 changed file with 71 additions and 21 deletions.
92 changes: 71 additions & 21 deletions SimpleLang/safety.v
100644 → 100755
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,50 @@ Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Import ListNotations.

From SimpleLang Require Export dynamics.
From SimpleLang Require Export dynamics.

Lemma typed_inversion_nat : forall (e : expr) (t : type) (Γ : TypeEnv.type_env),
typed Γ e t -> exists n, e = Nat n ->
t = TNat.
Proof.
Admitted.

Lemma canonical_forms_nat : forall (v : expr) (Γ : TypeEnv.type_env),
val v -> typed Γ v TNat -> exists n, v = (Nat n).
Proof. Admitted.
Proof.
intros v Γ Hv_val Hv_TNat. destruct v; try contradiction.
- admit. (* How to prove that [typed Γ unit TNat] is a contradiction? *)
- exists n; reflexivity.
- admit.
- admit.
- admit.
- admit.
- admit.
Admitted.

Lemma canonical_forms_bool : forall (v : expr) (Γ : TypeEnv.type_env),
val v -> typed Γ v TBool -> exists b, v = (Bool b).
Proof. Admitted.

Lemma canonical_forms_sum : forall (v : expr) (t1 t2 : type) (Γ : TypeEnv.type_env),
val v -> typed Γ v (TSum t1 t2)
-> exists v', val v' /\ (v = (inj1 v') \/ v = (inj2 v')).
val v -> typed Γ v (TSum t1 t2) ->
exists v', val v' /\ (v = (inj1 v') \/ v = (inj2 v')).
(** maybe? *)
Proof. Admitted.

Lemma canonical_forms_prod : forall (v : expr) (t1 t2 : type) (Γ : TypeEnv.type_env),
val v -> typed Γ v (TProd t1 t2) ->
exists v1 v2, val v1 /\ val v2 /\ v = pair v1 v2.
Proof. Admitted.

Lemma canonical_forms_fun : forall (v : expr) (t1 t2 : type) (Γ : TypeEnv.type_env),
val v -> typed Γ v (TFun t1 t2) ->
exists e, v = rec e.
Proof. Admitted.

Theorem progress : forall (e : expr) (t : type),
typed TypeEnv.empty e t ->
val e \/ (exists e', step e e').
val e \/ (exists e', step e e').
Proof.
intros e t H. induction H.
(* Induction on typing relation *)
Expand Down Expand Up @@ -168,31 +193,45 @@ Proof.
constructor; assumption.

(* Case: T_fst *)
- destruct IHtyped as [He1_val | He1_step].
(* e1 is a value *)
+ (* needs canonical_forms_pair *)admit.
(* e1 takes a step *)
+ admit.
- right. destruct IHtyped as [He_val | He_step].
(* e is a value *)
+ destruct (canonical_forms_prod e t1 t2 Γ He_val H) as [v1].
destruct H0 as [v2]. destruct H0; destruct H1.
rewrite H2. exists v1.
constructor; assumption.
(* e takes a step *)
+ destruct He_step as [e'].
exists (fst e').
constructor; assumption.

(* Case: T_snd *)
- admit.
- right. destruct IHtyped as [He_val | He_step].
(* e is a value *)
+ destruct (canonical_forms_prod e t1 t2 Γ He_val H) as [v1].
destruct H0 as [v2]. destruct H0; destruct H1.
rewrite H2. exists v2.
constructor; assumption.
(* e takes a step *)
+ destruct He_step as [e'].
exists (snd e').
constructor; assumption.

(* Case: T_inj1 *)
- destruct IHtyped as [He_val | He_step].
(* e is a value *)
+ left. simpl. apply He_val.
(* e takes a step *)
+ right. destruct He_step as [e''].
exists (inj1 e'').
+ right. destruct He_step as [e'].
exists (inj1 e').
constructor; assumption.

(* Case: T_inj2 *)
- destruct IHtyped as [He_val | He_step].
(* e is a value *)
+ left. simpl. apply He_val.
(* e takes a step *)
+ right. destruct He_step as [e''].
exists (inj2 e'').
+ right. destruct He_step as [e'].
exists (inj2 e').
constructor; assumption.

(* Case: T_match *)
Expand All @@ -212,14 +251,25 @@ Proof.
constructor; assumption.

(* Case: T_rec *)
- destruct IHtyped as [He_val | He_step].
(* e is a value *)
+ left; simpl; apply I.
(* e takes a step *)
+ admit.
- destruct IHtyped as [He_val | He_step];
left; simpl; apply I.

(* Case: T_app *)
- admit.
- right. destruct IHtyped1 as [He1_val | He1_step].
(* e1 is a value *)
+ destruct IHtyped2 as [He2_val | He2_step].
(* e2 is a value (and e1 is a value) *)
* destruct (canonical_forms_fun e1 t1 t2 Γ He1_val H) as [e].
exists (subst (subst e 0 e1) 1 e2).
rewrite H1; constructor; assumption.
(* e2 takes a step (and e1 is a value) *)
* destruct He2_step as [e2'].
exists (app e1 e2').
constructor; assumption.
(* e1 takes a step *)
+ destruct He1_step as [e1'].
exists (app e1' e2).
constructor; assumption.
Admitted.

Theorem preservation : forall (Γ : TypeEnv.type_env) (e e' : expr) (t : type),
Expand Down

0 comments on commit d58dbb8

Please sign in to comment.