Compositionality (ClassCompose.v)

Once all the machinery of ClassDistribute.v is in place, it is surprisingly simple to show how instantiations of that framework compose. The reasoning for composition is just like in Section 5 in the paper, that is, all we require is a proof that given two intersectors, applying the second one does not affect the intersected-predicate of the first one. When that is the case, all the other parts of two intersector modules easily compose.

Require Import Common.
Require Import Decide.
Require Import Tradition.
Require Import Convert.
Require Import Preprocess.
Require Import Extend.
Require Import Class.
Require Import ClassDistribute.
Import SumOfProducts.

Module Type Composable (LI : Intersector) (RI : Intersector).
Import LI.
Import RI.
Import Generics.
Import Decidable.
Import Proof.

Parameter composable_intersect : forall t : Tree CT, LI.Intersected t -> TForall LI.Intersected (RI.intersect t).

End Composable.

Module Composor (LI : Intersector) (RI : Intersector) (c : Composable LI RI) <: Intersector.
Import LI.
Import RI.
Import c.
Import Generics.
Import Decidable.
Import Proof.
Module RUIntersector := UIntersector RI.
Import RUIntersector.

Definition intersect : Tree CT -> SoP := fun (t : Tree CT) => (tbind RI.intersect) (LI.intersect t).

Lemma project : forall p : Tree CT, Sub Decidable (intersect p) (node p).
  intros.
  unfold intersect.
  apply sub_transd with (LI.intersect p).
  fold uintersect.
  apply uintersect_counitd.
  apply LI.project.
Qed.

Definition Intersected : Tree CT -> Prop := fun (t : Tree CT) => LI.Intersected t /\ RI.Intersected t.

Lemma tforall_bind : forall {A B : Type} (P : Tree B -> Prop) (f : Tree A -> Tree (Tree B)) (t : Tree (Tree A)), (TForall (fun tt : Tree A => TForall P (f tt)) t) -> TForall P (tbind f t).
  intros.
  induction t.
    apply tforall_leaf.
    simpl. inversion H. assumption.
    simpl. apply branch_tforall in H. inversion H. apply IHt1 in H0. apply IHt2 in H1. apply tforall_branch; assumption.
Qed.

Lemma tforall_split : forall {A : Type} (P Q : A -> Prop) (t : Tree A), TForall P t /\ TForall Q t -> TForall (fun tt => (P tt) /\ (Q tt)) t.
  intros.
  induction t.
    apply tforall_leaf.
    apply tforall_node. inversion H. apply node_tforall in H0. apply node_tforall in H1. split; assumption.
    inversion H. apply branch_tforall in H0. apply branch_tforall in H1. inversion H0. inversion H1. apply tforall_branch.
      apply IHt1. split; assumption.
      apply IHt2. split; assumption.
Qed.

Lemma tforall_split2 : forall {A : Type} (P Q : A -> Prop) (t : Tree A), TForall (fun tt => (P tt) /\ (Q tt)) t -> TForall P t /\ TForall Q t.
  intros.
  induction t.
    split; apply tforall_leaf.
    inversion H. inversion H1. split; apply tforall_node; assumption.
    inversion H. apply IHt1 in H2. apply IHt2 in H3. inversion H2. inversion H3.
      split; apply tforall_branch; assumption.
Qed.

Lemma intersected : forall p : Tree CT, TForall Intersected (intersect p).
  intros.
  unfold intersect.
  apply tforall_bind.
  assert (HLIntersected : TForall LI.Intersected (LI.intersect p)). apply LI.intersected.
  induction (LI.intersect p).
    apply tforall_leaf.
    apply tforall_node.
      inversion HLIntersected. unfold Intersected. apply tforall_split. split.
        apply composable_intersect. assumption.
        apply RI.intersected.
    inversion HLIntersected. apply IHs1 in H1. apply IHs2 in H2. apply tforall_branch; assumption.
Qed.

Lemma intersectedl : forall l r : Tree CT, Intersected (branch l r) -> Intersected l.
  intros. inversion H. apply LI.intersectedl in H0. apply RI.intersectedl in H1.
  unfold Intersected. split; assumption.
Qed.

Lemma intersectedr : forall l r : Tree CT, Intersected (branch l r) -> Intersected r.
  intros. inversion H. apply LI.intersectedr in H0. apply RI.intersectedr in H1.
  unfold Intersected. split; assumption.
Qed.

