Commit 9ecad48f authored by Robbert Krebbers's avatar Robbert Krebbers

Major simplification of F_mu logrel.

parent 0f96e059
......@@ -5,6 +5,8 @@ From iris.algebra Require Export upred_big_op.
Section typed_interp.
Context {Σ : iFunctor}.
Notation D := (valC -n> iProp lang Σ).
Implicit Types Δ : listC D.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
......@@ -14,21 +16,20 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp (Δ : varC -n> valC -n> iProp lang Σ) Γ vs e τ
(HΔ : x v, PersistentP (Δ x v)) :
Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) :
Γ ⊢ₜ e : τ
length Γ = length vs
[] zip_with (λ τ, interp τ Δ) Γ vs WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
intros Htyped. revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
iApply (big_and_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
rewrite lookup_zip_with; by simplify_option_eq.
- (* unit *) value_case.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1.
......@@ -70,35 +71,29 @@ Section typed_interp.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case.
iIntros { τi } "! %". iApply wp_TLam; iNext; simpl in *.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
by iDestruct (zip_with_context_interp_subst with "HΓ") as "?".
iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. simpl in *.
iApply (IHHtyped (τi :: Δ)). by rewrite fmap_length.
rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp τ' Δ)); iPureIntro; apply _|].
iIntros{w} "?". by rewrite interp_subst.
iIntros {w} "?". by rewrite interp_subst.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_wand_l.
iSplitL; [|iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
trivial].
+ iIntros {v} "#Hv".
value_case.
iApply wp_wand_l.
iSplitL; [|iApply (IHHtyped (interp (TRec τ) Δ :: Δ)); trivial].
+ iIntros {v} "#Hv". value_case.
change (fixpoint _) with (interp (TRec τ) Δ) at 1; trivial.
rewrite fixpoint_unfold; cbn.
iAlways; eauto.
+ by iDestruct (zip_with_context_interp_subst with "HΓ") as "?".
rewrite fixpoint_unfold /=. iAlways; eauto 10.
+ rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
- (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply IHHtyped; trivial].
iIntros {v}.
cbn [interp interp_rec cofe_mor_car].
rewrite fixpoint_unfold.
iIntros "#Hv"; cbn.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
iIntros {v} "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with (interp (TRec τ) Δ); simpl.
iDestruct "Hv" as {w} "#[% Hw]"; subst.
iApply wp_Fold; cbn; auto using to_of_val.
rewrite -interp_subst; trivial.
by rewrite -interp_subst.
Qed.
End typed_interp.
This diff is collapsed.
......@@ -2,34 +2,22 @@ From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Section Soundness.
Section soundness.
Let Σ := #[].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
Definition free_type_context : varC -n> valC -n> iProp lang (globalF Σ) :=
λne x y, True%I.
Lemma wp_soundness e τ :
[] ⊢ₜ e : τ True WP e {{ @interp (globalF Σ) τ free_type_context }}.
[] ⊢ₜ e : τ True WP e {{ @interp (globalF Σ) τ [] }}.
Proof.
iIntros {H} "". rewrite -(empty_env_subst e).
by iApply (@typed_interp _ _ _ []).
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.
eapply wp_soundness in H1; eauto.
edestruct (@wp_adequacy_reducible lang (globalF Σ)
(interp τ free_type_context)
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.
End soundness.
......@@ -30,25 +30,22 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
Γ ⊢ₜ Case e0 e1 e2 : ρ
| Lam_typed e τ1 τ2 : τ1 :: Γ ⊢ₜ e : τ2 Γ ⊢ₜ Lam e : TArrow τ1 τ2
| App_typed e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : TArrow τ1 τ2 Γ ⊢ₜ e2 : τ1 Γ ⊢ₜ App e1 e2 : τ2
| TLam_typed e τ : map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ TLam e : TForall τ
| TLam_typed e τ : subst (ren (+1)) <$> Γ ⊢ₜ e : τ Γ ⊢ₜ TLam e : TForall τ
| TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ Γ ⊢ₜ TApp e : τ.[τ'/]
| TFold e τ : map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ Fold e : TRec τ
| TFold e τ : subst (ren (+1)) <$> Γ ⊢ₜ e : τ Γ ⊢ₜ Fold e : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ Γ ⊢ₜ Unfold e : τ.[TRec τ/]
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Local Hint Extern 1 =>
match goal with
| H : context [length (map _ _)] |- _ => rewrite map_length in H
end : typed_subst_invariant.
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 ( {A} `{Ids A} `{Rename A}
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
assert ( x Γ, x < length (subst (ren (+1)) <$> Γ) x < length Γ).
{ intros ??. by rewrite fmap_length. }
assert ( {A} `{Ids A} `{Rename A} (s1 s2 : nat A) x,
(x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega typed_subst_invariant.
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -58,27 +55,11 @@ 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.
intros H1 H2. rewrite /env_subst.
eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first omega.
by simplify_option_eq.
Qed.
Local Opaque eq_nat_dec.
Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
iter m up (τ .: ids) x =
if lt_dec x m then ids x else
if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
Proof.
revert x τ.
induction m; intros x τ; cbn.
- destruct x; cbn.
+ destruct eq_nat_dec; auto with omega.
asimpl; trivial.
+ destruct eq_nat_dec; auto with omega.
- destruct x; asimpl; trivial.
rewrite IHm.
repeat destruct lt_dec; repeat destruct eq_nat_dec;
asimpl; auto with omega.
Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
......@@ -167,7 +167,7 @@ Proof.
Qed.
Lemma n_closed_subst_head_simpl n e w ws :
( f, e.[iter n up f] = e) ->
( f, e.[iter n up f] = e)
S (length ws) = n
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
......@@ -188,7 +188,7 @@ Proof.
Qed.
Lemma n_closed_subst_head_simpl_2 n e w w' ws :
( f, e.[iter n up f] = e) -> (S (S (length ws))) = n
( f, e.[iter n up f] = e) (S (S (length ws))) = n
e.[# w .: # w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
intros H1 H2.
......
From iris.algebra Require Export base.
From iris.algebra Require Import cofe.
From iris.algebra Require Import upred.
From iris.program_logic Require Import weakestpre.
From Autosubst Require Export Autosubst.
Import uPred.
Canonical Structure varC := leibnizC var.
......@@ -22,3 +24,19 @@ Section Autosubst_Lemmas.
repeat (case_match || asimpl || rewrite IH); auto with omega.
Qed.
End Autosubst_Lemmas.
Ltac properness :=
repeat match goal with
| |- ( _: _, _)%I ( _: _, _)%I => apply exist_proper =>?
| |- ( _: _, _)%I ( _: _, _)%I => apply forall_proper =>?
| |- (_ _)%I (_ _)%I => apply and_proper
| |- (_ _)%I (_ _)%I => apply or_proper
| |- (_ _)%I (_ _)%I => apply impl_proper
| |- (WP _ {{ _ }})%I (WP _ {{ _ }})%I => apply wp_proper =>?
| |- ( _)%I ( _)%I => apply later_proper
| |- ( _)%I ( _)%I => apply always_proper
end.
Ltac solve_proper_alt :=
repeat intro; (simpl + idtac);
by repeat match goal with H : _ {_} _|- _ => rewrite H end.
\ No newline at end of file
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