Library dev
Require Import Coq.Setoids.Setoid.
Require Import Basics.
Require Import Relations.
Require Import Bool.
Section S.
(* --------------------------------------------------------------------------
Connection between the notations of the article
and the coq definitions
-------------------------------------------------------------------------- *)
(* For each type and operator of the article, we bind the related coq definition,
and the coq notation whenever it exists.
expression : Exp
variables : Var
values : Value
environment : Env
update of environment ρ[x ↦ v] : update ρ x v
evaluation of an expression in an environment 〚e〛ρ : eval_expr e ρ
truth value of numerical values T(v) : eval_value v
dependences of expressions deps : deps
Underlying domain L : L
join ⊔ : join2 ⊔² ( Infinitary operator : join ⊔ )
narrow ⊓ : narrow2 ⊓² ( Infinitary operator : narrow ⊓ )
partial order ⊑ : incl ⊑
top ⊤ : top
bottom ⊥ : bottom
concretization γ : concr
transfer functions 〚·〛♯
for assignments 〚var := exp〛♯ : assign var exp
for tests 〚exp ◃〛♯ : assume exp
Predicates (p: C) : (p: pred)
true : PTrue
false : PFalse
not ¬ : PNot
and ∧ : PAnd
or ∨ : POr
entailment ⊢ : pred_implies ⊢
equivalence ⊣⊢ : pred_equiv ⊣⊢
evaluation on predicates:
- for an arbitrary valuation [val] from expressions to values : eval_pred val
- for an environment [env] from variables to values : eval_pred' env
kill function on predicates:
- kill+(x, p) : weaken_pred p x (replaces [x] by PTrue in [p])
- kill-(x, p) : strengthen_pred p x (replaces [x] by PFalse in [p])
CI-pairs (Φ: Lᵖʳᵉᵈ) : (ci: CI)
consequence "Φ ↓ p" : (consequence ci p) "ci ∎ p"
partial order ⊑↓ : CI_incl ⋐
equivalence ∼↓ : CI_equiv ≣
join ⊔↓ₚ : CI_join ⋓
narrow ⊓↓ₚ : CI_narrow ⋒
weak-join ⊔ₚ : CI_weak_join
optimized weak-join : CI_opt_weak_join
top : CI_top
bottom : CI_bottom
concretisation : CI_concr
transfer functions 〚·〛♯ₚ
for assignements 〚var := exp〛♯ₚ : CI_assign var exp
for tests 〚exp ◃〛♯ₚ : CI_assume exp
*)
(* --------------------------------------------------------------------------
Parameters of the development
-------------------------------------------------------------------------- *)
Variable Value: Type. (* Numerical Values *)
Variable Var: Type. (* Variables *)
Variable Exp: Type. (* Expressions *)
Variable E_dec: ∀ (e1 e2: Exp), {e1 = e2} + {¬e1 = e2}.
Definition Env: Type := Var → Value. (* Concrete state: environment *)
Variable eval_expr: Env → Exp → Value. (* Evaluation of expressions in an environment. *)
Variable eval_value: Value → Prop. (* Embedding values in Prop. *)
(* Assignment of a variable in an environment. *)
Variable update : Env → Var → Value → Env.
(* [update env var val] maps [var] to [val] and every other variables [var'] to
their previous value in [env]. *)
Variable update_correct : ∀ env var val,
(update env var val) var = val
∧ ∀ var', var' ≠ var → (update env var val) var' = env var'.
(* Dependence of an expression *)
Variable deps : Exp → Var → bool.
(* If the expression [exp] don't depend on the variable [var],
the an update of [var] don't affect the evaluation of [exp]. *)
Variable deps_correct : ∀ env var exp,
deps exp var = false
→ ∀ val, eval_expr (update env var val) exp = eval_expr env exp.
Require Import Basics.
Require Import Relations.
Require Import Bool.
Section S.
(* --------------------------------------------------------------------------
Connection between the notations of the article
and the coq definitions
-------------------------------------------------------------------------- *)
(* For each type and operator of the article, we bind the related coq definition,
and the coq notation whenever it exists.
expression : Exp
variables : Var
values : Value
environment : Env
update of environment ρ[x ↦ v] : update ρ x v
evaluation of an expression in an environment 〚e〛ρ : eval_expr e ρ
truth value of numerical values T(v) : eval_value v
dependences of expressions deps : deps
Underlying domain L : L
join ⊔ : join2 ⊔² ( Infinitary operator : join ⊔ )
narrow ⊓ : narrow2 ⊓² ( Infinitary operator : narrow ⊓ )
partial order ⊑ : incl ⊑
top ⊤ : top
bottom ⊥ : bottom
concretization γ : concr
transfer functions 〚·〛♯
for assignments 〚var := exp〛♯ : assign var exp
for tests 〚exp ◃〛♯ : assume exp
Predicates (p: C) : (p: pred)
true : PTrue
false : PFalse
not ¬ : PNot
and ∧ : PAnd
or ∨ : POr
entailment ⊢ : pred_implies ⊢
equivalence ⊣⊢ : pred_equiv ⊣⊢
evaluation on predicates:
- for an arbitrary valuation [val] from expressions to values : eval_pred val
- for an environment [env] from variables to values : eval_pred' env
kill function on predicates:
- kill+(x, p) : weaken_pred p x (replaces [x] by PTrue in [p])
- kill-(x, p) : strengthen_pred p x (replaces [x] by PFalse in [p])
CI-pairs (Φ: Lᵖʳᵉᵈ) : (ci: CI)
consequence "Φ ↓ p" : (consequence ci p) "ci ∎ p"
partial order ⊑↓ : CI_incl ⋐
equivalence ∼↓ : CI_equiv ≣
join ⊔↓ₚ : CI_join ⋓
narrow ⊓↓ₚ : CI_narrow ⋒
weak-join ⊔ₚ : CI_weak_join
optimized weak-join : CI_opt_weak_join
top : CI_top
bottom : CI_bottom
concretisation : CI_concr
transfer functions 〚·〛♯ₚ
for assignements 〚var := exp〛♯ₚ : CI_assign var exp
for tests 〚exp ◃〛♯ₚ : CI_assume exp
*)
(* --------------------------------------------------------------------------
Parameters of the development
-------------------------------------------------------------------------- *)
Variable Value: Type. (* Numerical Values *)
Variable Var: Type. (* Variables *)
Variable Exp: Type. (* Expressions *)
Variable E_dec: ∀ (e1 e2: Exp), {e1 = e2} + {¬e1 = e2}.
Definition Env: Type := Var → Value. (* Concrete state: environment *)
Variable eval_expr: Env → Exp → Value. (* Evaluation of expressions in an environment. *)
Variable eval_value: Value → Prop. (* Embedding values in Prop. *)
(* Assignment of a variable in an environment. *)
Variable update : Env → Var → Value → Env.
(* [update env var val] maps [var] to [val] and every other variables [var'] to
their previous value in [env]. *)
Variable update_correct : ∀ env var val,
(update env var val) var = val
∧ ∀ var', var' ≠ var → (update env var val) var' = env var'.
(* Dependence of an expression *)
Variable deps : Exp → Var → bool.
(* If the expression [exp] don't depend on the variable [var],
the an update of [var] don't affect the evaluation of [exp]. *)
Variable deps_correct : ∀ env var exp,
deps exp var = false
→ ∀ val, eval_expr (update env var val) exp = eval_expr env exp.
Underlying Abstract Domain
Lattice structure
Variable join: (L → Prop) → L.
Variable narrow: (L → Prop) → L.
Variable incl: L → L → Prop. (* Order relation *)
Variable bottom: L.
Variable top: L.
Notation "x ⊑ y" := (incl x y) (at level 30, no associativity) : type_scope.
Notation "⊔ s" := (join s) (at level 20, no associativity) : type_scope.
Notation "⊓ s" := (narrow s) (at level 20, no associativity) : type_scope.
(* ⊑ is an order relation *)
Variable incl_trans: ∀ l1 l2 l3, l1 ⊑ l2 → l2 ⊑ l3 → l1 ⊑ l3.
Variable incl_refl: ∀ l, l ⊑ l.
Variable incl_asym: ∀ l1 l2, l1 ⊑ l2 → l2 ⊑ l1 → l1 = l2.
(* [top] and [bottom] are respectively the greatest and the least element of L *)
Variable bottom_smallest: ∀ l, bottom ⊑ l.
Variable top_biggest: ∀ l, l ⊑ top.
(* [⊔ val] is the least upper bound of elements l such that [val l] *)
Variable join_bigger: ∀ l, ∀ (val: L → Prop), val l → l ⊑ ⊔ val.
Variable join_smallest: ∀ l, ∀ (val: L → Prop), (∀ l', val l' → l' ⊑ l) → ⊔ val ⊑ l.
(* [⊓ val] is the greatest lower bound of elements l such that [val l] *)
Variable narrow_smaller: ∀ l, ∀ (val: L → Prop), val l → ⊓ val ⊑ l.
Variable narrow_biggest: ∀ (val: L → Prop) l, (∀ l', val l' → l ⊑ l') → l ⊑ ⊓ val.
Variable L_dec: ∀ (l1 l2: L), {l1 = l2} + {¬l1 = l2}.
Add Parametric Relation: _ incl
reflexivity proved by incl_refl
transitivity proved by incl_trans
as rel_incl.
Variable narrow: (L → Prop) → L.
Variable incl: L → L → Prop. (* Order relation *)
Variable bottom: L.
Variable top: L.
Notation "x ⊑ y" := (incl x y) (at level 30, no associativity) : type_scope.
Notation "⊔ s" := (join s) (at level 20, no associativity) : type_scope.
Notation "⊓ s" := (narrow s) (at level 20, no associativity) : type_scope.
(* ⊑ is an order relation *)
Variable incl_trans: ∀ l1 l2 l3, l1 ⊑ l2 → l2 ⊑ l3 → l1 ⊑ l3.
Variable incl_refl: ∀ l, l ⊑ l.
Variable incl_asym: ∀ l1 l2, l1 ⊑ l2 → l2 ⊑ l1 → l1 = l2.
(* [top] and [bottom] are respectively the greatest and the least element of L *)
Variable bottom_smallest: ∀ l, bottom ⊑ l.
Variable top_biggest: ∀ l, l ⊑ top.
(* [⊔ val] is the least upper bound of elements l such that [val l] *)
Variable join_bigger: ∀ l, ∀ (val: L → Prop), val l → l ⊑ ⊔ val.
Variable join_smallest: ∀ l, ∀ (val: L → Prop), (∀ l', val l' → l' ⊑ l) → ⊔ val ⊑ l.
(* [⊓ val] is the greatest lower bound of elements l such that [val l] *)
Variable narrow_smaller: ∀ l, ∀ (val: L → Prop), val l → ⊓ val ⊑ l.
Variable narrow_biggest: ∀ (val: L → Prop) l, (∀ l', val l' → l ⊑ l') → l ⊑ ⊓ val.
Variable L_dec: ∀ (l1 l2: L), {l1 = l2} + {¬l1 = l2}.
Add Parametric Relation: _ incl
reflexivity proved by incl_refl
transitivity proved by incl_trans
as rel_incl.
Concretization: [concr l env] means that [env] si a concretization of [l].
Variable concr: L → Env → Prop.
(* The concretization is monotone, the concretization of [top] is the set of
all environments and the concretization of [bottom] is empty. *)
Variable concr_monotone: ∀ x y e, x ⊑ y → concr x e → concr y e.
Variable concr_top: ∀ e, concr top e.
Variable concr_bottom: ∀ e, ¬ concr bottom e.
(* The join is an over-approximation (through [concr]) of the union of
sets of environments: conséquence of the lattice structure and the monotony
of the concretization. *)
Lemma join_correct: ∀ val e,
(∃ l, val l ∧ concr l e) → concr (join val) e.
Proof.
intros val e [l [Hval Hconcr]]. apply concr_monotone with l.
apply join_bigger. assumption. assumption.
Qed.
(* The narrow is an over-approximation of the intersection of sets of
environments. *)
Variable narrow_correct: ∀ (val: L → Prop) (e: Env),
(∀ l, val l → concr l e) → concr (narrow val) e.
(* The concretization is monotone, the concretization of [top] is the set of
all environments and the concretization of [bottom] is empty. *)
Variable concr_monotone: ∀ x y e, x ⊑ y → concr x e → concr y e.
Variable concr_top: ∀ e, concr top e.
Variable concr_bottom: ∀ e, ¬ concr bottom e.
(* The join is an over-approximation (through [concr]) of the union of
sets of environments: conséquence of the lattice structure and the monotony
of the concretization. *)
Lemma join_correct: ∀ val e,
(∃ l, val l ∧ concr l e) → concr (join val) e.
Proof.
intros val e [l [Hval Hconcr]]. apply concr_monotone with l.
apply join_bigger. assumption. assumption.
Qed.
(* The narrow is an over-approximation of the intersection of sets of
environments. *)
Variable narrow_correct: ∀ (val: L → Prop) (e: Env),
(∀ l, val l → concr l e) → concr (narrow val) e.
Transfer Functions
Variable assign: Var → Exp → L → L.
Variable assume: Exp → L → L.
(* If the environment [env] is a concretization of [l] and if in [env],
the expression [exp] evaluates to [val], then [update env var val]
must be a concretization of [assign var exp l] *)
Variable assign_correct: ∀ (var:Var) (exp:Exp) (val:Value) (l:L) (env:Env),
concr l env →
val = eval_expr env exp →
concr (assign var exp l) (update env var val).
Variable assign_monotone: ∀ exp var (l l':L),
l ⊑ l' → assign var exp l ⊑ assign var exp l'.
(* If the environment [env] is a concretization of [l] and if in [env],
the expression [exp] evaluates to a positive value, then [env] must be
a concretization of [assum exp l]. *)
Variable assume_correct: ∀ (exp:Exp) (l:L) (env:Env),
concr l env →
eval_value (eval_expr env exp) →
concr (assume exp l) env.
Variable assume_monotone: ∀ exp (l l':L),
l ⊑ l' → assume exp l ⊑ assume exp l'.
Variable assign_bottom: ∀ var exp, assign var exp bottom = bottom.
Variable assume_bottom: ∀ exp, assume exp bottom = bottom.
(* --------------------------------------------------------------------------
Intermediate lemmas about join and narrow
-------------------------------------------------------------------------- *)
(* Definition of a join and narrow of arity 2. *)
Definition join2 l1 l2 := ⊔ (fun l ⇒ l = l1 ∨ l = l2).
Definition narrow2 l1 l2 := ⊓ (fun l ⇒ l = l1 ∨ l = l2).
Notation "x ⊔² y" := (join2 x y) (at level 21, left associativity) : type_scope.
Notation "x ⊓² y" := (narrow2 x y) (at level 21, left associativity) : type_scope.
Hint Unfold join2 narrow2.
Lemma join2_bigger_left: ∀ l1 l2, l1 ⊑ l1 ⊔² l2.
eauto. Qed.
Lemma join2_bigger_right: ∀ l1 l2, l2 ⊑ l1 ⊔² l2.
eauto. Qed.
Lemma narrow2_smaller_left: ∀ l1 l2, l1 ⊓² l2 ⊑ l1.
eauto. Qed.
Lemma narrow2_smaller_right: ∀ l1 l2, l1 ⊓² l2 ⊑ l2.
eauto. Qed.
Hint Resolve join2_bigger_left join2_bigger_right
narrow2_smaller_left narrow2_smaller_right.
Lemma join2_idempotent: ∀ l, l ⊔² l = l.
Proof.
intro l. apply incl_asym. apply join_smallest.
intros l' [H' | H']; rewrite H'; reflexivity.
apply join2_bigger_left.
Qed.
Add Parametric Morphism : join2
with signature incl ==> incl ==> incl
as join2_morphism_incl.
Proof.
intros.
apply join_smallest; intros.
destruct H1; subst; eapply incl_trans; eauto.
Qed.
Add Parametric Morphism : narrow2
with signature incl ==> incl ==> incl
as narrow2_morphism_incl.
Proof.
intros.
apply narrow_biggest; intros.
destruct H1; subst; eapply incl_trans; eauto.
Qed.
Lemma join2_sym: ∀ l1 l2, l1 ⊔² l2 = l2 ⊔² l1.
Proof.
intros; apply incl_asym; unfold join2;
apply join_smallest; intros; apply join_bigger; tauto.
Qed.
Lemma narrow2_sym: ∀ l1 l2, l1 ⊓² l2 = l2 ⊓² l1.
Proof.
intros; apply incl_asym; unfold narrow2;
apply narrow_biggest; intros; apply narrow_smaller; tauto.
Qed.
Lemma incl_narrow_weaken: ∀ (val1 val2: L → Prop),
(∀ l, val2 l → val1 l) →
⊓ val1 ⊑ ⊓ val2.
Proof.
intros.
apply narrow_biggest; intros.
apply narrow_smaller; auto.
Qed.
Lemma incl_narrow_weaken': ∀ (val1 val2: L → Prop),
(∀ l, val2 l → ∃ l', l' ⊑ l ∧ val1 l') →
⊓ val1 ⊑ ⊓ val2.
Proof.
intros.
apply narrow_biggest; intros.
destruct (H _ H0). apply incl_trans with x; intuition.
Qed.
Lemma narrow_exists_narrow: ∀ A (P1 : A → Prop) (P2 : A → L → Prop),
⊓(fun l ⇒ ∃ p, P1 p ∧ l = ⊓P2 p) =
⊓(fun l ⇒ ∃ p, P1 p ∧ P2 p l).
Proof.
intros; apply incl_asym.
- apply incl_narrow_weaken'; intros l [p [Hp1 Hp2]].
∃ (narrow (P2 p)); eauto.
- apply narrow_biggest; intros l [p [Hp1 Hp2]]; subst.
apply incl_narrow_weaken; eauto.
Qed.
Lemma narrow_exists_equiv: ∀ A (P1 P2: L → A → Prop),
(∀ l p, P1 l p ↔ P2 l p) →
⊓(fun l ⇒ ∃ p, P1 l p) = ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros; apply incl_asym; apply incl_narrow_weaken; intros l [p Hp]; ∃ p.
- rewrite H; auto.
- rewrite <- H; auto.
Qed.
Lemma narrow_exists_implies: ∀ A (P1 P2: L → A → Prop),
(∀ l p, P2 l p → P1 l p) →
⊓(fun l ⇒ ∃ p, P1 l p) ⊑ ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros; apply incl_narrow_weaken; intros l [p Hp]; ∃ p; auto.
Qed.
Lemma narrow_exists_or: ∀ A (P1 P2 : L → A → Prop),
⊓ (fun l ⇒ ∃ p, P1 l p ∨ P2 l p) =
⊓ (fun l ⇒ ∃ p, P1 l p) ⊓² ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros.
intros; apply incl_asym.
- apply narrow_biggest; intros.
destruct H; subst; apply incl_narrow_weaken; intros l [p Hp]; eauto.
- unfold narrow2.
apply incl_narrow_weaken'; intros l [p [Hp | Hp]].
+ ∃ (⊓(fun l0 ⇒ ∃ p0, P1 l0 p0)); split; eauto.
+ ∃ (⊓(fun l0 ⇒ ∃ p0, P2 l0 p0)); split; eauto.
Qed.
Lemma narrow_of_bottom: ∀ (val: L → Prop),
val bottom → narrow val = bottom.
Proof. eauto. Qed.
Lemma smaller_than_bottom_is_bottom: ∀ l, l ⊑ bottom ↔ l = bottom.
Proof. split. auto. intro H. rewrite H. reflexivity. Qed.
Lemma join_only_bottom: ∀ (val: L → Prop),
(∀ l, val l → l = bottom) →
join val = bottom.
Proof.
intros.
apply incl_asym; auto.
apply join_smallest; intros.
case (H _ H0); auto.
Qed.
(* --------------------------------------------------------------------------
Predicates
-------------------------------------------------------------------------- *)
Inductive pred :=
| PTrue
| PFalse
| PExpr: ∀ (e:Exp), pred
| PNot: ∀ (p:pred), pred
| PAnd: ∀ (p1 p2: pred), pred
| POr: ∀ (p1 p2: pred), pred
.
(* Evaluation of predicates.
Note that this function takes as argument any valuation from expressions
to Propositions, unrelated to an environment. *)
Fixpoint eval_pred (val: Exp → Value) p := match p with
| PTrue ⇒ True
| PFalse ⇒ False
| PExpr e ⇒ eval_value (val e)
| PNot p ⇒ not (eval_pred val p)
| PAnd p1 p2 ⇒ (eval_pred val p1) ∧ (eval_pred val p2)
| POr p1 p2 ⇒ (eval_pred val p1) ∨ (eval_pred val p2)
end.
(* Entailment of predicates. *)
Definition pred_implies p1 p2 :=
∀ val, (eval_pred val p1) → (eval_pred val p2).
Notation "p1 ⊢ p2" := (pred_implies p1 p2) (at level 20, no associativity) : type_scope.
Variable pred_implies_dec: ∀ p1 p2, { p1 ⊢ p2 } + { ¬ (p1 ⊢ p2) }.
(* Equivalence of predicates. *)
Definition pred_equiv p1 p2 :=
∀ val, (eval_pred val p1) ↔ (eval_pred val p2).
Notation "p1 ⊣⊢ p2" := (pred_equiv p1 p2) (at level 20, no associativity) : type_scope.
Hint Unfold pred_implies pred_equiv.
Ltac implies := unfold pred_implies; simpl; intuition.
Ltac equiv := unfold pred_equiv; simpl; intuition.
(* ⊢ is an order *)
Instance pred_implies_refl: Reflexive pred_implies. intuition. Qed.
Instance pred_implies_trans: Transitive pred_implies. intuition. Qed.
(* ⊣⊢ is an equivalence relation *)
Instance pred_equiv_refl: Reflexive pred_equiv. intuition. Qed.
Instance pred_equiv_trans: Transitive pred_equiv.
Proof.
red; unfold pred_equiv; intuition.
rewrite <- H0; rewrite <- H; auto.
rewrite H; rewrite H0; auto.
Qed.
Instance pred_equiv_symmetric: Symmetric pred_equiv.
Proof.
unfold pred_equiv, Symmetric; intuition.
- rewrite H; auto.
- rewrite <- H; auto.
Qed.
Variable assume: Exp → L → L.
(* If the environment [env] is a concretization of [l] and if in [env],
the expression [exp] evaluates to [val], then [update env var val]
must be a concretization of [assign var exp l] *)
Variable assign_correct: ∀ (var:Var) (exp:Exp) (val:Value) (l:L) (env:Env),
concr l env →
val = eval_expr env exp →
concr (assign var exp l) (update env var val).
Variable assign_monotone: ∀ exp var (l l':L),
l ⊑ l' → assign var exp l ⊑ assign var exp l'.
(* If the environment [env] is a concretization of [l] and if in [env],
the expression [exp] evaluates to a positive value, then [env] must be
a concretization of [assum exp l]. *)
Variable assume_correct: ∀ (exp:Exp) (l:L) (env:Env),
concr l env →
eval_value (eval_expr env exp) →
concr (assume exp l) env.
Variable assume_monotone: ∀ exp (l l':L),
l ⊑ l' → assume exp l ⊑ assume exp l'.
Variable assign_bottom: ∀ var exp, assign var exp bottom = bottom.
Variable assume_bottom: ∀ exp, assume exp bottom = bottom.
(* --------------------------------------------------------------------------
Intermediate lemmas about join and narrow
-------------------------------------------------------------------------- *)
(* Definition of a join and narrow of arity 2. *)
Definition join2 l1 l2 := ⊔ (fun l ⇒ l = l1 ∨ l = l2).
Definition narrow2 l1 l2 := ⊓ (fun l ⇒ l = l1 ∨ l = l2).
Notation "x ⊔² y" := (join2 x y) (at level 21, left associativity) : type_scope.
Notation "x ⊓² y" := (narrow2 x y) (at level 21, left associativity) : type_scope.
Hint Unfold join2 narrow2.
Lemma join2_bigger_left: ∀ l1 l2, l1 ⊑ l1 ⊔² l2.
eauto. Qed.
Lemma join2_bigger_right: ∀ l1 l2, l2 ⊑ l1 ⊔² l2.
eauto. Qed.
Lemma narrow2_smaller_left: ∀ l1 l2, l1 ⊓² l2 ⊑ l1.
eauto. Qed.
Lemma narrow2_smaller_right: ∀ l1 l2, l1 ⊓² l2 ⊑ l2.
eauto. Qed.
Hint Resolve join2_bigger_left join2_bigger_right
narrow2_smaller_left narrow2_smaller_right.
Lemma join2_idempotent: ∀ l, l ⊔² l = l.
Proof.
intro l. apply incl_asym. apply join_smallest.
intros l' [H' | H']; rewrite H'; reflexivity.
apply join2_bigger_left.
Qed.
Add Parametric Morphism : join2
with signature incl ==> incl ==> incl
as join2_morphism_incl.
Proof.
intros.
apply join_smallest; intros.
destruct H1; subst; eapply incl_trans; eauto.
Qed.
Add Parametric Morphism : narrow2
with signature incl ==> incl ==> incl
as narrow2_morphism_incl.
Proof.
intros.
apply narrow_biggest; intros.
destruct H1; subst; eapply incl_trans; eauto.
Qed.
Lemma join2_sym: ∀ l1 l2, l1 ⊔² l2 = l2 ⊔² l1.
Proof.
intros; apply incl_asym; unfold join2;
apply join_smallest; intros; apply join_bigger; tauto.
Qed.
Lemma narrow2_sym: ∀ l1 l2, l1 ⊓² l2 = l2 ⊓² l1.
Proof.
intros; apply incl_asym; unfold narrow2;
apply narrow_biggest; intros; apply narrow_smaller; tauto.
Qed.
Lemma incl_narrow_weaken: ∀ (val1 val2: L → Prop),
(∀ l, val2 l → val1 l) →
⊓ val1 ⊑ ⊓ val2.
Proof.
intros.
apply narrow_biggest; intros.
apply narrow_smaller; auto.
Qed.
Lemma incl_narrow_weaken': ∀ (val1 val2: L → Prop),
(∀ l, val2 l → ∃ l', l' ⊑ l ∧ val1 l') →
⊓ val1 ⊑ ⊓ val2.
Proof.
intros.
apply narrow_biggest; intros.
destruct (H _ H0). apply incl_trans with x; intuition.
Qed.
Lemma narrow_exists_narrow: ∀ A (P1 : A → Prop) (P2 : A → L → Prop),
⊓(fun l ⇒ ∃ p, P1 p ∧ l = ⊓P2 p) =
⊓(fun l ⇒ ∃ p, P1 p ∧ P2 p l).
Proof.
intros; apply incl_asym.
- apply incl_narrow_weaken'; intros l [p [Hp1 Hp2]].
∃ (narrow (P2 p)); eauto.
- apply narrow_biggest; intros l [p [Hp1 Hp2]]; subst.
apply incl_narrow_weaken; eauto.
Qed.
Lemma narrow_exists_equiv: ∀ A (P1 P2: L → A → Prop),
(∀ l p, P1 l p ↔ P2 l p) →
⊓(fun l ⇒ ∃ p, P1 l p) = ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros; apply incl_asym; apply incl_narrow_weaken; intros l [p Hp]; ∃ p.
- rewrite H; auto.
- rewrite <- H; auto.
Qed.
Lemma narrow_exists_implies: ∀ A (P1 P2: L → A → Prop),
(∀ l p, P2 l p → P1 l p) →
⊓(fun l ⇒ ∃ p, P1 l p) ⊑ ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros; apply incl_narrow_weaken; intros l [p Hp]; ∃ p; auto.
Qed.
Lemma narrow_exists_or: ∀ A (P1 P2 : L → A → Prop),
⊓ (fun l ⇒ ∃ p, P1 l p ∨ P2 l p) =
⊓ (fun l ⇒ ∃ p, P1 l p) ⊓² ⊓(fun l ⇒ ∃ p, P2 l p).
Proof.
intros.
intros; apply incl_asym.
- apply narrow_biggest; intros.
destruct H; subst; apply incl_narrow_weaken; intros l [p Hp]; eauto.
- unfold narrow2.
apply incl_narrow_weaken'; intros l [p [Hp | Hp]].
+ ∃ (⊓(fun l0 ⇒ ∃ p0, P1 l0 p0)); split; eauto.
+ ∃ (⊓(fun l0 ⇒ ∃ p0, P2 l0 p0)); split; eauto.
Qed.
Lemma narrow_of_bottom: ∀ (val: L → Prop),
val bottom → narrow val = bottom.
Proof. eauto. Qed.
Lemma smaller_than_bottom_is_bottom: ∀ l, l ⊑ bottom ↔ l = bottom.
Proof. split. auto. intro H. rewrite H. reflexivity. Qed.
Lemma join_only_bottom: ∀ (val: L → Prop),
(∀ l, val l → l = bottom) →
join val = bottom.
Proof.
intros.
apply incl_asym; auto.
apply join_smallest; intros.
case (H _ H0); auto.
Qed.
(* --------------------------------------------------------------------------
Predicates
-------------------------------------------------------------------------- *)
Inductive pred :=
| PTrue
| PFalse
| PExpr: ∀ (e:Exp), pred
| PNot: ∀ (p:pred), pred
| PAnd: ∀ (p1 p2: pred), pred
| POr: ∀ (p1 p2: pred), pred
.
(* Evaluation of predicates.
Note that this function takes as argument any valuation from expressions
to Propositions, unrelated to an environment. *)
Fixpoint eval_pred (val: Exp → Value) p := match p with
| PTrue ⇒ True
| PFalse ⇒ False
| PExpr e ⇒ eval_value (val e)
| PNot p ⇒ not (eval_pred val p)
| PAnd p1 p2 ⇒ (eval_pred val p1) ∧ (eval_pred val p2)
| POr p1 p2 ⇒ (eval_pred val p1) ∨ (eval_pred val p2)
end.
(* Entailment of predicates. *)
Definition pred_implies p1 p2 :=
∀ val, (eval_pred val p1) → (eval_pred val p2).
Notation "p1 ⊢ p2" := (pred_implies p1 p2) (at level 20, no associativity) : type_scope.
Variable pred_implies_dec: ∀ p1 p2, { p1 ⊢ p2 } + { ¬ (p1 ⊢ p2) }.
(* Equivalence of predicates. *)
Definition pred_equiv p1 p2 :=
∀ val, (eval_pred val p1) ↔ (eval_pred val p2).
Notation "p1 ⊣⊢ p2" := (pred_equiv p1 p2) (at level 20, no associativity) : type_scope.
Hint Unfold pred_implies pred_equiv.
Ltac implies := unfold pred_implies; simpl; intuition.
Ltac equiv := unfold pred_equiv; simpl; intuition.
(* ⊢ is an order *)
Instance pred_implies_refl: Reflexive pred_implies. intuition. Qed.
Instance pred_implies_trans: Transitive pred_implies. intuition. Qed.
(* ⊣⊢ is an equivalence relation *)
Instance pred_equiv_refl: Reflexive pred_equiv. intuition. Qed.
Instance pred_equiv_trans: Transitive pred_equiv.
Proof.
red; unfold pred_equiv; intuition.
rewrite <- H0; rewrite <- H; auto.
rewrite H; rewrite H0; auto.
Qed.
Instance pred_equiv_symmetric: Symmetric pred_equiv.
Proof.
unfold pred_equiv, Symmetric; intuition.
- rewrite H; auto.
- rewrite <- H; auto.
Qed.
eval is compatible with ⊣⊢ (for its second argument)
Add Parametric Morphism : eval_pred
with signature eq ==> pred_equiv ==> iff
as eval_morphism_pred_equiv.
Proof.
intros. unfold pred_equiv in H. rewrite H. intuition.
Qed.
with signature eq ==> pred_equiv ==> iff
as eval_morphism_pred_equiv.
Proof.
intros. unfold pred_equiv in H. rewrite H. intuition.
Qed.
⊢ is compatible with itself on the right, and its inverse on the left.
Add Parametric Morphism : pred_implies
with signature pred_implies --> pred_implies ==> impl
as pred_implies_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; auto.
Qed.
with signature pred_implies --> pred_implies ==> impl
as pred_implies_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; auto.
Qed.
PAnd is compatible with ⊢
Add Parametric Morphism : PAnd
with signature pred_implies ==> pred_implies ==> pred_implies
as PAnd_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; simpl in *; intuition.
Qed.
with signature pred_implies ==> pred_implies ==> pred_implies
as PAnd_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; simpl in *; intuition.
Qed.
POr is compatible with ⊢
Add Parametric Morphism : POr
with signature pred_implies ==> pred_implies ==> pred_implies
as POr_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; simpl in *; intuition.
Qed.
with signature pred_implies ==> pred_implies ==> pred_implies
as POr_morphism_pred_implies.
Proof.
intros x1 y1 H1 x2 y2 H2. unfold pred_implies in *; repeat intro; simpl in *; intuition.
Qed.
PAnd is compatible with ⊢
Add Parametric Morphism : PAnd
with signature pred_equiv ==> pred_equiv ==> pred_equiv
as PAnd_morphism_pred_equiv.
Proof.
unfold pred_equiv; intros x1 y1 H1 x2 y2 H2; split; simpl; intros.
- rewrite <- H1; rewrite <- H2; auto.
- rewrite H1; rewrite H2; auto.
Qed.
with signature pred_equiv ==> pred_equiv ==> pred_equiv
as PAnd_morphism_pred_equiv.
Proof.
unfold pred_equiv; intros x1 y1 H1 x2 y2 H2; split; simpl; intros.
- rewrite <- H1; rewrite <- H2; auto.
- rewrite H1; rewrite H2; auto.
Qed.
POr is compatible with ⊢
Add Parametric Morphism : POr
with signature pred_equiv ==> pred_equiv ==> pred_equiv
as POr_morphism_pred_equiv.
Proof.
unfold pred_equiv; intros x1 y1 H1 x2 y2 H2; split; simpl; intros.
- rewrite <- H1; rewrite <- H2; auto.
- rewrite H1; rewrite H2; auto.
Qed.
with signature pred_equiv ==> pred_equiv ==> pred_equiv
as POr_morphism_pred_equiv.
Proof.
unfold pred_equiv; intros x1 y1 H1 x2 y2 H2; split; simpl; intros.
- rewrite <- H1; rewrite <- H2; auto.
- rewrite H1; rewrite H2; auto.
Qed.
⊢ is compatible with ⊣⊢
Add Parametric Morphism : pred_implies
with signature pred_equiv ==> pred_equiv ==> iff
as pred_implies_morphism.
Proof.
unfold pred_equiv, pred_implies; intros; split; intros.
- rewrite <- H0. apply H1. rewrite H. auto.
- rewrite → H0. apply H1. rewrite <- H. auto.
Qed.
Lemma PAnd_idempotent: ∀ p, PAnd p p ⊣⊢ p.
Proof. intros p. equiv. Qed.
Lemma pred_equiv_dec: ∀ p1 p2, { p1 ⊣⊢ p2 } + { ¬ (p1 ⊣⊢ p2) }.
Proof.
intros; destruct (pred_implies_dec p1 p2).
- destruct (pred_implies_dec p2 p1).
+ left. unfold pred_implies, pred_equiv in *; intuition.
+ right. intro; apply n. rewrite H; auto.
- right. intro; apply n. rewrite H; auto.
Qed.
(* --------------------------------------------------------------------------
CI-pairs
--------------------------------------------------------------------------- *)
(* Notations for CI operations: ≣ ⋐ ⋑ ⋒ ⋓ *)
Record CI := {
context: pred;
map: pred → L
}.
(* Consequence. *)
(* [in_map ci P] is the set of elements of L linked to a predicates
that verifies P. *)
Definition in_map (ci: CI) (P: pred → Prop) : L → Prop :=
(fun l ⇒ ∃ p, P p ∧ l = map ci p).
Hint Unfold in_map.
Ltac simpl_in_map :=
let l := fresh "l" in
let p := fresh "p'" in
let H1 := fresh "H" p in
let H2 := fresh in
intros l [p [H1 H2]]; subst l;
unfold in_map; simpl map.
(* In a Ci-pair [ci], the consequence of a predicate [p] is the narrowing of
all elements of L linked to predicates [p'] such that p ∧ c ⊢ p',
with [c] context of [ci]. *)
Definition consequence (ci: CI) (p : pred) :=
narrow (in_map ci (fun p' ⇒ PAnd p (context ci) ⊢ p')).
Notation "ci ∎ p" := (consequence ci p) (at level 10, no associativity): type_scope.
(* [ci ∎ p] is more precise than the content of [ci] at [p]. *)
Lemma consequence_p_incl: ∀ ci p, ci ∎ p ⊑ map ci p.
Proof.
intros. apply narrow_smaller. ∃ p. implies.
Qed.
Definition false_bottom ci := map ci PFalse = bottom.
(* Guards that contradict the context imply bottom *)
Lemma consequence_contradiction_context: ∀ ci p,
false_bottom ci →
PAnd p (context ci) ⊢ PFalse →
ci ∎ p = bottom.
Proof.
intros [c I] p h_bot H; simpl in *; apply incl_asym; auto.
apply narrow_smaller; simpl.
∃ PFalse; auto.
Qed.
(* Compatibility of ∎ with ⊢ for context *)
Lemma CI_consequence_weaken_context: ∀ c1 c2 I p,
c1 ⊢ c2 → {| context := c1; map := I |} ∎ p ⊑ {| context := c2; map := I |} ∎ p.
Proof.
intros; unfold consequence; simpl.
apply narrow_biggest.
simpl_in_map.
apply narrow_smaller; ∃ p'; split; auto.
rewrite H; auto.
Qed.
(* Compatibility of ∎ with ⊑ for the elements of I *)
Lemma CI_consequence_weaken_map: ∀ c I1 I2 p,
(∀ q : pred, I1 q ⊑ I2 q) →
{| context := c; map := I1 |} ∎ p ⊑ {| context := c; map := I2 |} ∎ p.
Proof.
intros; unfold consequence; simpl.
apply incl_narrow_weaken'.
simpl_in_map.
∃ (I1 p'); split; eauto.
Qed.
(* Compatibility of ∎ with ⊢ for context and ⊑ for the elements of I *)
Lemma CI_consequence_weaken : ∀ ci1 ci2 p,
context ci1 ⊢ context ci2 → (∀ q : pred, map ci1 q ⊑ map ci2 q)
→ ci1 ∎ p ⊑ ci2 ∎ p.
Proof.
intros.
transitivity ({| context := context ci1; map := map ci2 |} ∎ p).
- apply CI_consequence_weaken_map; intuition.
- apply CI_consequence_weaken_context; intuition.
Qed.
(* Auxiliary lemma for proving that ⋓ computes upper bounds *)
Lemma CI_consequence_weaken_pred : ∀ ci p1 p2,
PAnd p1 (context ci) ⊢ p2 → ci ∎ p1 ⊑ ci ∎ p2.
Proof.
intros.
unfold consequence; simpl.
apply incl_narrow_weaken'. simpl_in_map.
∃ (map ci p'); intuition.
∃ p'; intuition. implies.
apply Hp'. simpl. intuition. apply H. simpl. intuition.
Qed.
(* --------------------------------------------------------------------------
Order and equivalence of CI-pairs
-------------------------------------------------------------------------- *)
(* Inclusion of CI-pairs. *)
Definition CI_incl (ci1 ci2: CI) :=
context ci1 ⊢ context ci2 ∧ ∀ p, ci1 ∎ p ⊑ ci2 ∎ p.
Notation "ci1 ⋐ ci2" := (CI_incl ci1 ci2) (at level 40, no associativity): type_scope.
Lemma CI_incl_weaken : ∀ ci1 ci2,
context ci1 ⊢ context ci2 → (∀ q : pred, map ci1 q ⊑ map ci2 q) → ci1 ⋐ ci2.
Proof.
intros ci1 ci2 Hc Hm.
unfold CI_incl. intuition. apply CI_consequence_weaken; assumption.
Qed.
(* Equivalence relation of CI-pairs. *)
Definition CI_equiv (ci1 ci2: CI) :=
context ci1 ⊣⊢ context ci2 ∧ ∀ p, ci1 ∎ p = ci2 ∎ p.
Notation "c1 ≣ c2" := (CI_equiv c1 c2) (at level 40, no associativity): type_scope.
(* ⋐ is an order *)
Instance CI_incl_refl: Reflexive CI_incl. unfold CI_incl; intuition. Qed.
Instance CI_incl_trans: Transitive CI_incl.
Proof. unfold Transitive, CI_incl; intuition; eauto. Qed.
(* ≣ is an equivalence relation *)
Instance CI_equiv_refl: Reflexive CI_equiv. unfold CI_equiv; intuition. Qed.
Instance CI_equiv_trans: Transitive CI_equiv.
Proof.
unfold Transitive, CI_equiv; intuition.
transitivity (context y); auto.
transitivity (y ∎ p); auto.
Qed.
Instance CI_equiv_symmetric: Symmetric CI_equiv.
Proof. unfold Symmetric, CI_equiv; intuition. Qed.
(* ⋐ is compatible with ≣ *)
Add Parametric Morphism : CI_incl
with signature CI_equiv ==> CI_equiv ==> iff
as CI_incl_morphism.
Proof.
unfold CI_equiv, CI_incl; split; intuition.
- rewrite <- H2; rewrite <- H; auto.
- rewrite <- H4; rewrite <- H3; auto.
- rewrite H2; rewrite H; auto.
- rewrite H4; rewrite H3; auto.
Qed.
(* ≣ is the kernel of ⋐ *)
Lemma CI_equiv_incl: ∀ ci1 ci2,
ci1 ≣ ci2 ↔ ci1 ⋐ ci2 ∧ ci2 ⋐ ci1.
Proof.
split.
- intro H; rewrite H; split; reflexivity.
- intros [[H1 H2] [H3 H4]]; split; auto.
split; auto.
Qed.
(* Bottom. *)
Definition CI_bottom := {|
context := PFalse;
map := fun p ⇒ match p with PFalse ⇒ bottom | _ ⇒ top end
|}.
(* Top. *)
Definition CI_top := {|
context := PTrue;
map := fun p ⇒ match p with PFalse ⇒ bottom | _ ⇒ top end
|}.
(* Bottom is the smallest CI-pairs. *)
Lemma CI_bottom_smallest: ∀ ci, CI_bottom ⋐ ci.
Proof.
intros; unfold CI_incl; split; simpl.
- implies.
- intros; transitivity bottom; auto.
unfold consequence, in_map; simpl.
apply narrow_smaller.
∃ PFalse; intuition.
implies.
Qed.
(* Top is the biggest CI-pairs. *)
Lemma CI_top_biggest: ∀ ci, false_bottom ci → ci ⋐ CI_top.
Proof.
intros ci Hbot; unfold CI_incl; split; simpl.
- implies.
- intros.
apply narrow_biggest; intros.
unfold in_map in H.
do 2 destruct H; subst; simpl in H.
unfold CI_top; simpl; destruct x; auto.
(* Only the cases where x = PFalse/p ⊢ PFalse remain *)
apply narrow_smaller.
unfold consequence, in_map; simpl.
∃ PFalse; split; auto.
generalize H; implies.
eapply H0; intuition eauto.
Qed.
Definition CI_subset (ci1 ci2: CI) :=
context ci1 ⊢ context ci2 ∧ ∀ p, map ci1 p ⊑ map ci2 p.
Lemma CI_incl_subset: ∀ ci1 ci2, CI_subset ci1 ci2 → ci1 ⋐ ci2.
Proof.
intros ci1 ci2 [Hc Hmap]. split. apply Hc.
intro p. apply incl_narrow_weaken'. intros l [x [Hx Hl]]; subst l.
∃ (map ci1 x). split. apply Hmap.
∃ x. split. rewrite Hc. implies. reflexivity.
Qed.
(* Equal CI-pairs are equivalent. *)
Lemma CI_equiv_equal: ∀ ci1 ci2,
context ci1 ⊣⊢ context ci2 →
(∀ p, map ci1 p = map ci2 p) →
ci1 ≣ ci2.
Proof.
intros ci1 ci2 Hc Hmap. rewrite CI_equiv_incl. split.
- apply CI_incl_subset. unfold CI_subset. split.
rewrite Hc. reflexivity. intro p. rewrite Hmap. reflexivity.
- apply CI_incl_subset. unfold CI_subset. split.
rewrite Hc. reflexivity. intro p. rewrite Hmap. reflexivity.
Qed.
(* --------------------------------------------------------------------------
Join of CI-pairs
-------------------------------------------------------------------------- *)
Definition CI_join (ci1 ci2: CI) := {|
context := (POr (context ci1) (context ci2));
map := fun p ⇒ ci1 ∎ p ⊔² ci2 ∎ p
|}.
Notation "c1 ⋓ c2" := (CI_join c1 c2) (at level 55, no associativity): type_scope.
(* In a join, PFalse is mapped to bottom. *)
Lemma CI_join_bottom: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (ci1 ⋓ ci2).
Proof.
intros [c1 I1] [c2 I2] H1 H2.
unfold consequence, in_map, join2; simpl.
apply join_only_bottom; intros.
destruct H; subst l; rewrite <- smaller_than_bottom_is_bottom.
- apply narrow_smaller; ∃ PFalse; implies.
- apply narrow_smaller; ∃ PFalse; implies.
Qed.
(* Symmetry of the join. *)
Lemma CI_join_sym_incl: ∀ ci1 ci2, (ci1 ⋓ ci2) ⋐ (ci2 ⋓ ci1).
Proof.
intros; destruct ci1 as [c1 I1 b1]; destruct ci2 as [c2 I2 b2].
unfold CI_join, CI_incl; simpl; split.
- red; simpl; tauto.
- intros; unfold consequence; simpl.
apply narrow_biggest; simpl_in_map.
apply narrow_smaller; ∃ p'; split.
+ unfold pred_implies in *; simpl in *; intuition.
+ rewrite join2_sym; auto.
Qed.
Lemma CI_join_sym: ∀ ci1 ci2, (ci1 ⋓ ci2) ≣ (ci2 ⋓ ci1).
Proof.
intros. rewrite CI_equiv_incl; auto using CI_join_sym_incl.
Qed.
(* The join of CI-pairs is an upper bound. *)
Lemma CI_join_bigger_left: ∀ ci1 ci2,
ci1 ⋐ (ci1 ⋓ ci2).
Proof.
split.
- unfold pred_implies; simpl; auto.
- intros.
transitivity (ci1 ∎ p ⊔² ci2 ∎ p); auto.
apply narrow_biggest; simpl_in_map.
apply join2_morphism_incl;
apply CI_consequence_weaken_pred; unfold pred_implies; intros; simpl in ×.
+ apply Hp'; simpl; intuition.
+ apply Hp'; simpl; intuition.
Qed.
Lemma CI_join_bigger_right: ∀ ci1 ci2,
ci2 ⋐ (ci1 ⋓ ci2).
Proof.
intros; rewrite (CI_join_sym); apply CI_join_bigger_left.
Qed.
(* The join of CI-pairs is *the least* upper bound. *)
Lemma CI_join_smallest:
∀ ci1 ci2 ci', ci1 ⋐ ci' → ci2 ⋐ ci' → (ci1 ⋓ ci2) ⋐ ci'.
Proof.
intros ci1 ci2 ci' [H11 H12] [H21 H22].
unfold CI_incl; simpl in *; split.
- rewrite H11; rewrite H21.
implies.
- intro p. apply incl_trans with (ci1 ∎ p ⊔² ci2 ∎ p).
+ apply consequence_p_incl.
+ apply join_smallest. intros l' [Hl' | Hl']; rewrite Hl'; intuition.
Qed.
(* ⋓ is compatible with ⋐ *)
Add Parametric Morphism : CI_join
with signature CI_incl ==> CI_incl ==> CI_incl
as CI_join_morphism_CI_incl.
Proof.
intros x1 y1 [Hxy11 Hxy12] x2 y2 [Hxy21 Hxy22].
unfold CI_join, CI_incl in *; simpl; split.
- rewrite Hxy11; rewrite Hxy21; auto.
- intros; apply incl_narrow_weaken'; simpl_in_map; simpl in ×.
∃ (x1 ∎ p' ⊔² x2 ∎ p'); split.
+ rewrite Hxy12; rewrite Hxy22; reflexivity.
+ ∃ p'; split; auto.
rewrite Hxy11; rewrite Hxy21; auto.
Qed.
(* ⋓ is compatible with ≣ *)
Add Parametric Morphism : CI_join
with signature CI_equiv ==> CI_equiv ==> CI_equiv
as CI_join_morphism.
Proof.
intros.
rewrite CI_equiv_incl; split.
- apply CI_join_morphism_CI_incl; auto. rewrite H; reflexivity. rewrite H0; reflexivity.
- apply CI_join_morphism_CI_incl; auto. rewrite H; reflexivity. rewrite H0; reflexivity.
Qed.
(* Alternative proof of symmetry *)
Lemma CI_join_sym': ∀ ci1 ci2, (ci1 ⋓ ci2) ≣ (ci2 ⋓ ci1).
Proof.
intros; rewrite CI_equiv_incl.
split;
(apply CI_join_smallest; [apply CI_join_bigger_right | apply CI_join_bigger_left]).
Qed.
(* Transitivity of the join. *)
Lemma CI_join_trans_incl: ∀ ci1 ci2 ci3, (ci1 ⋓ (ci2 ⋓ ci3)) ⋐ ((ci1 ⋓ ci2) ⋓ ci3).
Proof with auto using CI_join_bigger_left, CI_join_bigger_right.
intros; repeat apply CI_join_smallest.
- rewrite CI_join_bigger_left at 1...
- rewrite CI_join_bigger_right at 1...
- idtac...
Qed.
Lemma CI_join_trans: ∀ ci1 ci2 ci3, (ci1 ⋓ (ci2 ⋓ ci3)) ≣ ((ci1 ⋓ ci2) ⋓ ci3).
Proof.
intros; rewrite CI_equiv_incl; split.
- apply CI_join_trans_incl.
- rewrite (CI_join_sym _ ci3).
do 2 rewrite (CI_join_sym ci1).
rewrite (CI_join_sym ci2 ci3).
apply CI_join_trans_incl.
Qed.
(* --------------------------------------------------------------------------
Narrow on CI-pairs
-------------------------------------------------------------------------- *)
Definition CI_narrow (ci1 ci2 : CI) :=
{| context := (PAnd (context ci1) (context ci2));
map := fun p ⇒ map ci1 p ⊓² map ci2 p
|}.
Notation "ci1 ⋒ ci2" := (CI_narrow ci1 ci2) (at level 50, no associativity): type_scope.
(* In a narrowing, PFalse is mapped to bottom. *)
Lemma narrow_pfalse: ∀ ci1 ci2,
false_bottom ci1 ∨ false_bottom ci2 →
false_bottom (ci1 ⋒ ci2).
Proof.
unfold false_bottom.
intros ci1 ci2 [H | H]; simpl; rewrite H; unfold narrow2; intuition.
Qed.
(* Symmetry of thee narrow. *)
Lemma CI_narrow_sym_incl: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ (ci2 ⋒ ci1).
Proof.
intros ci1 ci2. split. implies.
intro p. apply incl_narrow_weaken. intros l [x [Hx Hl]]; subst l.
unfold in_map. ∃ x. unfold CI_narrow; simpl. split.
rewrite <- Hx. implies. apply narrow2_sym.
Qed.
Lemma CI_narrow_sym: ∀ ci1 ci2, (ci1 ⋒ ci2) ≣ (ci2 ⋒ ci1).
Proof.
intros. rewrite CI_equiv_incl; auto using CI_narrow_sym_incl.
Qed.
(* The narrow is a lower bound. *)
Lemma CI_narrow_smaller_left: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ ci1.
Proof.
intros.
unfold CI_incl; simpl; split.
- implies.
- intro. apply CI_consequence_weaken; simpl.
+ implies.
+ intro. unfold CI_narrow; unfold narrow2; simpl. intuition.
Qed.
Lemma CI_narrow_smaller_right: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ ci2.
Proof.
intros; rewrite (CI_narrow_sym); apply CI_narrow_smaller_left.
Qed.
(* The narrow of CI-pairs is *the greatest* lower bound. *)
Lemma CI_narrow_biggest : ∀ ci1 ci2 ci',
ci' ⋐ ci1 → ci' ⋐ ci2 → ci' ⋐ (ci1 ⋒ ci2).
Proof.
intros ci1 ci2 ci' [H1c H1m] [H2c H2m].
unfold CI_incl; simpl; split.
- rewrite <- H1c. rewrite <- H2c. implies.
- intro. apply narrow_biggest; simpl_in_map.
apply narrow_biggest.
intros l [Hl | Hl]; subst l.
+ transitivity (ci' ∎ p').
× apply CI_consequence_weaken_pred.
rewrite <- Hp'. simpl. rewrite <- H1c; rewrite <- H2c. implies.
× transitivity (ci1 ∎ p'). intuition.
apply consequence_p_incl.
(* TODO : factoring *)
+ transitivity (ci' ∎ p').
× apply CI_consequence_weaken_pred.
rewrite <- Hp'. simpl. rewrite <- H1c; rewrite <- H2c. implies.
× transitivity (ci2 ∎ p'). intuition.
apply consequence_p_incl.
Qed.
(* Prove 'rel z t' assuming 'rel x y', by 'rel z x' and 'rel y t' *)
Ltac transitivity2 eq :=
match type of eq with
| ?rel ?x ?y ⇒
match goal with |- rel ?z ?t ⇒
let H := fresh in assert (rel z x) as H;
[ | let H' := fresh in assert (rel y t) as H';
[ | transitivity x;
[ exact H
| transitivity y ;
[ exact eq | exact H' ]]]]
end
end.
(* ⋒ is compatible with ⋐ *)
Add Parametric Morphism : CI_narrow
with signature CI_incl ==> CI_incl ==> CI_incl
as CI_narrow_morphism_CI_incl.
Proof.
intros x1 y1 [Hxy11 Hxy12] x2 y2 [Hxy21 Hxy22].
unfold CI_narrow, CI_incl in *; simpl.
split.
- rewrite Hxy11; rewrite Hxy21; implies.
- unfold narrow2, consequence, in_map in *; simpl in *; intros.
do 2 rewrite narrow_exists_narrow.
assert (∀ p1 p2 p3, p1 ∧ (p2 ∨ p3) ↔ (p1 ∧ p2) ∨ (p1 ∧ p3)); [tauto |].
do 2 rewrite (narrow_exists_equiv _ _ _ (fun l p ⇒ H _ _ _)); clear H.
do 2 rewrite narrow_exists_or.
apply narrow2_morphism_incl.
+ transitivity2 (Hxy12 (PAnd p (context x2))).
× apply narrow_exists_implies. implies.
× apply narrow_exists_implies; intros l p0. rewrite Hxy21; implies.
+ transitivity2 (Hxy22 (PAnd p (context x1))).
× apply narrow_exists_implies. implies.
× apply narrow_exists_implies; intros l p0. rewrite Hxy11; implies.
Qed.
(* ⋒ is compatible with ≣ *)
Add Parametric Morphism : CI_narrow
with signature CI_equiv ==> CI_equiv ==> CI_equiv
as CI_narrow_morphism_CI_equiv.
Proof.
intros x1 x2 Hx y1 y2 Hy.
destruct (CI_equiv_incl x1 x2); destruct (CI_equiv_incl y1 y2).
rewrite CI_equiv_incl; split;
apply CI_narrow_morphism_CI_incl; intuition.
Qed.
(* TODO: this proof is independant of the considered lattice. *)
Lemma CI_narrow_assoc: ∀ a b c,
((a ⋒ b) ⋒ c) ≣ (a ⋒ (b ⋒ c)).
Proof.
intros. rewrite CI_equiv_incl. split.
- apply CI_narrow_biggest.
+ transitivity (a ⋒ b); apply CI_narrow_smaller_left.
+ apply CI_narrow_biggest.
× transitivity (a ⋒ b). apply CI_narrow_smaller_left. apply CI_narrow_smaller_right.
× apply CI_narrow_smaller_right.
- apply CI_narrow_biggest.
+ apply CI_narrow_biggest.
× apply CI_narrow_smaller_left.
× transitivity (b ⋒ c). apply CI_narrow_smaller_right. apply CI_narrow_smaller_left.
+ transitivity (b ⋒ c); apply CI_narrow_smaller_right.
Qed.
(* --------------------------------------------------------------------------
Weak-join of CI-pairs
-------------------------------------------------------------------------- *)
(* The weak-join on CI-pairs is defined as the narrowing of three CI-pairs. *)
(* First auxiliary function for the weak join:
gather implications like (p1 ∧ p2 ⇒ (map ci1 p1) ⊔ (map ci2 p2)) *)
Definition CI_conj_join (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒
⊓ (fun l ⇒
∃ p1 p2, PAnd p1 p2 ⊣⊢ p ∧
l = map ci1 p1 ⊔² map ci2 p2)
|}.
Lemma pfalse_conj_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_conj_join ci1 ci2).
Proof.
intros ci1 ci2 H1 H2.
apply narrow_of_bottom. ∃ PFalse, PFalse; split.
- red; implies.
- rewrite H1; rewrite H2.
unfold join2. symmetry. apply join_only_bottom. intuition.
Qed.
Lemma CI_join_incl_conj_join : ∀ ci1 ci2, (ci1 ⋓ ci2) ⋐ (CI_conj_join ci1 ci2).
Proof.
intros.
apply CI_incl_weaken.
- unfold CI_incl; simpl; reflexivity.
- intro q; simpl.
apply join_smallest. intros l [H_l | H_l]; subst l.
Ltac aux ci p q :=
apply incl_narrow_weaken';
intros l [p1 [p2 [Hq Hl]]]; rewrite Hl;
∃ (map ci p); intuition;
∃ p; intuition; rewrite <- Hq; implies.
+ aux ci1 p1 q. + aux ci2 p2 q.
Qed.
(* Second auxiliary function for the weak join:
gather implications like (¬ (context ci2) ∧ p ⇒ map ci1 p) *)
Definition CI_neg_join (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒ ⊓ in_map ci1 (fun p1 ⇒ PAnd p1 (PNot (context ci2)) ⊣⊢ p)
|}.
Lemma pfalse_neg_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_neg_join ci1 ci2).
Proof.
intros ci1 ci2 H1 H2.
apply narrow_of_bottom. ∃ PFalse. split.
- unfold pred_equiv; simpl; intuition.
- rewrite H1. reflexivity.
Qed.
Lemma CI_join_incl_neg_join: ∀ ci1 ci2,
false_bottom ci2 →
(ci1 ⋓ ci2) ⋐ (CI_neg_join ci1 ci2).
Proof.
intros ci1 ci2 Hbot2.
apply CI_incl_weaken.
- unfold CI_incl; simpl; reflexivity.
- intro q; simpl.
apply join_smallest. intros l [H_l | H_l]; subst l.
+ apply incl_narrow_weaken'; simpl_in_map.
∃ (map ci1 p'); intuition.
∃ p'; intuition. rewrite <- Hp'. implies.
+ apply narrow_biggest; simpl_in_map.
transitivity bottom.
× rewrite smaller_than_bottom_is_bottom.
apply narrow_of_bottom. ∃ PFalse. rewrite Hbot2. intuition.
rewrite <- Hp'. implies.
× apply bottom_smallest.
Qed.
Lemma CI_neg_join_subset: ∀ ci1 ci2 ci1' ci2',
CI_subset ci1 ci1' → context ci2 ⊣⊢ context ci2' →
CI_neg_join ci1 ci2 ⋐ CI_neg_join ci1' ci2'.
Proof.
intros ci1 ci2 ci1' ci2' [Hc1 Hm1] Hc2.
apply CI_incl_subset. unfold CI_subset. split.
- simpl. rewrite Hc1, Hc2. implies.
- intro p. unfold CI_neg_join; simpl. apply incl_narrow_weaken'.
intros l [x [Hp Hl]]; subst l. ∃ (map ci1 x).
split. apply Hm1.
unfold in_map. ∃ x. split. rewrite <- Hp.
equiv. apply H1. rewrite Hc2. apply H. apply H1. rewrite <- Hc2. apply H.
reflexivity.
Qed.
(* The final weak-join. *)
Definition CI_weak_join (ci1 ci2 : CI) :=
(CI_conj_join ci1 ci2) ⋒ ((CI_neg_join ci1 ci2) ⋒ (CI_neg_join ci2 ci1)).
Lemma CI_weak_join_bottom: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_weak_join ci1 ci2).
Proof.
intros; unfold CI_weak_join, false_bottom, join2, in_map in *; simpl.
apply narrow_of_bottom; left.
symmetry; apply narrow_of_bottom; ∃ PFalse, PFalse; split.
- equiv.
- symmetry.
apply join_only_bottom.
intros l [Hb | Hb]; congruence.
Qed.
Lemma CI_join_incl_weak_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
(ci1 ⋓ ci2) ⋐ (CI_weak_join ci1 ci2).
Proof.
intros. unfold CI_weak_join.
repeat apply CI_narrow_biggest.
- apply CI_join_incl_conj_join.
- apply CI_join_incl_neg_join; assumption.
- rewrite CI_join_sym'.
apply CI_join_incl_neg_join; assumption.
Qed.
(* The weak-join is a weaker join. *)
Lemma CI_join_incl_weak_join' : ∀ ci1 ci2 ci1' ci2',
false_bottom ci1' →
false_bottom ci2' →
ci1 ≣ ci1' → ci2 ≣ ci2' → (ci1 ⋓ ci2) ⋐ (CI_weak_join ci1' ci2').
Proof.
intros ci1 ci2 ci1' ci2' Hbot1 Hbot2 H1 H2.
rewrite H1, H2. apply CI_join_incl_weak_join; auto.
Qed.
(* --------------------------------------------------------------------------
Optimization of the weak-join
-------------------------------------------------------------------------- *)
(* [ci_shared] contains only implications that belong to both [ci1] and [ci2] ;
other predicates are bound to [top]. *)
Definition CI_shared (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒ if L_dec (map ci1 p) (map ci2 p) then map ci1 p else top
|}.
(* [ci_diff] contains only the elements of [ci1] mapped to different values
in [ci2]. All other elements are mapped to top. *)
Definition CI_diff (ci1 ci2 : CI) :=
{| context := context ci1;
map := fun p ⇒ if L_dec (map ci1 p) (map ci2 p) then top else (map ci1 p)
|}.
(* The optimized weak-join between two CI-pairs [ci1] and [ci2] is the narrow
between:
- the shared CI-pair [ci_shared] ;
- and the weak-join between the rests [ci1_diff] and [ci2_diff]. *)
Definition CI_opt_conj_join ci1 ci2 :=
(CI_conj_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Definition CI_opt_neg_join ci1 ci2 :=
(CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Definition CI_opt_weak_join ci1 ci2 :=
(CI_weak_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Lemma CI_opt_weak_join_pfalse: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_opt_conj_join ci1 ci2).
Proof.
unfold CI_opt_conj_join, false_bottom; intros ci1 ci2 H1 H2.
apply narrow_of_bottom; right.
simpl.
rewrite H1; rewrite H2.
destruct (L_dec bottom bottom); intuition.
Qed.
Lemma CI_shared_sym: ∀ ci1 ci2, CI_shared ci1 ci2 ≣ CI_shared ci2 ci1.
Proof.
intros. apply CI_equiv_equal. equiv.
intro p. simpl.
case (L_dec (map ci1 p) (map ci2 p)); intros Hmap;
case (L_dec (map ci2 p) (map ci1 p)); intros Hmap';
congruence.
Qed.
Lemma CI_diff_subset: ∀ ci1 ci2, CI_subset ci1 (CI_diff ci1 ci2).
Proof.
intros ci1 ci2. unfold CI_subset. split.
- implies.
- intro p. simpl. destruct L_dec. apply top_biggest. reflexivity.
Qed.
Lemma CI_weak_join_incl_shared: ∀ ci1 ci2,
CI_weak_join ci1 ci2 ⋐ CI_shared ci1 ci2.
Proof.
intros ci1 ci2. apply CI_incl_subset. split. implies.
intro p. simpl.
case (L_dec (map ci1 p) (map ci2 p)); intros Hmap.
rewrite narrow2_smaller_left. apply narrow_smaller.
∃ p, p. split. equiv. rewrite Hmap. rewrite join2_idempotent. reflexivity.
apply top_biggest.
Qed.
Lemma CI_opt_conj_join_equiv: ∀ ci1 ci2,
(CI_conj_join ci1 ci2) ≣ (CI_opt_conj_join ci1 ci2).
Proof.
intros ci1 ci2; split.
- simpl. equiv.
- intro p. unfold consequence; simpl. apply incl_asym.
+ apply incl_narrow_weaken'. simpl_in_map.
∃ (map (CI_conj_join ci1 ci2) p'). split.
× apply narrow_biggest. intros l [Hl | Hl]; subst l.
{ apply incl_narrow_weaken'. intros l [p1 [p2 [Hp Hl]]]; subst l.
∃ (map ci1 p1 ⊔² map ci2 p2). split.
- unfold CI_diff; simpl. apply join2_morphism_incl.
+ destruct (L_dec (map ci1 p1) (map ci2 p1)); auto.
+ destruct (L_dec (map ci2 p2) (map ci1 p2)); auto.
- ∃ p1, p2. intuition.
}
{ unfold CI_shared; simpl.
destruct (L_dec (map ci1 p') (map ci2 p')); auto.
transitivity (map ci1 p' ⊔² map ci2 p').
- apply narrow_smaller. ∃ p', p'. intuition. equiv.
- rewrite <- e. apply join_smallest. intros l [Hl|Hl]; subst l; intuition.
}
× ∃ p'. intuition. generalize Hp'; implies.
+ apply narrow_biggest. intros l [p' [Hp' Hl]]. subst l.
apply narrow_biggest. intros l [p1 [p2 [Hp12 Hl]]]. subst l.
case_eq (L_dec (map ci1 p1) (map ci2 p1)); intros Hmap1 Hdec1.
2: case_eq (L_dec (map ci1 p2) (map ci2 p2)); intros Hmap2 Hdec2.
Local Ltac CI_conj_join_opt_equiv_solve :=
apply narrow_smaller; red;
match goal with Hp' : _ ⊢ ?p', Hp12: PAnd ?p1 ?p2 ⊣⊢ ?p' |- ∃ p0, _ ∧ ?F ?q = ?F p0 ⇒
∃ q ; split; [transitivity p'; [rewrite <- Hp' | rewrite <- Hp12]; implies | auto]
end.
× transitivity (map (CI_opt_conj_join ci1 ci2) p1).
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_shared ci1 ci2) p1). apply narrow_smaller. auto.
unfold CI_shared; simpl. rewrite Hdec1. auto.
× transitivity (map (CI_opt_conj_join ci1 ci2) p2).
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_shared ci1 ci2) p2). apply narrow_smaller. intuition.
unfold CI_shared; simpl. rewrite Hdec2. eauto.
× transitivity (map (CI_opt_conj_join ci1 ci2) p').
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_conj_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) p').
apply narrow_smaller; auto.
apply narrow_smaller; ∃ p1, p2; split; auto.
unfold CI_diff; simpl.
rewrite Hdec1. destruct (L_dec (map ci2 p2) (map ci1 p2)); solve [intuition | congruence].
Qed.
Lemma CI_opt_neg_join_incl: ∀ ci1 ci2,
((CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2))
⋐ (CI_neg_join ci1 ci2).
Proof.
intros. split.
- equiv. unfold pred_implies; simpl. intros val [H _]. apply H.
- intro p.
apply narrow_biggest. intros l [x [Hx Hl]]; subst l.
apply narrow_biggest. intros l [y [Hy Hl]]; subst l.
case_eq (L_dec (map ci1 y) (map ci2 y)); intros Hmap Hdec.
+ transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1) ⋒ CI_shared ci1 ci2) y).
× { apply narrow_smaller. ∃ y. split.
- simpl. rewrite PAnd_idempotent. rewrite Hx. rewrite <- Hy. implies.
- reflexivity. }
× apply narrow_smaller. right.
unfold CI_shared; simpl. rewrite Hdec. reflexivity.
+ transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1) ⋒ CI_shared ci1 ci2) x).
× { apply narrow_smaller. ∃ x. split.
- simpl. rewrite PAnd_idempotent. apply Hx.
- reflexivity. }
× { transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) x).
- apply narrow_smaller. left. reflexivity.
- apply narrow_smaller. ∃ y. split. implies.
simpl. rewrite Hdec. reflexivity. }
Qed.
Lemma CI_opt_weak_join_correct: ∀ ci1 ci2,
CI_opt_weak_join ci1 ci2 ≣ CI_weak_join ci1 ci2.
Proof.
intros ci1 ci2. rewrite CI_equiv_incl. split.
- apply CI_narrow_biggest.
+ unfold CI_opt_weak_join. unfold CI_weak_join.
rewrite CI_narrow_sym. rewrite <- CI_narrow_assoc.
rewrite CI_narrow_smaller_left.
rewrite CI_narrow_sym. transitivity (CI_opt_conj_join ci1 ci2).
× unfold CI_opt_conj_join. reflexivity.
× rewrite <- CI_opt_conj_join_equiv. reflexivity.
+ apply CI_narrow_biggest.
× { unfold CI_opt_weak_join. unfold CI_weak_join. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right.
rewrite CI_narrow_sym. rewrite <- CI_narrow_assoc.
rewrite CI_narrow_smaller_left.
rewrite CI_narrow_sym. apply CI_opt_neg_join_incl.
}
× { unfold CI_opt_weak_join. unfold CI_weak_join. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right. rewrite CI_shared_sym.
apply CI_opt_neg_join_incl.
}
- apply CI_narrow_biggest.
+ apply CI_narrow_biggest.
× unfold CI_weak_join. rewrite CI_narrow_smaller_left.
rewrite CI_opt_conj_join_equiv. apply CI_narrow_smaller_left.
× { unfold CI_weak_join. rewrite CI_narrow_smaller_right.
apply CI_narrow_biggest.
- rewrite CI_narrow_smaller_left.
apply CI_neg_join_subset. apply CI_diff_subset. implies.
- rewrite CI_narrow_smaller_right.
apply CI_neg_join_subset. apply CI_diff_subset. implies.
}
+ apply CI_weak_join_incl_shared.
Qed.
(* --------------------------------------------------------------------------
Concretization
-------------------------------------------------------------------------- *)
(* Evaluation of predicates in an environment. *)
Definition eval_pred' (env: Env) : pred → Prop :=
eval_pred (fun e ⇒ eval_expr env e).
(* Two equivalent concretizations. *)
Definition CI_concr ci env :=
eval_pred' env (context ci)
∧ ∀ p, eval_pred' env p → concr (map ci p) env.
Definition CI_concr' ci env :=
eval_pred' env (context ci)
∧ ∀ p, eval_pred' env p → concr (ci ∎ p) env.
Lemma CI_concr_equiv : ∀ ci env, CI_concr' ci env ↔ CI_concr ci env.
Proof.
intros ci env. split; intros [Hc Hm]; split; intuition.
- apply Hm in H. apply concr_monotone with (ci ∎ p).
apply consequence_p_incl. assumption.
- apply narrow_correct. intros l [x [Hx Hl]]. subst l.
apply Hm. apply Hx. simpl. intuition.
Qed.
Lemma Ci_concr_true: ∀ ci env,
CI_concr ci env → concr ((map ci) (PTrue)) env.
Proof.
intros ci env [_ H]. apply (H PTrue). unfold eval_pred'. simpl. trivial.
Qed.
Lemma CI_concr_monotone: ∀ x y e, x ⋐ y → CI_concr x e → CI_concr y e.
Proof.
intros ci1 ci2 e. repeat rewrite <- CI_concr_equiv.
intros [Hic Him] [Hcc Hcm]. split.
- apply Hic. apply Hcc.
- intros p Hp. apply Hcm in Hp. apply concr_monotone with (ci1 ∎ p).
apply Him. apply Hp.
Qed.
Lemma CI_join_correct: ∀ ci1 ci2 env,
CI_concr ci1 env ∨ CI_concr ci2 env → CI_concr (CI_join ci1 ci2) env.
Proof.
intros ci1 ci2 env [H | H].
apply CI_concr_monotone with ci1. apply CI_join_bigger_left. assumption.
apply CI_concr_monotone with ci2. apply CI_join_bigger_right. assumption.
Qed.
Lemma CI_narrow_correct: ∀ ci1 ci2 env,
CI_concr ci1 env → CI_concr ci2 env → CI_concr (CI_narrow ci1 ci2) env.
Proof.
intros ci1 ci2 env [Hc1 Hm1] [Hc2 Hm2]. split.
- simpl. split; assumption.
- intros p H. simpl. apply narrow_correct. intros l [Hl | Hl]; subst l.
apply Hm1. assumption. apply Hm2. assumption.
Qed.
(* Predicated Analyses *)
Definition strengthen ci p :=
{| context := PAnd (context ci) p;
map := map ci
|}.
Lemma refine_when_bottom : ∀ ci p env,
map ci p = bottom → (CI_concr ci env ↔ CI_concr (strengthen ci (PNot p)) env).
Proof.
intros ci p env Hbot. split; intros [Hc Hm]; split; simpl in ×.
- unfold eval_pred'; simpl. intuition. apply Hm in H. rewrite Hbot in H.
apply concr_bottom in H. assumption.
- apply Hm.
- destruct Hc as [Hc Hp]. apply Hc.
- apply Hm.
Qed.
Definition refined ci :=
{| context := context ci;
map := fun p ⇒ narrow (in_map ci (fun h ⇒ PAnd p (context ci) ⊣⊢ PAnd h (context ci)))
|}.
Lemma ci_bottom_refined: ∀ ci,
false_bottom ci →
false_bottom (refined ci).
Proof.
intros ci H. apply narrow_of_bottom. unfold in_map. ∃ PFalse. equiv.
Qed.
Lemma refine_by_context: ∀ ci, ci ≣ refined ci.
Proof.
intros ci. split. equiv.
intro p. apply incl_asym.
- apply narrow_biggest. intros l [x [Hx Hl]]. subst l. simpl in Hx.
apply narrow_biggest. intros l [y [Hy Hl]]. subst l.
apply narrow_smaller. unfold in_map. ∃ y. split.
transitivity (PAnd x (context ci)). rewrite <- Hx. implies. rewrite Hy. implies.
reflexivity.
- apply incl_narrow_weaken'.
intros l [x [Hx Hl]]. subst l. ∃ (map (refined ci) x). split.
apply narrow_smaller. ∃ x. split. implies. reflexivity.
∃ x. simpl. split. assumption. reflexivity.
Qed.
(* --------------------------------------------------------------------------
Transfer Functions
-------------------------------------------------------------------------- *)
(* Dependence of predicates: extension of the dependence of expressions. *)
Fixpoint pred_deps p var := match p with
| PTrue | PFalse ⇒ false
| PExpr e ⇒ deps e var
| PNot p ⇒ pred_deps p var
| PAnd p1 p2 | POr p1 p2 ⇒ pred_deps p1 var || pred_deps p2 var
end.
(* If a predicate [p] don't depend on a variable [var], then
the predicate has the same evaluation on an environment [env]
before and after any update of [var]. *)
Lemma pred_deps_correct: ∀ p var env,
pred_deps p var = false →
∀ val, eval_pred' env p = eval_pred' (update env var val) p.
Proof.
intros p var env Hd val.
induction p; auto.
- unfold eval_pred'. simpl. eapply deps_correct in Hd.
rewrite Hd. reflexivity.
- apply IHp in Hd. unfold eval_pred' in ×. simpl. rewrite Hd. reflexivity.
- simpl in Hd. apply orb_false_iff in Hd. destruct Hd as [Hd1 Hd2].
apply IHp1 in Hd1. apply IHp2 in Hd2.
unfold eval_pred' in ×. simpl. rewrite Hd1. rewrite Hd2. reflexivity.
- simpl in Hd. apply orb_false_iff in Hd. destruct Hd as [Hd1 Hd2].
apply IHp1 in Hd1. apply IHp2 in Hd2.
unfold eval_pred' in ×. simpl. rewrite Hd1. rewrite Hd2. reflexivity.
Qed.
(* Transfer function for the assignment [var := exp]. *)
Definition CI_assign var exp ci :=
{| context := if pred_deps (context ci) var then PTrue else context ci;
map := fun p ⇒ if pred_deps p var then top else assign var exp (map ci p)
|}.
Lemma CI_assign_correct: ∀ var exp val ci env,
CI_concr ci env → val = eval_expr env exp →
CI_concr (CI_assign var exp ci) (update env var val).
Proof.
intros var exp val ci env [Hc Hm] Hv. split.
- simpl. case_eq (pred_deps (context ci) var); intros Hdeps.
+ unfold eval_pred'. simpl. tauto.
+ apply pred_deps_correct with (env := env) (val := val) in Hdeps.
rewrite <- Hdeps. assumption.
- intros p Hp. simpl. case_eq (pred_deps p var); intros Hdeps.
+ apply concr_top.
+ apply assign_correct. apply Hm.
apply pred_deps_correct with (env := env) (val := val) in Hdeps.
rewrite Hdeps. assumption.
assumption.
Qed.
Lemma CI_assign_precise: ∀ var exp l ci,
(map ci) (PTrue) ⊑ l → (map (CI_assign var exp ci)) (PTrue) ⊑ assign var exp l.
Proof.
intros var exp l ci H. simpl.
apply assign_monotone. apply H.
Qed.
with signature pred_equiv ==> pred_equiv ==> iff
as pred_implies_morphism.
Proof.
unfold pred_equiv, pred_implies; intros; split; intros.
- rewrite <- H0. apply H1. rewrite H. auto.
- rewrite → H0. apply H1. rewrite <- H. auto.
Qed.
Lemma PAnd_idempotent: ∀ p, PAnd p p ⊣⊢ p.
Proof. intros p. equiv. Qed.
Lemma pred_equiv_dec: ∀ p1 p2, { p1 ⊣⊢ p2 } + { ¬ (p1 ⊣⊢ p2) }.
Proof.
intros; destruct (pred_implies_dec p1 p2).
- destruct (pred_implies_dec p2 p1).
+ left. unfold pred_implies, pred_equiv in *; intuition.
+ right. intro; apply n. rewrite H; auto.
- right. intro; apply n. rewrite H; auto.
Qed.
(* --------------------------------------------------------------------------
CI-pairs
--------------------------------------------------------------------------- *)
(* Notations for CI operations: ≣ ⋐ ⋑ ⋒ ⋓ *)
Record CI := {
context: pred;
map: pred → L
}.
(* Consequence. *)
(* [in_map ci P] is the set of elements of L linked to a predicates
that verifies P. *)
Definition in_map (ci: CI) (P: pred → Prop) : L → Prop :=
(fun l ⇒ ∃ p, P p ∧ l = map ci p).
Hint Unfold in_map.
Ltac simpl_in_map :=
let l := fresh "l" in
let p := fresh "p'" in
let H1 := fresh "H" p in
let H2 := fresh in
intros l [p [H1 H2]]; subst l;
unfold in_map; simpl map.
(* In a Ci-pair [ci], the consequence of a predicate [p] is the narrowing of
all elements of L linked to predicates [p'] such that p ∧ c ⊢ p',
with [c] context of [ci]. *)
Definition consequence (ci: CI) (p : pred) :=
narrow (in_map ci (fun p' ⇒ PAnd p (context ci) ⊢ p')).
Notation "ci ∎ p" := (consequence ci p) (at level 10, no associativity): type_scope.
(* [ci ∎ p] is more precise than the content of [ci] at [p]. *)
Lemma consequence_p_incl: ∀ ci p, ci ∎ p ⊑ map ci p.
Proof.
intros. apply narrow_smaller. ∃ p. implies.
Qed.
Definition false_bottom ci := map ci PFalse = bottom.
(* Guards that contradict the context imply bottom *)
Lemma consequence_contradiction_context: ∀ ci p,
false_bottom ci →
PAnd p (context ci) ⊢ PFalse →
ci ∎ p = bottom.
Proof.
intros [c I] p h_bot H; simpl in *; apply incl_asym; auto.
apply narrow_smaller; simpl.
∃ PFalse; auto.
Qed.
(* Compatibility of ∎ with ⊢ for context *)
Lemma CI_consequence_weaken_context: ∀ c1 c2 I p,
c1 ⊢ c2 → {| context := c1; map := I |} ∎ p ⊑ {| context := c2; map := I |} ∎ p.
Proof.
intros; unfold consequence; simpl.
apply narrow_biggest.
simpl_in_map.
apply narrow_smaller; ∃ p'; split; auto.
rewrite H; auto.
Qed.
(* Compatibility of ∎ with ⊑ for the elements of I *)
Lemma CI_consequence_weaken_map: ∀ c I1 I2 p,
(∀ q : pred, I1 q ⊑ I2 q) →
{| context := c; map := I1 |} ∎ p ⊑ {| context := c; map := I2 |} ∎ p.
Proof.
intros; unfold consequence; simpl.
apply incl_narrow_weaken'.
simpl_in_map.
∃ (I1 p'); split; eauto.
Qed.
(* Compatibility of ∎ with ⊢ for context and ⊑ for the elements of I *)
Lemma CI_consequence_weaken : ∀ ci1 ci2 p,
context ci1 ⊢ context ci2 → (∀ q : pred, map ci1 q ⊑ map ci2 q)
→ ci1 ∎ p ⊑ ci2 ∎ p.
Proof.
intros.
transitivity ({| context := context ci1; map := map ci2 |} ∎ p).
- apply CI_consequence_weaken_map; intuition.
- apply CI_consequence_weaken_context; intuition.
Qed.
(* Auxiliary lemma for proving that ⋓ computes upper bounds *)
Lemma CI_consequence_weaken_pred : ∀ ci p1 p2,
PAnd p1 (context ci) ⊢ p2 → ci ∎ p1 ⊑ ci ∎ p2.
Proof.
intros.
unfold consequence; simpl.
apply incl_narrow_weaken'. simpl_in_map.
∃ (map ci p'); intuition.
∃ p'; intuition. implies.
apply Hp'. simpl. intuition. apply H. simpl. intuition.
Qed.
(* --------------------------------------------------------------------------
Order and equivalence of CI-pairs
-------------------------------------------------------------------------- *)
(* Inclusion of CI-pairs. *)
Definition CI_incl (ci1 ci2: CI) :=
context ci1 ⊢ context ci2 ∧ ∀ p, ci1 ∎ p ⊑ ci2 ∎ p.
Notation "ci1 ⋐ ci2" := (CI_incl ci1 ci2) (at level 40, no associativity): type_scope.
Lemma CI_incl_weaken : ∀ ci1 ci2,
context ci1 ⊢ context ci2 → (∀ q : pred, map ci1 q ⊑ map ci2 q) → ci1 ⋐ ci2.
Proof.
intros ci1 ci2 Hc Hm.
unfold CI_incl. intuition. apply CI_consequence_weaken; assumption.
Qed.
(* Equivalence relation of CI-pairs. *)
Definition CI_equiv (ci1 ci2: CI) :=
context ci1 ⊣⊢ context ci2 ∧ ∀ p, ci1 ∎ p = ci2 ∎ p.
Notation "c1 ≣ c2" := (CI_equiv c1 c2) (at level 40, no associativity): type_scope.
(* ⋐ is an order *)
Instance CI_incl_refl: Reflexive CI_incl. unfold CI_incl; intuition. Qed.
Instance CI_incl_trans: Transitive CI_incl.
Proof. unfold Transitive, CI_incl; intuition; eauto. Qed.
(* ≣ is an equivalence relation *)
Instance CI_equiv_refl: Reflexive CI_equiv. unfold CI_equiv; intuition. Qed.
Instance CI_equiv_trans: Transitive CI_equiv.
Proof.
unfold Transitive, CI_equiv; intuition.
transitivity (context y); auto.
transitivity (y ∎ p); auto.
Qed.
Instance CI_equiv_symmetric: Symmetric CI_equiv.
Proof. unfold Symmetric, CI_equiv; intuition. Qed.
(* ⋐ is compatible with ≣ *)
Add Parametric Morphism : CI_incl
with signature CI_equiv ==> CI_equiv ==> iff
as CI_incl_morphism.
Proof.
unfold CI_equiv, CI_incl; split; intuition.
- rewrite <- H2; rewrite <- H; auto.
- rewrite <- H4; rewrite <- H3; auto.
- rewrite H2; rewrite H; auto.
- rewrite H4; rewrite H3; auto.
Qed.
(* ≣ is the kernel of ⋐ *)
Lemma CI_equiv_incl: ∀ ci1 ci2,
ci1 ≣ ci2 ↔ ci1 ⋐ ci2 ∧ ci2 ⋐ ci1.
Proof.
split.
- intro H; rewrite H; split; reflexivity.
- intros [[H1 H2] [H3 H4]]; split; auto.
split; auto.
Qed.
(* Bottom. *)
Definition CI_bottom := {|
context := PFalse;
map := fun p ⇒ match p with PFalse ⇒ bottom | _ ⇒ top end
|}.
(* Top. *)
Definition CI_top := {|
context := PTrue;
map := fun p ⇒ match p with PFalse ⇒ bottom | _ ⇒ top end
|}.
(* Bottom is the smallest CI-pairs. *)
Lemma CI_bottom_smallest: ∀ ci, CI_bottom ⋐ ci.
Proof.
intros; unfold CI_incl; split; simpl.
- implies.
- intros; transitivity bottom; auto.
unfold consequence, in_map; simpl.
apply narrow_smaller.
∃ PFalse; intuition.
implies.
Qed.
(* Top is the biggest CI-pairs. *)
Lemma CI_top_biggest: ∀ ci, false_bottom ci → ci ⋐ CI_top.
Proof.
intros ci Hbot; unfold CI_incl; split; simpl.
- implies.
- intros.
apply narrow_biggest; intros.
unfold in_map in H.
do 2 destruct H; subst; simpl in H.
unfold CI_top; simpl; destruct x; auto.
(* Only the cases where x = PFalse/p ⊢ PFalse remain *)
apply narrow_smaller.
unfold consequence, in_map; simpl.
∃ PFalse; split; auto.
generalize H; implies.
eapply H0; intuition eauto.
Qed.
Definition CI_subset (ci1 ci2: CI) :=
context ci1 ⊢ context ci2 ∧ ∀ p, map ci1 p ⊑ map ci2 p.
Lemma CI_incl_subset: ∀ ci1 ci2, CI_subset ci1 ci2 → ci1 ⋐ ci2.
Proof.
intros ci1 ci2 [Hc Hmap]. split. apply Hc.
intro p. apply incl_narrow_weaken'. intros l [x [Hx Hl]]; subst l.
∃ (map ci1 x). split. apply Hmap.
∃ x. split. rewrite Hc. implies. reflexivity.
Qed.
(* Equal CI-pairs are equivalent. *)
Lemma CI_equiv_equal: ∀ ci1 ci2,
context ci1 ⊣⊢ context ci2 →
(∀ p, map ci1 p = map ci2 p) →
ci1 ≣ ci2.
Proof.
intros ci1 ci2 Hc Hmap. rewrite CI_equiv_incl. split.
- apply CI_incl_subset. unfold CI_subset. split.
rewrite Hc. reflexivity. intro p. rewrite Hmap. reflexivity.
- apply CI_incl_subset. unfold CI_subset. split.
rewrite Hc. reflexivity. intro p. rewrite Hmap. reflexivity.
Qed.
(* --------------------------------------------------------------------------
Join of CI-pairs
-------------------------------------------------------------------------- *)
Definition CI_join (ci1 ci2: CI) := {|
context := (POr (context ci1) (context ci2));
map := fun p ⇒ ci1 ∎ p ⊔² ci2 ∎ p
|}.
Notation "c1 ⋓ c2" := (CI_join c1 c2) (at level 55, no associativity): type_scope.
(* In a join, PFalse is mapped to bottom. *)
Lemma CI_join_bottom: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (ci1 ⋓ ci2).
Proof.
intros [c1 I1] [c2 I2] H1 H2.
unfold consequence, in_map, join2; simpl.
apply join_only_bottom; intros.
destruct H; subst l; rewrite <- smaller_than_bottom_is_bottom.
- apply narrow_smaller; ∃ PFalse; implies.
- apply narrow_smaller; ∃ PFalse; implies.
Qed.
(* Symmetry of the join. *)
Lemma CI_join_sym_incl: ∀ ci1 ci2, (ci1 ⋓ ci2) ⋐ (ci2 ⋓ ci1).
Proof.
intros; destruct ci1 as [c1 I1 b1]; destruct ci2 as [c2 I2 b2].
unfold CI_join, CI_incl; simpl; split.
- red; simpl; tauto.
- intros; unfold consequence; simpl.
apply narrow_biggest; simpl_in_map.
apply narrow_smaller; ∃ p'; split.
+ unfold pred_implies in *; simpl in *; intuition.
+ rewrite join2_sym; auto.
Qed.
Lemma CI_join_sym: ∀ ci1 ci2, (ci1 ⋓ ci2) ≣ (ci2 ⋓ ci1).
Proof.
intros. rewrite CI_equiv_incl; auto using CI_join_sym_incl.
Qed.
(* The join of CI-pairs is an upper bound. *)
Lemma CI_join_bigger_left: ∀ ci1 ci2,
ci1 ⋐ (ci1 ⋓ ci2).
Proof.
split.
- unfold pred_implies; simpl; auto.
- intros.
transitivity (ci1 ∎ p ⊔² ci2 ∎ p); auto.
apply narrow_biggest; simpl_in_map.
apply join2_morphism_incl;
apply CI_consequence_weaken_pred; unfold pred_implies; intros; simpl in ×.
+ apply Hp'; simpl; intuition.
+ apply Hp'; simpl; intuition.
Qed.
Lemma CI_join_bigger_right: ∀ ci1 ci2,
ci2 ⋐ (ci1 ⋓ ci2).
Proof.
intros; rewrite (CI_join_sym); apply CI_join_bigger_left.
Qed.
(* The join of CI-pairs is *the least* upper bound. *)
Lemma CI_join_smallest:
∀ ci1 ci2 ci', ci1 ⋐ ci' → ci2 ⋐ ci' → (ci1 ⋓ ci2) ⋐ ci'.
Proof.
intros ci1 ci2 ci' [H11 H12] [H21 H22].
unfold CI_incl; simpl in *; split.
- rewrite H11; rewrite H21.
implies.
- intro p. apply incl_trans with (ci1 ∎ p ⊔² ci2 ∎ p).
+ apply consequence_p_incl.
+ apply join_smallest. intros l' [Hl' | Hl']; rewrite Hl'; intuition.
Qed.
(* ⋓ is compatible with ⋐ *)
Add Parametric Morphism : CI_join
with signature CI_incl ==> CI_incl ==> CI_incl
as CI_join_morphism_CI_incl.
Proof.
intros x1 y1 [Hxy11 Hxy12] x2 y2 [Hxy21 Hxy22].
unfold CI_join, CI_incl in *; simpl; split.
- rewrite Hxy11; rewrite Hxy21; auto.
- intros; apply incl_narrow_weaken'; simpl_in_map; simpl in ×.
∃ (x1 ∎ p' ⊔² x2 ∎ p'); split.
+ rewrite Hxy12; rewrite Hxy22; reflexivity.
+ ∃ p'; split; auto.
rewrite Hxy11; rewrite Hxy21; auto.
Qed.
(* ⋓ is compatible with ≣ *)
Add Parametric Morphism : CI_join
with signature CI_equiv ==> CI_equiv ==> CI_equiv
as CI_join_morphism.
Proof.
intros.
rewrite CI_equiv_incl; split.
- apply CI_join_morphism_CI_incl; auto. rewrite H; reflexivity. rewrite H0; reflexivity.
- apply CI_join_morphism_CI_incl; auto. rewrite H; reflexivity. rewrite H0; reflexivity.
Qed.
(* Alternative proof of symmetry *)
Lemma CI_join_sym': ∀ ci1 ci2, (ci1 ⋓ ci2) ≣ (ci2 ⋓ ci1).
Proof.
intros; rewrite CI_equiv_incl.
split;
(apply CI_join_smallest; [apply CI_join_bigger_right | apply CI_join_bigger_left]).
Qed.
(* Transitivity of the join. *)
Lemma CI_join_trans_incl: ∀ ci1 ci2 ci3, (ci1 ⋓ (ci2 ⋓ ci3)) ⋐ ((ci1 ⋓ ci2) ⋓ ci3).
Proof with auto using CI_join_bigger_left, CI_join_bigger_right.
intros; repeat apply CI_join_smallest.
- rewrite CI_join_bigger_left at 1...
- rewrite CI_join_bigger_right at 1...
- idtac...
Qed.
Lemma CI_join_trans: ∀ ci1 ci2 ci3, (ci1 ⋓ (ci2 ⋓ ci3)) ≣ ((ci1 ⋓ ci2) ⋓ ci3).
Proof.
intros; rewrite CI_equiv_incl; split.
- apply CI_join_trans_incl.
- rewrite (CI_join_sym _ ci3).
do 2 rewrite (CI_join_sym ci1).
rewrite (CI_join_sym ci2 ci3).
apply CI_join_trans_incl.
Qed.
(* --------------------------------------------------------------------------
Narrow on CI-pairs
-------------------------------------------------------------------------- *)
Definition CI_narrow (ci1 ci2 : CI) :=
{| context := (PAnd (context ci1) (context ci2));
map := fun p ⇒ map ci1 p ⊓² map ci2 p
|}.
Notation "ci1 ⋒ ci2" := (CI_narrow ci1 ci2) (at level 50, no associativity): type_scope.
(* In a narrowing, PFalse is mapped to bottom. *)
Lemma narrow_pfalse: ∀ ci1 ci2,
false_bottom ci1 ∨ false_bottom ci2 →
false_bottom (ci1 ⋒ ci2).
Proof.
unfold false_bottom.
intros ci1 ci2 [H | H]; simpl; rewrite H; unfold narrow2; intuition.
Qed.
(* Symmetry of thee narrow. *)
Lemma CI_narrow_sym_incl: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ (ci2 ⋒ ci1).
Proof.
intros ci1 ci2. split. implies.
intro p. apply incl_narrow_weaken. intros l [x [Hx Hl]]; subst l.
unfold in_map. ∃ x. unfold CI_narrow; simpl. split.
rewrite <- Hx. implies. apply narrow2_sym.
Qed.
Lemma CI_narrow_sym: ∀ ci1 ci2, (ci1 ⋒ ci2) ≣ (ci2 ⋒ ci1).
Proof.
intros. rewrite CI_equiv_incl; auto using CI_narrow_sym_incl.
Qed.
(* The narrow is a lower bound. *)
Lemma CI_narrow_smaller_left: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ ci1.
Proof.
intros.
unfold CI_incl; simpl; split.
- implies.
- intro. apply CI_consequence_weaken; simpl.
+ implies.
+ intro. unfold CI_narrow; unfold narrow2; simpl. intuition.
Qed.
Lemma CI_narrow_smaller_right: ∀ ci1 ci2, (ci1 ⋒ ci2) ⋐ ci2.
Proof.
intros; rewrite (CI_narrow_sym); apply CI_narrow_smaller_left.
Qed.
(* The narrow of CI-pairs is *the greatest* lower bound. *)
Lemma CI_narrow_biggest : ∀ ci1 ci2 ci',
ci' ⋐ ci1 → ci' ⋐ ci2 → ci' ⋐ (ci1 ⋒ ci2).
Proof.
intros ci1 ci2 ci' [H1c H1m] [H2c H2m].
unfold CI_incl; simpl; split.
- rewrite <- H1c. rewrite <- H2c. implies.
- intro. apply narrow_biggest; simpl_in_map.
apply narrow_biggest.
intros l [Hl | Hl]; subst l.
+ transitivity (ci' ∎ p').
× apply CI_consequence_weaken_pred.
rewrite <- Hp'. simpl. rewrite <- H1c; rewrite <- H2c. implies.
× transitivity (ci1 ∎ p'). intuition.
apply consequence_p_incl.
(* TODO : factoring *)
+ transitivity (ci' ∎ p').
× apply CI_consequence_weaken_pred.
rewrite <- Hp'. simpl. rewrite <- H1c; rewrite <- H2c. implies.
× transitivity (ci2 ∎ p'). intuition.
apply consequence_p_incl.
Qed.
(* Prove 'rel z t' assuming 'rel x y', by 'rel z x' and 'rel y t' *)
Ltac transitivity2 eq :=
match type of eq with
| ?rel ?x ?y ⇒
match goal with |- rel ?z ?t ⇒
let H := fresh in assert (rel z x) as H;
[ | let H' := fresh in assert (rel y t) as H';
[ | transitivity x;
[ exact H
| transitivity y ;
[ exact eq | exact H' ]]]]
end
end.
(* ⋒ is compatible with ⋐ *)
Add Parametric Morphism : CI_narrow
with signature CI_incl ==> CI_incl ==> CI_incl
as CI_narrow_morphism_CI_incl.
Proof.
intros x1 y1 [Hxy11 Hxy12] x2 y2 [Hxy21 Hxy22].
unfold CI_narrow, CI_incl in *; simpl.
split.
- rewrite Hxy11; rewrite Hxy21; implies.
- unfold narrow2, consequence, in_map in *; simpl in *; intros.
do 2 rewrite narrow_exists_narrow.
assert (∀ p1 p2 p3, p1 ∧ (p2 ∨ p3) ↔ (p1 ∧ p2) ∨ (p1 ∧ p3)); [tauto |].
do 2 rewrite (narrow_exists_equiv _ _ _ (fun l p ⇒ H _ _ _)); clear H.
do 2 rewrite narrow_exists_or.
apply narrow2_morphism_incl.
+ transitivity2 (Hxy12 (PAnd p (context x2))).
× apply narrow_exists_implies. implies.
× apply narrow_exists_implies; intros l p0. rewrite Hxy21; implies.
+ transitivity2 (Hxy22 (PAnd p (context x1))).
× apply narrow_exists_implies. implies.
× apply narrow_exists_implies; intros l p0. rewrite Hxy11; implies.
Qed.
(* ⋒ is compatible with ≣ *)
Add Parametric Morphism : CI_narrow
with signature CI_equiv ==> CI_equiv ==> CI_equiv
as CI_narrow_morphism_CI_equiv.
Proof.
intros x1 x2 Hx y1 y2 Hy.
destruct (CI_equiv_incl x1 x2); destruct (CI_equiv_incl y1 y2).
rewrite CI_equiv_incl; split;
apply CI_narrow_morphism_CI_incl; intuition.
Qed.
(* TODO: this proof is independant of the considered lattice. *)
Lemma CI_narrow_assoc: ∀ a b c,
((a ⋒ b) ⋒ c) ≣ (a ⋒ (b ⋒ c)).
Proof.
intros. rewrite CI_equiv_incl. split.
- apply CI_narrow_biggest.
+ transitivity (a ⋒ b); apply CI_narrow_smaller_left.
+ apply CI_narrow_biggest.
× transitivity (a ⋒ b). apply CI_narrow_smaller_left. apply CI_narrow_smaller_right.
× apply CI_narrow_smaller_right.
- apply CI_narrow_biggest.
+ apply CI_narrow_biggest.
× apply CI_narrow_smaller_left.
× transitivity (b ⋒ c). apply CI_narrow_smaller_right. apply CI_narrow_smaller_left.
+ transitivity (b ⋒ c); apply CI_narrow_smaller_right.
Qed.
(* --------------------------------------------------------------------------
Weak-join of CI-pairs
-------------------------------------------------------------------------- *)
(* The weak-join on CI-pairs is defined as the narrowing of three CI-pairs. *)
(* First auxiliary function for the weak join:
gather implications like (p1 ∧ p2 ⇒ (map ci1 p1) ⊔ (map ci2 p2)) *)
Definition CI_conj_join (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒
⊓ (fun l ⇒
∃ p1 p2, PAnd p1 p2 ⊣⊢ p ∧
l = map ci1 p1 ⊔² map ci2 p2)
|}.
Lemma pfalse_conj_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_conj_join ci1 ci2).
Proof.
intros ci1 ci2 H1 H2.
apply narrow_of_bottom. ∃ PFalse, PFalse; split.
- red; implies.
- rewrite H1; rewrite H2.
unfold join2. symmetry. apply join_only_bottom. intuition.
Qed.
Lemma CI_join_incl_conj_join : ∀ ci1 ci2, (ci1 ⋓ ci2) ⋐ (CI_conj_join ci1 ci2).
Proof.
intros.
apply CI_incl_weaken.
- unfold CI_incl; simpl; reflexivity.
- intro q; simpl.
apply join_smallest. intros l [H_l | H_l]; subst l.
Ltac aux ci p q :=
apply incl_narrow_weaken';
intros l [p1 [p2 [Hq Hl]]]; rewrite Hl;
∃ (map ci p); intuition;
∃ p; intuition; rewrite <- Hq; implies.
+ aux ci1 p1 q. + aux ci2 p2 q.
Qed.
(* Second auxiliary function for the weak join:
gather implications like (¬ (context ci2) ∧ p ⇒ map ci1 p) *)
Definition CI_neg_join (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒ ⊓ in_map ci1 (fun p1 ⇒ PAnd p1 (PNot (context ci2)) ⊣⊢ p)
|}.
Lemma pfalse_neg_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_neg_join ci1 ci2).
Proof.
intros ci1 ci2 H1 H2.
apply narrow_of_bottom. ∃ PFalse. split.
- unfold pred_equiv; simpl; intuition.
- rewrite H1. reflexivity.
Qed.
Lemma CI_join_incl_neg_join: ∀ ci1 ci2,
false_bottom ci2 →
(ci1 ⋓ ci2) ⋐ (CI_neg_join ci1 ci2).
Proof.
intros ci1 ci2 Hbot2.
apply CI_incl_weaken.
- unfold CI_incl; simpl; reflexivity.
- intro q; simpl.
apply join_smallest. intros l [H_l | H_l]; subst l.
+ apply incl_narrow_weaken'; simpl_in_map.
∃ (map ci1 p'); intuition.
∃ p'; intuition. rewrite <- Hp'. implies.
+ apply narrow_biggest; simpl_in_map.
transitivity bottom.
× rewrite smaller_than_bottom_is_bottom.
apply narrow_of_bottom. ∃ PFalse. rewrite Hbot2. intuition.
rewrite <- Hp'. implies.
× apply bottom_smallest.
Qed.
Lemma CI_neg_join_subset: ∀ ci1 ci2 ci1' ci2',
CI_subset ci1 ci1' → context ci2 ⊣⊢ context ci2' →
CI_neg_join ci1 ci2 ⋐ CI_neg_join ci1' ci2'.
Proof.
intros ci1 ci2 ci1' ci2' [Hc1 Hm1] Hc2.
apply CI_incl_subset. unfold CI_subset. split.
- simpl. rewrite Hc1, Hc2. implies.
- intro p. unfold CI_neg_join; simpl. apply incl_narrow_weaken'.
intros l [x [Hp Hl]]; subst l. ∃ (map ci1 x).
split. apply Hm1.
unfold in_map. ∃ x. split. rewrite <- Hp.
equiv. apply H1. rewrite Hc2. apply H. apply H1. rewrite <- Hc2. apply H.
reflexivity.
Qed.
(* The final weak-join. *)
Definition CI_weak_join (ci1 ci2 : CI) :=
(CI_conj_join ci1 ci2) ⋒ ((CI_neg_join ci1 ci2) ⋒ (CI_neg_join ci2 ci1)).
Lemma CI_weak_join_bottom: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_weak_join ci1 ci2).
Proof.
intros; unfold CI_weak_join, false_bottom, join2, in_map in *; simpl.
apply narrow_of_bottom; left.
symmetry; apply narrow_of_bottom; ∃ PFalse, PFalse; split.
- equiv.
- symmetry.
apply join_only_bottom.
intros l [Hb | Hb]; congruence.
Qed.
Lemma CI_join_incl_weak_join : ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
(ci1 ⋓ ci2) ⋐ (CI_weak_join ci1 ci2).
Proof.
intros. unfold CI_weak_join.
repeat apply CI_narrow_biggest.
- apply CI_join_incl_conj_join.
- apply CI_join_incl_neg_join; assumption.
- rewrite CI_join_sym'.
apply CI_join_incl_neg_join; assumption.
Qed.
(* The weak-join is a weaker join. *)
Lemma CI_join_incl_weak_join' : ∀ ci1 ci2 ci1' ci2',
false_bottom ci1' →
false_bottom ci2' →
ci1 ≣ ci1' → ci2 ≣ ci2' → (ci1 ⋓ ci2) ⋐ (CI_weak_join ci1' ci2').
Proof.
intros ci1 ci2 ci1' ci2' Hbot1 Hbot2 H1 H2.
rewrite H1, H2. apply CI_join_incl_weak_join; auto.
Qed.
(* --------------------------------------------------------------------------
Optimization of the weak-join
-------------------------------------------------------------------------- *)
(* [ci_shared] contains only implications that belong to both [ci1] and [ci2] ;
other predicates are bound to [top]. *)
Definition CI_shared (ci1 ci2 : CI) :=
{| context := (POr (context ci1) (context ci2));
map := fun p ⇒ if L_dec (map ci1 p) (map ci2 p) then map ci1 p else top
|}.
(* [ci_diff] contains only the elements of [ci1] mapped to different values
in [ci2]. All other elements are mapped to top. *)
Definition CI_diff (ci1 ci2 : CI) :=
{| context := context ci1;
map := fun p ⇒ if L_dec (map ci1 p) (map ci2 p) then top else (map ci1 p)
|}.
(* The optimized weak-join between two CI-pairs [ci1] and [ci2] is the narrow
between:
- the shared CI-pair [ci_shared] ;
- and the weak-join between the rests [ci1_diff] and [ci2_diff]. *)
Definition CI_opt_conj_join ci1 ci2 :=
(CI_conj_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Definition CI_opt_neg_join ci1 ci2 :=
(CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Definition CI_opt_weak_join ci1 ci2 :=
(CI_weak_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2).
Lemma CI_opt_weak_join_pfalse: ∀ ci1 ci2,
false_bottom ci1 →
false_bottom ci2 →
false_bottom (CI_opt_conj_join ci1 ci2).
Proof.
unfold CI_opt_conj_join, false_bottom; intros ci1 ci2 H1 H2.
apply narrow_of_bottom; right.
simpl.
rewrite H1; rewrite H2.
destruct (L_dec bottom bottom); intuition.
Qed.
Lemma CI_shared_sym: ∀ ci1 ci2, CI_shared ci1 ci2 ≣ CI_shared ci2 ci1.
Proof.
intros. apply CI_equiv_equal. equiv.
intro p. simpl.
case (L_dec (map ci1 p) (map ci2 p)); intros Hmap;
case (L_dec (map ci2 p) (map ci1 p)); intros Hmap';
congruence.
Qed.
Lemma CI_diff_subset: ∀ ci1 ci2, CI_subset ci1 (CI_diff ci1 ci2).
Proof.
intros ci1 ci2. unfold CI_subset. split.
- implies.
- intro p. simpl. destruct L_dec. apply top_biggest. reflexivity.
Qed.
Lemma CI_weak_join_incl_shared: ∀ ci1 ci2,
CI_weak_join ci1 ci2 ⋐ CI_shared ci1 ci2.
Proof.
intros ci1 ci2. apply CI_incl_subset. split. implies.
intro p. simpl.
case (L_dec (map ci1 p) (map ci2 p)); intros Hmap.
rewrite narrow2_smaller_left. apply narrow_smaller.
∃ p, p. split. equiv. rewrite Hmap. rewrite join2_idempotent. reflexivity.
apply top_biggest.
Qed.
Lemma CI_opt_conj_join_equiv: ∀ ci1 ci2,
(CI_conj_join ci1 ci2) ≣ (CI_opt_conj_join ci1 ci2).
Proof.
intros ci1 ci2; split.
- simpl. equiv.
- intro p. unfold consequence; simpl. apply incl_asym.
+ apply incl_narrow_weaken'. simpl_in_map.
∃ (map (CI_conj_join ci1 ci2) p'). split.
× apply narrow_biggest. intros l [Hl | Hl]; subst l.
{ apply incl_narrow_weaken'. intros l [p1 [p2 [Hp Hl]]]; subst l.
∃ (map ci1 p1 ⊔² map ci2 p2). split.
- unfold CI_diff; simpl. apply join2_morphism_incl.
+ destruct (L_dec (map ci1 p1) (map ci2 p1)); auto.
+ destruct (L_dec (map ci2 p2) (map ci1 p2)); auto.
- ∃ p1, p2. intuition.
}
{ unfold CI_shared; simpl.
destruct (L_dec (map ci1 p') (map ci2 p')); auto.
transitivity (map ci1 p' ⊔² map ci2 p').
- apply narrow_smaller. ∃ p', p'. intuition. equiv.
- rewrite <- e. apply join_smallest. intros l [Hl|Hl]; subst l; intuition.
}
× ∃ p'. intuition. generalize Hp'; implies.
+ apply narrow_biggest. intros l [p' [Hp' Hl]]. subst l.
apply narrow_biggest. intros l [p1 [p2 [Hp12 Hl]]]. subst l.
case_eq (L_dec (map ci1 p1) (map ci2 p1)); intros Hmap1 Hdec1.
2: case_eq (L_dec (map ci1 p2) (map ci2 p2)); intros Hmap2 Hdec2.
Local Ltac CI_conj_join_opt_equiv_solve :=
apply narrow_smaller; red;
match goal with Hp' : _ ⊢ ?p', Hp12: PAnd ?p1 ?p2 ⊣⊢ ?p' |- ∃ p0, _ ∧ ?F ?q = ?F p0 ⇒
∃ q ; split; [transitivity p'; [rewrite <- Hp' | rewrite <- Hp12]; implies | auto]
end.
× transitivity (map (CI_opt_conj_join ci1 ci2) p1).
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_shared ci1 ci2) p1). apply narrow_smaller. auto.
unfold CI_shared; simpl. rewrite Hdec1. auto.
× transitivity (map (CI_opt_conj_join ci1 ci2) p2).
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_shared ci1 ci2) p2). apply narrow_smaller. intuition.
unfold CI_shared; simpl. rewrite Hdec2. eauto.
× transitivity (map (CI_opt_conj_join ci1 ci2) p').
CI_conj_join_opt_equiv_solve.
transitivity (map (CI_conj_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) p').
apply narrow_smaller; auto.
apply narrow_smaller; ∃ p1, p2; split; auto.
unfold CI_diff; simpl.
rewrite Hdec1. destruct (L_dec (map ci2 p2) (map ci1 p2)); solve [intuition | congruence].
Qed.
Lemma CI_opt_neg_join_incl: ∀ ci1 ci2,
((CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) ⋒ (CI_shared ci1 ci2))
⋐ (CI_neg_join ci1 ci2).
Proof.
intros. split.
- equiv. unfold pred_implies; simpl. intros val [H _]. apply H.
- intro p.
apply narrow_biggest. intros l [x [Hx Hl]]; subst l.
apply narrow_biggest. intros l [y [Hy Hl]]; subst l.
case_eq (L_dec (map ci1 y) (map ci2 y)); intros Hmap Hdec.
+ transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1) ⋒ CI_shared ci1 ci2) y).
× { apply narrow_smaller. ∃ y. split.
- simpl. rewrite PAnd_idempotent. rewrite Hx. rewrite <- Hy. implies.
- reflexivity. }
× apply narrow_smaller. right.
unfold CI_shared; simpl. rewrite Hdec. reflexivity.
+ transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1) ⋒ CI_shared ci1 ci2) x).
× { apply narrow_smaller. ∃ x. split.
- simpl. rewrite PAnd_idempotent. apply Hx.
- reflexivity. }
× { transitivity (map (CI_neg_join (CI_diff ci1 ci2) (CI_diff ci2 ci1)) x).
- apply narrow_smaller. left. reflexivity.
- apply narrow_smaller. ∃ y. split. implies.
simpl. rewrite Hdec. reflexivity. }
Qed.
Lemma CI_opt_weak_join_correct: ∀ ci1 ci2,
CI_opt_weak_join ci1 ci2 ≣ CI_weak_join ci1 ci2.
Proof.
intros ci1 ci2. rewrite CI_equiv_incl. split.
- apply CI_narrow_biggest.
+ unfold CI_opt_weak_join. unfold CI_weak_join.
rewrite CI_narrow_sym. rewrite <- CI_narrow_assoc.
rewrite CI_narrow_smaller_left.
rewrite CI_narrow_sym. transitivity (CI_opt_conj_join ci1 ci2).
× unfold CI_opt_conj_join. reflexivity.
× rewrite <- CI_opt_conj_join_equiv. reflexivity.
+ apply CI_narrow_biggest.
× { unfold CI_opt_weak_join. unfold CI_weak_join. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right.
rewrite CI_narrow_sym. rewrite <- CI_narrow_assoc.
rewrite CI_narrow_smaller_left.
rewrite CI_narrow_sym. apply CI_opt_neg_join_incl.
}
× { unfold CI_opt_weak_join. unfold CI_weak_join. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right. rewrite CI_narrow_assoc.
rewrite CI_narrow_smaller_right. rewrite CI_shared_sym.
apply CI_opt_neg_join_incl.
}
- apply CI_narrow_biggest.
+ apply CI_narrow_biggest.
× unfold CI_weak_join. rewrite CI_narrow_smaller_left.
rewrite CI_opt_conj_join_equiv. apply CI_narrow_smaller_left.
× { unfold CI_weak_join. rewrite CI_narrow_smaller_right.
apply CI_narrow_biggest.
- rewrite CI_narrow_smaller_left.
apply CI_neg_join_subset. apply CI_diff_subset. implies.
- rewrite CI_narrow_smaller_right.
apply CI_neg_join_subset. apply CI_diff_subset. implies.
}
+ apply CI_weak_join_incl_shared.
Qed.
(* --------------------------------------------------------------------------
Concretization
-------------------------------------------------------------------------- *)
(* Evaluation of predicates in an environment. *)
Definition eval_pred' (env: Env) : pred → Prop :=
eval_pred (fun e ⇒ eval_expr env e).
(* Two equivalent concretizations. *)
Definition CI_concr ci env :=
eval_pred' env (context ci)
∧ ∀ p, eval_pred' env p → concr (map ci p) env.
Definition CI_concr' ci env :=
eval_pred' env (context ci)
∧ ∀ p, eval_pred' env p → concr (ci ∎ p) env.
Lemma CI_concr_equiv : ∀ ci env, CI_concr' ci env ↔ CI_concr ci env.
Proof.
intros ci env. split; intros [Hc Hm]; split; intuition.
- apply Hm in H. apply concr_monotone with (ci ∎ p).
apply consequence_p_incl. assumption.
- apply narrow_correct. intros l [x [Hx Hl]]. subst l.
apply Hm. apply Hx. simpl. intuition.
Qed.
Lemma Ci_concr_true: ∀ ci env,
CI_concr ci env → concr ((map ci) (PTrue)) env.
Proof.
intros ci env [_ H]. apply (H PTrue). unfold eval_pred'. simpl. trivial.
Qed.
Lemma CI_concr_monotone: ∀ x y e, x ⋐ y → CI_concr x e → CI_concr y e.
Proof.
intros ci1 ci2 e. repeat rewrite <- CI_concr_equiv.
intros [Hic Him] [Hcc Hcm]. split.
- apply Hic. apply Hcc.
- intros p Hp. apply Hcm in Hp. apply concr_monotone with (ci1 ∎ p).
apply Him. apply Hp.
Qed.
Lemma CI_join_correct: ∀ ci1 ci2 env,
CI_concr ci1 env ∨ CI_concr ci2 env → CI_concr (CI_join ci1 ci2) env.
Proof.
intros ci1 ci2 env [H | H].
apply CI_concr_monotone with ci1. apply CI_join_bigger_left. assumption.
apply CI_concr_monotone with ci2. apply CI_join_bigger_right. assumption.
Qed.
Lemma CI_narrow_correct: ∀ ci1 ci2 env,
CI_concr ci1 env → CI_concr ci2 env → CI_concr (CI_narrow ci1 ci2) env.
Proof.
intros ci1 ci2 env [Hc1 Hm1] [Hc2 Hm2]. split.
- simpl. split; assumption.
- intros p H. simpl. apply narrow_correct. intros l [Hl | Hl]; subst l.
apply Hm1. assumption. apply Hm2. assumption.
Qed.
(* Predicated Analyses *)
Definition strengthen ci p :=
{| context := PAnd (context ci) p;
map := map ci
|}.
Lemma refine_when_bottom : ∀ ci p env,
map ci p = bottom → (CI_concr ci env ↔ CI_concr (strengthen ci (PNot p)) env).
Proof.
intros ci p env Hbot. split; intros [Hc Hm]; split; simpl in ×.
- unfold eval_pred'; simpl. intuition. apply Hm in H. rewrite Hbot in H.
apply concr_bottom in H. assumption.
- apply Hm.
- destruct Hc as [Hc Hp]. apply Hc.
- apply Hm.
Qed.
Definition refined ci :=
{| context := context ci;
map := fun p ⇒ narrow (in_map ci (fun h ⇒ PAnd p (context ci) ⊣⊢ PAnd h (context ci)))
|}.
Lemma ci_bottom_refined: ∀ ci,
false_bottom ci →
false_bottom (refined ci).
Proof.
intros ci H. apply narrow_of_bottom. unfold in_map. ∃ PFalse. equiv.
Qed.
Lemma refine_by_context: ∀ ci, ci ≣ refined ci.
Proof.
intros ci. split. equiv.
intro p. apply incl_asym.
- apply narrow_biggest. intros l [x [Hx Hl]]. subst l. simpl in Hx.
apply narrow_biggest. intros l [y [Hy Hl]]. subst l.
apply narrow_smaller. unfold in_map. ∃ y. split.
transitivity (PAnd x (context ci)). rewrite <- Hx. implies. rewrite Hy. implies.
reflexivity.
- apply incl_narrow_weaken'.
intros l [x [Hx Hl]]. subst l. ∃ (map (refined ci) x). split.
apply narrow_smaller. ∃ x. split. implies. reflexivity.
∃ x. simpl. split. assumption. reflexivity.
Qed.
(* --------------------------------------------------------------------------
Transfer Functions
-------------------------------------------------------------------------- *)
(* Dependence of predicates: extension of the dependence of expressions. *)
Fixpoint pred_deps p var := match p with
| PTrue | PFalse ⇒ false
| PExpr e ⇒ deps e var
| PNot p ⇒ pred_deps p var
| PAnd p1 p2 | POr p1 p2 ⇒ pred_deps p1 var || pred_deps p2 var
end.
(* If a predicate [p] don't depend on a variable [var], then
the predicate has the same evaluation on an environment [env]
before and after any update of [var]. *)
Lemma pred_deps_correct: ∀ p var env,
pred_deps p var = false →
∀ val, eval_pred' env p = eval_pred' (update env var val) p.
Proof.
intros p var env Hd val.
induction p; auto.
- unfold eval_pred'. simpl. eapply deps_correct in Hd.
rewrite Hd. reflexivity.
- apply IHp in Hd. unfold eval_pred' in ×. simpl. rewrite Hd. reflexivity.
- simpl in Hd. apply orb_false_iff in Hd. destruct Hd as [Hd1 Hd2].
apply IHp1 in Hd1. apply IHp2 in Hd2.
unfold eval_pred' in ×. simpl. rewrite Hd1. rewrite Hd2. reflexivity.
- simpl in Hd. apply orb_false_iff in Hd. destruct Hd as [Hd1 Hd2].
apply IHp1 in Hd1. apply IHp2 in Hd2.
unfold eval_pred' in ×. simpl. rewrite Hd1. rewrite Hd2. reflexivity.
Qed.
(* Transfer function for the assignment [var := exp]. *)
Definition CI_assign var exp ci :=
{| context := if pred_deps (context ci) var then PTrue else context ci;
map := fun p ⇒ if pred_deps p var then top else assign var exp (map ci p)
|}.
Lemma CI_assign_correct: ∀ var exp val ci env,
CI_concr ci env → val = eval_expr env exp →
CI_concr (CI_assign var exp ci) (update env var val).
Proof.
intros var exp val ci env [Hc Hm] Hv. split.
- simpl. case_eq (pred_deps (context ci) var); intros Hdeps.
+ unfold eval_pred'. simpl. tauto.
+ apply pred_deps_correct with (env := env) (val := val) in Hdeps.
rewrite <- Hdeps. assumption.
- intros p Hp. simpl. case_eq (pred_deps p var); intros Hdeps.
+ apply concr_top.
+ apply assign_correct. apply Hm.
apply pred_deps_correct with (env := env) (val := val) in Hdeps.
rewrite Hdeps. assumption.
assumption.
Qed.
Lemma CI_assign_precise: ∀ var exp l ci,
(map ci) (PTrue) ⊑ l → (map (CI_assign var exp ci)) (PTrue) ⊑ assign var exp l.
Proof.
intros var exp l ci H. simpl.
apply assign_monotone. apply H.
Qed.
Transfer Function for the test assume(exp)
Fixpoint pred_assume pred exp := match pred with
| PTrue ⇒ PTrue
| PFalse ⇒ PFalse
| PExpr e ⇒ if E_dec e exp then PTrue else PExpr e
| PNot p ⇒ PNot (pred_assume p exp)
| PAnd p1 p2 ⇒ PAnd (pred_assume p1 exp) (pred_assume p2 exp)
| POr p1 p2 ⇒ POr (pred_assume p1 exp) (pred_assume p2 exp)
end.
Definition CI_assume exp ci :=
let h := PExpr exp in
{| context := PAnd (context ci) h;
map := fun p ⇒ narrow ( fun l ⇒ ∃ p', p ⊣⊢ pred_assume p' exp
∧ l = assume exp (map ci p'))
|}.
Lemma ci_bottom_assume: ∀ exp ci,
false_bottom ci →
false_bottom (CI_assume exp ci).
Proof.
intros exp ci H. apply narrow_of_bottom.
unfold in_map. ∃ PFalse. split. implies.
rewrite H. symmetry. apply assume_bottom.
Qed.
Lemma pred_assume_correct: ∀ pred exp (val: Exp → Value),
eval_value (val exp) → (eval_pred val (pred_assume pred exp) ↔ eval_pred val pred).
Proof.
intros pred exp val Hv. induction pred; simpl in *; intuition.
- destruct (E_dec e exp) as [He | _]. rewrite He. apply Hv. apply H.
- destruct (E_dec e exp) as [He | _]; simpl. tauto. apply H.
Qed.
Lemma pred_assume_correct': ∀ exp env pred,
eval_value (eval_expr env exp) →
(eval_pred' env (pred_assume pred exp) ↔ eval_pred' env pred).
Proof.
intros exp env pred Hv. apply pred_assume_correct. apply Hv.
Qed.
Lemma CI_assume_correct: ∀ exp ci env,
CI_concr ci env →
eval_value (eval_expr env exp) →
CI_concr (CI_assume exp ci) env.
Proof.
intros exp ci env [Hc Hm] Hv. split.
- unfold eval_pred'. simpl. auto.
- intros p Hp. simpl. apply narrow_correct. simpl_in_map.
apply assume_correct.
+ apply Hm. rewrite <- (pred_assume_correct' exp env p').
× unfold eval_pred'. rewrite <- Hp'. exact Hp.
× apply Hv.
+ apply Hv.
Qed.
Lemma CI_assume_precise: ∀ exp l ci,
(map ci) (PTrue) ⊑ l → (map (CI_assume exp ci)) (PTrue) ⊑ assume exp l.
Proof.
intros exp l ci H. simpl. apply incl_trans with (assume exp (map ci PTrue)).
apply narrow_smaller. ∃ PTrue. intuition.
apply assume_monotone. apply H.
Qed.
Extension of CI_assume from expression to predicates.
Fixpoint CI_assume_pred pred ci := match pred with
| PTrue ⇒ ci
| PFalse ⇒ CI_bottom
| PExpr exp ⇒ CI_assume exp ci
| PNot p ⇒ ci
| PAnd p1 p2 ⇒ CI_narrow (CI_assume_pred p1 ci) (CI_assume_pred p2 ci)
| POr p1 p2 ⇒ CI_join (CI_assume_pred p1 ci) (CI_assume_pred p2 ci)
end.
Lemma CI_assume_pred_correct: ∀ pred ci env,
CI_concr ci env →
eval_pred' env pred →
CI_concr (CI_assume_pred pred ci) env.
Proof.
intros pred ci env H Hv. induction pred; simpl; intuition.
- contradict Hv.
- apply CI_assume_correct. apply H. apply Hv.
- simpl. apply CI_narrow_correct. apply IHpred1. apply Hv. apply IHpred2. apply Hv.
- simpl. apply CI_join_correct. destruct Hv as [Hv | Hv].
+ left. apply IHpred1. apply Hv.
+ right. apply IHpred2. apply Hv.
Qed.
Transfer function for the assignment [var := exp].
(* CI-pair after an assignment. Two operators on predicates, weaken and strengthen, are used
to modify the guards in the context and the guards respectively. *)
Definition make_CI_assign (weaken strengthen: pred → Var → Exp → pred) var exp ci :=
{| context := weaken (context ci) var exp;
map := fun p ⇒
narrow (fun l ⇒ ∃ p', l = assign var exp (map ci p') ∧
p ⊣⊢ strengthen p' var exp)
|}.
(* Soundness theorem for the operators weaken and strengthen. *)
Definition weaken_correct weaken := ∀ p env var exp,
eval_pred' env p → eval_pred' (update env var (eval_expr env exp)) (weaken p var exp).
Definition strengthen_correct strengthen := ∀ p env var exp,
eval_pred' (update env var (eval_expr env exp)) (strengthen p var exp) → eval_pred' env p.
(* The soundness properties of weaken and strengthen ensure the soundness of the
transfer function for assignments. *)
Lemma make_CI_assign_correct: ∀ weaken strengthen, ∀ var exp val ci env,
weaken_correct weaken → strengthen_correct strengthen →
CI_concr ci env → val = eval_expr env exp →
CI_concr (make_CI_assign weaken strengthen var exp ci) (update env var val).
Proof.
intros weaken strengthen var exp val CI env
weaken_correct strengthen_correct [Hc Hm] Hv; simpl in ×.
split.
- simpl. subst val.
apply (weaken_correct _ _ _ _); auto.
- intros p Hp. simpl.
apply narrow_correct; simpl_in_map.
apply assign_correct; auto.
apply Hm. subst val.
eapply (strengthen_correct _ _ _ _).
unfold eval_pred' in Hp; rewrite H in Hp; eassumption.
Qed.
(* Auxiliary function to define one possible instance of weaken and strengthen.
Replaces the expressions that depend on v by PTrue or PFalse depending on the polarity. *)
Fixpoint kill_pred (pos:bool) p v := match p with
| PTrue ⇒ PTrue
| PFalse ⇒ PFalse
| PExpr e ⇒ if deps e v then (if pos then PTrue else PFalse) else PExpr e
| PNot p ⇒ PNot (kill_pred (negb pos) p v)
| PAnd p1 p2 ⇒ PAnd (kill_pred pos p1 v) (kill_pred pos p2 v)
| POr p1 p2 ⇒ POr (kill_pred pos p1 v) (kill_pred pos p2 v)
end.
Weakening of a predicate: change all positive (resp. negative) occurrences of an
expression depending on v by PTrue (resp. PFalse). Ignore the expression.
Strenghtening of a predicate: converse operation (w.r.t polarity) of weaken_pred
Definition strengthen_pred pred var (_:Exp) := kill_pred false pred var.
(* Weakening a valid predicate results in a valid predicate that no longer
depends on the variable. Conversely, if a strengthened predicate is valid,
so is its non-strengthened version *)
Lemma weaken_strengthen_pred_correct: ∀ val env var exp p,
(eval_pred' env p →
eval_pred' (update env var val) (weaken_pred p var exp))
∧
(eval_pred' (update env var val) (strengthen_pred p var exp) →
eval_pred' env p).
Proof.
induction p; split; unfold eval_pred'; simpl; intros;
try solve [intuition];
unfold weaken_pred, strengthen_pred in *; simpl in *;
case_eq (deps e var); intro Hdeps; simpl in ×.
- auto.
- rewrite deps_correct; auto.
- rewrite Hdeps in H; red in H. intuition.
- rewrite Hdeps in H; simpl in H.
rewrite deps_correct in H; auto.
Qed.
Lemma weaken_pred_correct: weaken_correct weaken_pred.
Proof.
unfold weaken_correct; intros.
destruct (weaken_strengthen_pred_correct (eval_expr env exp) env var exp p). auto.
Qed.
Lemma strengthen_pred_correct: strengthen_correct strengthen_pred.
Proof.
unfold strengthen_correct; intros.
destruct (weaken_strengthen_pred_correct (eval_expr env exp) env var exp p). auto.
Qed.
(* Optimized transfer function for the assignment [var := exp]. Predicates
that involve var are not completely removed, but instead weakened or strengthened. *)
Definition CI_assign_opt := make_CI_assign weaken_pred strengthen_pred.
Lemma CI_assign_opt_correct: ∀ var exp val ci env,
CI_concr ci env → val = eval_expr env exp →
CI_concr (CI_assign_opt var exp ci) (update env var val).
Proof.
intros.
apply make_CI_assign_correct; auto using weaken_pred_correct, strengthen_pred_correct.
Qed.
Lemma CI_assign_opt_precise: ∀ var exp l ci,
(map ci) (PTrue) ⊑ l → (map (CI_assign_opt var exp ci)) (PTrue) ⊑ assign var exp l.
Proof.
intros var exp l ci H. simpl. apply incl_trans with (assign var exp (map ci PTrue)).
apply narrow_smaller. ∃ PTrue. intuition.
apply assign_monotone. apply H.
Qed.
End S.
(* Weakening a valid predicate results in a valid predicate that no longer
depends on the variable. Conversely, if a strengthened predicate is valid,
so is its non-strengthened version *)
Lemma weaken_strengthen_pred_correct: ∀ val env var exp p,
(eval_pred' env p →
eval_pred' (update env var val) (weaken_pred p var exp))
∧
(eval_pred' (update env var val) (strengthen_pred p var exp) →
eval_pred' env p).
Proof.
induction p; split; unfold eval_pred'; simpl; intros;
try solve [intuition];
unfold weaken_pred, strengthen_pred in *; simpl in *;
case_eq (deps e var); intro Hdeps; simpl in ×.
- auto.
- rewrite deps_correct; auto.
- rewrite Hdeps in H; red in H. intuition.
- rewrite Hdeps in H; simpl in H.
rewrite deps_correct in H; auto.
Qed.
Lemma weaken_pred_correct: weaken_correct weaken_pred.
Proof.
unfold weaken_correct; intros.
destruct (weaken_strengthen_pred_correct (eval_expr env exp) env var exp p). auto.
Qed.
Lemma strengthen_pred_correct: strengthen_correct strengthen_pred.
Proof.
unfold strengthen_correct; intros.
destruct (weaken_strengthen_pred_correct (eval_expr env exp) env var exp p). auto.
Qed.
(* Optimized transfer function for the assignment [var := exp]. Predicates
that involve var are not completely removed, but instead weakened or strengthened. *)
Definition CI_assign_opt := make_CI_assign weaken_pred strengthen_pred.
Lemma CI_assign_opt_correct: ∀ var exp val ci env,
CI_concr ci env → val = eval_expr env exp →
CI_concr (CI_assign_opt var exp ci) (update env var val).
Proof.
intros.
apply make_CI_assign_correct; auto using weaken_pred_correct, strengthen_pred_correct.
Qed.
Lemma CI_assign_opt_precise: ∀ var exp l ci,
(map ci) (PTrue) ⊑ l → (map (CI_assign_opt var exp ci)) (PTrue) ⊑ assign var exp l.
Proof.
intros var exp l ci H. simpl. apply incl_trans with (assign var exp (map ci PTrue)).
apply narrow_smaller. ∃ PTrue. intuition.
apply assign_monotone. apply H.
Qed.
End S.
This page has been generated by coqdoc