Lemma texists_bind : forall {A B : Type} (P : B -> Prop) (f : A -> Tree B) (t : Tree A), TExists (fun (tt : A) => TExists P (f tt)) t -> TExists P (tbind f t).
  intros.
  induction t.
    inversion H.
    simpl. inversion H. assumption.
    inversion H.
      apply IHt1 in H1. simpl. apply texists_left. assumption.
      apply IHt2 in H1. simpl. apply texists_right. assumption.
Qed.

Lemma dnf_split_right : forall (P Q : Tree CT -> Prop) (t : T), DNF (fun (tt : Tree CT) => (P tt) /\ (Q tt)) t -> ((DNF P t) /\ (DNF Q t)).
  intros.
  unfold DNF. inversion H. apply tforall_split2 in H1. inversion H1. split; exists x; try assumption.
Qed.

Lemma sub_bind : forall (R : T -> T -> Prop) (f : Tree CT -> Tree (Tree CT)) (p : SoP) (t : Tree (Tree CT)), TExists (fun (tt : Tree CT) => Sub R p (f tt)) t -> Sub R p (tbind f t).
  intros.
  induction t; inversion H.
    assumption.
    apply IHt1 in H1. simpl. apply sub_unionl. assumption.
    apply IHt2 in H1. simpl. apply sub_unionr. assumption.
Qed.

Lemma CTR_mono : forall (R S : T -> T -> Prop), (forall (t1 t2 : T), R t1 t2 -> S t1 t2) -> (forall (ct1 ct2 : CT), (CTR R) ct1 ct2 -> (CTR S) ct1 ct2).
  intros.
  unfold CTR.
  unfold CTR in H0.
  apply H in H0.
  assumption.
Qed.

Lemma sub_prod_mono : forall (R S : CT -> CT -> Prop) (l r : Tree CT), (forall (t1 t2 : CT), R t1 t2 -> S t1 t2) -> SubProd R l r -> SubProd S l r.
  intros R S l r impl sub.
  unfold SubProd in sub.
  induction r.
    apply tforall_leaf.
    apply tforall_node. inversion sub; subst. apply texists_mono with (fun l1 : CT => R l1 a). intros. apply impl. assumption. assumption.
    inversion sub. apply IHr1 in H1. apply IHr2 in H2. apply tforall_branch; assumption.
Qed.

Lemma sub_mono : forall (R S : T -> T -> Prop) (l r : SoP), (forall (t1 t2 : T), R t1 t2 -> S t1 t2) -> Sub R l r -> Sub S l r.
  intros.
  unfold Sub in H0. induction l.
    apply tforall_leaf.
    apply tforall_node. inversion H0. subst.
      apply texists_mono with (SubProd (CTR R) a). intros. apply sub_prod_mono with (CTR R). apply CTR_mono. assumption. assumption. assumption.
    inversion H0. subst. apply IHl1 in H3. apply IHl2 in H4. apply tforall_branch; assumption.
Qed.

Lemma intersect_promote_R : forall (R : T -> T -> Prop), AdmitsD R -> forall (p p' : Tree CT), (forall p' : Tree CT, SubProd (CTR R) p p' -> SubProd (CTInversion R) p p') -> Intersected p -> SubProd (CTR R) p p' -> Sub R (node p) (intersect p').
  intros R admits p p' inv pre sub.
  unfold intersect.
  unfold Intersected in pre. destruct pre as [ prel prer ]. pose proof (LI.intersect_promote_R R admits p p' inv prel sub) as subl. clear sub prel. inversion subl. subst. clear subl. rename H0 into subl. induction subl; simpl.
   apply RI.intersect_promote_R; try assumption.
   apply sub_unionl. assumption.
   apply sub_unionr. assumption.
Qed.

Lemma tswaps_union : forall (lsop rsop : SoP) (pos : Position), tswaps (union (generic lsop) (generic rsop)) pos = Nat.max (tswaps (generic lsop) pos) (tswaps (generic rsop) pos).
  intros.
  unfold tswaps at 1.
  rewrite (tinvariant_eq _ (union _ _)). simpl. reflexivity.
Qed.

Lemma intersect_swaps : forall (p : Tree CT) (pos : Position), tswaps (generic (intersect p)) pos <= tswaps (generic (node p)) pos.
  intros.
  unfold intersect.
  rewrite <- LI.intersect_swaps.
  induction (LI.intersect p).
    reflexivity.
    simpl @tbind. apply RI.intersect_swaps.
    simpl @tbind. unfold generic. simpl. rewrite -> tswaps_union. rewrite -> tswaps_union.
      apply max_mono; assumption.
Qed.

End Composor.

This page has been generated by coqdoc