Disjointness (ClassDisjoint.v)

This file shows a simple extension implemented in the framework of ClassDistribute.v. The module type disjointness makes some assumption about a given disjointness predicate, the implementation of the intersector is straightforward from there. An interesting fact that we can prove at the end: disjointness is in fact composable after ANY other extension.
Require Import Common.
Require Import Decide.
Require Import Tradition.
Require Import Convert.
Require Import Preprocess.
Require Import Extend.
Require Import Class.
Require Import ClassDistribute.
Require Import ClassCompose.
Import SumOfProducts.
Import Generics.

Module Type Disjointness.

Parameter Disjointness : Class -> Class -> Prop.
Parameter Disjointness_symm : forall c1 c2 : Class, Disjointness c1 c2 -> Disjointness c2 c1.
Parameter Disjointness_antirefl : forall c : Class, Disjointness c c -> False.
Parameter Disjointness_inh : forall (c1 c2 c3 : Class) (t : T), Disjointness c1 c2 -> pInh c3 c1 t -> Disjointness c3 c2.
Parameter Disjointness_dec : forall c1 c2 : Class, {Disjointness c1 c2} + {~ Disjointness c1 c2}.

End Disjointness.

Module DsjIntersect (Disjointness : Disjointness) <: Intersector.
Import Disjointness.

Lemma Disjointness_trans : forall (c1 c2 c3 : Class) (t : T), Disjointness c1 c2 -> PreInh c3 c1 t -> Disjointness c3 c2.
  intros c1 c2 c3 t Hdsj HpreInh.
  induction HpreInh.
    assumption.
    apply IHHpreInh in Hdsj.
    apply Disjointness_inh with c' c't; assumption.
Qed.

Inductive CTdsj : CT -> CT -> Prop :=
  ct_dsj : forall (c1 c2 : Class) (ti1 to1 ti2 to2 : T), Disjointness c1 c2 -> CTdsj (cclass c1 ti1 to1) (cclass c2 ti2 to2).

Lemma CTdsj_dec : forall ct1 ct2 : CT, {CTdsj ct1 ct2} + {~ CTdsj ct1 ct2}.
  intros ct1 ct2.
  destruct ct1 as [|c1 ti1 to1].
    right. unfold not. intros H. inversion H.
    destruct ct2 as [|c2 ti2 to2].
      right. unfold not. intros H. inversion H.
      destruct (Disjointness_dec c1 c2).
        left. apply ct_dsj. assumption.
        right. unfold not. intros. inversion H. contradiction.
Qed.

Lemma CTdsj_symm : forall ct1 ct2 : CT, CTdsj ct1 ct2 -> CTdsj ct2 ct1.
  intros.
  induction H.
  apply Disjointness_symm in H.
  apply ct_dsj. assumption.
Qed.

