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: forall (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 : forall env var val, (update env var val) var = val /\ forall 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 : forall env var exp, deps exp var = false -> forall val, eval_expr (update env var val) exp = eval_expr env exp. (** Underlying Abstract Domain *) Variable L: Type. (** 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: forall l1 l2 l3, l1 ⊑ l2 -> l2 ⊑ l3 -> l1 ⊑ l3. Variable incl_refl: forall l, l ⊑ l. Variable incl_asym: forall l1 l2, l1 ⊑ l2 -> l2 ⊑ l1 -> l1 = l2. (* [top] and [bottom] are respectively the greatest and the least element of L *) Variable bottom_smallest: forall l, bottom ⊑ l. Variable top_biggest: forall l, l ⊑ top. (* [⊔ val] is the least upper bound of elements l such that [val l] *) Variable join_bigger: forall l, forall (val: L -> Prop), val l -> l ⊑ ⊔ val. Variable join_smallest: forall l, forall (val: L -> Prop), (forall l', val l' -> l' ⊑ l) -> ⊔ val ⊑ l. (* [⊓ val] is the greatest lower bound of elements l such that [val l] *) Variable narrow_smaller: forall l, forall (val: L -> Prop), val l -> ⊓ val ⊑ l. Variable narrow_biggest: forall (val: L -> Prop) l, (forall l', val l' -> l ⊑ l') -> l ⊑ ⊓ val. Variable L_dec: forall (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: forall x y e, x ⊑ y -> concr x e -> concr y e. Variable concr_top: forall e, concr top e. Variable concr_bottom: forall 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: forall val e, (exists 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: forall (val: L -> Prop) (e: Env), (forall 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: forall (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: forall 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: forall (exp:Exp) (l:L) (env:Env), concr l env -> eval_value (eval_expr env exp) -> concr (assume exp l) env. Variable assume_monotone: forall exp (l l':L), l ⊑ l' -> assume exp l ⊑ assume exp l'. Variable assign_bottom: forall var exp, assign var exp bottom = bottom. Variable assume_bottom: forall 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: forall l1 l2, l1 ⊑ l1 ⊔² l2. eauto. Qed. Lemma join2_bigger_right: forall l1 l2, l2 ⊑ l1 ⊔² l2. eauto. Qed. Lemma narrow2_smaller_left: forall l1 l2, l1 ⊓² l2 ⊑ l1. eauto. Qed. Lemma narrow2_smaller_right: forall l1 l2, l1 ⊓² l2 ⊑ l2. eauto. Qed. Hint Resolve join2_bigger_left join2_bigger_right narrow2_smaller_left narrow2_smaller_right. Lemma join2_idempotent: forall 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: forall 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: forall 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: forall (val1 val2: L -> Prop), (forall l, val2 l -> val1 l) -> ⊓ val1 ⊑ ⊓ val2. Proof. intros. apply narrow_biggest; intros. apply narrow_smaller; auto. Qed. Lemma incl_narrow_weaken': forall (val1 val2: L -> Prop), (forall l, val2 l -> exists 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: forall A (P1 : A -> Prop) (P2 : A -> L -> Prop), ⊓(fun l => exists p, P1 p /\ l = ⊓P2 p) = ⊓(fun l => exists p, P1 p /\ P2 p l). Proof. intros; apply incl_asym. - apply incl_narrow_weaken'; intros l [p [Hp1 Hp2]]. exists (narrow (P2 p)); eauto. - apply narrow_biggest; intros l [p [Hp1 Hp2]]; subst. apply incl_narrow_weaken; eauto. Qed. Lemma narrow_exists_equiv: forall A (P1 P2: L -> A -> Prop), (forall l p, P1 l p <-> P2 l p) -> ⊓(fun l => exists p, P1 l p) = ⊓(fun l => exists p, P2 l p). Proof. intros; apply incl_asym; apply incl_narrow_weaken; intros l [p Hp]; exists p. - rewrite H; auto. - rewrite <- H; auto. Qed. Lemma narrow_exists_implies: forall A (P1 P2: L -> A -> Prop), (forall l p, P2 l p -> P1 l p) -> ⊓(fun l => exists p, P1 l p) ⊑ ⊓(fun l => exists p, P2 l p). Proof. intros; apply incl_narrow_weaken; intros l [p Hp]; exists p; auto. Qed. Lemma narrow_exists_or: forall A (P1 P2 : L -> A -> Prop), ⊓ (fun l => exists p, P1 l p \/ P2 l p) = ⊓ (fun l => exists p, P1 l p) ⊓² ⊓(fun l => exists 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]]. + exists (⊓(fun l0 => exists p0, P1 l0 p0)); split; eauto. + exists (⊓(fun l0 => exists p0, P2 l0 p0)); split; eauto. Qed. Lemma narrow_of_bottom: forall (val: L -> Prop), val bottom -> narrow val = bottom. Proof. eauto. Qed. Lemma smaller_than_bottom_is_bottom: forall l, l ⊑ bottom <-> l = bottom. Proof. split. auto. intro H. rewrite H. reflexivity. Qed. Lemma join_only_bottom: forall (val: L -> Prop), (forall 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: forall (e:Exp), pred | PNot: forall (p:pred), pred | PAnd: forall (p1 p2: pred), pred | POr: forall (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 := forall 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: forall p1 p2, { p1 ⊢ p2 } + { ~ (p1 ⊢ p2) }. (* Equivalence of predicates. *) Definition pred_equiv p1 p2 := forall 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. (** ⊢ 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. (** 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. (** 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. (** 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. (** 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. (** ⊢ 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: forall p, PAnd p p ⊣⊢ p. Proof. intros p. equiv. Qed. Lemma pred_equiv_dec: forall 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 => exists 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: forall ci p, ci ∎ p ⊑ map ci p. Proof. intros. apply narrow_smaller. exists p. implies. Qed. Definition false_bottom ci := map ci PFalse = bottom. (* Guards that contradict the context imply bottom *) Lemma consequence_contradiction_context: forall 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. exists PFalse; auto. Qed. (* Compatibility of ∎ with ⊢ for context *) Lemma CI_consequence_weaken_context: forall 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; exists p'; split; auto. rewrite H; auto. Qed. (* Compatibility of ∎ with ⊑ for the elements of I *) Lemma CI_consequence_weaken_map: forall c I1 I2 p, (forall 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. exists (I1 p'); split; eauto. Qed. (* Compatibility of ∎ with ⊢ for context and ⊑ for the elements of I *) Lemma CI_consequence_weaken : forall ci1 ci2 p, context ci1 ⊢ context ci2 -> (forall 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 : forall ci p1 p2, PAnd p1 (context ci) ⊢ p2 -> ci ∎ p1 ⊑ ci ∎ p2. Proof. intros. unfold consequence; simpl. apply incl_narrow_weaken'. simpl_in_map. exists (map ci p'); intuition. exists 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 /\ forall p, ci1 ∎ p ⊑ ci2 ∎ p. Notation "ci1 ⋐ ci2" := (CI_incl ci1 ci2) (at level 40, no associativity): type_scope. Lemma CI_incl_weaken : forall ci1 ci2, context ci1 ⊢ context ci2 -> (forall 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 /\ forall 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: forall 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: forall ci, CI_bottom ⋐ ci. Proof. intros; unfold CI_incl; split; simpl. - implies. - intros; transitivity bottom; auto. unfold consequence, in_map; simpl. apply narrow_smaller. exists PFalse; intuition. implies. Qed. (* Top is the biggest CI-pairs. *) Lemma CI_top_biggest: forall 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. exists PFalse; split; auto. generalize H; implies. eapply H0; intuition eauto. Qed. Definition CI_subset (ci1 ci2: CI) := context ci1 ⊢ context ci2 /\ forall p, map ci1 p ⊑ map ci2 p. Lemma CI_incl_subset: forall 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. exists (map ci1 x). split. apply Hmap. exists x. split. rewrite Hc. implies. reflexivity. Qed. (* Equal CI-pairs are equivalent. *) Lemma CI_equiv_equal: forall ci1 ci2, context ci1 ⊣⊢ context ci2 -> (forall 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: forall 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; exists PFalse; implies. - apply narrow_smaller; exists PFalse; implies. Qed. (* Symmetry of the join. *) Lemma CI_join_sym_incl: forall 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; exists p'; split. + unfold pred_implies in *; simpl in *; intuition. + rewrite join2_sym; auto. Qed. Lemma CI_join_sym: forall 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: forall 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: forall 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: forall 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 *. exists (x1 ∎ p' ⊔² x2 ∎ p'); split. + rewrite Hxy12; rewrite Hxy22; reflexivity. + exists 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': forall 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: forall 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: forall 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: forall 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: forall 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. exists x. unfold CI_narrow; simpl. split. rewrite <- Hx. implies. apply narrow2_sym. Qed. Lemma CI_narrow_sym: forall 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: forall 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: forall 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 : forall 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 (forall 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: forall 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 => exists p1 p2, PAnd p1 p2 ⊣⊢ p /\ l = map ci1 p1 ⊔² map ci2 p2) |}. Lemma pfalse_conj_join : forall 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. exists PFalse, PFalse; split. - red; implies. - rewrite H1; rewrite H2. unfold join2. symmetry. apply join_only_bottom. intuition. Qed. Lemma CI_join_incl_conj_join : forall 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; exists (map ci p); intuition; exists 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 : forall 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. exists PFalse. split. - unfold pred_equiv; simpl; intuition. - rewrite H1. reflexivity. Qed. Lemma CI_join_incl_neg_join: forall 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. exists (map ci1 p'); intuition. exists p'; intuition. rewrite <- Hp'. implies. + apply narrow_biggest; simpl_in_map. transitivity bottom. * rewrite smaller_than_bottom_is_bottom. apply narrow_of_bottom. exists PFalse. rewrite Hbot2. intuition. rewrite <- Hp'. implies. * apply bottom_smallest. Qed. Lemma CI_neg_join_subset: forall 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. exists (map ci1 x). split. apply Hm1. unfold in_map. exists 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: forall 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; exists PFalse, PFalse; split. - equiv. - symmetry. apply join_only_bottom. intros l [Hb | Hb]; congruence. Qed. Lemma CI_join_incl_weak_join : forall 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' : forall 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: forall 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: forall 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: forall 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: forall 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. exists p, p. split. equiv. rewrite Hmap. rewrite join2_idempotent. reflexivity. apply top_biggest. Qed. Lemma CI_opt_conj_join_equiv: forall 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. exists (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. exists (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. - exists 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. exists p', p'. intuition. equiv. - rewrite <- e. apply join_smallest. intros l [Hl|Hl]; subst l; intuition. } * exists 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' |- exists p0, _ /\ ?F ?q = ?F p0 => exists 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; exists 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: forall 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. exists 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. exists 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. exists y. split. implies. simpl. rewrite Hdec. reflexivity. } Qed. Lemma CI_opt_weak_join_correct: forall 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) /\ forall p, eval_pred' env p -> concr (map ci p) env. Definition CI_concr' ci env := eval_pred' env (context ci) /\ forall p, eval_pred' env p -> concr (ci ∎ p) env. Lemma CI_concr_equiv : forall 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: forall 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: forall 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: forall 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: forall 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 : forall 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: forall ci, false_bottom ci -> false_bottom (refined ci). Proof. intros ci H. apply narrow_of_bottom. unfold in_map. exists PFalse. equiv. Qed. Lemma refine_by_context: forall 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. exists 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. exists (map (refined ci) x). split. apply narrow_smaller. exists x. split. implies. reflexivity. exists 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: forall p var env, pred_deps p var = false -> forall 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: forall 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: forall 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 => exists p', p ⊣⊢ pred_assume p' exp /\ l = assume exp (map ci p')) |}. Lemma ci_bottom_assume: forall exp ci, false_bottom ci -> false_bottom (CI_assume exp ci). Proof. intros exp ci H. apply narrow_of_bottom. unfold in_map. exists PFalse. split. implies. rewrite H. symmetry. apply assume_bottom. Qed. Lemma pred_assume_correct: forall 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': forall 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: forall 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: forall 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. exists 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: forall 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 => exists 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 := forall 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 := forall 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: forall weaken strengthen, forall 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. *) Definition weaken_pred pred var (_:Exp) := kill_pred true pred var. (** 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: forall 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: forall 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: forall 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. exists PTrue. intuition. apply assign_monotone. apply H. Qed. End S.