Lvc.ValueOpts
Require Import CSet Le.
Require Import Plus Util AllInRel Map.
Require Import CSet Val Var Env EnvTy Equiv.Sim IL Fresh Annotation MoreExp Coherence RenamedApart.
Require Import SetOperations Liveness Filter Eqn.
Set Implicit Arguments.
Inductive eqn_sound : list (params×set var×eqns×eqns)
→ stmt → stmt
→ eqns
→ ann (set var × set var)
→ Prop :=
| EqnOpr x Lv s s´ e Gamma e´ G G´ ang
: eqn_sound Lv s s´ {EqnEq (Var x) e ; { EqnEq (Var x) e´ ; Gamma } } ang
→ entails Gamma {EqnApx e e´}
→ Exp.freeVars e´ ⊆ G
→ eqn_sound Lv (stmtLet x e s) (stmtLet x e´ s´) Gamma
(ann1 (G,G´) ang)
| EqnIf Lv e e´ s s´ t t´ Gamma G G´ ang1 ang2
: eqn_sound Lv s s´ {EqnEq (UnOp 0 e) (Con val_true); Gamma} ang1
→ eqn_sound Lv t t´ {EqnEq (UnOp 0 e) (Con val_false); Gamma} ang2
→ entails Gamma {(EqnApx e e´)}
→ eqn_sound Lv (stmtIf e s t) (stmtIf e´ s´ t´) Gamma
(ann2 (G,G´) ang1 ang2)
| EqnGoto l Y Y´ Lv Gamma Z Γf EqS Gf G G´
: get Lv (counted l) (Z,Gf,Γf, EqS)
→ length Y = length Y´
→ entails Gamma (subst_eqns (sid [Z <-- Y´]) EqS)
→ entails Gamma (list_EqnApx Y Y´)
→ eqn_sound Lv (stmtApp l Y) (stmtApp l Y´) Gamma (ann0 (G,G´))
| EqnReturn Lv e e´ Gamma G G´
: entails Gamma {(EqnApx e e´)}
→ eqn_sound Lv (stmtReturn e) (stmtReturn e´) Gamma (ann0 (G,G´))
| EqnExtern x f Lv s s´ Y Y´ Gamma G G´ ang
: eqn_sound Lv s s´ Gamma ang
→ entails Gamma (list_EqnApx Y Y´)
→ list_union (List.map Exp.freeVars Y´) ⊆ G
→ length Y = length Y´
→ eqn_sound Lv (stmtExtern x f Y s) (stmtExtern x f Y´ s´) Gamma
(ann1 (G,G´) ang)
| EqnLet Lv Z s s´ t t´ Gamma Γ2 EqS G G´ angs angb
: eqn_sound ((Z, G, Γ2, EqS)::Lv) s s´ (EqS ∪ Γ2) angs
→ eqn_sound ((Z, G ,Γ2, EqS)::Lv) t t´ Gamma angb
→ eqns_freeVars EqS ⊆ G ++ of_list Z
→ eqns_freeVars Γ2 ⊆ G
→ entails Gamma Γ2
→ eqn_sound Lv (stmtFun Z s t) (stmtFun Z s´ t´) Gamma
(ann2 (G,G´) angs angb)
| EqnUnsat Lv s s´ Gamma ang
: unsatisfiable Gamma
→ eqn_sound Lv s s´ Gamma ang.
Definition ArgRel´ (E E´:onv val) (a:list var×set var×eqns×eqns) (VL VL´: list val) : Prop :=
let ´(Z, G, Gamma, EqS) := a in
length Z = length VL
∧ VL = VL´
∧ satisfiesAll (E[Z <-- List.map Some VL]) (EqS ∪ Gamma).
Definition ParamRel´ (a:params×set var×eqns×eqns) (Z Z´ : list var) : Prop :=
let ´(Zb, G, Gamma, EqS) := a in
Z = Z´ ∧ Zb = Z.
Definition BlockRel´ (G´:set var) (V V´:onv val) (a:params×set var×eqns×eqns) (b b´:F.block) : Prop :=
let ´(Zb, G, Gamma, EqS) := a in
G ∩ of_list Zb [=] {}
∧ G ⊆ G´
∧ eqns_freeVars EqS ⊆ G ∪ of_list Zb
∧ satisfiesAll (F.block_E b) Gamma
∧ agree_on eq G (F.block_E b) V
∧ agree_on eq G (F.block_E b´) V´
∧ eqns_freeVars Gamma ⊆ G.
Instance AR lv V V´ : ProofRelation (params×set var×eqns×eqns) := {
ArgRel := ArgRel´;
ParamRel := ParamRel´;
BlockRel := BlockRel´ lv V V´
}.
Defined.
Instance subst_exp_Proper Z Y
: Proper (_eq ==> _eq) (subst_exp (sid [Z <-- Y])).
Instance subst_eqn_Proper ϱ
: Proper (_eq ==> _eq) (subst_eqn ϱ).
Instance subst_eqns_morphism
: Proper (eq ==> Equal ==> Equal) subst_eqns.
Instance subst_eqns_morphism_subset
: Proper (eq ==> Subset ==> Subset) subst_eqns.
Instance subst_eqns_morphism_subset_flip
: Proper (eq ==> flip Subset ==> flip Subset) subst_eqns.
Lemma in_subst_eqns (Gamma:eqns) ϱ gamma
: gamma ∈ Gamma
→ subst_eqn ϱ gamma ∈ subst_eqns ϱ Gamma.
Instance exp_freeVars_Proper
: Proper (eq ==> Equal) Exp.freeVars.
Instance freeVars_Proper
: Proper (_eq ==> _eq) freeVars.
Lemma eqns_freeVars_incl (Gamma:eqns) gamma
: gamma ∈ Gamma
→ freeVars gamma ⊆ eqns_freeVars Gamma.
Lemma eqns_freeVars_union Gamma Γ´
: eqns_freeVars (Gamma ∪ Γ´) [=] eqns_freeVars (Gamma) ∪ eqns_freeVars Γ´.
Lemma fold_union_add X `{OrderedType X} x Γ
: fold union ({x; Γ}) {}[=]
x ∪ fold union Γ {}.
Lemma eqns_freeVars_add Gamma e
: eqns_freeVars {e; Gamma} [=] eqns_freeVars (Gamma) ∪ freeVars e.
Lemma eqns_freeVars_add2 Gamma e e´
: eqns_freeVars ({e; { e´; Gamma } }) [=] eqns_freeVars (Gamma) ∪ freeVars e ∪ freeVars e´.
Lemma eqns_freeVars_add´ Gamma e
: eqns_freeVars ({e ; Gamma}) [=] eqns_freeVars (Gamma) ∪ freeVars e.
Ltac dowith c t :=
match goal with
| [ H : c _ _ _ _ |- _ ] ⇒ t H
end.
Lemma satisfiesAll_union E Gamma Γ´
: satisfiesAll E (Gamma ∪ Γ´)
↔ satisfiesAll E Gamma ∧ satisfiesAll E Γ´.
Lemma satisfies_update_dead E gamma x v
: satisfies E gamma
→ x ∉ freeVars gamma
→ satisfies (E[x <- v]) gamma.
Lemma satisfiesAll_add E gamma Gamma
: satisfiesAll E {gamma ; Gamma}
↔ satisfies E gamma ∧ satisfiesAll E Gamma.
Lemma satisfies_update_dead_list E gamma Z vl
: length Z = length vl
→ satisfies E gamma
→ freeVars gamma ∩ of_list Z [=] ∅
→ satisfies (E[Z <-- vl]) gamma.
Lemma satisfiesAll_update_dead E Gamma Z vl
: length Z = length vl
→ satisfiesAll E Gamma
→ eqns_freeVars Gamma ∩ of_list Z [=] ∅
→ satisfiesAll (E[Z <-- vl]) Gamma.
Lemma eval_exp_subst E y Y Z e
: length Z = length Y
→ ⎣y ⎦ = omap (exp_eval E) Y
→ exp_eval (E [Z <-- List.map Some y]) e =
exp_eval E (subst_exp (sid [Z <-- Y]) e).
Lemma agree_on_onvLe {X} `{OrderedType.OrderedType X} (V V´:onv X) Z vl
: onvLe V V´
→ onvLe (V [Z <-- vl]) (V´ [Z <-- vl]).
Lemma simL´_update r A (AR AR´:ProofRelation A) LV L L´ L1 L2
: AIR5 (simB sim_progeq r AR) L L´ LV L1 L2
→ (∀ x b b´, @BlockRel _ AR x b b´ → @BlockRel _ AR´ x b b´)
→ (∀ a Z Z´, @ParamRel _ AR a Z Z´ → @ParamRel _ AR´ a Z Z´)
→ (∀ V V´ a VL VL´, @ArgRel _ AR V V´ a VL VL´ ↔ @ArgRel _ AR´ V V´ a VL VL´)
→ L = L1
→ L´ = L2
→ AIR5 (simB sim_progeq r AR´) L L´ LV L1 L2.
Lemma entails_subset Γ Γ´
: Γ´ ⊆ Γ
→ entails Γ Γ´.
Lemma entails_add Gamma gamma Γ´
: entails Gamma ({{gamma}} ∪ Γ´)
→ entails Gamma Γ´.
Lemma entails_add´ Gamma gamma Γ´
: entails Gamma Γ´
→ entails Gamma {{gamma}}
→ entails Gamma {gamma; Γ´}.
Lemma entails_monotonic_add Gamma Γ´ gamma
: entails Gamma Γ´ → entails (gamma ∪ Gamma) Γ´.
Lemma entails_union_split Gamma Γ´ Γ´´
: entails Gamma (Γ´ ∪ Γ´´)
→ entails Gamma (Γ´)
∧ entails Gamma (Γ´´).
Lemma entails_union Gamma Γ´ Γ´´
: entails Gamma (Γ´)
∧ entails Gamma (Γ´´)
→ entails Gamma (Γ´ ∪ Γ´´).
Lemma entails_add_single Gamma gamma Γ´
: entails Gamma Γ´
→ entails Gamma {gamma}
→ entails Gamma {gamma; Γ´}.
Instance satisfiesAll_Equal_morphism
: Proper (eq ==> Equal ==> iff) satisfiesAll.
Lemma entails_monotone Γ1 Γ2 Γ1´
: entails Γ1 Γ2
→ Γ1 ⊆ Γ1´
→ entails Γ1´ Γ2.
Instance entails_morphism_add gamma
: Proper (entails ==> entails) (add gamma).
Instance map_freeVars_morphism
: Proper (Subset ==> Subset) (map freeVars).
Instance eqns_freeVars_morphism
: Proper (Subset ==> Subset) eqns_freeVars.
Instance eqns_freeVars_morphism_flip
: Proper (flip Subset ==> flip Subset) eqns_freeVars.
Instance eqns_freeVars_morphism_equal
: Proper (Equal ==> Equal) eqns_freeVars.
Instance entails_morphism_impl
: Proper (Subset ==> flip Subset ==> impl) entails.
Instance entails_morphism_flip_impl
: Proper (flip Subset ==> Subset ==> flip impl) entails.
Instance entails_morphism_impl_iff
: Proper (Equal ==> Equal ==> iff) entails.
Lemma entails_union´ Gamma Γ´ Γ´´ Γ´´´
: Γ´´´ ⊆ Γ´ ∪ Γ´´
→ entails Gamma (Γ´)
→ entails Gamma (Γ´´)
→ entails Gamma (Γ´´´).
Instance entails_refl
: Reflexive (entails).
Lemma entails_empty s
: entails s ∅.
Lemma entails_eqns_trans Gamma e e´ e´´
: EqnEq e e´ ∈ Gamma
→ EqnEq e´ e´´ ∈ Gamma
→ entails Gamma {EqnEq e e´´}.
Lemma entails_eqns_apx_refl e Gamma
: entails Gamma {EqnApx e e}.
Lemma satisfiesAll_subst V Gamma Γf Z EqS Y y bE G
: length Z = length Y
→ eqns_freeVars EqS ⊆ G ∪ of_list Z
→ G ∩ of_list Z [=] ∅
→ entails Gamma (subst_eqns (sid [Z <-- Y]) EqS)
→ satisfiesAll V Gamma
→ agree_on eq G V bE
→ ⎣y ⎦ = omap (exp_eval V) Y
→ satisfiesAll bE Γf
→ satisfiesAll (bE [Z <-- List.map Some y]) EqS.
Lemma in_eqns_freeVars x gamma Gamma
: x \In freeVars gamma
→ gamma ∈ Gamma
→ x \In eqns_freeVars Gamma.
Lemma satisfiesAll_update x Gamma V e e´ y
: x ∉ eqns_freeVars Gamma
→ x ∉ Exp.freeVars e
→ x ∉ Exp.freeVars e´
→ satisfiesAll V Gamma
→ ⎣y ⎦ = exp_eval V e
→ ⎣y ⎦ = exp_eval V e´
→ satisfiesAll (V [x <- ⎣y ⎦])
({EqnEq (Var x) e ; {EqnEq (Var x) e´; Gamma } }).
Lemma satisfiesAll_update_dead_single x Gamma V y
: x ∉ eqns_freeVars Gamma
→ satisfiesAll V Gamma
→ satisfiesAll (V [x <- ⎣y ⎦]) Gamma.
Lemma satisfiesAll_monotone E Gamma Γ´
: satisfiesAll E Gamma
→ Γ´ ⊆ Gamma
→ satisfiesAll E Γ´.
Lemma not_entails_antitone Gamma Γ´ gamma
: not_entails Γ´ gamma
→ Gamma ⊆ Γ´
→ not_entails Gamma gamma.
Lemma unsatisfiable_monotone Gamma Γ´
: unsatisfiable Gamma
→ Gamma ⊆ Γ´
→ unsatisfiable Γ´.
Lemma eqn_sound_monotone Es Γ1 Γ1´ s s´ ang
: renamedApart s ang
→ eqn_sound Es s s´ Γ1 ang
→ Γ1 ⊆ Γ1´
→ eqn_sound Es s s´ Γ1´ ang.
Instance entails_entails_morphism_impl
: Proper (flip entails ==> entails ==> impl) entails.
Instance entails_entails_morphism_flip_impl
: Proper (entails ==> flip entails ==> flip impl) entails.
Lemma entails_inert Γ1 Γ2 Γ2´
: entails Γ2 Γ2´
→ entails (Γ1 ∪ Γ2) (Γ1 ∪ Γ2´).
Lemma entails_inert_add x Γ2 Γ2´
: entails Γ2 Γ2´
→ entails {x ; Γ2} {x ; Γ2´}.
Lemma entails_transitive Γ Γ´ Γ´´
: entails Γ Γ´ → entails Γ´ Γ´´ → entails Γ Γ´´.
Instance entails_trans : Transitive entails.
Lemma not_entails_entails_antitone Gamma Γ´ gamma
: not_entails Γ´ gamma
→ entails Γ´ Gamma
→ not_entails Gamma gamma.
Lemma unsatisfiable_entails_monotone Gamma Γ´
: unsatisfiable Gamma
→ entails Γ´ Gamma
→ unsatisfiable Γ´.
Lemma eqn_sound_entails_monotone Es Γ1 Γ1´ s s´ ang
: renamedApart s ang
→ eqn_sound Es s s´ Γ1 ang
→ entails Γ1´ Γ1
→ eqn_sound Es s s´ Γ1´ ang.
Lemma omap_exp_eval_onvLe Y E E´ v
: onvLe E E´
→ omap (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v.
Lemma omap_satisfies_list_EqnApx V Y Y´ v
: length Y = length Y´
→ satisfiesAll V (list_EqnApx Y Y´)
→ omap (exp_eval V) Y = ⎣ v ⎦
→ omap (exp_eval V) Y´ = ⎣ v ⎦.
Lemma sim_vopt r L L´ V V´ s s´ LV Gamma ang
: satisfiesAll V Gamma
→ eqn_sound LV s s´ Gamma ang
→ simL´ sim_progeq r (AR (fst (getAnn ang)) V V´) LV L L´
→ renamedApart s ang
→ eqns_freeVars Gamma ⊆ fst (getAnn ang)
→ onvLe V V´
→ sim´r r (L,V, s) (L´,V´, s´).
Print Assumptions sim_vopt.
Require Import Plus Util AllInRel Map.
Require Import CSet Val Var Env EnvTy Equiv.Sim IL Fresh Annotation MoreExp Coherence RenamedApart.
Require Import SetOperations Liveness Filter Eqn.
Set Implicit Arguments.
Inductive eqn_sound : list (params×set var×eqns×eqns)
→ stmt → stmt
→ eqns
→ ann (set var × set var)
→ Prop :=
| EqnOpr x Lv s s´ e Gamma e´ G G´ ang
: eqn_sound Lv s s´ {EqnEq (Var x) e ; { EqnEq (Var x) e´ ; Gamma } } ang
→ entails Gamma {EqnApx e e´}
→ Exp.freeVars e´ ⊆ G
→ eqn_sound Lv (stmtLet x e s) (stmtLet x e´ s´) Gamma
(ann1 (G,G´) ang)
| EqnIf Lv e e´ s s´ t t´ Gamma G G´ ang1 ang2
: eqn_sound Lv s s´ {EqnEq (UnOp 0 e) (Con val_true); Gamma} ang1
→ eqn_sound Lv t t´ {EqnEq (UnOp 0 e) (Con val_false); Gamma} ang2
→ entails Gamma {(EqnApx e e´)}
→ eqn_sound Lv (stmtIf e s t) (stmtIf e´ s´ t´) Gamma
(ann2 (G,G´) ang1 ang2)
| EqnGoto l Y Y´ Lv Gamma Z Γf EqS Gf G G´
: get Lv (counted l) (Z,Gf,Γf, EqS)
→ length Y = length Y´
→ entails Gamma (subst_eqns (sid [Z <-- Y´]) EqS)
→ entails Gamma (list_EqnApx Y Y´)
→ eqn_sound Lv (stmtApp l Y) (stmtApp l Y´) Gamma (ann0 (G,G´))
| EqnReturn Lv e e´ Gamma G G´
: entails Gamma {(EqnApx e e´)}
→ eqn_sound Lv (stmtReturn e) (stmtReturn e´) Gamma (ann0 (G,G´))
| EqnExtern x f Lv s s´ Y Y´ Gamma G G´ ang
: eqn_sound Lv s s´ Gamma ang
→ entails Gamma (list_EqnApx Y Y´)
→ list_union (List.map Exp.freeVars Y´) ⊆ G
→ length Y = length Y´
→ eqn_sound Lv (stmtExtern x f Y s) (stmtExtern x f Y´ s´) Gamma
(ann1 (G,G´) ang)
| EqnLet Lv Z s s´ t t´ Gamma Γ2 EqS G G´ angs angb
: eqn_sound ((Z, G, Γ2, EqS)::Lv) s s´ (EqS ∪ Γ2) angs
→ eqn_sound ((Z, G ,Γ2, EqS)::Lv) t t´ Gamma angb
→ eqns_freeVars EqS ⊆ G ++ of_list Z
→ eqns_freeVars Γ2 ⊆ G
→ entails Gamma Γ2
→ eqn_sound Lv (stmtFun Z s t) (stmtFun Z s´ t´) Gamma
(ann2 (G,G´) angs angb)
| EqnUnsat Lv s s´ Gamma ang
: unsatisfiable Gamma
→ eqn_sound Lv s s´ Gamma ang.
Definition ArgRel´ (E E´:onv val) (a:list var×set var×eqns×eqns) (VL VL´: list val) : Prop :=
let ´(Z, G, Gamma, EqS) := a in
length Z = length VL
∧ VL = VL´
∧ satisfiesAll (E[Z <-- List.map Some VL]) (EqS ∪ Gamma).
Definition ParamRel´ (a:params×set var×eqns×eqns) (Z Z´ : list var) : Prop :=
let ´(Zb, G, Gamma, EqS) := a in
Z = Z´ ∧ Zb = Z.
Definition BlockRel´ (G´:set var) (V V´:onv val) (a:params×set var×eqns×eqns) (b b´:F.block) : Prop :=
let ´(Zb, G, Gamma, EqS) := a in
G ∩ of_list Zb [=] {}
∧ G ⊆ G´
∧ eqns_freeVars EqS ⊆ G ∪ of_list Zb
∧ satisfiesAll (F.block_E b) Gamma
∧ agree_on eq G (F.block_E b) V
∧ agree_on eq G (F.block_E b´) V´
∧ eqns_freeVars Gamma ⊆ G.
Instance AR lv V V´ : ProofRelation (params×set var×eqns×eqns) := {
ArgRel := ArgRel´;
ParamRel := ParamRel´;
BlockRel := BlockRel´ lv V V´
}.
Defined.
Instance subst_exp_Proper Z Y
: Proper (_eq ==> _eq) (subst_exp (sid [Z <-- Y])).
Instance subst_eqn_Proper ϱ
: Proper (_eq ==> _eq) (subst_eqn ϱ).
Instance subst_eqns_morphism
: Proper (eq ==> Equal ==> Equal) subst_eqns.
Instance subst_eqns_morphism_subset
: Proper (eq ==> Subset ==> Subset) subst_eqns.
Instance subst_eqns_morphism_subset_flip
: Proper (eq ==> flip Subset ==> flip Subset) subst_eqns.
Lemma in_subst_eqns (Gamma:eqns) ϱ gamma
: gamma ∈ Gamma
→ subst_eqn ϱ gamma ∈ subst_eqns ϱ Gamma.
Instance exp_freeVars_Proper
: Proper (eq ==> Equal) Exp.freeVars.
Instance freeVars_Proper
: Proper (_eq ==> _eq) freeVars.
Lemma eqns_freeVars_incl (Gamma:eqns) gamma
: gamma ∈ Gamma
→ freeVars gamma ⊆ eqns_freeVars Gamma.
Lemma eqns_freeVars_union Gamma Γ´
: eqns_freeVars (Gamma ∪ Γ´) [=] eqns_freeVars (Gamma) ∪ eqns_freeVars Γ´.
Lemma fold_union_add X `{OrderedType X} x Γ
: fold union ({x; Γ}) {}[=]
x ∪ fold union Γ {}.
Lemma eqns_freeVars_add Gamma e
: eqns_freeVars {e; Gamma} [=] eqns_freeVars (Gamma) ∪ freeVars e.
Lemma eqns_freeVars_add2 Gamma e e´
: eqns_freeVars ({e; { e´; Gamma } }) [=] eqns_freeVars (Gamma) ∪ freeVars e ∪ freeVars e´.
Lemma eqns_freeVars_add´ Gamma e
: eqns_freeVars ({e ; Gamma}) [=] eqns_freeVars (Gamma) ∪ freeVars e.
Ltac dowith c t :=
match goal with
| [ H : c _ _ _ _ |- _ ] ⇒ t H
end.
Lemma satisfiesAll_union E Gamma Γ´
: satisfiesAll E (Gamma ∪ Γ´)
↔ satisfiesAll E Gamma ∧ satisfiesAll E Γ´.
Lemma satisfies_update_dead E gamma x v
: satisfies E gamma
→ x ∉ freeVars gamma
→ satisfies (E[x <- v]) gamma.
Lemma satisfiesAll_add E gamma Gamma
: satisfiesAll E {gamma ; Gamma}
↔ satisfies E gamma ∧ satisfiesAll E Gamma.
Lemma satisfies_update_dead_list E gamma Z vl
: length Z = length vl
→ satisfies E gamma
→ freeVars gamma ∩ of_list Z [=] ∅
→ satisfies (E[Z <-- vl]) gamma.
Lemma satisfiesAll_update_dead E Gamma Z vl
: length Z = length vl
→ satisfiesAll E Gamma
→ eqns_freeVars Gamma ∩ of_list Z [=] ∅
→ satisfiesAll (E[Z <-- vl]) Gamma.
Lemma eval_exp_subst E y Y Z e
: length Z = length Y
→ ⎣y ⎦ = omap (exp_eval E) Y
→ exp_eval (E [Z <-- List.map Some y]) e =
exp_eval E (subst_exp (sid [Z <-- Y]) e).
Lemma agree_on_onvLe {X} `{OrderedType.OrderedType X} (V V´:onv X) Z vl
: onvLe V V´
→ onvLe (V [Z <-- vl]) (V´ [Z <-- vl]).
Lemma simL´_update r A (AR AR´:ProofRelation A) LV L L´ L1 L2
: AIR5 (simB sim_progeq r AR) L L´ LV L1 L2
→ (∀ x b b´, @BlockRel _ AR x b b´ → @BlockRel _ AR´ x b b´)
→ (∀ a Z Z´, @ParamRel _ AR a Z Z´ → @ParamRel _ AR´ a Z Z´)
→ (∀ V V´ a VL VL´, @ArgRel _ AR V V´ a VL VL´ ↔ @ArgRel _ AR´ V V´ a VL VL´)
→ L = L1
→ L´ = L2
→ AIR5 (simB sim_progeq r AR´) L L´ LV L1 L2.
Lemma entails_subset Γ Γ´
: Γ´ ⊆ Γ
→ entails Γ Γ´.
Lemma entails_add Gamma gamma Γ´
: entails Gamma ({{gamma}} ∪ Γ´)
→ entails Gamma Γ´.
Lemma entails_add´ Gamma gamma Γ´
: entails Gamma Γ´
→ entails Gamma {{gamma}}
→ entails Gamma {gamma; Γ´}.
Lemma entails_monotonic_add Gamma Γ´ gamma
: entails Gamma Γ´ → entails (gamma ∪ Gamma) Γ´.
Lemma entails_union_split Gamma Γ´ Γ´´
: entails Gamma (Γ´ ∪ Γ´´)
→ entails Gamma (Γ´)
∧ entails Gamma (Γ´´).
Lemma entails_union Gamma Γ´ Γ´´
: entails Gamma (Γ´)
∧ entails Gamma (Γ´´)
→ entails Gamma (Γ´ ∪ Γ´´).
Lemma entails_add_single Gamma gamma Γ´
: entails Gamma Γ´
→ entails Gamma {gamma}
→ entails Gamma {gamma; Γ´}.
Instance satisfiesAll_Equal_morphism
: Proper (eq ==> Equal ==> iff) satisfiesAll.
Lemma entails_monotone Γ1 Γ2 Γ1´
: entails Γ1 Γ2
→ Γ1 ⊆ Γ1´
→ entails Γ1´ Γ2.
Instance entails_morphism_add gamma
: Proper (entails ==> entails) (add gamma).
Instance map_freeVars_morphism
: Proper (Subset ==> Subset) (map freeVars).
Instance eqns_freeVars_morphism
: Proper (Subset ==> Subset) eqns_freeVars.
Instance eqns_freeVars_morphism_flip
: Proper (flip Subset ==> flip Subset) eqns_freeVars.
Instance eqns_freeVars_morphism_equal
: Proper (Equal ==> Equal) eqns_freeVars.
Instance entails_morphism_impl
: Proper (Subset ==> flip Subset ==> impl) entails.
Instance entails_morphism_flip_impl
: Proper (flip Subset ==> Subset ==> flip impl) entails.
Instance entails_morphism_impl_iff
: Proper (Equal ==> Equal ==> iff) entails.
Lemma entails_union´ Gamma Γ´ Γ´´ Γ´´´
: Γ´´´ ⊆ Γ´ ∪ Γ´´
→ entails Gamma (Γ´)
→ entails Gamma (Γ´´)
→ entails Gamma (Γ´´´).
Instance entails_refl
: Reflexive (entails).
Lemma entails_empty s
: entails s ∅.
Lemma entails_eqns_trans Gamma e e´ e´´
: EqnEq e e´ ∈ Gamma
→ EqnEq e´ e´´ ∈ Gamma
→ entails Gamma {EqnEq e e´´}.
Lemma entails_eqns_apx_refl e Gamma
: entails Gamma {EqnApx e e}.
Lemma satisfiesAll_subst V Gamma Γf Z EqS Y y bE G
: length Z = length Y
→ eqns_freeVars EqS ⊆ G ∪ of_list Z
→ G ∩ of_list Z [=] ∅
→ entails Gamma (subst_eqns (sid [Z <-- Y]) EqS)
→ satisfiesAll V Gamma
→ agree_on eq G V bE
→ ⎣y ⎦ = omap (exp_eval V) Y
→ satisfiesAll bE Γf
→ satisfiesAll (bE [Z <-- List.map Some y]) EqS.
Lemma in_eqns_freeVars x gamma Gamma
: x \In freeVars gamma
→ gamma ∈ Gamma
→ x \In eqns_freeVars Gamma.
Lemma satisfiesAll_update x Gamma V e e´ y
: x ∉ eqns_freeVars Gamma
→ x ∉ Exp.freeVars e
→ x ∉ Exp.freeVars e´
→ satisfiesAll V Gamma
→ ⎣y ⎦ = exp_eval V e
→ ⎣y ⎦ = exp_eval V e´
→ satisfiesAll (V [x <- ⎣y ⎦])
({EqnEq (Var x) e ; {EqnEq (Var x) e´; Gamma } }).
Lemma satisfiesAll_update_dead_single x Gamma V y
: x ∉ eqns_freeVars Gamma
→ satisfiesAll V Gamma
→ satisfiesAll (V [x <- ⎣y ⎦]) Gamma.
Lemma satisfiesAll_monotone E Gamma Γ´
: satisfiesAll E Gamma
→ Γ´ ⊆ Gamma
→ satisfiesAll E Γ´.
Lemma not_entails_antitone Gamma Γ´ gamma
: not_entails Γ´ gamma
→ Gamma ⊆ Γ´
→ not_entails Gamma gamma.
Lemma unsatisfiable_monotone Gamma Γ´
: unsatisfiable Gamma
→ Gamma ⊆ Γ´
→ unsatisfiable Γ´.
Lemma eqn_sound_monotone Es Γ1 Γ1´ s s´ ang
: renamedApart s ang
→ eqn_sound Es s s´ Γ1 ang
→ Γ1 ⊆ Γ1´
→ eqn_sound Es s s´ Γ1´ ang.
Instance entails_entails_morphism_impl
: Proper (flip entails ==> entails ==> impl) entails.
Instance entails_entails_morphism_flip_impl
: Proper (entails ==> flip entails ==> flip impl) entails.
Lemma entails_inert Γ1 Γ2 Γ2´
: entails Γ2 Γ2´
→ entails (Γ1 ∪ Γ2) (Γ1 ∪ Γ2´).
Lemma entails_inert_add x Γ2 Γ2´
: entails Γ2 Γ2´
→ entails {x ; Γ2} {x ; Γ2´}.
Lemma entails_transitive Γ Γ´ Γ´´
: entails Γ Γ´ → entails Γ´ Γ´´ → entails Γ Γ´´.
Instance entails_trans : Transitive entails.
Lemma not_entails_entails_antitone Gamma Γ´ gamma
: not_entails Γ´ gamma
→ entails Γ´ Gamma
→ not_entails Gamma gamma.
Lemma unsatisfiable_entails_monotone Gamma Γ´
: unsatisfiable Gamma
→ entails Γ´ Gamma
→ unsatisfiable Γ´.
Lemma eqn_sound_entails_monotone Es Γ1 Γ1´ s s´ ang
: renamedApart s ang
→ eqn_sound Es s s´ Γ1 ang
→ entails Γ1´ Γ1
→ eqn_sound Es s s´ Γ1´ ang.
Lemma omap_exp_eval_onvLe Y E E´ v
: onvLe E E´
→ omap (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v.
Lemma omap_satisfies_list_EqnApx V Y Y´ v
: length Y = length Y´
→ satisfiesAll V (list_EqnApx Y Y´)
→ omap (exp_eval V) Y = ⎣ v ⎦
→ omap (exp_eval V) Y´ = ⎣ v ⎦.
Lemma sim_vopt r L L´ V V´ s s´ LV Gamma ang
: satisfiesAll V Gamma
→ eqn_sound LV s s´ Gamma ang
→ simL´ sim_progeq r (AR (fst (getAnn ang)) V V´) LV L L´
→ renamedApart s ang
→ eqns_freeVars Gamma ⊆ fst (getAnn ang)
→ onvLe V V´
→ sim´r r (L,V, s) (L´,V´, s´).
Print Assumptions sim_vopt.