Commit 23c3d518 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc clean up.

parent ac24a813
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import ownership adequacy.
Section soundness.
Definition Σ := #[ auth.authGF heapUR ].
Let Σ := #[ auth.authGF heapUR ].
Lemma wp_soundness e τ σ :
[] ⊢ₜ e : τ
......
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import ownership adequacy.
Section soundness.
Definition Σ := #[ auth.authGF heapUR ].
Let Σ := #[ auth.authGF heapUR ].
Lemma wp_soundness e τ σ :
[] ⊢ₜ e : τ
......
......@@ -4,7 +4,6 @@ From iris_logrel.stlc Require Export lang typing.
(** interp : is a unary logical relation. *)
Section logrel.
Context {Σ : iFunctor}.
Implicit Types P Q R : iProp lang Σ.
Fixpoint interp (τ : type) (w : val) : iProp lang Σ :=
match τ with
......@@ -16,28 +15,6 @@ Fixpoint interp (τ : type) (w : val) : iProp lang Σ :=
v, interp τ1 v WP App (of_val w) (of_val v) {{ interp τ2 }}
end%I.
Global Instance interp_always_stable τ v : PersistentP (interp τ v).
Global Instance interp_persistent τ v : PersistentP (interp τ v).
Proof. revert v; induction τ=> v /=; apply _. Qed.
Lemma typed_subst_invariant Γ e τ s1 s2 :
Γ ⊢ₜ e : τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( s1 s2 x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
by rewrite Hv.
Qed.
End logrel.
......@@ -5,27 +5,17 @@ From iris.program_logic Require Import adequacy.
Section soundness.
Let Σ := #[].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with ids. by asimpl. Qed.
Lemma wp_soundness e τ : [] ⊢ₜ e : τ True WP e {{ @interp (globalF Σ) τ }}.
Proof.
iIntros {H} "".
rewrite -(empty_env_subst e).
iApply typed_interp; eauto.
iIntros {H} "". rewrite -(empty_env_subst e). iApply typed_interp; eauto.
Qed.
Theorem Soundness e τ :
[] ⊢ₜ e : τ
e' thp, rtc step ([e], tt) (e' :: thp, tt)
¬ reducible e' tt is_Some (to_val e').
Theorem soundness e τ e' thp :
[] ⊢ₜ e : τ rtc step ([e], ()) (e' :: thp, ())
is_Some (to_val e') reducible e' ().
Proof.
intros H1 e' thp Hstp Hnr.
apply wp_soundness in H1.
edestruct(@wp_adequacy_reducible lang (globalF Σ)
(interp τ) e e' (e' :: thp) tt )
as [Ha|Ha]; eauto using ucmra_unit_valid; try tauto.
- iIntros "H". iApply H1.
intros. eapply wp_adequacy_reducible; eauto using ucmra_unit_valid.
- iIntros "H". by iApply wp_soundness.
- constructor.
Qed.
End soundness.
......@@ -24,3 +24,28 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| App_typed e1 e2 τ1 τ2 :
Γ ⊢ₜ e1 : TArrow τ1 τ2 Γ ⊢ₜ e2 : τ1 Γ ⊢ₜ App e1 e2 : τ2
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Lemma typed_subst_invariant Γ e τ s1 s2 :
Γ ⊢ₜ e : τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( s1 s2 x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
by rewrite Hv.
Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with ids. by asimpl. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment