Qcert.NRAEnv.Context.cNRAEnvContextLift
Section cNRAEnvContext.
Context {fruntime:foreign_runtime}.
Fixpoint lift_nra_context (c:nra_ctxt) : cnraenv_ctxt :=
match c with
| CHole x'
⇒ CNHole x'
| CPlug a
⇒ CNPlug (cnraenv_of_nra a)
| CABinop b c1 c2
⇒ CANBinop b (lift_nra_context c1) (lift_nra_context c2)
| CAUnop u c
⇒ CANUnop u (lift_nra_context c)
| CAMap c1 c2
⇒ CANMap (lift_nra_context c1) (lift_nra_context c2)
| CAMapConcat c1 c2
⇒ CANMapConcat (lift_nra_context c1) (lift_nra_context c2)
| CAProduct c1 c2
⇒ CANProduct (lift_nra_context c1) (lift_nra_context c2)
| CASelect c1 c2
⇒ CANSelect (lift_nra_context c1) (lift_nra_context c2)
| CADefault c1 c2
⇒ CANDefault (lift_nra_context c1) (lift_nra_context c2)
| CAEither c1 c2
⇒ CANEither (lift_nra_context c1) (lift_nra_context c2)
| CAEitherConcat c1 c2
⇒ CANEitherConcat (lift_nra_context c1) (lift_nra_context c2)
| CAApp c1 c2
⇒ CANApp (lift_nra_context c1) (lift_nra_context c2)
end.
Lemma aec_simplify_lift_commute c :
aec_simplify (lift_nra_context c) = lift_nra_context (ac_simplify c).
Lemma aec_holes_lift c:
aec_holes (lift_nra_context c) = ac_holes c.
Lemma lift_nra_context_subst c n a :
lift_nra_context (ac_subst c n a) =
aec_subst (lift_nra_context c) n (cnraenv_of_nra a).
Lemma lift_nra_context_substs c ps :
lift_nra_context (ac_substs c ps) =
aec_substs (lift_nra_context c)
(map (fun xy ⇒ (fst xy, cnraenv_of_nra (snd xy))) ps).
Definition cnraenv_eq_under h c env (op1 op2:cnraenv) : Prop :=
(∀ (x:data)
(dn_x:data_normalized h x),
h ⊢ₑ op1 @ₑ x ⊣ c;env = h ⊢ₑ op2 @ₑ x ⊣ c;env)%cnraenv.
Definition cnraenv_ctxt_equiv_under h c env (c1 c2 : cnraenv_ctxt)
:= ∀ (ps:list (nat × cnraenv)),
match aec_simplify (aec_substs c1 ps),
aec_simplify (aec_substs c2 ps)
with
| CNPlug a1, CNPlug a2 ⇒ cnraenv_eq_under h c env a1 a2
| _, _ ⇒ True
end.
Lemma cnraenv_eq_under_equiv (op1 op2:cnraenv) :
(∀ h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env), cnraenv_eq_under h c env op1 op2) ↔
cnraenv_eq op1 op2.
Lemma cnraenv_ctxt_equiv_under_equiv (op1 op2:cnraenv_ctxt) :
(∀ h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env), cnraenv_ctxt_equiv_under h c env op1 op2) ↔
cnraenv_ctxt_equiv cnraenv_eq op1 op2.
Lemma roundtrip_env e h c env :
Forall (fun x ⇒ data_normalized h (snd x)) c →
data_normalized h env →
cnraenv_eq_under h c env
((cnraenv_of_nra (nra_of_cnraenv e )
◯ (‵[| ("PBIND", ‵(env))|] ⊕ (‵[|("PCONST", ‵(drec (rec_sort c)))|] ⊕‵[| ("PDATA", ID)|])))%cnraenv)
e.
Instance ae_under_equiv h c env : Equivalence (cnraenv_eq_under h c env).
Instance aeu_Binop_proper h c env :
Proper
(eq ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANBinop.
Instance aeu_Unop_proper h c env :
Proper
(eq ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANUnop.
Instance aeu_Map_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env):
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANMap.
Instance aeu_MapConcat_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANMapConcat.
Instance aeu_Product_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANProduct.
Instance aeu_Select_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env):
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANSelect.
Instance aeu_Default_proper h c env :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANDefault.
Instance aeu_Either_proper h c env :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANEither.
Instance aeu_EitherConcat_proper h c env :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANEitherConcat.
Instance aeu_App_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env ==>
cnraenv_eq_under h c env) ANApp.
Instance aec_under_refl h c env : Reflexive (cnraenv_ctxt_equiv_under h c env).
Instance aecu_Plug_proper h c env : Proper (cnraenv_eq_under h c env ==> cnraenv_ctxt_equiv_under h c env) CNPlug.
Instance aecu_Binop_proper h c env :
Proper
(eq ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANBinop.
Instance aecu_Unop_proper h c env :
Proper
(eq ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANUnop.
Instance aecu_Map_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env):
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANMap.
Instance aecu_MapConcat_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANMapConcat.
Instance aecu_Product_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANProduct.
Instance aecu_Select_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANSelect.
Instance aecu_Default_proper h c env :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANDefault.
Instance aecu_Either_proper h c env :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANEither.
Instance aecu_EitherConcat_proper h c env :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANEitherConcat.
Instance aecu_App_proper h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) :
Proper
(cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env ==>
cnraenv_ctxt_equiv_under h c env) CANApp.
Lemma aec_substs_under_prop_part2 h c env (dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c) (dn_env:data_normalized h env) e ps1 ps2 :
Forall2 (fun xy1 xy2 ⇒ (fst xy1) = (fst xy2)
∧ cnraenv_eq_under h c env (snd xy1) (snd xy2)) ps1 ps2
→ cnraenv_ctxt_equiv_under
h c env
(aec_substs (lift_nra_context e) ps1)
(aec_substs (lift_nra_context e) ps2).
Lemma f2_roundtrip h c env ps
(dn_c:Forall (fun x ⇒ data_normalized h (snd x)) c)
(dn_env:data_normalized h env) :
Forall2
(fun xy1 xy2 : nat × cnraenv ⇒
fst xy1 = fst xy2 ∧ cnraenv_eq_under h c env (snd xy1) (snd xy2))
(map
(fun x : nat × cnraenv ⇒
(fst x,
(cnraenv_of_nra (nra_of_cnraenv (snd x))
◯ (‵[| ("PBIND", ‵(env))|] ⊕ (‵[| ("PCONST", ‵(drec (rec_sort c)))|] ⊕ ‵[| ("PDATA", ID)|])))%cnraenv))
ps) ps.
Global Instance lift_nra_context_proper : Proper (nra_ctxt_equiv nra_eq ==> cnraenv_ctxt_equiv cnraenv_eq) lift_nra_context.
Global Instance lift_nra_context_strict_proper : Proper (nra_ctxt_equiv_strict nra_eq ==> cnraenv_ctxt_equiv_strict cnraenv_eq) lift_nra_context.
This is just a restatement of lift_nra_context_proper
which visually looks more like the paper version.
For the mechanization, lift_nra_context_proper
is nicer, since it explicitly states that lift_nra_context
is a morphism between the two equivalences
and registers that relationship with the rewriting infrastructure
of Coq.
Theorem contextual_equivalence_lifting (c₁ c₂:nra_ctxt) :
c₁ ≡ₐ c₂ → lift_nra_context c₁ ≡ₑ lift_nra_context c₂.
End cNRAEnvContext.
c₁ ≡ₐ c₂ → lift_nra_context c₁ ≡ₑ lift_nra_context c₂.
End cNRAEnvContext.