Composability (Section5.v)
Some Intersectors can be easily composed. The criterion for this composability is IntersectedPreservation, i.e. that, given two Intersectors, the second Intersector's intersect function does not invalidate the intersectedness predicate of the first Intersector. The module type Composability lets a user provide a proof of that for a given pair of Intersectors.
Require Import List.
Require Import Nat.
Require Import Util.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Require Import Section4_Proofs.
Import Relation_Operators.
Import List.
Import ListNotations.
Module Type Composability (M_traditional : Traditional) (M_intersector_l M_intersector_r : Intersector M_traditional).
Import M_traditional.
Parameter IntersectedPreservation : forall ls : list Lit, M_intersector_l.intersected ls -> Integrated M_intersector_l.intersected (M_intersector_r.intersect ls).
End Composability.
Require Import Nat.
Require Import Util.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Require Import Section4_Proofs.
Import Relation_Operators.
Import List.
Import ListNotations.
Module Type Composability (M_traditional : Traditional) (M_intersector_l M_intersector_r : Intersector M_traditional).
Import M_traditional.
Parameter IntersectedPreservation : forall ls : list Lit, M_intersector_l.intersected ls -> Integrated M_intersector_l.intersected (M_intersector_r.intersect ls).
End Composability.
Composition
Given two Intersectors Il and Ir and a proof of IntersectedPreservation (i.e. Composability) between the two, this module proves all the necessary Requirements for a new Intersector module where intersect is defined as Integrate Ir.intersect (Il.intersect ls) and extension tl tr is defined as Il.extension tl tr \/ Ir.extension tl tr. Requirements 1 - 6 are already proven by Traditional and do not change when Intersectors are composed. Requirements 7 - 12 are proved here for the new definitions of intersect, intersected and extension. This satisfies the "Intersector Composability" Theorem in the paper.Module Composition (M_traditional : Traditional) (M_intersector_l M_intersector_r : Intersector M_traditional) (M_composability : Composability M_traditional M_intersector_l M_intersector_r) <: Intersector M_traditional.
Import M_traditional.
Import M_composability.
Module M_traditional_dec := TraditionalDec M_traditional.
Import M_traditional_dec.
Module Intl := Integrated M_traditional M_intersector_l.
Module Intr := Integrated M_traditional M_intersector_r.
Import Intl.
Import Intr.
Module Il := M_intersector_l.
Module Ir := M_intersector_r.
Import Ir.
Import Il.
Import Intl.M_sopinfrastructure.
Import M_traditional_dec.M_Infrastructure.
Definitions of ⊓, φ, and extension
Straightfoward composition of their respective counterparts in the two given Intersector modules, as described in the paper.Definition intersect (ls : list Lit) := Integrate Ir.intersect (Il.intersect ls).
Definition intersected (ls : list Lit) := Il.intersected ls /\ Ir.intersected ls.
Definition extension (tl tr : T) : Prop := Il.extension tl tr \/ Ir.extension tl tr.
Lemma IntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (Integrate intersect tl) tr.
intros tl tr Hext. unfold dsubf. destruct Hext as [Hext | Hext].
apply dsuba_trans with ((Integrate Il.intersect tl)); [|apply Il.IntersectorCompleteness; assumption]. unfold intersect. rewrite -> Integrate_stacked. apply rsub_dsub. apply Intr.Dereliction. apply rsub_refl.
apply dsuba_trans with ((Integrate Ir.intersect tl)); [|apply Ir.IntersectorCompleteness; assumption]. unfold intersect. rewrite -> Integrate_stacked. apply rsub_dsub. apply Intr.Promotion; [apply Intr.IntegratorIntegrated|]. apply Intr.Dereliction. apply Intl.Dereliction. apply rsub_refl.
Qed.
Lemma rsubfi_refl : forall t : T, rsubf (@IPremise) t t.
intros t; constructor; induction t; try (constructor; assumption).
apply ui_uni_l; constructor; assumption.
apply ui_int_r; constructor; assumption.
constructor. pose proof (LiteralReflexivity l) as [r Hr]. apply Lsub with r. intros tl tr Hprem. inversion Hprem; subst. apply Hr in H. subst. apply IntegratedReflexivity.
Qed.
Lemma IntersectorSoundness : forall ls : list Lit, dsubda (@DPremise) extension (Intersect ls) (intersect ls).
intros ls. unfold intersect. apply dsubda_trans with (Il.intersect ls).
unfold extension. apply (@dsubda_mono) with (A := Il.extension); [auto|apply Il.IntersectorSoundness].
unfold extension. apply (@dsubda_mono) with (A := Ir.extension); [auto|]. apply Intr.IntegratedSoundness. apply rsubfi_refl.
Qed.
Lemma MeasurePreservation : forall tl tr : T, clos_refl_trans M mlt (m (Integrate intersect tl) tr) (m tl tr).
intros tl tr. apply rt_trans with (m (Integrate Il.intersect tl) tr); [|apply Il.MeasurePreservation]. unfold intersect. rewrite -> Integrate_stacked. apply Ir.MeasurePreservation.
Qed.
Lemma LiteralDereliction : forall ls : list Lit, rsub (intersect ls) (Intersect ls).
intros ls. apply rsub_trans with (Il.intersect ls); [|apply Il.LiteralDereliction]. unfold intersect. apply Dereliction. apply rsub_refl.
Qed.
Lemma IntersectorIntegrated : forall ls : list Lit, Integrated intersected (intersect ls).
unfold intersect. intros ls. unfold intersected. apply Integrated_and; split.
pose proof (Il.IntersectorIntegrated ls) as Hii; pose proof (Integrated_SumOfProducts _ _ Hii) as Hsop; remember (Il.intersect ls) as tl; clear Heqtl; induction Hsop; simpl; [apply I | simpl in Hii; split; [apply IHHsop1 | apply IHHsop2]; (apply Hintr || apply Hii) |]; pose proof (Integrate_ProductOfLiterals Ir.intersect _ H) as Hpolint; rewrite -> Hpolint; assert (Hint : Il.intersected (Tlits t H)); [clear Hpolint; generalize H; intros H'; remember (Il.intersected) as P; clear HeqP; apply (ProductOfLiterals_Integrated_int _ H) in Hii; generalize dependent P; induction H; intros P Hii; try apply Hii; simpl in *; apply IHProductOfLiterals1 with (H' := H) in Hii; apply IHProductOfLiterals2 with (H' := H0) in Hii; rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_l H') H); rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_r H') H0); assumption | apply IntersectedPreservation; assumption].
apply (Intr.IntegratorIntegrated (Il.intersect ls)).
Qed.
Lemma LiteralPromotion : forall (ls ls' : list Lit) (rs : list (sig2T RRule)), Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' -> incl (map proj2T1 rs) ls -> intersected ls -> exists rs' : list (sig2T RRule), Exists_Intersection (fun ls'' => ls'' = map proj2T2 rs' /\ incl (map proj2T1 rs') ls /\ Forall (fun r' : sig2T RRule => forall tl tr :T, RPremise (proj2V r') tl tr -> rsubam (@RPremise) (fun tl' tr' => Exists (fun r => RPremise (proj2V r) tl' tr') rs) tl tr) rs') (intersect ls').
intros ls ls' rs Hmatch Hincl Hint. unfold intersected in Hint. destruct Hint as [Hintl Hintr]. pose proof (Il.LiteralPromotion ls ls' rs Hmatch Hincl Hintl) as [rsl Hsubl]. unfold intersect. pose proof (Integrated_SumOfProducts Il.intersected _ (Il.IntersectorIntegrated ls')) as Hsopl. remember (Il.intersect ls') as til. clear Heqtil. induction Hsopl.
inversion Hsubl.
inversion Hsubl; [apply IHHsopl1 in H | apply IHHsopl2 in H]; clear IHHsopl1 IHHsopl2; destruct H as [rsx Hex]; exists rsx; simpl; [left | right]; assumption.
destruct H.
simpl in *. pose proof (Ir.LiteralPromotion ls [] rsl) as [rsr Hsubr]; [constructor| apply Hsubl |assumption|]. exists rsr. pose proof (Integrated_SumOfProducts Ir.intersected _ (Ir.IntersectorIntegrated [])) as Hsopr. induction Hsopr.
inversion Hsubr.
destruct Hsubr as [Hsubr | Hsubr]; [apply IHHsopr1 in Hsubr | apply IHHsopr2 in Hsubr]; simpl; [left | right]; assumption.
destruct H; simpl in *; try (destruct Hsubr as [Heq' [Hincl' Hfa']]; split; [assumption| split; [assumption|mono]]).
intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H. destruct H as [rx [HInrx Hpremx]]. destruct Hsubl as [Heq [Hinclls Hfa]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl tr Hpremx).
apply (ram_mono tl tl' tr' tr); assumption.
apply ram_lit with r0; assumption.
intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H. destruct H as [rx [HInrx Hpremx]]. destruct Hsubl as [Heq [Hinclls Hfa]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl tr Hpremx).
apply (ram_mono tl tl' tr' tr); assumption.
apply ram_lit with r0; assumption.
revert Hsubr. destruct Hsubl as [Heq [Hincll Hfa]]. apply Integrated_int_mono. intros lsx. apply Integrated_int_mono. intros lsx' [Heq' [Hincl' Hfa']]. split; [assumption| split; [assumption|]]. mono. intros rx HInrx Hfarx tlx trx Hprem. apply Hfarx in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H1. destruct H1 as [rx' [HInrx' Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx' HInrx' tl0 tr0 Hpremx).
apply (ram_mono tl0 tl' tr' tr0); assumption.
apply ram_lit with r; assumption.
simpl in *. destruct Hsubl as [Heq [Hincll Hfa]]. pose proof (Ir.LiteralPromotion ls [l] rsl) as [rsr Hsubr]; [constructor; [|constructor] | assumption |assumption|].
destruct rsl as [|r rsl]; [inversion Heq|]. simpl in Heq. inversion Heq; subst. apply Exists_cons_hd. reflexivity.
exists rsr. pose proof (Integrated_SumOfProducts Ir.intersected _ (Ir.IntersectorIntegrated [l])) as Hsopr. induction Hsopr.
inversion Hsubr.
destruct Hsubr as [Hsubr | Hsubr]; [apply IHHsopr1 in Hsubr | apply IHHsopr2 in Hsubr]; [left | right]; assumption.
destruct H; simpl in *; try (destruct Hsubr as [Heq' [Hincl' Hfa']]; split; [assumption| split; [assumption|mono]]).
intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H. destruct H as [rx [HInrx Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl tr Hpremx).
apply (ram_mono tl tl' tr' tr); assumption.
apply ram_lit with r0; assumption.
intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H. destruct H as [rx [HInrx Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl tr Hpremx).
apply (ram_mono tl tl' tr' tr); assumption.
apply ram_lit with r0; assumption.
revert Hsubr. apply Integrated_int_mono. intros lsx. apply Integrated_int_mono. intros lsx' [Heq' [Hincl' Hfa']]. split; [assumption| split; [assumption|]]. mono. intros rx HInrx Hfarx tlx trx Hprem. apply Hfarx in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H1. destruct H1 as [rx' [HInrx' Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx' HInrx' tl0 tr0 Hpremx).
apply (ram_mono tl0 tl' tr' tr0); assumption.
apply ram_lit with r; assumption.
apply Exists_Intersection_int_exists in Hsubl. destruct Hsubl as [Hpol [Heq [HIncl Hfa]]]. pose proof (Ir.LiteralPromotion ls (Tlits (TIsect tl tr) Hpol) rsl) as [rsr Hsubr]; [|assumption|assumption|].
rewrite -> Heq. apply Forall_forall. intros l HIn. apply Exists_exists. apply in_map_iff in HIn. destruct HIn as [r [Heqr HIn]]. exists r. split; assumption.
rewrite -> Integrate_ProductOfLiterals with (Hpol := Hpol). rewrite -> Heq in *. pose proof (Integrated_SumOfProducts Ir.intersected _ (Ir.IntersectorIntegrated (map proj2T2 rsl))) as Hsopr. remember (Ir.intersect (map proj2T2 rsl)) as tir. clear Heqtir. induction Hsopr.
inversion Hsubr.
inversion Hsubr; [apply IHHsopr1 in H1 | apply IHHsopr2 in H1]; clear IHHsopr1 IHHsopr2; destruct H1 as [rsx Hex]; exists rsx; simpl; [left | right]; assumption.
destruct H1.
simpl in *. exists rsr; split; [apply Hsubr | split; [apply Hsubr|]]. destruct Hsubr as [Heq' [Hincl' Hfa']]. mono. intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H1. destruct H1 as [rx [HInrx Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl0 tr0 Hpremx).
apply (ram_mono tl0 tl' tr' tr0); assumption.
apply ram_lit with r0; assumption.
simpl in *. exists rsr; split; [apply Hsubr | split; [apply Hsubr|]]. destruct Hsubr as [Heq' [Hincl' Hfa']]. mono. intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H1. destruct H1 as [rx [HInrx Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl0 tr0 Hpremx).
apply (ram_mono tl0 tl' tr' tr0); assumption.
apply ram_lit with r0; assumption.
apply Exists_Intersection_int_exists in Hsubr. destruct Hsubr as [Hpol' [Heq' [Hincl' Hfa']]]. exists (rsr). apply Exists_Intersection_int_exists. exists Hpol'. split; [assumption | split; [assumption|]]. mono. intros r HInr Hfar tlx trx Hprem. apply Hfar in Hprem. induction Hprem; try (constructor; assumption).
apply Exists_exists in H1. destruct H1 as [rx [HInrx Hpremx]]. rewrite -> Forall_forall in Hfa. apply (Hfa rx HInrx tl1 tr1 Hpremx).
apply (ram_mono tl1 tl' tr' tr1); assumption.
apply ram_lit with r0; assumption.
Qed.
End Composition.
This page has been generated by coqdoc