Commit 1e8e112a authored by Dan Frumin's avatar Dan Frumin

Prove that contexual refinement is preorder and a precongruence

parent f33a4e73
......@@ -225,3 +225,49 @@ Proof.
all: rewrite -(dom_fmap (subst (ren (+1))) Γ); eauto.
by eapply typed_X_closed.
Qed.
Instance ctx_refines_reflexive Γ τ :
Reflexive (fun e1 e2 => ctx_refines Γ e1 e2 τ).
Proof.
intros e K thp σ v τ' Hτ' Hty Hst.
eexists _,_. apply Hst.
Qed.
Instance ctx_refines_transitive Γ τ :
Transitive (fun e1 e2 => ctx_refines Γ e1 e2 τ).
Proof.
intros e1 e2 e3 Hctx1 Hctx2 K thp σ v τ' Hτ' Hty Hst.
destruct (Hctx1 K thp σ v τ' Hτ' Hty Hst) as [thp' [σ' Hst']].
by apply (Hctx2 K thp' σ' v τ' Hτ').
Qed.
Lemma fill_ctx_app (K K' : ctx) (e : expr) :
fill_ctx K' (fill_ctx K e) = fill_ctx (K' ++ K) e.
Proof. by rewrite /fill_ctx foldr_app. Qed.
Lemma typed_ctx_compose (K K' : ctx) (Γ1 Γ2 Γ3 : stringmap type) (τ1 τ2 τ3 : type) :
typed_ctx K Γ1 τ1 Γ2 τ2
typed_ctx K' Γ2 τ2 Γ3 τ3
typed_ctx (K' ++ K) Γ1 τ1 Γ3 τ3.
Proof.
revert Γ1 Γ2 Γ3 τ1 τ2 τ3.
induction K' as [|k K'] => Γ1 Γ2 Γ3 τ1 τ2 τ3.
- by inversion 2; simplify_eq/=.
- intros HK.
inversion 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]; simplify_eq/=.
specialize (IHK' _ _ _ _ _ _ HK Hx2).
econstructor; eauto.
Qed.
Lemma ctx_refines_congruence Γ e1 e2 τ Γ' τ' K :
(Closed (dom _ Γ) e1)
(Closed (dom _ Γ) e2)
typed_ctx K Γ τ Γ' τ'
Γ e1 ctx e2 : τ
Γ' fill_ctx K e1 ctx fill_ctx K e2 : τ'.
Proof.
intros H1 H2 HK Hctx K' thp σ v τ'' Hτ'' Hty.
rewrite !fill_ctx_app => Hst.
apply (Hctx (K' ++ K) thp σ v τ'' Hτ''); auto.
eapply typed_ctx_compose; eauto.
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