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.
Import Relation_Operators.
Import List.
Import ListNotations.
Module SOP_Infrastructure (M_Traditional : Traditional).
Import M_Traditional.
Module M_TraditionalDec := TraditionalDec(M_Traditional).
Import M_TraditionalDec.
Module M_Infrastructure := M_TraditionalDec.M_Infrastructure.
Import M_Infrastructure.
Notation sop := (list (list Lit)).
Lemma integrate_intersect (intersect : list Lit -> list (list Lit)) (i : list Lit) : SopIntegrate intersect (Intersect i) = intersect i.
revert intersect. induction i; simpl; intro intersect.
reflexivity.
apply IHi.
Qed.
Lemma rsub_rsubam (R : T -> T -> Prop) : forall tl tr : T, rsub tl tr -> rsubam (@RPremise) R tl tr.
apply (uirec_alt (fun ll lr => lsub (@RPremise) rsub ll lr -> lsub (@RPremise) (rsubam (@RPremise) R) ll lr) (fun tl tr => rsub tl tr -> rsubam (@RPremise) R tl tr)).
intros ll lr IH Hsub. inversion Hsub. apply Lsub with r. intros tl tr Hprem. apply IH with r; [|apply H]; assumption.
intros tl tr Huir Hsub. apply rsubf_uisub in Hsub. induction Hsub; try (constructor; assumption).
apply ForallCrossPairs_singleton_forward in Huir; apply Huir in H; inversion H; subst. apply ram_lit with r. assumption.
apply ram_int_ll. apply IHHsub. apply uirec_int_l in Huir. apply Huir.
apply ram_int_lr. apply IHHsub. apply uirec_int_l in Huir. apply Huir.
apply ram_int_r; [apply IHHsub1 | apply IHHsub2]; apply uirec_int_r in Huir; apply Huir.
apply ram_uni_rl; apply IHHsub; apply uirec_uni_r in Huir; apply Huir.
apply ram_uni_rr; apply IHHsub; apply uirec_uni_r in Huir; apply Huir.
apply ram_uni_l; [apply IHHsub1 | apply IHHsub2]; apply uirec_uni_l in Huir; apply Huir.
Qed.
Require Import Nat.
Require Import Util.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Import Relation_Operators.
Import List.
Import ListNotations.
Module SOP_Infrastructure (M_Traditional : Traditional).
Import M_Traditional.
Module M_TraditionalDec := TraditionalDec(M_Traditional).
Import M_TraditionalDec.
Module M_Infrastructure := M_TraditionalDec.M_Infrastructure.
Import M_Infrastructure.
Notation sop := (list (list Lit)).
Lemma integrate_intersect (intersect : list Lit -> list (list Lit)) (i : list Lit) : SopIntegrate intersect (Intersect i) = intersect i.
revert intersect. induction i; simpl; intro intersect.
reflexivity.
apply IHi.
Qed.
Lemma rsub_rsubam (R : T -> T -> Prop) : forall tl tr : T, rsub tl tr -> rsubam (@RPremise) R tl tr.
apply (uirec_alt (fun ll lr => lsub (@RPremise) rsub ll lr -> lsub (@RPremise) (rsubam (@RPremise) R) ll lr) (fun tl tr => rsub tl tr -> rsubam (@RPremise) R tl tr)).
intros ll lr IH Hsub. inversion Hsub. apply Lsub with r. intros tl tr Hprem. apply IH with r; [|apply H]; assumption.
intros tl tr Huir Hsub. apply rsubf_uisub in Hsub. induction Hsub; try (constructor; assumption).
apply ForallCrossPairs_singleton_forward in Huir; apply Huir in H; inversion H; subst. apply ram_lit with r. assumption.
apply ram_int_ll. apply IHHsub. apply uirec_int_l in Huir. apply Huir.
apply ram_int_lr. apply IHHsub. apply uirec_int_l in Huir. apply Huir.
apply ram_int_r; [apply IHHsub1 | apply IHHsub2]; apply uirec_int_r in Huir; apply Huir.
apply ram_uni_rl; apply IHHsub; apply uirec_uni_r in Huir; apply Huir.
apply ram_uni_rr; apply IHHsub; apply uirec_uni_r in Huir; apply Huir.
apply ram_uni_l; [apply IHHsub1 | apply IHHsub2]; apply uirec_uni_l in Huir; apply Huir.
Qed.
One of the biggest workhorse Lemmas in the following proofs is SopIntegrated_flat_map.
All it says is that with sops we can split the functionality of the Integrator DNFc into first getting the type into DNF/an sop representation and then just flat_map what was previously the continuation c onto the resulting sop.
This comes in useful in untangling induction cases where SopIntegrate is applied to an intersection of two types.
Lemma SopIntegrate_flat_map : forall (t : T) (f : (list Lit) -> list (list Lit)), SopIntegrate f t = flat_map f (SopIntegrate (fun ls => [ls]) t).
induction t; intros f; try reflexivity.
simpl. rewrite -> app_nil_r. reflexivity.
simpl. simpl. rewrite -> flat_map_app. rewrite -> IHt1. rewrite -> IHt2. reflexivity.
simpl. simpl. rewrite -> IHt1. symmetry. rewrite -> IHt1. symmetry. rewrite -> flat_map_flat_map. apply flat_map_mono. intros ls. rewrite -> IHt2. symmetry. rewrite -> IHt2. symmetry. rewrite -> flat_map_flat_map. simpl. apply flat_map_mono. intros ls'. rewrite -> app_nil_r. reflexivity.
simpl. rewrite -> app_nil_r. reflexivity.
Qed.
Lemma SopIntegrated_flat_map (P : list Lit -> Prop) (f : list Lit -> sop) : forall s : sop, SopIntegrated (fun ls => SopIntegrated P (f ls)) s -> SopIntegrated P (flat_map f s).
intros s Hint. induction Hint.
simpl. constructor.
simpl. apply Forall_app; split; [|assumption]. apply H.
Qed.
Lemma InType_lit_In : forall (l : Lit) (t : T), (exists ls : list Lit, In ls (SopIntegrate (fun ls => [ls]) t) /\ In l ls) -> InType (TLit l) t.
intros l t [ls [HInls HInl]]. generalize dependent l. generalize dependent ls. induction t; intros ls HInls l' HInl.
simpl in HInls; inversion HInls; subst; contradiction.
simpl in HInls; inversion HInls; subst; contradiction.
simpl in HInls. apply in_app_iff in HInls. destruct HInls as [HInls | HInls]; [pose proof (IHt1 _ HInls _ HInl) | pose proof (IHt2 _ HInls _ HInl)]; apply InType_TUni; auto.
simpl in HInls. rewrite -> SopIntegrate_flat_map in HInls. apply in_flat_map in HInls. destruct HInls as [ls1 [HInls1 HInls]]. rewrite -> SopIntegrate_flat_map in HInls. apply in_flat_map in HInls. destruct HInls as [ls2 [HInls2 HInls]]. apply In_singleton in HInls. subst. apply in_app_iff in HInl. destruct HInl as [H | H]; [pose proof (IHt1 _ HInls1 _ H) | pose proof (IHt2 _ HInls2 _ H)]; apply InType_TIsect; auto.
simpl in HInls. inversion HInls; subst; [|contradiction]. apply In_singleton in HInl. subst. apply it_eq.
Qed.
Lemma InType_TBot : forall t : T, InType t TBot -> t = TBot.
intros t HIn. remember TBot as tbot. induction HIn; subst; repeat remove_eq_implications.
reflexivity.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
Qed.
Lemma InType_TTop : forall t : T, InType t TTop -> t = TTop.
intros t HIn. remember TTop as ttop. induction HIn; subst; repeat remove_eq_implications.
reflexivity.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
Qed.
Lemma InType_TLit : forall (t : T) (l: Lit), InType t (TLit l) -> t = (TLit l).
intros t l HIn. remember (TLit l) as tlit. induction HIn; subst; repeat remove_eq_implications.
reflexivity.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
inversion IHHIn0.
Qed.
Lemma ui2sop_sop2ui (s : sop) : ui2sop (sop2ui s) = s.
unfold ui2sop. induction s; simpl.
reflexivity.
rewrite integrate_intersect. simpl. f_equal. assumption.
Qed.
Definition meet (sl sr : sop) : sop := flat_map (fun ls => map (fun ls' => ls ++ ls') sr) sl.
Fixpoint ui2sop_meet (t : T) : sop :=
match t with
| TTop => [[]]
| TBot => []
| TUni tl tr => (ui2sop_meet tl) ++ (ui2sop_meet tr)
| TIsect tl tr => meet (ui2sop_meet tl) (ui2sop_meet tr)
| TLit l => [[l]]
end.
Lemma ui2sop_meet_ui2sop : forall t : T, ui2sop t = ui2sop_meet t.
intros t. induction t; try reflexivity.
simpl. rewrite <- IHt1. rewrite <- IHt2. unfold ui2sop. simpl. reflexivity.
simpl. rewrite <- IHt1. rewrite <- IHt2. unfold ui2sop. simpl. rewrite -> SopIntegrate_flat_map. unfold meet. apply flat_map_mono. intros ls HInls. rewrite -> SopIntegrate_flat_map. reflexivity.
Qed.
Lemma meet_empty_r : forall sl : sop, meet sl [] = [].
induction sl; [|simpl; rewrite -> IHsl]; reflexivity.
Qed.
Lemma rsub_sop2ui_app_l : forall (sl sr : sop) (t : T), rsub (sop2ui sl) t -> rsub (sop2ui sr) t -> rsub (sop2ui (sl ++ sr)) t.
intros sl sr t Hl Hr. induction sl; [assumption|]. simpl. constructor. simpl in Hl. apply rsubf_uisub in Hl. apply uisub_uni_l in Hl. destruct Hl as [Hll Hlr]. apply Rsubf in Hll. apply Rsubf in Hlr. apply ui_uni_l; apply rsubf_uisub; [|apply IHsl]; assumption.
Qed.
Lemma Integrated_int_P : forall (P : list Lit -> Prop) (t : T), Integrated_int P t -> exists l : list Lit, P l.
intros P t. generalize dependent P. induction t; intros P Hdnfp; simpl in Hdnfp; try contradiction.
exists []. assumption.
apply IHt1 in Hdnfp. destruct Hdnfp as [l Ht2]. apply IHt2 in Ht2. destruct Ht2 as [l' Hp]. exists (l ++ l'). assumption.
exists [l]. assumption.
Qed.
Lemma Integrated_int_ProductOfLiterals : forall (P : list Lit -> Prop) (t : T), Integrated_int P t -> ProductOfLiterals t.
intros P t. generalize dependent P. induction t; intros P Hdnfp; try (constructor; fail); try (inversion Hdnfp; fail).
simpl in Hdnfp. pose proof (IHt1 _ Hdnfp). apply POL_int; [assumption|]. apply Integrated_int_P in Hdnfp. destruct Hdnfp as [l Ht2]. apply IHt2 in Ht2. assumption.
Qed.
Lemma Integrated_SumOfProducts : forall (P : list Lit -> Prop) (t : T), Integrated P t -> SumOfProducts t.
intros P t. generalize dependent P. induction t; intros P Hdnfp; try (constructor; constructor; fail).
simpl in Hdnfp. apply SOP_uni; [apply (IHt1 P) |apply (IHt2 P)]; apply Hdnfp.
simpl in Hdnfp. apply SOP_prod. apply POL_int.
apply Integrated_int_ProductOfLiterals in Hdnfp. assumption.
apply Integrated_int_P in Hdnfp. destruct Hdnfp as [l Ht2]. apply Integrated_int_ProductOfLiterals in Ht2. assumption.
Qed.
Lemma ProductOfLiterals_bot : @ProductOfLiterals Lit TBot -> False. intros H. inversion H. Qed.
Lemma ProductOfLiterals_uni : forall tl tr : T, ProductOfLiterals (TUni tl tr) -> False. intros tl tr H. inversion H. Qed.
Lemma ProductOfLiterals_int_l : forall {tl tr : T}, ProductOfLiterals (TIsect tl tr) -> ProductOfLiterals tl. intros tl tr H. inversion H. assumption. Qed.
Lemma ProductOfLiterals_int_r : forall {tl tr : T}, ProductOfLiterals (TIsect tl tr) -> ProductOfLiterals tr. intros tl tr H. inversion H. assumption. Qed.
Lemma SumOfProducts_uni_l : forall {tl tr : T}, SumOfProducts (TUni tl tr) -> SumOfProducts tl. intros tl tr H. inversion H. assumption. inversion H0. Qed.
Lemma SumOfProducts_uni_r : forall {tl tr : T}, SumOfProducts (TUni tl tr) -> SumOfProducts tr. intros tl tr H. inversion H. assumption. inversion H0. Qed.
Lemma SumOfProducts_int : forall {tl tr : T}, SumOfProducts (TIsect tl tr) -> ProductOfLiterals (TIsect tl tr). intros tl tr H. inversion H. assumption. Qed.
Fixpoint Tlits (t : T) (POL : ProductOfLiterals t) : list Lit.
destruct t.
apply [].
apply ProductOfLiterals_bot in POL. contradiction.
apply ProductOfLiterals_uni in POL. contradiction.
pose proof (ProductOfLiterals_int_l POL) as Hl. pose proof (ProductOfLiterals_int_r POL) as Hr. apply ((Tlits t1 Hl) ++ (Tlits t2 Hr)).
apply [l].
Defined.
Lemma Tlits_ProductOfLiterals_irrel : forall {t : T} (Hpol Hpol' : ProductOfLiterals t), Tlits t Hpol = Tlits t Hpol'.
induction t; intros Hpol Hpol'; try reflexivity; simpl.
inversion Hpol.
inversion Hpol.
apply app_eq; [apply IHt1 | apply IHt2].
Qed.
Lemma Tlits_ui2sop : forall {t : T} (Hpol : ProductOfLiterals t), [Tlits t Hpol] = ui2sop t.
intros t. induction t; intros Hpol.
reflexivity.
inversion Hpol.
inversion Hpol.
simpl. unfold ui2sop. simpl. rewrite -> SopIntegrate_flat_map. fold (ui2sop t1). rewrite <- IHt1 with (ProductOfLiterals_int_l Hpol). simpl. rewrite -> app_nil_r. rewrite -> SopIntegrate_flat_map. fold (ui2sop t2). rewrite <- IHt2 with (ProductOfLiterals_int_r Hpol). simpl. reflexivity.
reflexivity.
Qed.
Lemma Integrated_int_P_insop : forall (P : list Lit -> Prop) (t : T), Integrated_int P t -> exists l : list Lit, In l (ui2sop t) /\ P l.
intros P t. generalize dependent P. induction t; intros P Hdnfp; try contradiction.
exists []. split; [apply in_eq| assumption].
rewrite <- (Tlits_ui2sop (Integrated_int_ProductOfLiterals _ _ Hdnfp)).
simpl in Hdnfp. generalize (Integrated_int_ProductOfLiterals P (TIsect t1 t2) Hdnfp). intros Hpos. pose proof (Tlits_ui2sop (Integrated_int_ProductOfLiterals _ _ Hdnfp)) as Ht1. remember (Integrated_int_ProductOfLiterals _ _ _) as Hpos1. clear HeqHpos1. apply IHt1 in Hdnfp. destruct Hdnfp as [l [Ht2In Hdnfp]]. pose proof (Tlits_ui2sop (Integrated_int_ProductOfLiterals _ _ Hdnfp)) as Ht2. remember (Integrated_int_ProductOfLiterals _ _ _) as Hpos2. clear HeqHpos2. apply IHt2 in Hdnfp. destruct Hdnfp as [l' [HIn Hp]]. exists (l ++ l'). split; [|assumption]. simpl. rewrite <- Ht1 in Ht2In. rewrite <- Ht2 in HIn. inversion Ht2In; subst; [|contradiction]. inversion HIn; subst; [|contradiction]. left. apply app_eq; apply Tlits_ProductOfLiterals_irrel.
exists [l]; split; [apply in_eq | assumption].
Qed.
Lemma Exists_Intersection_ProductOfLiterals : forall (P : list Lit -> Prop) (t : T), ProductOfLiterals t -> (Exists_Intersection P t <-> Integrated_int P t).
intros P t Hpol. split; intros H.
destruct Hpol; simpl in *; assumption.
destruct Hpol; simpl in *; assumption.
Qed.
Lemma Exists_Intersection_int_exists : forall (P : list Lit -> Prop) (tl tr : T), Exists_Intersection P (TIsect tl tr) <-> exists Hpol : ProductOfLiterals (TIsect tl tr), P (Tlits (TIsect tl tr) Hpol).
intros P tl tr; split; intros Hex.
unfold Exists_Intersection in Hex. pose proof (Integrated_int_ProductOfLiterals _ _ Hex) as Hpos. exists Hpos. revert Hex Hpos. generalize (TIsect tl tr) as t. induction t; intros Hint Hpos.
apply Hint.
inversion Hint.
inversion Hint.
pose proof (Integrated_int_P_insop _ _ Hint) as [ls [HIn HP]]. rewrite <- (Tlits_ui2sop Hpos) in HIn. inversion HIn; subst; [|contradiction]. assumption.
simpl in *. assumption.
destruct Hex as [Hpol Hp]. remember (TIsect tl tr) as t. clear tl tr Heqt. generalize dependent P. generalize Hpol. induction Hpol; intros Hpol' P Hp.
apply Hp.
apply Hp.
simpl. apply Exists_Intersection_ProductOfLiterals; [assumption|]. apply IHHpol1 with (Hpol := Hpol1). apply Exists_Intersection_ProductOfLiterals; [assumption|]. apply IHHpol2 with (Hpol := Hpol2). simpl in *. rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_l Hpol') Hpol1) in Hp. rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_r Hpol') Hpol2) in Hp. assumption.
Qed.
Lemma IntegrateIntegrated_P : forall (f : list Lit -> T) (P : list Lit -> Prop) (Hisectint : forall ls : list Lit, Integrated P (f ls)), forall t : T, Integrated P (Integrate f t).
intros f P Hisectint t. revert f P Hisectint. induction t; intros f P Hisectint.
simpl. apply Hisectint.
apply I.
simpl. split; [apply IHt1 | apply IHt2]; assumption.
simpl. apply IHt1. intros ls. apply IHt2. intros ls'. apply Hisectint.
simpl. apply Hisectint.
Qed.
Lemma ProductOfLiterals_ui2sop : forall {t : T}, ProductOfLiterals t -> { ls : list Lit | ui2sop t = [ls]}.
intros t Hpol. induction t.
exists []. reflexivity.
apply ProductOfLiterals_bot in Hpol. contradiction.
apply ProductOfLiterals_uni in Hpol. contradiction.
destruct (IHt1 (ProductOfLiterals_int_l Hpol)) as [lsl Heql]. destruct (IHt2 (ProductOfLiterals_int_r Hpol)) as [lsr Heqr]. exists (lsl ++ lsr). unfold ui2sop. simpl. clear IHt1 IHt2. rewrite -> SopIntegrate_flat_map. fold (ui2sop t1). rewrite -> Heql. simpl. rewrite -> SopIntegrate_flat_map. fold (ui2sop t2). rewrite -> Heqr. simpl. reflexivity.
exists [l]. reflexivity.
Qed.
Lemma ui2sop_sopof_ui : forall t : T, SumOfProducts t -> sopof (ui2sop t) t.
intros t Hsop. induction Hsop; try (unfold ui2sop; simpl; repeat constructor; assumption).
unfold ui2sop. induction H; try (repeat constructor; assumption).
simpl. rewrite -> SopIntegrate_flat_map. fold (ui2sop tl). destruct (ProductOfLiterals_ui2sop H) as [lsl Hlsl]. rewrite -> Hlsl. simpl. rewrite -> app_nil_r. rewrite -> SopIntegrate_flat_map. fold (ui2sop tr). destruct (ProductOfLiterals_ui2sop H0) as [lsr Hlsr]. rewrite -> Hlsr. simpl. fold (ui2sop tl) in IHProductOfLiterals1. rewrite -> Hlsl in IHProductOfLiterals1. fold (ui2sop tr) in IHProductOfLiterals2. rewrite -> Hlsr in IHProductOfLiterals2. inversion IHProductOfLiterals1; subst; inversion IHProductOfLiterals2; subst.
repeat constructor; assumption.
inversion H0.
inversion H.
inversion H0.
Qed.
Lemma rsubam_join (A : T -> T -> Prop) : forall tl tr : T, rsubam (@RPremise) (rsubam (@RPremise) A) tl tr -> rsubam (@RPremise) A tl tr.
intros tl tr Hsub. induction Hsub; try (constructor; assumption); try assumption.
apply ram_mono with tl' tr'; assumption.
apply ram_lit with r; assumption.
Qed.
Lemma rsubam_bind (A A' : T -> T -> Prop) : (forall tl tr : T, A tl tr -> rsubam (@RPremise) A' tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubam (@RPremise) A' tl tr.
intros Himpl tl tr Hsub. pose proof (rsubam_mono _ _ Himpl tl tr Hsub) as Hsub'. apply rsubam_join in Hsub'. assumption.
Qed.
Lemma rsubam_mono (A A' : T -> T -> Prop) : (forall tl tr : T, A tl tr -> A' tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubam (@RPremise) A' tl tr.
intros aa'. apply rsubam_bind. intros tl tr a. apply ram_assumption. apply aa'. assumption.
Qed.
Lemma ruisub_suisub {P : Lit -> Lit -> Prop} : forall (ls : list Lit) (t : T), ruisub (fun lr : Lit => Exists (fun ll => P ll lr) ls) t -> suisub P [ls] t.
intros ls t Hsub. constructor; [|constructor]. assumption.
Qed.
Lemma ruisub_mono (P P' : Lit -> Prop) : (forall l : Lit , P l -> P' l) -> forall t : T, ruisub P t -> ruisub P' t.
intros Himpl t Hrui. induction Hrui; try (constructor; assumption).
apply rui_lit. apply Himpl. assumption.
Qed.
Lemma suisub_meet_l (R : Lit -> Lit -> Prop) (sl sr : sop) (t : T) : suisub R sl t \/ suisub R sr t -> suisub R (meet sl sr) t.
intros [Hsub | Hsub]; (induction Hsub; [simpl; try rewrite -> meet_empty_r; constructor|]); simpl.
apply Forall_app; split; [|assumption]. clear IHHsub. induction sr; simpl; constructor; [|assumption]. clear Hsub IHsr. induction H; try (constructor; assumption). constructor. apply Exists_app_or. left. assumption.
clear IHHsub. induction sl; simpl; constructor.
clear Hsub IHsl. induction H; try (constructor; assumption). constructor. apply Exists_app_or; right; apply H.
apply Forall_app; split; [|assumption]. apply Forall_map. mono. intros ls HIn Hsub. clear HIn IHsl H. induction Hsub; try (constructor; assumption). constructor. apply Exists_app_or. right. assumption.
Qed.
Lemma uisub_suisub (R : Lit -> Lit -> Prop) (tl tr : T) : uisub R tl tr -> suisub R (ui2sop tl) tr.
intros Hsub. rewrite -> ui2sop_meet_ui2sop. induction Hsub; try (repeat constructor; assumption).
induction (ui2sop_meet tl); repeat constructor; assumption.
simpl. apply suisub_meet_l. left. assumption.
simpl. apply suisub_meet_l. right. assumption.
induction (ui2sop_meet tl); repeat constructor; inversion IHHsub1; inversion IHHsub2; subst; try (assumption || apply IHs; assumption). forall_and H. mono. intros l' HIn' [Hruil Hruir]. constructor; assumption.
induction (ui2sop_meet tl); repeat constructor; inversion IHHsub; subst; try (assumption || apply IHs; assumption). mono. intros l' HInl' Hrui. apply rui_uni_l; assumption.
induction (ui2sop_meet tl); try (repeat constructor; inversion IHHsub; subst; (assumption || apply IHs; assumption)). inversion IHHsub; subst. constructor; [constructor; assumption|]. mono. intros l' HInl' Hrui. apply rui_uni_r; assumption.
simpl. apply Forall_app; split; assumption.
Qed.
Lemma uisub_suisub' (R : Lit -> Lit -> Prop) (sl : sop) (tr : T) : uisub R (sop2ui sl) tr -> suisub R sl tr.
rewrite <- (ui2sop_sop2ui sl) at 2. apply uisub_suisub.
Qed.
Lemma suisub_uisub (R : Lit -> Lit -> Prop) (sl : sop) (tr : T) : suisub R sl tr -> uisub R (sop2ui sl) tr.
intros Hsub. unfold suisub in Hsub. induction Hsub; try (constructor; assumption).
simpl. apply ui_uni_l; [|assumption]. clear Hsub IHHsub. induction H; try (constructor; assumption).
apply Exists_exists in H. destruct H as [l' [HIn HR]]. apply in_split in HIn. destruct HIn as [l1 [l2 Heq]]. subst. induction l1.
simpl. apply ui_int_ll. constructor; assumption.
apply ui_int_lr. assumption.
Qed.
Lemma dsuba_dsubda (Assumed : T -> T -> Prop) : forall tl tr : T, dsuba (@DPremise) Assumed tl tr -> dsubda (@DPremise) Assumed tl tr.
intros tl tr Hsub. induction Hsub; try (constructor; assumption).
apply dsubda_trans with tm; assumption.
apply dsubda_lit with r; assumption.
Qed.
Lemma Integrated_int_Integrated {P : list Lit -> Prop} : forall t : T, Integrated_int P t -> Integrated P t.
intros t Hp. destruct t; (assumption || contradiction).
Qed.
Lemma SopIntegrated_mono (P P' : list Lit -> Prop) : (forall ls : list Lit, P ls -> P' ls) -> forall s : sop, SopIntegrated P s -> SopIntegrated P' s.
intros Himpl s Hint. induction s.
constructor.
constructor; [apply Himpl | apply IHs]; inversion Hint; assumption.
Qed.
Lemma ssub_mono (R R' : Lit -> Lit -> Prop) (sl sr : sop) : (forall ll lr : Lit, R ll lr -> R' ll lr) -> ssub R sl sr -> ssub R' sl sr.
intros Himpl Hsub. induction Hsub.
constructor.
constructor; [|assumption]. mono. intros ls HIn Hfa. mono. intros ll HInl Hex. mono. intros l' HInl'. apply Himpl.
Qed.
Lemma ssub_trans {Rl Rm Rr : Lit -> Lit -> Prop} {sl sm sr : sop} : (forall ll lr : Lit, (exists2 lm : Lit, Rl ll lm & Rr lm lr) -> Rm ll lr) -> ssub Rl sl sm -> ssub Rr sm sr -> ssub Rm sl sr.
intros rlrm slm smr. induction slm as [ | il sl ilm slm ]; constructor; try assumption. clear slm IHslm. induction ilm as [ im sm ilm | im sm ilm ]; inversion smr; clear smr; subst; try auto. clear H2. rename H1 into imr. induction imr as [ ir sr imr | ir sr imr ]; try auto. constructor. induction imr as [ | lr ir lmr imr ]; constructor; try assumption. clear imr IHimr. induction lmr as [ lm im lmr | lm im lmr ]; inversion ilm; clear ilm; subst; try auto. clear H2. rename H1 into lim. induction lim as [ ll il lim | ll il lim ]; try auto. constructor. apply rlrm. apply ex_intro2 with lm; assumption.
Qed.
Lemma ssub_suisub (R : Lit -> Lit -> Prop) (sl sr : sop) : ssub R sl sr -> suisub R sl (sop2ui sr).
intros Hsub. unfold ssub in Hsub. unfold suisub. mono. intros ls HInls Hex. apply Exists_exists in Hex. destruct Hex as [lsr [HInlsr Hfa]]. apply in_split in HInlsr. destruct HInlsr as [l1 [l2 Heq]]. subst. induction l1.
simpl. apply rui_uni_l. induction Hfa; simpl; repeat constructor; assumption.
simpl. apply rui_uni_r. assumption.
Qed.
Lemma suisub_ssub (R : Lit -> Lit -> Prop) (sl : sop) (tr : T) : suisub R sl tr -> ssub R sl (ui2sop tr).
intros Hsub. induction Hsub; constructor; try assumption.
clear Hsub IHHsub. induction H; try (repeat constructor; assumption).
rewrite -> ui2sop_meet_ui2sop. simpl. unfold meet. repeat rewrite <- ui2sop_meet_ui2sop. induction (ui2sop tl).
inversion IHruisub1. simpl. inversion IHruisub1; subst; apply Exists_app_or; [left; clear IHl0 IHruisub1 | right; apply IHl0; assumption]. induction (ui2sop tr); inversion IHruisub2; subst; [left; apply Forall_app; split; assumption | right ; apply IHl1; assumption].
unfold ui2sop. simpl. apply Exists_app_or. left. assumption.
unfold ui2sop. simpl. apply Exists_app_or. right. assumption.
Qed.
Lemma suisub_ssub' (R : Lit -> Lit -> Prop) (sl sr : sop) : suisub R sl (sop2ui sr) -> ssub R sl sr.
rewrite <- (ui2sop_sop2ui sr) at 2. apply suisub_ssub.
Qed.
Lemma ruirec_isect {P : Lit -> Prop} : forall tl tr : T, ruirec P (TIsect tl tr) -> ruirec P tl /\ ruirec P tr.
intros tl tr Hrui. unfold ruirec in Hrui. induction tl; simpl in *; try (split; [constructor | assumption]).
apply Forall_app in Hrui. destruct Hrui as [Hrui12 Hruir]. apply Forall_app in Hrui12. destruct Hrui12 as [Hrui1 Hrui2]. promotehyp IHtl1; [apply Forall_app; split; assumption|]. promotehyp IHtl2; [apply Forall_app; split; assumption|]. split; [unfold ruirec; simpl; apply Forall_app; split|] ; (apply IHtl1 || apply IHtl2).
apply Forall_app in Hrui. destruct Hrui as [Hrui12 Hruir]. apply Forall_app in Hrui12. destruct Hrui12 as [Hrui1 Hrui2]. promotehyp IHtl1; [apply Forall_app; split; assumption|]. promotehyp IHtl2; [apply Forall_app; split; assumption|]. split; [unfold ruirec; simpl; apply Forall_app; split|] ; (apply IHtl1 || apply IHtl2).
inversion Hrui; subst; split ; [constructor; [|constructor]|]; assumption.
Qed.
Lemma ruirec_uni {P : Lit -> Prop} : forall tl tr : T, ruirec P (TUni tl tr) -> ruirec P tl /\ ruirec P tr.
intros tl tr Hrui. unfold ruirec in Hrui. induction tl; simpl in *; try (split; [constructor | assumption]).
apply Forall_app in Hrui. destruct Hrui as [Hrui12 Hruir]. apply Forall_app in Hrui12. destruct Hrui12 as [Hrui1 Hrui2]. promotehyp IHtl1; [apply Forall_app; split; assumption|]. promotehyp IHtl2; [apply Forall_app; split; assumption|]. split; [unfold ruirec; simpl; apply Forall_app; split|] ; (apply IHtl1 || apply IHtl2).
apply Forall_app in Hrui. destruct Hrui as [Hrui12 Hruir]. apply Forall_app in Hrui12. destruct Hrui12 as [Hrui1 Hrui2]. promotehyp IHtl1; [apply Forall_app; split; assumption|]. promotehyp IHtl2; [apply Forall_app; split; assumption|]. split; [unfold ruirec; simpl; apply Forall_app; split|] ; (apply IHtl1 || apply IHtl2).
inversion Hrui; subst; split ; [constructor; [|constructor]|]; assumption.
Qed.
Lemma dsuba_uni_l_parts : forall (tl tr t : T), dsuba (@DPremise) (fun _ _ => False) (TUni tl tr) t -> dsuba (@DPremise) (fun _ _ => False) tl t /\ dsuba (@DPremise) (fun _ _ => False) tr t.
intros tl tr t Hsub. split; (apply dsuba_trans with (TUni tl tr); [|assumption]); [apply dsuba_uni_rl | apply dsuba_uni_rr].
Qed.
Lemma SopIntegrate_Integrate (f : list Lit -> T) (g : list Lit -> sop) (Hfg : forall ls : list Lit, (ui2sop (f ls)) = g ls) : forall t : T, SopIntegrate (fun ls => [ls]) (Integrate f t) = SopIntegrate (fun ls => (g ls)) t.
intros t. generalize dependent g. generalize dependent f. induction t; intros f g Hfg; simpl.
apply Hfg.
reflexivity.
rewrite -> (IHt1 f g Hfg). rewrite -> (IHt2 f g Hfg). reflexivity.
apply IHt1. intros ls. apply IHt2. intros ls'. apply Hfg.
apply Hfg.
Qed.
Lemma uisub_sop2ui_app {R : Lit -> Lit -> Prop} : forall (t : T) (sl sr : sop), uisub R t (sop2ui (sl ++ sr)) -> uisub R t (TUni (sop2ui sl) (sop2ui sr)).
intros t sl sr Hsub.
generalize dependent t. induction sl; intros t Hsub; simpl in *.
constructor; assumption.
remember (TUni (Intersect a) (sop2ui (sl ++ sr))) as tuni. induction Hsub; try (inversion Heqtuni; fail); try (repeat remove_eq_implications; constructor; assumption); clear IHHsub; inversion Heqtuni; subst; clear Heqtuni.
repeat constructor; assumption.
apply IHsl in Hsub. clear IHsl. remember (TUni (sop2ui sl) (sop2ui sr)) as tuni. induction Hsub; try (inversion Heqtuni; fail); try (repeat remove_eq_implications; constructor; assumption); clear IHHsub; inversion Heqtuni; subst; clear Heqtuni; repeat constructor; assumption.
Qed.
Lemma uisub_intersect {R : Lit -> Lit -> Prop} : forall (t : T) (ls : list Lit), uisub R t (Intersect ls) <-> Forall (fun l : Lit => uisub R t (TLit l)) ls.
intros t ls; split; intros H.
induction ls.
constructor.
constructor; simpl in H; apply uisub_int_r in H; [|apply IHls]; apply H.
induction H.
constructor; fail.
simpl. apply ui_int_r; assumption.
Qed.
Lemma ui2sop_sop2ui_sublists {R : Lit -> Lit -> Prop} : forall (t : T) (s : sop), uisub R t (sop2ui s) -> forall s' : sop, Forall (fun ls : list Lit => Exists (fun ls' : list Lit => incl ls' ls) s') s -> uisub R t (sop2ui s').
intros t s Hsub s' Hfa. generalize dependent t; induction Hfa; intros t Hsub.
simpl in Hsub. apply (uisub_bot _ _ Hsub).
simpl in Hsub. remember (TUni (Intersect x) (sop2ui l)) as tuni. induction Hsub; try (inversion Heqtuni; fail); try (repeat remove_eq_implications; constructor; assumption); clear IHHsub; inversion Heqtuni; subst; clear Heqtuni.
apply Exists_exists in H. destruct H as [ls [HIn Hincl]]. apply in_split in HIn. destruct HIn as [l1 [l2 Heq]]; subst. clear IHHfa Hfa. induction l1.
simpl. apply ui_uni_rl. apply uisub_intersect. apply uisub_intersect in Hsub. rewrite -> Forall_forall in Hsub. apply Forall_forall. intros l' HIn; apply Hsub; apply Hincl; assumption.
simpl. apply ui_uni_rr. assumption.
apply IHHfa; assumption.
Qed.
Lemma dsubda_mono {A A' : T -> T -> Prop} : (forall tl tr : T, A tl tr -> A' tl tr) -> forall tl tr : T, dsubda (@DPremise) A tl tr -> dsubda (@DPremise) A' tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
apply dsubda_trans with tm; assumption.
apply dsubda_assume. apply Himpl; assumption.
apply dsubda_lit with r. assumption.
Qed.
Lemma Integrate_ProductOfLiterals (f : list Lit -> T) : forall (t : T) (Hpol : ProductOfLiterals t), Integrate f t = f (Tlits t Hpol).
intros t Hpol. generalize Hpol; generalize dependent f. induction Hpol; intros f Hpol'.
reflexivity.
reflexivity.
simpl. rewrite -> IHHpol1 with (Hpol := Hpol1). rewrite -> IHHpol2 with (Hpol := Hpol2). rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_l Hpol') Hpol1). rewrite -> (Tlits_ProductOfLiterals_irrel (ProductOfLiterals_int_r Hpol') Hpol2). reflexivity.
Qed.
Lemma ProductOfLiterals_Integrated_int {P : list Lit -> Prop} : forall t : T, ProductOfLiterals t -> Integrated P t -> Integrated_int P t.
intros t Hpol Hint. destruct Hpol; assumption.
Qed.
Lemma Integrated_int_mono : forall (P P' : list Lit -> Prop) (Himpl : forall ls : list Lit, P ls -> P' ls) (t : T), Integrated_int P t -> Integrated_int P' t.
intros P P' Himpl t Hint. generalize dependent P'. generalize dependent P. induction t; intros P Hint P' Himpl; simpl in *.
apply Himpl. assumption.
apply Hint.
apply Hint.
apply (IHt1 _ Hint). intros ls HInt'. apply (IHt2 _ HInt'). intros ls'; apply Himpl.
apply Himpl. assumption.
Qed.
Lemma Integrated_mono : forall (P P' : list Lit -> Prop) (Himpl : forall ls : list Lit, P ls -> P' ls) (t : T), Integrated P t -> Integrated P' t.
intros P P' Himpl t Hint. generalize dependent P'. generalize dependent P. induction t; intros P Hint P' Himpl; simpl in *.
apply Himpl. assumption.
apply Hint.
destruct Hint as [Hintl Hintr]; split; [apply (IHt1 _ Hintl) | apply (IHt2 _ Hintr)]; assumption.
revert Hint. apply Integrated_int_mono. intros ls. apply Integrated_int_mono. intros ls'. apply Himpl.
apply Himpl. assumption.
Qed.
Lemma Integrated_int_and : forall (Pl Pr : list Lit -> Prop) (t : T), (Integrated_int Pl t /\ Integrated_int Pr t) <-> Integrated_int (fun ls => Pl ls /\ Pr ls) t.
intros Pl Pr t; split; intros H.
destruct H as [Hl Hr]. generalize dependent Pl. generalize dependent Pr. induction t; intros Pr Hr Pl Hl; simpl in *; try (try split; assumption).
pose proof (IHt1 _ Hl _ Hr). revert H. apply Integrated_int_mono. intros ls [Hir Hil]. apply (IHt2 _ Hir _ Hil).
generalize dependent Pr. generalize dependent Pl. induction t; intros Pl Pr Hint; simpl in *; try (split; assumption); try assumption. split; revert Hint; apply Integrated_int_mono; intros ls Hint; apply (IHt2 _ _ Hint).
Qed.
Lemma Integrated_and : forall (Pl Pr : list Lit -> Prop) (t : T), (Integrated Pl t /\ Integrated Pr t) <-> Integrated (fun ls => Pl ls /\ Pr ls) t.
intros Pl Pr t; split; intros H.
destruct H as [Hl Hr]. generalize dependent Pl. generalize dependent Pr. induction t; intros Pr Hr Pl Hl; simpl in *; try (try split; assumption).
split; [apply IHt1 | apply IHt2]; (apply Hr || apply Hl).
clear IHt1 IHt2. pose proof (conj Hl Hr) as Hc. apply Integrated_int_and in Hc. revert Hc. apply Integrated_int_mono. intros ls [Hintl Hintr]. apply Integrated_int_and; split; assumption.
generalize dependent Pr. generalize dependent Pl. induction t; intros Pl Pr Hint; simpl in *; try (split; assumption); try assumption.
destruct Hint as [Hintl Hintr]. apply IHt1 in Hintl. apply IHt2 in Hintr. split; split; (apply Hintl || apply Hintr).
split; revert Hint; apply Integrated_int_mono; intros ls; apply Integrated_int_mono; intros ls' H; apply H.
Qed.
Lemma Integrate_mono : forall (f g : list Lit -> T), (forall ls : list Lit, f ls = g ls) -> forall t : T, Integrate f t = Integrate g t.
intros f g Heq t. generalize dependent g. generalize dependent f. induction t; intros f g Heq; try reflexivity; try apply Heq.
simpl. rewrite -> (IHt1 f g); [|assumption]. rewrite -> (IHt2 f g); [|assumption]. reflexivity.
simpl. apply IHt1. intros ls. apply IHt2. intros ls'. apply Heq.
Qed.
Lemma Integrate_stacked : forall (f g : list Lit -> T) (t : T), Integrate (fun ls => Integrate g (f ls)) t = Integrate g (Integrate f t).
intros f g t. generalize dependent g. generalize dependent f. induction t; intros f g; try reflexivity.
simpl in *. rewrite -> IHt1. rewrite -> IHt2. reflexivity.
simpl in *. rewrite <- IHt1. apply Integrate_mono. intros ls. apply IHt2.
Qed.
Lemma uisub_dnf : forall t : T, uisub (lsub (@RPremise) rsub) (sop2ui (ui2sop t)) t.
induction t; try (constructor; assumption).
unfold ui2sop in *. simpl. unfold sop2ui in *. induction (SopIntegrate (fun ls => [ls]) t1).
apply ui_uni_rr. assumption.
simpl. apply ui_uni_l; simpl in IHt1; apply uisub_uni_l in IHt1; destruct IHt1; [apply ui_uni_rl|apply IHl]; assumption.
rewrite -> ui2sop_meet_ui2sop in *. simpl. apply ui_int_r; apply suisub_uisub; apply suisub_meet_l; [left | right]; apply uisub_suisub'; assumption.
simpl. apply ui_uni_l; constructor. apply rsubf_uisub. apply rsub_refl.
Qed.
Lemma Intersect_ProductOfLiterals : forall ls : list Lit, ProductOfLiterals (Intersect ls).
induction ls; simpl; repeat constructor. assumption.
Qed.
Lemma Integrate_Integrate_dnf {f : list Lit -> T} : forall t : T, Integrate f t = Integrate f (Integrate (fun ls => Intersect ls) t).
intros t; generalize dependent f; induction t; intros f; try reflexivity.
simpl. rewrite -> IHt1. rewrite -> IHt2. reflexivity.
simpl. rewrite <- Integrate_stacked. apply Integrate_mono. intros ls. rewrite <- Integrate_stacked. apply Integrate_mono. intros ls'. rewrite -> (Integrate_ProductOfLiterals _ _ (Intersect_ProductOfLiterals (ls ++ ls'))). clear IHt1 IHt2. f_equal. induction (ls ++ ls'); [reflexivity|]. simpl. f_equal. rewrite -> IHl at 1. simpl. apply Tlits_ProductOfLiterals_irrel.
Qed.
Lemma Intersect_Integrated : forall t : T, Integrated (fun _ => True) (Integrate Intersect t).
intros t. assert (Hf : forall ls : list Lit, Integrated (fun _ => True) (Intersect ls)). (intros ls; induction ls; [apply I|simpl; apply ProductOfLiterals_Integrated_int; [apply Intersect_ProductOfLiterals|assumption]]). remember Intersect as f. clear Heqf. generalize dependent f.
induction t; intros f Hf; try apply I; try apply Hf.
simpl. split; [apply IHt1 | apply IHt2]; assumption.
simpl. apply IHt1. intros ls. apply IHt2. intros ls'. apply Hf.
Qed.
Lemma Tlits_Intersect : forall (ls : list Lit) (Hpol : ProductOfLiterals (Intersect ls)), Tlits (Intersect ls) Hpol = ls.
induction ls; intros Hpol.
reflexivity.
simpl. f_equal. apply IHls.
Qed.
Definition dnf : T -> T := Integrate Intersect.
Inductive unionof {P : T -> Prop} : T -> list T -> Prop :=
| unionof_leaf (t : T) : P t -> unionof t [t]
| unionof_bot : unionof TBot []
| unionof_uni (tl tr : T) (ll lr : list T) : unionof tl ll -> unionof tr lr -> unionof (TUni tl tr) (ll ++ lr)
.
Arguments unionof : clear implicits.
Lemma SumOfProducts_unionof : forall t : T, SumOfProducts t -> exists l : list T, unionof ProductOfLiterals t l.
intros t Hsop. induction Hsop.
exists []. constructor; fail.
destruct IHHsop1 as [ll IHl]. destruct IHHsop2 as [lr IHr]. exists (ll ++ lr). constructor; assumption.
exists [t]; constructor; assumption.
Qed.
Lemma unionof_mono (P P' : T -> Prop) : (forall t : T, P t -> P' t) -> forall (t : T) (l : list T), unionof P t l -> unionof P' t l.
intros Himpl t l Huof. induction Huof; constructor.
apply Himpl. assumption.
assumption.
assumption.
Qed.
Lemma Tlits_lits : forall (t : T) (Hpol : ProductOfLiterals t), Tlits t Hpol = lits t.
intros t Hpol. pose Hpol as H. induction H; try reflexivity.
simpl. rewrite -> IHProductOfLiterals1. rewrite -> IHProductOfLiterals2. reflexivity.
Qed.
Lemma lits_Intersect : forall ls : list Lit, lits (Intersect ls) = ls.
induction ls; [reflexivity|]. simpl. f_equal; assumption.
Qed.
Lemma dsubda_int_l_swap {Assumed : T -> T -> Prop} : forall tl tr t : T, dsubda (@DPremise) Assumed (TIsect tl tr) t -> dsubda (@DPremise) Assumed (TIsect tr tl) t.
intros tl tr t Hsub. apply dsubda_trans with (TIsect tl tr); [|assumption]. clear Hsub. apply dsubda_int_r; constructor; fail.
Qed.
Lemma SumOfProducts_IntegrateIsect : forall (tl tr : T) (ll lr : list T), unionof ProductOfLiterals tl ll -> unionof ProductOfLiterals tr lr -> exists l : list T, unionof ProductOfLiterals (Integrate Intersect (TIsect tl tr)) l /\ forall (tl' tr' : T), In tl' ll -> In tr' lr -> exists t : T, In t l /\ lits t = lits tl' ++ lits tr'.
intros tl tr ll lr Hul Hur. simpl. induction Hul.
rewrite -> (Integrate_ProductOfLiterals _ _ H). induction Hur.
rewrite -> (Integrate_ProductOfLiterals _ _ H0). pose proof H as H'. induction H'; simpl.
pose proof H0 as H''. induction H''; simpl.
exists [TTop]. split; [apply unionof_leaf; constructor; fail|]; intros tl tr Htl Htr; exists TTop; split; [apply in_eq|]; inversion Htl; inversion Htr; try contradiction; subst; reflexivity.
exists [TIsect (TLit l) TTop]. split; [apply unionof_leaf; repeat constructor; fail|]. intros tl tr Htl Htr; exists (TIsect (TLit l) TTop); split; [apply in_eq|]; inversion Htl; inversion Htr; try contradiction; subst; reflexivity.
pose proof (IHH''1 (ProductOfLiterals_int_l H0)) as [l1 IH1]; clear IHH''1. pose proof (IHH''2 (ProductOfLiterals_int_r H0)) as [l2 IH2]; clear IHH''2. remember (Tlits tl _) as tll. clear Heqtll. generalize dependent l2. generalize dependent l1. induction tll; intros l1 IH1 l2 IH2.
simpl. destruct IH1 as [IH1 IH1']; inversion IH1; subst. exists l2. destruct IH2 as [IH2 IH2']; inversion IH2; subst.
split.
apply unionof_leaf. apply Intersect_ProductOfLiterals.
intros tlx trx Htlx Htrx. eexists; split; [apply in_eq|]. inversion Htlx; inversion Htrx; try contradiction; subst. rewrite -> lits_Intersect. rewrite -> Tlits_lits. pose proof (IH1' TTop tl (or_introl (eq_refl TTop)) (or_introl (eq_refl tl))) as [t [HIn Heq]]. inversion HIn; [|contradiction]; subst. simpl in *. rewrite <- Heq. reflexivity.
destruct (Tlits tr (ProductOfLiterals_int_r H0)); simpl; inversion H3.
destruct (Tlits tr (ProductOfLiterals_int_r H0)); simpl; inversion H2.
simpl in *. destruct IH1 as [IH1 IH1']; inversion IH1. subst. destruct IH2 as [IH2 IH2']; inversion IH2; subst; (eexists; split; [apply unionof_leaf; constructor; [constructor|apply Intersect_ProductOfLiterals]|]); intros tlx trx Htlx Htrx; eexists; (split; [apply in_eq|]); inversion Htlx; inversion Htrx; try contradiction; subst; simpl; repeat rewrite -> Tlits_lits; repeat rewrite -> lits_Intersect; pose proof (IH1' _ _ (or_introl (eq_refl TTop)) (or_introl (eq_refl _))) as [t [HIn Heq]]; (inversion HIn; [|contradiction]); subst; simpl in *; rewrite <- Heq; rewrite -> lits_Intersect; reflexivity.
eexists; split; [apply unionof_leaf; constructor; assumption || apply Intersect_ProductOfLiterals|]. intros tl tr Htl Htr; eexists; split; [apply in_eq|]; inversion Htl; inversion Htr; try contradiction; subst. rewrite -> Tlits_lits. simpl. rewrite -> lits_Intersect. reflexivity.
eexists; split; [apply unionof_leaf; apply Intersect_ProductOfLiterals|]. intros tl' tr' Htl' Htr'; eexists; split; [apply in_eq|]; inversion Htl'; inversion Htr'; try contradiction; subst. repeat rewrite -> Tlits_lits. simpl. repeat rewrite -> lits_Intersect. reflexivity.
exists []. split.
constructor.
intros; contradiction; fail.
simpl. destruct IHHur1 as [ll' [IH1 IH1']]. destruct IHHur2 as [lr' [IH2 IH2']]. exists (ll' ++ lr'). split.
constructor; [revert IH1 | revert IH2]; apply unionof_mono; simpl; intros t' Hpol; assumption.
intros tl' tr' Htl' Htr'; inversion Htl'; apply in_app_or in Htr'; try contradiction; subst. destruct Htr' as [Htr' | Htr']; [pose proof (IH1' tl' tr' (in_eq tl' []) Htr') as [t [HIn Heq]]|pose proof (IH2' tl' tr' (in_eq tl' []) Htr') as [t [HIn Heq]]]; exists t; (split; [|assumption]) ; apply in_app_iff; [left | right]; assumption.
simpl. exists []. split; [constructor|intros; contradiction].
simpl. destruct IHHul1 as [ll' [IH1 IH1']]. destruct IHHul2 as [lr' [IH2 IH2']]. exists (ll' ++ lr'). split.
constructor; [revert IH1 | revert IH2]; apply unionof_mono; simpl; intros t' Hpol; assumption.
intros tl' tr' Htl' Htr'; apply in_app_or in Htl'; try contradiction; subst. destruct Htl' as [Htl' | Htl']; [pose proof (IH1' tl' tr' Htl' Htr') as [t [HIn Heq]]|pose proof (IH2' tl' tr' Htl' Htr') as [t [HIn Heq]]]; exists t; (split; [|assumption]) ; apply in_app_iff; [left | right]; assumption.
Qed.
Lemma dsubda_dnf {Assumed : T -> T -> Prop}: forall t : T, dsubda (@DPremise) Assumed t (dnf t).
induction t; try apply dsubda_refl.
unfold dnf in *; simpl; apply dsubda_uni_l; [apply dsubda_trans with (dnf t1) | apply dsubda_trans with (dnf t2)]; assumption || (constructor; fail).
pose proof (SumOfProducts_unionof _ (Integrated_SumOfProducts _ _ (Intersect_Integrated t1))) as [l1 Hl1]. pose proof (SumOfProducts_unionof _ (Integrated_SumOfProducts _ _ (Intersect_Integrated t2))) as [l2 Hl2]. pose proof (SumOfProducts_IntegrateIsect _ _ _ _ Hl1 Hl2) as [l [Hl Hl']]. unfold dnf in *. simpl. rewrite -> Integrate_Integrate_dnf. simpl in Hl. apply dsubda_trans with (TIsect (Integrate Intersect t1) (Integrate Intersect t2)).
apply dsubda_int_r; [apply dsubda_trans with t1 | apply dsubda_trans with t2]; (constructor; fail) || assumption.
clear IHt1 IHt2. remember (fun _ => Integrate _ t2) as f. rewrite -> Integrate_mono with (f := f) (g := fun ls => Integrate (fun ls' => Intersect (ls ++ ls')) (Integrate Intersect t2)); subst; [|intros; apply Integrate_Integrate_dnf]. remember (Integrate _ (Integrate _ t1)) as t. clear Heqt. remember (Integrate _ t1) as ti1. remember (Integrate _ t2) as ti2. clear Heqti1 Heqti2. induction Hl1.
induction Hl2.
induction Hl.
pose proof (Hl' t0 t3 (in_eq t0 []) (in_eq t3 [])) as [tx [HIn Heq]]. inversion HIn; [subst | contradiction]. clear Hl' HIn. assert (Hincl : incl (lits tx) (lits t0 ++ lits t3)) by (rewrite -> Heq; apply incl_refl). clear Heq. induction H1.
constructor; fail.
simpl in Hincl. assert (HIn : In l (lits t0 ++ lits t3)) by (apply Hincl; apply in_eq). clear Hincl. apply in_app_iff in HIn. destruct HIn as [HIn | HIn]; [induction H; simpl in HIn; try (inversion HIn; try contradiction; subst; constructor; fail) | induction H0; try (inversion HIn; try contradiction; subst; constructor; fail)]; apply in_app_iff in HIn; destruct HIn as [HIn | HIn]; repeat remove_eq_implications; [apply dsubda_trans with (TIsect tl t3) | apply dsubda_trans with (TIsect tr t3) | apply dsubda_trans with (TIsect t0 tl) | apply dsubda_trans with (TIsect t0 tr)]; try assumption; apply dsubda_int_r; (constructor; fail) || (apply dsubda_trans with (TIsect tl tr); constructor; fail).
simpl in Hincl. apply dsubda_int_r; [apply IHProductOfLiterals1 | apply IHProductOfLiterals2]; intros x HIn; apply Hincl; apply in_app_iff; [left | right]; assumption.
pose proof (Hl' t0 t3 (in_eq t0 []) (in_eq t3 [])) as [tx [HIn Heq]]; inversion HIn.
pose proof (Hl' t0 t3 (in_eq t0 []) (in_eq t3 [])) as [tx [HIn Heq]]; apply in_app_iff in HIn; destruct HIn as [HIn | HIn]; [apply dsubda_trans with tl | apply dsubda_trans with tr]; (constructor; fail) || apply IHHl1 || apply IHHl2; intros tl' tr' HInl' HInr'; exists tx; inversion HInl'; inversion HInr'; try contradiction; subst; split; assumption.
apply dsubda_trans with TBot; constructor; fail.
apply dsubda_trans with (TUni (TIsect t0 tl) (TIsect t0 tr)); [apply dsubda_dist|]; apply dsubda_uni_l; apply IHHl2_1 || apply IHHl2_2 ; intros; apply Hl'; assumption || apply in_app_iff; [left | right]; assumption.
apply dsubda_trans with TBot; constructor; fail.
apply dsubda_int_l_swap. apply dsubda_trans with (TUni (TIsect ti2 tl) (TIsect ti2 tr)); [apply dsubda_dist|]; apply dsubda_uni_l; apply dsubda_int_l_swap; apply IHHl1_1 || apply IHHl1_2; intros; apply Hl'; assumption || apply in_app_iff; [left | right]; assumption.
unfold dnf. simpl. apply dsubda_int_r; constructor; fail.
Qed.
Lemma dsubda_isect_r {Assumed : T -> T -> Prop} : forall t tl tr : T, dsubda (@DPremise) Assumed t (TIsect tl tr) -> dsubda (@DPremise) Assumed t tl /\ dsubda (@DPremise) Assumed t tr.
intros t tl tr Hsub. split; (apply dsubda_trans with (TIsect tl tr); [assumption | constructor; fail]).
Qed.
Lemma sop2ui_unionof : forall s : sop, unionof ProductOfLiterals (sop2ui s) (map Intersect s).
induction s.
constructor; fail.
simpl. fold ([Intersect a] ++ (map Intersect s)). constructor; [|assumption]. clear IHs. induction a; constructor; apply Intersect_ProductOfLiterals.
Qed.
Lemma dsubda_sop_r_incl {Assumed : T -> T -> Prop} : forall (t : T) (s s' : sop), incl s s' -> dsubda (@DPremise) Assumed t (sop2ui s) -> dsubda (@DPremise) Assumed t (sop2ui s').
intros t s s' Hincl Hsub. apply dsubda_trans with (sop2ui s); [assumption|]; clear Hsub. induction s.
constructor; fail.
simpl. apply dsubda_uni_l; [|apply IHs; intros x HIn; apply Hincl; apply in_cons; assumption]; clear IHs. assert (HIn : In a s') by (apply Hincl; apply in_eq). clear Hincl. apply in_split in HIn. destruct HIn as [l1 [l2 Heq]]. subst. induction l1.
simpl. constructor; fail.
simpl. eapply dsubda_trans; [apply IHl1|constructor;fail].
Qed.
Lemma dsubda_sopof {Assumed : T -> T -> Prop} : forall (s : sop) (t : T), sopof s t -> dsubda (@DPremise) Assumed t (sop2ui s).
intros s t Hsopof. induction Hsopof.
induction H.
simpl. apply dsubda_trans with (TIsect (TLit l) (TTop)); [constructor|]; constructor; fail.
simpl. constructor; fail.
induction H; simpl in *.
apply dsubda_trans with (TIsect (TUni (TIsect (TLit l) TTop) TBot) (TUni (Intersect lsr) TBot)).
apply dsubda_int_r; [apply dsubda_trans with (TUni (TIsect (TLit l) TTop) TBot); [|constructor; fail] | apply dsubda_trans with (TUni (Intersect lsr) TBot); [|constructor; fail]]; [apply dsubda_trans with (TLit l) | apply dsubda_trans with tr]; assumption || constructor; fail.
eapply dsubda_trans; [apply dsubda_dist|]. apply dsubda_uni_l; [| apply dsubda_trans with TBot; constructor; fail]. apply dsubda_int_l_swap. eapply dsubda_trans; [apply dsubda_dist|]. apply dsubda_uni_l; [|apply dsubda_trans with TBot; constructor; fail]. apply dsubda_trans with (TIsect (TLit l) (Intersect lsr)); [|constructor; fail]. apply dsubda_int_r; [|constructor; fail]. apply dsubda_trans with (TIsect (TLit l) TTop); constructor; fail.
eapply dsubda_trans; [|apply IHpolof2]; constructor; fail.
clear IHpolof3 IHpolof4. apply dsubda_trans with (TIsect (TUni (Intersect (lsl ++ lsr0)) TBot) (TUni (Intersect lsr) TBot)).
apply dsubda_int_r; [apply dsubda_trans with (TIsect tl tr0) | apply dsubda_trans with tr]; assumption || constructor; fail.
clear IHpolof1 IHpolof2. eapply dsubda_trans; [apply dsubda_dist|]. apply dsubda_uni_l; [| apply dsubda_trans with TBot; constructor; fail]. apply dsubda_int_l_swap. eapply dsubda_trans; [apply dsubda_dist|]. apply dsubda_uni_l; [|apply dsubda_trans with TBot; constructor; fail]. apply dsubda_trans with (Intersect ((lsl ++ lsr0) ++ lsr)); [|constructor; fail]. apply dsubda_int_l_swap. induction (lsl ++ lsr0); simpl.
constructor; fail.
apply dsubda_int_r; [apply dsubda_trans with (TIsect (TLit a) (Intersect l)); constructor; fail|]. eapply dsubda_trans; [|apply IHl]. apply dsubda_int_r; [| constructor; fail]. eapply dsubda_trans; [apply dsubda_int_ll|constructor;fail].
constructor; fail.
apply dsubda_uni_l.
apply dsubda_sop_r_incl with sl; [|assumption]. apply incl_appl. apply incl_refl.
apply dsubda_sop_r_incl with sr; [|assumption]. apply incl_appr. apply incl_refl.
Qed.
End SOP_Infrastructure.
This page has been generated by coqdoc