From ac10cd49fe1ee2f18de2f16bd7b9fd926fd6f3f6 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Sat, 21 May 2016 12:01:46 +0200
Subject: [PATCH] Prove type soundness for stlc

---
 _CoqProject        |  1 +
 stlc/fundamental.v |  7 +++----
 stlc/soundness.v   | 37 +++++++++++++++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 4 deletions(-)
 create mode 100644 stlc/soundness.v

diff --git a/_CoqProject b/_CoqProject
index 82f21fa..98757eb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@ stlc/typing.v
 stlc/rules.v
 stlc/logrel.v
 stlc/fundamental.v
+stlc/soundness.v
 F_mu/lang.v
 F_mu/typing.v
 F_mu/rules.v
diff --git a/stlc/fundamental.v b/stlc/fundamental.v
index c57f5db..84fb0bc 100644
--- a/stlc/fundamental.v
+++ b/stlc/fundamental.v
@@ -31,15 +31,14 @@ Section typed_interp.
        --------------------------------------□
        (_ ∧ _)) => iSplit
   end : itauto.
-  
-  
+
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
     iApply (@wp_bind _ _ _ [ctx]);
     iApply wp_impl_l;
     iSplit; [| iApply Hp; trivial]; cbn;
     eapply (@always_intro _ _ _ _);
     iIntros {v} Hv.
-              
+
   Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
 
   Lemma typed_interp Γ vs e τ :
@@ -97,4 +96,4 @@ Section typed_interp.
       iApply "Hv"; auto with itauto.
   Qed.
 
-End typed_interp.
+End typed_interp.
\ No newline at end of file
diff --git a/stlc/soundness.v b/stlc/soundness.v
new file mode 100644
index 0000000..6fcdaba
--- /dev/null
+++ b/stlc/soundness.v
@@ -0,0 +1,37 @@
+Require Import iris.proofmode.tactics.
+Require Import iris.program_logic.hoare.
+Require Import iris.program_logic.lifting.
+Require Import iris.algebra.upred_big_op.
+Require Import stlc.lang stlc.typing stlc.rules stlc.logrel stlc.fundamental.
+Require Import iris.program_logic.adequacy.
+Import uPred.
+
+Section Soundness.
+  Context {Σ : iFunctor}.
+
+  Lemma empty_env_subst e : e.[env_subst []] = e.
+    replace (env_subst []) with (ids) by reflexivity.
+    asimpl; trivial.
+  Qed.
+
+  Lemma wp_soundness e τ : typed [] e τ → True ⊢ WP e {{@interp Σ τ}}.
+  Proof.
+    iIntros {H} "".
+    rewrite -(empty_env_subst e).
+    iApply typed_interp; eauto.
+  Qed.
+
+  Theorem Soundness e τ :
+    typed [] e τ →
+    ∀ e' thp, rtc step ([e], tt) (e' :: thp, tt) →
+              ¬ reducible e' tt → is_Some (to_val e').
+  Proof.
+    intros H1 e' thp Hstp Hnr.
+    apply wp_soundness in H1.
+    edestruct(@wp_adequacy_reducible lang Σ ⊤ (interp τ) e e' (e' :: thp) tt ∅)
+      as [Ha|Ha]; eauto using cmra_unit_valid; try tauto.
+    - iIntros "H". iApply H1.
+    - constructor.
+  Qed.
+
+End Soundness.
\ No newline at end of file
-- 
GitLab