Commit a17bf389 authored by Amin Timany's avatar Amin Timany

Change congruence lemmas of Fμ,ref,par

The case of lam and case expressions that before required the terms to be
well-typed now require terms to be closed.

Separated definition context and context refinement from soundness_binary file.
parent d0763bf2
Require Import iris_logrel.prelude.base.
From iris_logrel.F_mu_ref_par Require Import lang typing rules_binary
rules logrel_binary fundamental_binary.
Local Notation expr := (expr lang).
Inductive context_item : Type :=
| CTX_Lam
| CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr)
(* Products *)
| CTX_PairL (e2 : expr)
| CTX_PairR (e1 : expr)
| CTX_Fst
| CTX_Snd
(* Sums *)
| CTX_InjL
| CTX_InjR
| CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
(* Nat bin op *)
| CTX_NBOPL (op : NatBinOP) (e2 : expr)
| CTX_NBOPR (op : NatBinOP) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Concurrency *)
| CTX_Fork
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare and swap used for fine-grained concurrency *)
| CTX_CAS_L (e1 : expr) (e2 : expr)
| CTX_CAS_M (e0 : expr) (e2 : expr)
| CTX_CAS_R (e0 : expr) (e1 : expr).
Fixpoint fill_ctx_item (ctx : context_item) (e : expr) : expr :=
match ctx with
| CTX_Lam => Lam e
| CTX_AppL e2 => App e e2
| CTX_AppR e1 => App e1 e
| CTX_PairL e2 => Pair e e2
| CTX_PairR e1 => Pair e1 e
| CTX_Fst => Fst e
| CTX_Snd => Snd e
| CTX_InjL => InjL e
| CTX_InjR => InjR e
| CTX_CaseL e1 e2 => Case e e1 e2
| CTX_CaseM e0 e2 => Case e0 e e2
| CTX_CaseR e0 e1 => Case e0 e1 e
| CTX_NBOPL op e2 => NBOP op e e2
| CTX_NBOPR op e1 => NBOP op e1 e
| CTX_IfL e1 e2 => If e e1 e2
| CTX_IfM e0 e2 => If e0 e e2
| CTX_IfR e0 e1 => If e0 e1 e
| CTX_Fold => Fold e
| CTX_Unfold => Unfold e
| CTX_TLam => TLam e
| CTX_TApp => TApp e
| CTX_Fork => Fork e
| CTX_Alloc => Alloc e
| CTX_Load => Load e
| CTX_StoreL e2 => Store e e2
| CTX_StoreR e1 => Store e1 e
| CTX_CAS_L e1 e2 => CAS e e1 e2
| CTX_CAS_M e0 e2 => CAS e0 e e2
| CTX_CAS_R e0 e1 => CAS e0 e1 e
end.
Definition context := list context_item.
Definition fill_ctx K e := foldr fill_ctx_item e K.
Local Open Scope bin_logrel_scope.
(** typed context *)
Inductive typed_context_item :
context_item (list type) type (list type) type Prop :=
| TP_CTX_Lam : Γ τ τ',
typed_context_item CTX_Lam (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
| TP_CTX_AppL (e2 : expr) : Γ τ τ',
typed Γ e2 τ
typed_context_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
| TP_CTX_AppR (e1 : expr) : Γ τ τ',
typed Γ e1 (TArrow τ τ')
typed_context_item (CTX_AppR e1) Γ τ Γ τ'
| TP_CTX_PairL (e2 : expr) : Γ τ τ',
typed Γ e2 τ'
typed_context_item (CTX_PairL e2) Γ τ Γ (TProd τ τ')
| TP_CTX_PairR (e1 : expr) : Γ τ τ',
typed Γ e1 τ
typed_context_item (CTX_PairR e1) Γ τ' Γ (TProd τ τ')
| TP_CTX_Fst : Γ τ τ',
typed_context_item CTX_Fst Γ (TProd τ τ') Γ τ
| TP_CTX_Snd : Γ τ τ',
typed_context_item CTX_Snd Γ (TProd τ τ') Γ τ'
| TP_CTX_InjL : Γ τ τ',
typed_context_item CTX_InjL Γ τ Γ (TSum τ τ')
| TP_CTX_InjR : Γ τ τ',
typed_context_item CTX_InjR Γ τ' Γ (TSum τ τ')
| TP_CTX_CaseL (e1 : expr) (e2 : expr) : Γ τ1 τ2 τ',
typed (τ1 :: Γ) e1 τ' typed (τ2 :: Γ) e2 τ'
typed_context_item (CTX_CaseL e1 e2) Γ (TSum τ1 τ2) Γ τ'
| TP_CTX_CaseM (e0 : expr) (e2 : expr) : Γ τ1 τ2 τ',
typed Γ e0 (TSum τ1 τ2) typed (τ2 :: Γ) e2 τ'
typed_context_item (CTX_CaseM e0 e2) (τ1 :: Γ) τ' Γ τ'
| TP_CTX_CaseR (e0 : expr) (e1 : expr) : Γ τ1 τ2 τ',
typed Γ e0 (TSum τ1 τ2) typed (τ1 :: Γ) e1 τ'
typed_context_item (CTX_CaseR e0 e1) (τ2 :: Γ) τ' Γ τ'
| TP_CTX_IfL (e1 : expr) (e2 : expr) : Γ τ,
typed Γ e1 τ typed Γ e2 τ
typed_context_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
| TP_CTX_IfM (e0 : expr) (e2 : expr) : Γ τ,
typed Γ e0 (TBool) typed Γ e2 τ
typed_context_item (CTX_IfM e0 e2) Γ τ Γ τ
| TP_CTX_IfR (e0 : expr) (e1 : expr) : Γ τ,
typed Γ e0 (TBool) typed Γ e1 τ
typed_context_item (CTX_IfR e0 e1) Γ τ Γ τ
| TP_CTX_NBOPL op (e2 : expr) : Γ,
typed Γ e2 TNat
typed_context_item (CTX_NBOPL op e2) Γ TNat Γ (NatBinOP_res_type op)
| TP_CTX_NBOPR op (e1 : expr) : Γ,
typed Γ e1 TNat
typed_context_item (CTX_NBOPR op e1) Γ TNat Γ (NatBinOP_res_type op)
| TP_CTX_Fold : Γ τ,
typed_context_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold : Γ τ,
typed_context_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
| TP_CTX_TLam : Γ τ,
typed_context_item
CTX_TLam (map (λ t : type, t.[ren (+1)]) Γ) τ Γ (TForall τ)
| TP_CTX_TApp : Γ τ τ',
typed_context_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
| TP_CTX_Fork : Γ,
typed_context_item CTX_Fork Γ TUnit Γ TUnit
| TPCTX_Alloc : Γ τ,
typed_context_item CTX_Alloc Γ τ Γ (Tref τ)
| TP_CTX_Load : Γ τ,
typed_context_item CTX_Load Γ (Tref τ) Γ τ
| TP_CTX_StoreL (e2 : expr) : Γ τ,
typed Γ e2 τ
typed_context_item (CTX_StoreL e2) Γ (Tref τ) Γ TUnit
| TP_CTX_StoreR (e1 : expr) : Γ τ,
typed Γ e1 (Tref τ)
typed_context_item (CTX_StoreR e1) Γ τ Γ TUnit
| TP_CTX_CasL (e1 : expr) (e2 : expr) : Γ τ,
EqType τ typed Γ e1 τ typed Γ e2 τ
typed_context_item (CTX_CAS_L e1 e2) Γ (Tref τ) Γ TBool
| TP_CTX_CasM (e0 : expr) (e2 : expr) : Γ τ,
EqType τ typed Γ e0 (Tref τ) typed Γ e2 τ
typed_context_item (CTX_CAS_M e0 e2) Γ τ Γ TBool
| TP_CTX_CasR (e0 : expr) (e1 : expr) : Γ τ,
EqType τ typed Γ e0 (Tref τ) typed Γ e1 τ
typed_context_item (CTX_CAS_R e0 e1) Γ τ Γ TBool.
Lemma typed_context_item_typed k Γ τ Γ' τ' e :
typed Γ e τ typed_context_item k Γ τ Γ' τ'
typed Γ' (fill_ctx_item k e) τ'.
Proof. intros H1 H2; induction H2; simpl; eauto using typed. Qed.
Inductive typed_context :
context (list type) type (list type) type Prop :=
| TPCTX_nil : Γ τ, typed_context nil Γ τ Γ τ
| TPCTX_cons : Γ1 τ1 Γ2 τ2 Γ3 τ3 k K,
typed_context_item k Γ2 τ2 Γ3 τ3
typed_context K Γ1 τ1 Γ2 τ2
typed_context (k :: K) Γ1 τ1 Γ3 τ3.
Lemma typed_context_typed K Γ τ Γ' τ' e :
typed Γ e τ typed_context K Γ τ Γ' τ' typed Γ' (fill_ctx K e) τ'.
Proof.
intros H1 H2; induction H2; simpl; eauto using typed_context_item_typed.
Qed.
Lemma typed_context_n_closed K Γ τ Γ' τ' e :
( f, e.[iter (List.length Γ) up f] = e) typed_context K Γ τ Γ' τ'
f, (fill_ctx K e).[iter (List.length Γ') up f] = (fill_ctx K e).
Proof.
intros H1 H2; induction H2; simpl; auto.
(induction H => f); asimpl; simpl in *;
repeat match goal with H : _ |- _ => rewrite map_length in H end;
try f_equal;
eauto using typed_n_closed;
try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
Qed.
Definition context_refines Γ e e' τ :=
K,
typed_context K Γ τ [] TUnit
thp h v, rtc step ([fill_ctx K e], ) ((# v) :: thp, h)
thp' h' v',
rtc step ([fill_ctx K e'], ) ((# v') :: thp', h').
\ No newline at end of file
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import lang examples.lock typing
logrel_binary fundamental_binary rules_binary rules.
rules_binary rules.
Import uPred.
Section CG_Stack.
......
......@@ -142,11 +142,12 @@ Section typed_interp.
Unshelve. all: trivial.
Qed.
Lemma typed_binary_interp_Case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 {HΔ : ✓✓ Δ}
(Htyped2 : typed (τ1 :: Γ) e1 τ3)
(Htyped3 : typed (τ2 :: Γ) e2 τ3)
(Htyped2' : typed (τ1 :: Γ) e1' τ3)
(Htyped3' : typed (τ2 :: Γ) e2' τ3)
Lemma typed_binary_interp_Case Δ Γ (e0 e1 e2 e0' e1' e2' : expr) τ1 τ2 τ3
{HΔ : ✓✓ Δ}
(Hclosed2 : f, e1.[iter (S (List.length Γ)) up f] = e1)
(Hclosed3 : f, e2.[iter (S (List.length Γ)) up f] = e2)
(Hclosed2' : f, e1'.[iter (S (List.length Γ)) up f] = e1')
(Hclosed3' : f, e2'.[iter (S (List.length Γ)) up f] = e2')
(IHHtyped1 : Δ Γ e0 log e0' TSum τ1 τ2)
(IHHtyped2 : Δ τ1 :: Γ e1 log e1' τ3)
(IHHtyped3 : Δ τ2 :: Γ e2 log e2' τ3)
......@@ -165,7 +166,7 @@ Section typed_interp.
iApply wp_case_inl; auto 1 using to_of_val.
asimpl.
specialize (IHHtyped2 (w::vs)); simpl in IHHtyped2.
erewrite <- ?typed_subst_head_simpl in IHHtyped2; eauto;
erewrite <- ?n_closed_subst_head_simpl in IHHtyped2; eauto;
simpl; try rewrite map_length; eauto with f_equal. iNext.
iApply IHHtyped2; auto 2.
iFrame "Hheap Hspec Hw HΓ"; trivial.
......@@ -177,7 +178,7 @@ Section typed_interp.
iApply wp_case_inr; auto 1 using to_of_val.
asimpl.
specialize (IHHtyped3 (w::vs)); simpl in IHHtyped3.
erewrite <- ?typed_subst_head_simpl in IHHtyped3; eauto;
erewrite <- ?n_closed_subst_head_simpl in IHHtyped3; eauto;
simpl; try rewrite map_length; eauto with f_equal. iNext.
iApply IHHtyped3; auto 2.
iFrame "Hheap Hspec Hw HΓ"; trivial.
......@@ -228,9 +229,9 @@ Section typed_interp.
Unshelve. all: eauto using to_of_val.
Qed.
Lemma typed_binary_interp_Lam Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(Htyped : typed (TArrow τ1 τ2 :: τ1 :: Γ) e τ2)
(Htyped' : typed (TArrow τ1 τ2 :: τ1 :: Γ) e' τ2)
Lemma typed_binary_interp_Lam Δ Γ (e e' : expr) τ1 τ2 {HΔ : ✓✓ Δ}
(Hclosed : f, e.[iter (S (S (List.length Γ))) up f] = e)
(Hclosed' : f, e'.[iter (S (S (List.length Γ))) up f] = e')
(IHHtyped : Δ TArrow τ1 τ2 :: τ1 :: Γ e log e' τ2)
:
Δ Γ Lam e log Lam e' TArrow τ1 τ2.
......@@ -246,7 +247,7 @@ Section typed_interp.
specialize (IHHtyped ((LamV e.[upn 2 (env_subst (map fst vs))],
LamV e'.[upn 2 (env_subst (map snd vs))])
:: v :: vs)). simpl in IHHtyped.
erewrite <- ?typed_subst_head_simpl_2 in IHHtyped; eauto; simpl;
erewrite <- ?n_closed_subst_head_simpl_2 in IHHtyped; eauto; simpl;
try rewrite map_length; auto.
iApply IHHtyped; auto.
repeat iSplitR; trivial. repeat iSplit; trivial.
......@@ -561,9 +562,11 @@ Section typed_interp.
- eapply typed_binary_interp_Snd; trivial.
- eapply typed_binary_interp_InjL; trivial.
- eapply typed_binary_interp_InjR; trivial.
- eapply typed_binary_interp_Case; eauto.
- eapply typed_binary_interp_Case; eauto;
match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
- eapply typed_binary_interp_If; eauto.
- eapply typed_binary_interp_Lam; eauto.
- eapply typed_binary_interp_Lam; eauto;
match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
- eapply typed_binary_interp_App; trivial.
- eapply typed_binary_interp_TLam; trivial.
- eapply typed_binary_interp_TApp; trivial.
......
This diff is collapsed.
......@@ -137,10 +137,61 @@ Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed.
Notation "# v" := (of_val v) (at level 20).
Lemma n_closed_invariant n (e : expr) s1 s2 :
( f, e.[iter n up f] = e) ( x, x < n s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Hnc. specialize (Hnc (ren (+1))).
revert n Hnc s1 s2.
(induction e => m Hmc s1 s2 H1); asimpl in *; try f_equal;
try (match goal with H : _ |- _ => eapply H end; eauto;
try inversion Hmc; try match goal with H : _ |- _ => (by rewrite H) end;
fail).
- apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega.
asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega.
inversion Hmc; omega.
- unfold upn in *.
change (e.[up (up (iter m up (ren (+1))))]) with
(e.[iter (S (S m)) up (ren (+1))]) in *.
apply (IHe (S (S m))).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|[|x]] H2; [by cbv|by cbv |].
asimpl; rewrite H1; auto with omega.
- change (e1.[up (iter m up (ren (+1)))]) with
(e1.[iter (S m) up (ren (+1))]) in *.
apply (IHe0 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
- change (e2.[up (iter m up (ren (+1)))]) with
(e2.[iter (S m) up (ren (+1))]) in *.
apply (IHe1 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
Qed.
Lemma typed_n_closed Γ τ e :
typed Γ e τ -> ( f, e.[iter (List.length Γ) up f] = e).
Proof.
intros H. induction H => f; asimpl; unfold upn; simpl in *; auto with f_equal.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
- by f_equal; rewrite map_length in IHtyped.
Qed.
Lemma n_closed_subst_head_simpl n e w ws :
( f, e.[iter n up f] = e) ->
S (List.length ws) = n
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
......@@ -148,10 +199,19 @@ Proof.
by rewrite Hv.
Qed.
Lemma n_closed_subst_head_simpl_2 n e w w' ws :
( f, e.[iter n up f] = e) -> (S (S (List.length ws))) = n
e.[# w .: # w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
by rewrite Hv.
Qed.
Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
typed Δ e τ -> List.length Δ = 2 + (List.length ws)
e.[# w .: # w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)]
.
e.[# w .: # w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto => /= -[|[|x]] H3 //=.
......
......@@ -27,6 +27,7 @@ F_mu_ref_par/rules_binary.v
F_mu_ref_par/logrel_binary.v
F_mu_ref_par/fundamental_binary.v
F_mu_ref_par/soundness_unary.v
F_mu_ref_par/context_refinement.v
F_mu_ref_par/soundness_binary.v
F_mu_ref_par/examples/lock.v
F_mu_ref_par/examples/counter.v
......
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