Inductive ICTdsj : Tree CT -> CT -> Prop :=
  | ict_dsj_node : forall ct ct', CTdsj ct' ct -> ICTdsj (node ct') ct
  | ict_dsj_left : forall (t1 t2 : Tree CT) (ct : CT), ICTdsj t1 ct -> ICTdsj (branch t1 t2) ct
  | ict_dsj_right : forall (t1 t2 : Tree CT) (ct : CT), ICTdsj t2 ct -> ICTdsj (branch t1 t2) ct
.

Lemma ICTdsj_dec : forall (t : Tree CT) (ct : CT), {ICTdsj t ct} + {~ ICTdsj t ct}.
  intros.
  induction t.
    right. unfold not. intros. inversion H.
    destruct (CTdsj_dec a ct).
      left. apply ict_dsj_node. assumption.
      right. unfold not. intros. inversion H. contradiction.
    destruct IHt1.
      left. apply ict_dsj_left. assumption.
      destruct IHt2.
        left. apply ict_dsj_right. assumption.
        right. unfold not. intros H. inversion H; contradiction.
Qed.

Inductive Idsj : Tree CT -> Tree CT -> Prop :=
  | i_dsj_node : forall (ct : CT) (t : Tree CT), ICTdsj t ct -> Idsj (node ct) t
  | i_dsj_left : forall (t11 t12 t2 : Tree CT), Idsj t11 t2 -> Idsj (branch t11 t12) t2
  | i_dsj_right : forall (t11 t12 t2 : Tree CT), Idsj t12 t2 -> Idsj (branch t11 t12) t2
.

Lemma Idsj_dec : forall t1 t2 : Tree CT, {Idsj t1 t2} + {~ Idsj t1 t2}.
  intros.
  induction t1.
    right. unfold not. intros. inversion H.
    destruct (ICTdsj_dec t2 a).
      left. apply i_dsj_node. assumption.
      right. unfold not. intros. inversion H. contradiction.
    destruct IHt1_1.
      left. apply i_dsj_left. assumption.
      destruct IHt1_2.
        left. apply i_dsj_right. assumption.
        right. unfold not. intros. inversion H; contradiction.
Qed.

Lemma Idsj_symm : forall t1 t2 : Tree CT, Idsj t1 t2 -> Idsj t2 t1.
  intros.
  induction H.
    induction t.
      inversion H.
      inversion H. subst. apply CTdsj_symm in H1. apply ict_dsj_node in H1. apply i_dsj_node. assumption.
      inversion H; subst.
        apply IHt1 in H3. apply i_dsj_left. assumption.
        apply IHt2 in H3. apply i_dsj_right. assumption.
    clear H. induction t2.
      inversion IHIdsj.
      inversion IHIdsj. subst. apply (ict_dsj_left t11 t12 a) in H0. apply i_dsj_node. assumption.
      inversion IHIdsj; subst.
        apply IHt2_1 in H2. apply i_dsj_left. assumption.
        apply IHt2_2 in H2. apply i_dsj_right. assumption.
    clear H. induction t2.
      inversion IHIdsj.
      inversion IHIdsj. subst. apply (ict_dsj_right t11 t12 a) in H0. apply i_dsj_node. assumption.
      inversion IHIdsj; subst.
        apply IHt2_1 in H2. apply i_dsj_left. assumption.
        apply IHt2_2 in H2. apply i_dsj_right. assumption.
Qed.

Inductive IIntersected : Tree CT -> Prop :=
  | ileaf : IIntersected leaf
  | inode : forall ct : CT, IIntersected (node ct)
  | ibranch : forall (t1 t2 : Tree CT), IIntersected t1 -> IIntersected t2 -> ~Idsj t1 t2 -> IIntersected (branch t1 t2).

Definition Intersected : Tree CT -> Prop := IIntersected.

Inductive NotIntersected : Tree CT -> Prop :=
  | ni_left : forall (t1 t2 : Tree CT), NotIntersected t1 -> NotIntersected (branch t1 t2)
  | ni_right : forall (t1 t2 : Tree CT), NotIntersected t2 -> NotIntersected (branch t1 t2)
  | ni_branch : forall (t1 t2 : Tree CT), Idsj t1 t2 -> NotIntersected (branch t1 t2).

Lemma Intersected_dec : forall t : Tree CT, {Intersected t} + {~ Intersected t}.
  intros.
  induction t.
    left. apply ileaf.
    left. apply inode.
    destruct IHt1.
      destruct IHt2.
        destruct (Idsj_dec t1 t2).
          right. unfold not. intros. inversion H. contradiction.
          left. apply ibranch; assumption.
        right. unfold not. intros. inversion H; contradiction.
      right. unfold not. intros. inversion H; contradiction.
Qed.

Lemma NotIntersected_dec : forall t : Tree CT, {NotIntersected t} + {~ NotIntersected t}.
  intros.
  induction t.
    right. unfold not. intros H. inversion H.
    right. unfold not. intros H. inversion H.
    destruct IHt1.
      left. apply ni_left. assumption.
      destruct IHt2.
        left. apply ni_right. assumption.
        destruct (Idsj_dec t1 t2).
          left. apply ni_branch. assumption.
          right. unfold not. intros. inversion H; contradiction.
Qed.

Lemma Intersected_NotIntersected : forall t : Tree CT, Intersected t <-> ~ NotIntersected t.
  unfold not. intros. split; intros.
    induction H.
      inversion H0.
      inversion H0.
      inversion H0; subst; try contradiction.
    induction t.
      apply ileaf.
      apply inode.
      destruct (NotIntersected_dec t1).
        assert False. apply H. apply ni_left. assumption. contradiction.
        destruct (NotIntersected_dec t2).
          assert False. apply H. apply ni_right. assumption. contradiction.
          destruct (Idsj_dec t1 t2).
            assert False. apply H. apply ni_branch. assumption. contradiction.
            apply IHt1 in n. apply IHt2 in n0. apply ibranch; assumption.
Qed.

Lemma NotIntersected_Intersected : forall t : Tree CT, NotIntersected t <-> ~ Intersected t.
  unfold not. intros. split; intros.
  induction H; inversion H0; contradiction.
  induction t.
    pose proof ileaf. apply H in H0. contradiction.
    pose proof inode. apply H in H0. contradiction.
    destruct (Intersected_dec t1).
      destruct (Intersected_dec t2).
        destruct (Idsj_dec t1 t2).
          apply ni_branch. assumption.
          assert False. apply H. apply ibranch; assumption. contradiction.
        apply IHt2 in n. apply ni_right. assumption.
      apply IHt1 in n. apply ni_left. assumption.
Qed.

Definition intersect (t : Tree CT) : SoP :=
  match (Intersected_dec t) with
  | Specif.left _ => node t
  | Specif.right _ => leaf
  end.

Import Decidable.

Lemma project : forall p : Tree CT, Sub Decidable (intersect p) (node p).
  intros.
  unfold intersect.
  destruct (Intersected_dec p).
    apply sub_refl. unfold Decidable. apply drefl_R. unfold AdmitsD. apply Proof.proof_admits.
    unfold Sub. apply tforall_leaf.
Qed.

Lemma intersected : forall p : Tree CT, TForall Intersected (intersect p).
  intros.
  unfold intersect.
  destruct (Intersected_dec p).
    apply tforall_node. assumption.
    apply tforall_leaf.
Qed.

Lemma intersectedl : forall l r : Tree CT, Intersected (branch l r) -> Intersected l.
  intros.
  inversion H. assumption.
Qed.

Lemma intersectedr : forall l r : Tree CT, Intersected (branch l r) -> Intersected r.
  intros.
  inversion H. assumption.
Qed.

Lemma dsj_exists : forall t1 t2 : Tree CT, Idsj t1 t2 -> TExists (fun (ct1 : CT) => TExists (fun (ct2 : CT) => CTdsj ct1 ct2) t2) t1.
  intros.
  induction H.
    apply texists_node.
    induction H.
      apply texists_node. apply CTdsj_symm. assumption.
      apply texists_left. assumption.
      apply texists_right. assumption.
    apply texists_left. assumption.
    apply texists_right. assumption.
Qed.

Lemma ICTdsj_exists : forall (t : Tree CT) (ct : CT), ICTdsj t ct <-> TExists (fun (ct' : CT) => CTdsj ct' ct) t.
  intros. split; intros.
    induction H; subst.
      apply texists_node. assumption.
      apply texists_left. assumption.
      apply texists_right. assumption.
    induction H.
      apply ict_dsj_node. assumption.
      apply ict_dsj_left. assumption.
      apply ict_dsj_right. assumption.
Qed.

Lemma intersection_dsj_CT : forall (R : T -> T -> Prop) (ct1 ct2 : CT) (t : Tree CT), CTdsj ct1 ct2 -> TExists (fun l : CT => CTInversion R l ct1) t -> ICTdsj t ct2.
  intros R ct1 ct2 t Hdsj Hexists.
  inversion Hdsj. subst.
  induction Hexists.
    apply ict_dsj_node. inversion H0. subst. apply ct_dsj. apply Disjointness_trans with c1 c't; assumption.
    apply ict_dsj_left. assumption.
    apply ict_dsj_right. assumption.
Qed.

Lemma dsj_CTinversion_dsj : forall (R : T -> T -> Prop) (ct1 ct2 ct3 : CT), CTdsj ct1 ct2 -> CTInversion R ct3 ct1 -> CTdsj ct2 ct3.
  intros.
  inversion H0; subst; inversion H; subst.
    apply ct_dsj. apply Disjointness_symm. apply Disjointness_trans with c' c't; assumption.
Qed.

Lemma Idsj_exists_ICTdsj : forall (R : T -> T -> Prop) (ct : CT) (t1 t2 : Tree CT), ICTdsj t2 ct -> TExists (fun l : CT => CTInversion R l ct) t1 -> Idsj t1 t2.
  intros.
  induction H0.
    apply i_dsj_node. apply ICTdsj_exists. apply ICTdsj_exists in H. apply texists_mono with (fun ct' : CT => CTdsj ct' ct). intros. apply dsj_CTinversion_dsj with R ct. apply CTdsj_symm. assumption. assumption. assumption.
    apply i_dsj_left. assumption.
    apply i_dsj_right. assumption.
Qed.

Lemma Idsj_refl_NotIntersected : forall t : Tree CT, Idsj t t -> NotIntersected t.
  intros.
  induction t; inversion H; subst.
    inversion H1. inversion H2. apply Disjointness_antirefl in H6. contradiction.
    apply Idsj_symm in H3. inversion H3.
      apply IHt1 in H4. apply ni_left. assumption.
      apply ni_branch. apply Idsj_symm. assumption.
    apply Idsj_symm in H3. inversion H3.
      apply ni_branch. assumption.
      apply IHt2 in H4. apply ni_right. assumption.
Qed.

Lemma intersect_Idsj_sub : forall (R : T -> T -> Prop), AdmitsD R -> forall (p t1 t2 : Tree CT), SubProd (CTInversion R) p (branch t1 t2) -> Idsj t1 t2 -> NotIntersected p.
  intros R admits p t1 t2 sub disjoint.
  inversion sub as [| | x1 x2 subl subr]. subst. clear sub.
  induction disjoint. apply node_tforall in subl. pose proof (Idsj_exists_ICTdsj R ct p t H subl). clear H. clear subl. apply Idsj_symm in H0.
    induction H0.
      apply node_tforall in subr. pose proof (Idsj_exists_ICTdsj R ct0 t t H subr). apply Idsj_refl_NotIntersected. assumption.
      inversion subr. apply IHIdsj in H2. assumption.
      inversion subr. apply IHIdsj in H3. assumption.
    inversion subl. apply IHdisjoint in H1. assumption.
      assumption.
    inversion subl. apply IHdisjoint in H2. assumption.
      assumption.
Qed.

Lemma intersect_swaps : forall (p : Tree CT) (pos : Position), tswaps (generic (intersect p)) pos <= tswaps (generic (node p)) pos.
  intros.
  unfold intersect.
  destruct (Intersected_dec p).
    auto. simpl. unfold tswaps at 1. rewrite (tinvariant_eq _ bottom). simpl. apply le_0_n.
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.
  unfold intersect.
  destruct (Intersected_dec p').
    unfold Sub. apply tforall_node. apply texists_node. apply H1.
    rewrite <- NotIntersected_Intersected in n.
    induction n.
      apply IHn. inversion H1. apply H4.
      apply IHn. inversion H1. apply H5.
      apply H in H1. pose proof (intersect_Idsj_sub R X p t1 t2 H1 H2). rewrite -> NotIntersected_Intersected in H3. contradiction.
Qed.

End DsjIntersect.

Module DsjIntersectComposable (D : Disjointness).

  Module DsjIntersect := (DsjIntersect D).

  Module Type DsjComposable (I : Intersector) <: (Composable I DsjIntersect).

    Lemma composable_intersect : forall t : Tree CT, I.Intersected t -> TForall I.Intersected (DsjIntersect.intersect t).
      intros.
      unfold DsjIntersect.intersect.
      destruct (DsjIntersect.Intersected_dec t).
        apply tforall_node. assumption.
        apply tforall_leaf.
    Qed.

  End DsjComposable.
End DsjIntersectComposable.


This page has been generated by coqdoc