Added safety-file for progress/preservation

logsem · Nov 10, 2020 · b0f67c5 · b0f67c5
1 parent f20b561
commit b0f67c5
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/SimpleLang/safety.v b/SimpleLang/safety.v
@@ -0,0 +1,16 @@
+Require Import Coq.Arith.PeanoNat.
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+From SimpleLang Require Export dynamics. 
+
+Theorem progress : forall (e : expr) (t : type), 
+  typed TypeEnv.empty e t ->
+  val e \/ (exists  e', step e e').
+Proof. Admitted.
+
+Theorem preservation : forall (Γ : TypeEnv.type_env) (e e' : expr) (t : type),
+  typed Γ e t ->
+  step e e' ->
+  typed Γ e' t.
+Proof. Admitted.