DNF and Intersectors (ClassDistribute.v)
This file is the second part of our example of applying our framework to a specific language. In a sense, it builds its own framwork for that particular language, and in large parts, minus the caveat discussed in the step-by-step guide, corresponds to what we do in the paper. That is, for the specific language with generic classes, unions and intersections that we built, we define a notion of intersectors and intersected predicates similar to what we have in the paper for arbitrary literals, unions, and intersections. Later files contain reasoning about the composability of this mini-framework, which is exaclty what we have in the paper in Section 5, and an instantiation of this mini-framework for disjointness reasoning, similar to what we have in Section 6. The first parts of this file build up the machinery to talk about DNFing types and reasoning about them in their DNFed form as "Sums of Products", or SoPs. A natural representation of SoPs would be to use lists of lists of literals (where the inner lists of literals are intersections of literals, and the outer lists of those are unions of those intersections). However, to combat the problems explained in the caveat part of the step-by-step guide, the representation here instead is as trees of trees of literals (the idea being that if one splits a tree at the right point, its left and right branches may still be intersected if the whole tree was).Require Import Common.
Require Import Decide.
Require Import Tradition.
Require Import Convert.
Require Import Preprocess.
Require Import Extend.
Require Import Class.
Require Import Wf_nat.
Require Import Max.
Require Import Plus.
Module SumOfProducts.
Import Generics.
Import Decidable.
Import Proof.
Import DRule.
Inductive Tree (A : Type) : Type
:= leaf
| node (a : A)
| branch (l r : Tree A).
Arguments leaf [A].
Arguments node [A].
Arguments branch [A].
Definition tfold {A B : Type} (bleaf : B) (bnode : A -> B) (bbranch : B -> B -> B) : Tree A -> B
:= fix tfold (t : Tree A) : B
:= match t with
| leaf => bleaf
| node a => bnode a
| branch l r => bbranch (tfold l) (tfold r)
end.
Definition tmap {A B : Type} (f : A -> B) : Tree A -> Tree B
:= tfold leaf (fun a => node (f a)) (@branch B).
Definition tbind {A B : Type} (f : A -> Tree B) : Tree A -> Tree B
:= tfold leaf f (@branch B).
Inductive TForall {A : Type} (P : A -> Prop) : Tree A -> Prop
:= tforall_leaf : TForall P leaf
| tforall_node (a : A) : P a -> TForall P (node a)
| tforall_branch (l r : Tree A) : TForall P l -> TForall P r -> TForall P (branch l r).
Inductive TExists {A : Type} (P : A -> Prop) : Tree A -> Prop
:= texists_node (a : A) : P a -> TExists P (node a)
| texists_left (l r : Tree A) : TExists P l -> TExists P (branch l r)
| texists_right (l r : Tree A) : TExists P r -> TExists P (branch l r).
Lemma node_tforall {A : Type} (P : A -> Prop) {a : A} : TForall P (node a) -> P a.
intro f. inversion f. assumption.
Qed.
Lemma branch_tforall {A : Type} (P : A -> Prop) {l r : Tree A} : TForall P (branch l r) -> TForall P l /\ TForall P r.
intro f. inversion f. split; assumption.
Qed.
Lemma tforall_map {A B : Type} (P : B -> Prop) (f : A -> B) (t : Tree A) : TForall (fun a => P (f a)) t -> TForall P (tmap f t).
intro p. induction p; simpl; constructor; assumption.
Qed.
Lemma tforall_mono {A : Type} (P P' : A -> Prop) (imp : forall a : A, P a -> P' a) (t : Tree A) : TForall P t -> TForall P' t.
intro f. induction f; constructor; try apply imp; assumption.
Qed.
Lemma node_texists {A : Type} (P : A -> Prop) {a : A} : TExists P (node a) -> P a.
intro f. inversion f. assumption.
Qed.
Lemma texists_mono {A : Type} (P P' : A -> Prop) (imp : forall a : A, P a -> P' a) (t : Tree A) : TExists P t -> TExists P' t.
intro e. induction e; constructor; try apply imp; assumption.
Qed.
Inductive CT : Type
:= cparameter
| cclass (c : Class) (i o : T).
Definition ctot (c : CT) : T
:= match c with
| cparameter => parameter
| cclass c i o => class c i o
end.
Definition SoP : Type
:= Tree (Tree CT).
Definition tprod {A : Type} (pair : A -> A -> A) (l r : Tree A) : Tree A
:= tbind (fun l => tmap (pair l) r) l.
Definition meet : SoP -> SoP -> SoP
:= tprod (@branch CT).
Section SubProd.
Variable R : CT -> CT -> Prop.
Definition SubProd (l : Tree CT) : Tree CT -> Prop
:= TForall (fun r => TExists (fun l => R l r) l).
Lemma sub_intersectionl (l r p : Tree CT) : SubProd l p -> SubProd (branch l r) p.
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. apply texists_left. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_intersectionr (l r p : Tree CT) : SubProd r p -> SubProd (branch l r) p.
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. apply texists_right. assumption.
apply tforall_branch; assumption.
Qed.
Lemma subprod_refl (refl : forall t : CT, R t t) (p : Tree CT) : SubProd p p.
induction p.
apply tforall_leaf.
apply tforall_node. apply texists_node. apply refl.
apply tforall_branch; [ apply sub_intersectionl | apply sub_intersectionr ]; assumption.
Qed.
End SubProd.
Section Sub.
Variable R : T -> T -> Prop.
Definition CTR (ct ct' : CT) : Prop
:= R (ctot ct) (ctot ct').
Definition Sub (l r : SoP) : Prop
:= TForall (fun l => TExists (SubProd CTR l) r) l.
Lemma sub_bottom (sop : SoP) : TForall (fun p => False) sop -> Sub sop leaf.
intro sub. induction sub.
apply tforall_leaf.
destruct H.
apply tforall_branch; assumption.
Qed.
Lemma sub_node (sop : SoP) (p' : Tree CT) : TForall (fun p => SubProd CTR p p') sop -> Sub sop (node p').
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. apply texists_node. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_unionl (sop l r : SoP) : Sub sop l -> Sub sop (branch l r).
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. apply texists_left. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_unionr (sop l r : SoP) : Sub sop r -> Sub sop (branch l r).
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. apply texists_right. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_refl (refl : forall t : T, R t t) (sop : SoP) : Sub sop sop.
induction sop.
apply tforall_leaf.
apply tforall_node. apply texists_node. apply subprod_refl. intro t. apply refl.
apply tforall_branch; [ apply sub_unionl | apply sub_unionr ]; assumption.
Qed.
Lemma bottom_sub (sop : SoP) : Sub sop leaf -> TForall (fun p => False) sop.
intro sub. induction sub.
apply tforall_leaf.
inversion H.
apply tforall_branch; assumption.
Qed.
Lemma node_sub (sop : SoP) (p' : Tree CT) : Sub sop (node p') -> TForall (fun p => SubProd CTR p p') sop.
intro sub. induction sub.
apply tforall_leaf.
apply tforall_node. inversion H. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_meet (sop l r : SoP) : Sub sop l -> Sub sop r -> Sub sop (meet l r).
intro subl. revert r. induction subl; intros r' subr.
apply tforall_leaf.
apply tforall_node. apply node_tforall in subr. rename H into subl. rename a into sop. revert r' subr. induction subl; intros r' subr; simpl.
revert a H. induction subr; intros l' subl; simpl.
apply texists_node. apply tforall_branch; assumption.
apply texists_left. apply IHsubr. assumption.
apply texists_right. apply IHsubr. assumption.
apply texists_left. apply IHsubl. assumption.
apply texists_right. apply IHsubl. assumption.
apply branch_tforall in subr. destruct subr as [ subrl subrr ]. apply tforall_branch; [ apply IHsubl1 | apply IHsubl2 ]; assumption.
Qed.
Lemma sub_meetl (l r sop : SoP) : Sub l sop -> Sub (meet l r) sop.
intro sub. induction sub; simpl.
apply tforall_leaf.
induction H; simpl.
apply sub_node. apply tforall_map. induction r.
apply tforall_leaf.
apply tforall_node. apply sub_intersectionl. assumption.
apply tforall_branch; assumption.
apply sub_unionl. assumption.
apply sub_unionr. assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_meetr (l r sop : SoP) : Sub r sop -> Sub (meet l r) sop.
intro sub. induction l; simpl.
apply tforall_leaf.
apply tforall_map. induction sub.
apply tforall_leaf.
apply tforall_node. induction H.
apply texists_node. apply sub_intersectionr. assumption.
apply texists_left. assumption.
apply texists_right. assumption.
apply tforall_branch; assumption.
apply tforall_branch; assumption.
Qed.
Lemma sub_meet_l (sop l r : SoP) : Sub sop (meet l r) -> Sub sop l.
revert l r. induction sop; simpl; intros l r sub.
apply tforall_leaf.
apply tforall_node. inversion sub. clear sub. subst. induction l; simpl in *.
inversion H0.
apply texists_node. induction r; simpl in *.
inversion H0.
inversion H0. clear H0. subst. inversion H1. assumption.
inversion H0; clear H0; subst.
apply IHr1. assumption.
apply IHr2. assumption.
inversion H0; clear H0; subst.
apply texists_left. apply IHl1. assumption.
apply texists_right. apply IHl2. assumption.
inversion sub. clear sub. subst. apply tforall_branch; [ apply IHsop1 with r | apply IHsop2 with r ]; assumption.
Qed.
Lemma sub_meet_r (sop l r : SoP) : Sub sop (meet l r) -> Sub sop r.
revert l r. induction sop; simpl; intros l r sub.
apply tforall_leaf.
apply tforall_node. inversion sub. clear sub. subst. induction l; simpl in *.
inversion H0.
induction r; simpl in *.
inversion H0.
inversion H0. clear H0. subst. apply texists_node. inversion H1. assumption.
inversion H0; clear H0; subst.
apply texists_left. apply IHr1. assumption.
apply texists_right. apply IHr2. assumption.
inversion H0; clear H0; subst.
apply IHl1. assumption.
apply IHl2. assumption.
inversion sub. clear sub. subst. apply tforall_branch; [ apply IHsop1 with l | apply IHsop2 with l ]; assumption.
Qed.
End Sub.
Definition sub_transd (sop1 sop2 sop3 : SoP) : Sub Decidable sop1 sop2 -> Sub Decidable sop2 sop3 -> Sub Decidable sop1 sop3.
intro sub. revert sop3. induction sub; intros sop3 sub'.
apply tforall_leaf.
apply tforall_node. revert sop3 sub'. induction H; intros sop3 sub'.
inversion sub'. clear sub'. subst. revert a H. induction H1; intros p1 sub.
apply texists_node. induction H.
apply tforall_leaf.
apply tforall_node. induction H.
inversion sub. clear sub. subst. induction H1.
apply texists_node. revert H0 H. apply trans.
apply texists_left. assumption.
apply texists_right. assumption.
apply IHTExists. inversion sub. assumption.
apply IHTExists. inversion sub. assumption.
apply tforall_branch; assumption.
apply texists_left. apply IHTExists. assumption.
apply texists_right. apply IHTExists. assumption.
apply IHTExists. inversion sub'. assumption.
apply IHTExists. inversion sub'. assumption.
apply tforall_branch.
apply IHsub1. assumption.
apply IHsub2. assumption.
Qed.
Definition generic (sop : SoP) : T
:= tfold bottom (fun p => tfold top ctot intersection p) union sop.
Fixpoint dnf (t : T) : SoP
:= match t with
| parameter => node (node cparameter)
| top => node leaf
| intersection l r => meet (dnf l) (dnf r)
| bottom => leaf
| union l r => branch (dnf l) (dnf r)
| class c i o => node (node (cclass c i o))
end.
Lemma parameter_generic (sop : SoP) : parameter = generic sop -> node (node cparameter) = sop.
intro e. destruct sop; try (inversion e; fail). destruct a; try (inversion e; fail). destruct a; try (inversion e; fail). reflexivity.
Qed.
Lemma top_generic (sop : SoP) : top = generic sop -> node leaf = sop.
intro e. destruct sop; try (inversion e; fail). destruct a; try (inversion e; fail).
reflexivity.
destruct a; try (inversion e; fail).
Qed.
Lemma intersection_generic (l r : T) (sop : SoP) : intersection l r = generic sop -> exists l' : Tree CT, exists2 r' : Tree CT, l = generic (node l') /\ r = generic (node r') & node (branch l' r') = sop.
intro e. destruct sop; try (inversion e; fail). destruct a; try (inversion e; fail).
destruct a; try (inversion e; fail).
simpl in e. inversion e. clear e. subst. apply ex_intro with a1. apply ex_intro2 with a2; [ split | ]; reflexivity.
Qed.
Lemma bottom_generic (sop : SoP) : bottom = generic sop -> leaf = sop.
intro e. destruct sop; try (inversion e; fail).
reflexivity.
destruct a; try (inversion e; fail). destruct a; try (inversion e; fail).
Qed.
Lemma union_generic (l r : T) (sop : SoP) : union l r = generic sop -> exists l' : SoP, exists2 r' : SoP, l = generic l' /\ r = generic r' & branch l' r' = sop.
intro e. destruct sop; try (inversion e; fail).
destruct a; try (inversion e; fail). destruct a; try (inversion e; fail).
simpl in e. inversion e. clear e. subst. apply ex_intro with sop1. apply ex_intro2 with sop2; [ split | ]; reflexivity.
Qed.
Lemma class_generic (c : Class) (i o : T) (sop : SoP) : class c i o = generic sop -> node (node (cclass c i o)) = sop.
intro e. destruct sop; try (inversion e; fail). destruct a; try (inversion e; fail). destruct a; try (inversion e; fail). simpl in e. inversion e. reflexivity.
Qed.
Lemma transposel (R : T -> T -> Prop) (admits : AdmitsD R) (sop : SoP) (t' : T) : Sub R sop (dnf t') -> R (generic sop) t'.
revert sop. induction t'; simpl; intros sop sub.
induction sub; simpl.
apply admits with (dbottom _). intro req. destruct req.
inversion H. clear H. subst. inversion H1. clear H1. subst. induction H0; simpl in *.
assumption.
apply admits with (dintersectionl _ _ _). simpl. intros _. assumption.
apply admits with (dintersectionr _ _ _). simpl. intros _. assumption.
apply admits with (dunion _ _ _). simpl. intros [ | ]; assumption.
apply admits with (dtop _). simpl. intros [].
apply admits with (dintersection _ _ _). simpl. intros [ | ].
apply IHt'1. revert sub. apply sub_meet_l.
apply IHt'2. revert sub. apply sub_meet_r.
induction sub; simpl.
apply admits with (dbottom _). intro req. destruct req.
inversion H.
apply admits with (dunion _ _ _). simpl. intros [ | ]; assumption.
induction sub; simpl.
apply admits with (dbottom _). intro req. destruct req.
inversion H; clear H; subst.
apply admits with (dunionl _ _ _). simpl. intros _. apply (IHt'1 (node a)). apply tforall_node. assumption.
apply admits with (dunionr _ _ _). simpl. intros _. apply (IHt'2 (node a)). apply tforall_node. assumption.
apply admits with (dunion _ _ _). simpl. intros [ | ]; assumption.
induction sub; simpl.
apply admits with (dbottom _). intro req. destruct req.
inversion H. clear H. subst. inversion H1. clear H1. subst. induction H0; simpl in *.
assumption.
apply admits with (dintersectionl _ _ _). simpl. intros _. assumption.
apply admits with (dintersectionr _ _ _). simpl. intros _. assumption.
apply admits with (dunion _ _ _). simpl. intros [ | ]; assumption.
Qed.
Definition DNF (P : Tree CT -> Prop) (t : T) : Prop
:= exists2 sop : SoP, generic sop = t & TForall P sop.
Lemma transposer (P : Tree CT -> Prop) (R : T -> T -> Prop) (pl : forall l r : Tree CT, P (branch l r) -> P l) (pr : forall l r : Tree CT, P (branch l r) -> P r) (admits : AdmitsD R) (inverts : Inverts (DNF P) R) (sop : SoP) (t' : T) : TForall P sop -> R (generic sop) t' -> Sub R sop (dnf t').
intros p r. apply inverts in r; [ | eapply ex_intro2; [ reflexivity | assumption ] ]. rename r into inversion. remember (generic sop) as t. revert sop Heqt p. induction inversion as [ t t' con ass _ rec ]. intros sop e p. destruct con; simpl in *.
apply parameter_generic in e. subst. apply tforall_node. apply texists_node. apply tforall_node. apply texists_node. apply admits with dparameter. assumption.
subst. clear ass rec. induction sop.
apply tforall_leaf.
apply tforall_node. apply texists_node. apply tforall_leaf.
inversion p. apply tforall_branch; [ apply IHsop1 | apply IHsop2 ]; assumption.
clear ass. apply intersection_generic in e. destruct e as [ l' [ r' [ el er ] e ] ]. subst. inversion p. clear p. subst. rename H0 into pl'. apply pl in pl'. apply tforall_node in pl'. pose proof (rec tt (ex_intro2 _ _ (node l') eq_refl pl') (node l') eq_refl) as rec. apply node_tforall in rec; try assumption. apply tforall_node. revert rec. apply texists_mono. apply tforall_mono. intros c e. apply texists_left. assumption.
clear ass. apply intersection_generic in e. destruct e as [ l' [ r' [ el er ] e ] ]. subst. inversion p. clear p. subst. rename H0 into pr'. apply pr in pr'. apply tforall_node in pr'. pose proof (rec tt (ex_intro2 _ _ (node r') eq_refl pr') (node r') eq_refl) as rec. apply node_tforall in rec; try assumption. apply tforall_node. revert rec. apply texists_mono. apply tforall_mono. intros c e. apply texists_right. assumption.
subst. pose proof (rec left (ex_intro2 _ _ sop eq_refl p) sop eq_refl) as recl. pose proof (rec right (ex_intro2 _ _ sop eq_refl p) sop eq_refl) as recr. clear rec ass. simpl in *. apply sub_meet; [ apply recl | apply recr ]; assumption.
apply bottom_generic in e. subst. apply tforall_leaf.
subst. pose proof (rec tt (ex_intro2 _ _ sop eq_refl p) sop eq_refl p) as rec. revert rec. apply tforall_mono. intros t e. apply texists_left. assumption.
subst. pose proof (rec tt (ex_intro2 _ _ sop eq_refl p) sop eq_refl p) as rec. revert rec. apply tforall_mono. intros t e. apply texists_right. assumption.
apply union_generic in e. destruct e as [ l' [ r' [ el er ] e ] ]. subst. inversion p. clear p. subst. rename H1 into pl'. rename H2 into pr'. pose proof (rec left (ex_intro2 _ _ _ eq_refl pl') l' eq_refl) as recl. pose proof (rec right (ex_intro2 _ _ _ eq_refl pr') r' eq_refl) as recr. clear ass rec. apply tforall_branch; [ apply recl | apply recr ]; assumption.
apply class_generic in e. subst. apply tforall_node. apply texists_node. apply tforall_node. apply texists_node. apply admits with (dclass _ _ _ _ _ _ _ p0). assumption.
Qed.
Definition swaps : Measure (Position -> nat) (nat -> nat -> nat).
apply measure.
intro pos. exact 0.
intros ml mr pos. exact (max (ml pos) (mr pos)).
intro pos. exact 0.
intros ml mr pos. exact (max (ml pos) (mr pos)).
intros mc mi mo pos. destruct pos.
exact (mc (mi right) (mo left)).
exact (max (S (mi left)) (mo right)).
exact max.
intros mc mc' mt mi mo. exact (max (mc mi mo) (mc' (mt (fun pos => match pos with right => mi | left => mo end) right) (mt (fun pos => match pos with left => mo | right => mi end) left))).
Defined.
Definition tswaps (t : T) := tinvariant swaps t (fun _ => 0).
Definition cswaps := cinvariant swaps.
Lemma tswaps_fill (i o t : T) (pos : Position) : tswaps (fill i o t) pos = tinvariant swaps t (fun pos' => match pos, pos' with left, left => tswaps o left | left, right => tswaps i right | right, left => tswaps i left | right, right => tswaps o right end) pos.
revert i o pos. induction t; intros i o pos; simpl.
rewrite tinvariant_eq. destruct pos; reflexivity.
unfold tswaps at 1. repeat rewrite (tinvariant_eq _ top). reflexivity.
unfold tswaps at 1. repeat rewrite (tinvariant_eq _ (intersection _ _)). fold (tswaps i). fold (tswaps (fill i o t1)). fold (tswaps (fill i o t2)). simpl. f_equal; [ apply IHt1 | apply IHt2 ].
unfold tswaps at 1. repeat rewrite (tinvariant_eq _ bottom). reflexivity.
unfold tswaps at 1. repeat rewrite (tinvariant_eq _ (union _ _)). fold (tswaps i). fold (tswaps (fill i o t1)). fold (tswaps (fill i o t2)). simpl. f_equal; [ apply IHt1 | apply IHt2 ].
unfold tswaps at 1. repeat rewrite (tinvariant_eq _ (class _ _ _)). fold (tswaps (fill o i t1)). fold (tswaps (fill i o t2)). fold cswaps. simpl. repeat rewrite IHt1. repeat rewrite IHt2. destruct pos; reflexivity.
Qed.
Inductive CTInversion (R : T -> T -> Prop) : CT -> CT -> Prop
:= ctparameter : CTInversion R cparameter cparameter
| ctclass (c : Class) (i o : T) (c' : Class) (i' o' : T) (c't : T) : PreInh c c' c't -> R i' (fill o i c't) -> R (fill i o c't) o' -> CTInversion R (cclass c i o) (cclass c' i' o').
End SumOfProducts.
The Intersector Module Type
This module type specifies the mini-framework created here. The required parts are as follows:- intersect is just like the intersector in the paper, except that the requirement that the result be in DNF is already exposed in the return type
- project is exactly Literal Dereliction (Requirement 10)
- Intersected is the intersected predicate in the paper
- intersected is exactly the Intersector Integrated Requirement (Requirement 11)
- intersectedl and intersectedr are not in the paper, they are exactly the caveat we discussed in the step-by-step guide
- intersect_promote_R corresponds to Literal Promotion (Requirement 12)
- intersect_swaps expresses that the swaps measure we use to prove well-foundedness is maintained by the intersector, so this corresponds to Requirement 9 (Measure Preservation)
Module Type Intersector.
Import SumOfProducts.
Import Generics.
Import Decidable.
Import Proof.
Parameter intersect : Tree CT -> SoP.
Parameter project : forall p : Tree CT, Sub Decidable (intersect p) (node p).
Parameter Intersected : Tree CT -> Prop.
Parameter intersected : forall p : Tree CT, TForall Intersected (intersect p).
Parameter intersectedl : forall l r : Tree CT, Intersected (branch l r) -> Intersected l.
Parameter intersectedr : forall l r : Tree CT, Intersected (branch l r) -> Intersected r.
Parameter 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').
Parameter intersect_swaps : forall (p : Tree CT) (pos : Position), tswaps (generic (intersect p)) pos <= tswaps (generic (node p)) pos.
End Intersector.
Module UIntersector (II : Intersector).
Import SumOfProducts.
Import II.
Import Generics.
Import Decidable.
Import Proof.
Definition UIntersected : SoP -> Prop
:= TForall Intersected.
Definition uintersect : SoP -> SoP
:= tbind intersect.
Lemma uintersected (sop : SoP) : UIntersected (uintersect sop).
induction sop; simpl.
apply tforall_leaf.
apply intersected.
apply tforall_branch; assumption.
Qed.
Lemma uintersect_counitd (sop : SoP) : Sub Decidable (uintersect sop) sop.
induction sop; simpl.
apply tforall_leaf.
apply project.
apply tforall_branch; [ apply sub_unionl | apply sub_unionr ]; assumption.
Qed.
Lemma uintersect_derelictd (sop sop' : SoP) : Sub Decidable sop sop' -> Sub Decidable (uintersect sop) sop'.
apply sub_transd. apply uintersect_counitd.
Qed.
Definition sub_trans_R (R : T -> T -> Prop) : (forall t1 t2 t3 t4 : T, DNF Intersected t1 -> Decidable t1 t2 -> R t2 t3 -> Decidable t3 t4 -> R t1 t4) -> forall (sop1 sop2 sop3 sop4 : SoP), UIntersected sop1 -> Sub Decidable sop1 sop2 -> Sub R sop2 sop3 -> Sub Decidable sop3 sop4 -> Sub R sop1 sop4.
intros trans sop1 sop2 sop3 sop4 pre d sub d'. induction pre.
apply tforall_leaf.
inversion d. clear d. subst. apply tforall_node. induction H1.
inversion sub. clear sub. subst. induction H2.
inversion d'. clear d'. subst. induction H3.
apply texists_node. induction H2.
apply tforall_leaf.
apply tforall_node. induction H2.
inversion H1. clear H1. subst. induction H4.
inversion H0. clear H0. subst. induction H4.
apply texists_node. revert H0 H1 H2. apply trans. apply ex_intro2 with (node (node a)); try reflexivity. apply tforall_node. assumption.
apply texists_left. apply IHTExists. apply intersectedl in H. assumption.
apply texists_right. apply IHTExists. apply intersectedr in H. assumption.
apply IHTExists. inversion H0. assumption.
apply IHTExists. inversion H0. assumption.
apply IHTExists. inversion H1. assumption.
apply IHTExists. inversion H1. assumption.
apply tforall_branch; assumption.
apply texists_left. assumption.
apply texists_right. assumption.
apply IHTExists. inversion d'. assumption.
apply IHTExists. inversion d'. assumption.
apply IHTExists. inversion sub. assumption.
apply IHTExists. inversion sub. assumption.
inversion d. apply tforall_branch; [ apply IHpre1 | apply IHpre2 ]; assumption.
Qed.
Lemma upromote' (R : T -> T -> Prop) : (forall t, R t t) -> AdmitsD R -> Inverts (DNF Intersected) R -> forall (sop sop' : SoP), TForall Intersected sop -> Sub R sop sop' -> Sub R sop (uintersect sop').
intros refl admits inverts p p' intersected sub. induction sub.
apply tforall_leaf.
inversion intersected. clear intersected. subst. induction H; simpl.
apply intersect_promote_R; try assumption. clear a0 H. intros p' sub. induction sub.
apply tforall_leaf.
apply tforall_node. induction H.
apply texists_node. apply inverts in H; [ | apply ex_intro2 with (node (node a)); try reflexivity; apply tforall_node; assumption ]. remember (ctot a). remember (ctot a0). destruct H. destruct con; destruct a; destruct a0; try (inversion Heqt; inversion Heqt0; fail).
apply ctparameter.
inversion Heqt. inversion Heqt0. subst. simpl in *. apply ctclass with c't; try assumption.
apply (H contravariant).
apply (H covariant).
apply texists_left. apply IHTExists. apply intersectedl in H1. assumption.
apply texists_right. apply IHTExists. apply intersectedr in H1. assumption.
apply tforall_branch; assumption.
apply tforall_node. apply texists_left. inversion IHTExists. assumption.
apply tforall_node. apply texists_right. inversion IHTExists. assumption.
inversion intersected. apply tforall_branch; [ apply IHsub1 | apply IHsub2 ]; assumption.
Qed.
Lemma upromote (R : T -> T -> Prop) : (forall t, R t t) -> AdmitsD R -> Inverts (DNF Intersected) R -> forall (sop sop' : SoP), Sub R (uintersect sop) sop' -> Sub R (uintersect sop) (uintersect sop').
intros. apply upromote'; try assumption. apply uintersected.
Qed.
Lemma uintersect_monod (sop sop' : SoP) : Sub Decidable sop sop' -> Sub Decidable (uintersect sop) (uintersect sop').
intro sub. apply upromote; try clear sop sop' sub.
apply Generics.DDRule.refl.
apply Decidable.Proof.proof_admits.
intros t t' _ d. induction d as [ t t' con ass rec ]. apply inversion with con; try assumption. intros req _. apply rec.
apply uintersect_derelictd. assumption.
Qed.
End UIntersector.
Module Distributive (II : Intersector).
Import II.
Import SumOfProducts.
Import Generics.
Module UIntersector := UIntersector II.
Import UIntersector.
Module I <: Comonad T DRule ORule DDRule.
Import DRule.
Import DDRule.
Module Decidable := Decidable.
Import Decidable.
Import Proof.
Definition i (t : T) := generic (uintersect (dnf t)).
Lemma counit (t : T) : Decidable (i t) t.
unfold i. apply transposel; try apply Decidable.Proof.proof_admits. induction t; simpl.
apply project.
apply project.
apply sub_meet.
apply uintersect_derelictd. apply sub_meetl. apply sub_refl. apply Generics.DDRule.refl.
apply uintersect_derelictd. apply sub_meetr. apply sub_refl. apply Generics.DDRule.refl.
apply tforall_leaf.
apply tforall_branch; [ apply sub_unionl | apply sub_unionr ]; assumption.
apply project.
Qed.
Local Lemma generic_tprod_l (l r : SoP) : Decidable (generic (tprod (@branch CT) l r)) (generic l).
revert r. induction l; simpl; intro r.
apply proof with (dbottom _). intro req. destruct req.
revert a. induction r; simpl; intro l.
apply proof with (dbottom _). intro req. destruct req.
apply proof with (dintersectionl _ _ _). simpl. intros _. apply refl.
apply proof with (dunion _ _ _). simpl. intro req. destruct req.
apply IHr1.
apply IHr2.
apply proof with (dunion _ _ _). simpl. intro req. destruct req.
apply proof with (dunionl _ _ _). simpl. intros _. apply IHl1.
apply proof with (dunionr _ _ _). simpl. intros _. apply IHl2.
Qed.
Local Lemma generic_tprod_r (l r : SoP) : Decidable (generic (tprod (@branch CT) l r)) (generic r).
revert r. induction l; simpl; intro r.
apply proof with (dbottom _). intro req. destruct req.
revert a. induction r; simpl; intro l.
apply proof with (dbottom _). intro req. destruct req.
apply proof with (dintersectionr _ _ _). simpl. intros _. apply refl.
apply proof with (dunion _ _ _). simpl. intro req. destruct req.
apply proof with (dunionl _ _ _). simpl. intros _. apply IHr1.
apply proof with (dunionr _ _ _). simpl. intros _. apply IHr2.
apply proof with (dunion _ _ _). simpl. intro req. destruct req.
apply IHl1.
apply IHl2.
Qed.
Definition Preprocessed := DNF Intersected.
Lemma i_preprocessed (t : T) : Preprocessed (i t).
apply ex_intro2 with (uintersect (dnf t)); try reflexivity. apply uintersected.
Qed.
Definition Opt {t t' : T} {con : DCon t t'} (req : DReq con) : option (Preprocessed t -> Preprocessed (DAss req left)).
destruct con; simpl in req; try (destruct req; fail).
apply Some. intro pre. simpl. destruct pre as [ sop e int ]. symmetry in e. apply intersection_generic in e. destruct e as [ l' [ r' [ el _ ] e ] ]. subst. inversion int. clear int. subst. apply intersectedl in H0. eapply ex_intro2; try reflexivity. apply tforall_node. assumption.
apply Some. intro pre. simpl. destruct pre as [ sop e int ]. symmetry in e. apply intersection_generic in e. destruct e as [ l' [ r' [ _ er ] e ] ]. subst. inversion int. clear int. subst. apply intersectedr in H0. eapply ex_intro2; try reflexivity. apply tforall_node. assumption.
apply Some. intro pre. destruct req; assumption.
apply Some. intro pre. destruct req. simpl. assumption.
apply Some. intro pre. destruct req. simpl. assumption.
apply Some. intro pre. destruct pre as [ sop e ]. symmetry in e. apply union_generic in e. destruct e as [ l' [ r' [ el er ] e ] ]. simpl. subst. inversion H. clear H. subst. destruct req; [ apply ex_intro2 with l' | apply ex_intro2 with r' ]; auto.
apply None.
Defined.
Lemma sub_admits (R : T -> T -> Prop) (admits : AdmitsD R) (sop sop' : SoP) : Sub R sop sop' -> R (generic sop) (generic sop').
intro sub. induction sub; simpl.
apply admits with (dbottom _). intro req. destruct req.
induction H; simpl.
induction H; simpl.
apply admits with (dtop _). intro req. destruct req.
induction H; simpl.
assumption.
apply admits with (dintersectionl _ _ _). simpl. intros _. assumption.
apply admits with (dintersectionr _ _ _). simpl. intros _. assumption.
apply admits with (dintersection _ _ _). simpl. intro req. destruct req; assumption.
apply admits with (dunionl _ _ _). simpl. intros _. assumption.
apply admits with (dunionr _ _ _). simpl. intros _. assumption.
apply admits with (dunion _ _ _). simpl. intro req. destruct req; assumption.
Qed.
Lemma dnf_generic (sop : SoP) : dnf (generic sop) = sop.
induction sop; simpl.
reflexivity.
induction a; simpl.
reflexivity.
destruct a; reflexivity.
rewrite IHa1. rewrite IHa2. simpl. reflexivity.
f_equal; assumption.
Qed.
Lemma i_promote_R (R : T -> T -> Prop) : (forall t, R t t) -> (forall t1 t2 t3 t4 : T, Decidable t1 t2 -> R t2 t3 -> Decidable t3 t4 -> R t1 t4) -> AdmitsD R -> Inverts Preprocessed R -> forall (t t' : T) (con : DCon t t'), Preprocessed t -> (forall req : DReq con, R (DAss req left) (DAss req right)) -> (forall req : DReq con, Preprocessed (DAss req left) -> R (DAss req left) (i (DAss req right))) -> R t (i t').
intros refl _ admits inverts t t' con pre ass _. unfold i in *. destruct pre as [ sop e dnf ]. symmetry in e. rewrite e. apply transposel; try assumption. rewrite dnf_generic. apply upromote'; try assumption. apply transposer with Intersected; try assumption.
exact intersectedl.
exact intersectedr.
rewrite <- e. apply admits with con. assumption.
Qed.
End I.
Import I.
Module WFI <: WellFoundedComonad T DRule ORule DDRule I.
Import DRule.
Module Decidable := Decidable.
Import Decidable.
Module PRule := PreprocessingRules T DRule ORule DDRule I.
Import PRule.
Fixpoint height (t : T) : nat
:= match t as t return nat with
| parameter => 1
| top => 1
| intersection l r => S (max (height l) (height r))
| bottom => 1
| union l r => S (max (height l) (height r))
| class c i o => S (max (height i) (height o))
end.
Inductive Decrease (l r l' r' : T) : Prop
:= dswaps
: plus (tswaps l left) (tswaps r right) < plus (tswaps l' left) (tswaps r' right)
-> Decrease l r l' r'
| dheightr
: plus (tswaps l left) (tswaps r right) <= plus (tswaps l' left) (tswaps r' right)
-> height r < height r'
-> Decrease l r l' r'
| dheightl
: plus (tswaps l left) (tswaps r right) <= plus (tswaps l' left) (tswaps r' right)
-> height r <= height r'
-> height l < height l'
-> Decrease l r l' r'.
Inductive Acc2 {A B : Type} (R : A -> B -> A -> B -> Prop) (a : A) (b : B) : Prop
:= acc2 : (forall (a' : A) (b' : B), R a' b' a b -> Acc2 R a' b') -> Acc2 R a b.
Lemma decrease_acc (l r : T) : Acc2 Decrease l r.
change (Acc2 Decrease (fst (l, r)) (snd (l, r))). generalize (well_founded_ltof (prod T T) (fun tt' => let (t, t') := tt' in plus (tswaps t left) (tswaps t' right)) (pair l r)). generalize (l, r). clear l r. intros p aswaps. induction aswaps as [ p _ rswaps ]. unfold ltof in rswaps. assert (plus (tswaps (fst p) left) (tswaps (snd p) right) <= plus (tswaps (fst p) left) (tswaps (snd p) right)) as lswaps; [ reflexivity | ]. revert lswaps. generalize p at 1 2 5 6. intros p' lswaps. destruct p as [ l r ]. destruct p' as [ l' r' ]. simpl in *. pose proof (well_founded_ltof T height r') as aheightr. revert l' lswaps. induction aheightr as [ r' _ rheightr ]. intros l' lswaps. unfold ltof in rheightr. assert (height r' <= height r') as lheightr; [ reflexivity | ]. revert lswaps lheightr. rename l' into l''. generalize r' at 1 2 4. intros r'' lswaps lheightr. pose proof (well_founded_ltof T height l'') as aheightl. revert r'' lswaps lheightr. induction aheightl as [ l'' _ rheightl ]. intros r'' lswaps lheightr. unfold ltof in rheightl. constructor. intros l''' r''' d. destruct d as [ dswaps | dswaps dheightr | dswaps dheightr dheightl ].
apply (rswaps (l''', r''')). unfold lt. etransitivity; [ exact dswaps | exact lswaps ].
apply rheightr.
unfold lt. etransitivity; [ exact dheightr | exact lheightr ].
unfold lt. etransitivity; [ exact dswaps | exact lswaps ].
apply rheightl.
assumption.
unfold lt. etransitivity; [ exact dswaps | exact lswaps ].
unfold lt. etransitivity; [ exact dheightr | exact lheightr ].
Qed.
Lemma max_S (l r : nat) : exists m : nat, max (S l) r = S m.
destruct r; simpl; eapply ex_intro; reflexivity.
Qed.
Lemma uintersect_swaps (sop : SoP) (pos : Position) : tswaps (generic (uintersect sop)) pos <= tswaps (generic sop) pos.
induction sop; simpl.
reflexivity.
apply intersect_swaps.
unfold tswaps. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. fold (tswaps (generic (uintersect sop1))). fold (tswaps (generic (uintersect sop2))). apply max_mono; assumption.
Qed.
Lemma tswaps_i (t : T) (pos : Position) : tswaps (i t) pos <= tswaps t pos.
unfold i. rewrite uintersect_swaps. revert pos. induction t; intro pos; unfold i; simpl; auto.
unfold tswaps at 2. rewrite (tinvariant_eq _ (intersection _ _)). simpl. fold (tswaps t1). fold (tswaps t2). etransitivity; [ | apply max_mono; [ apply IHt1 | apply IHt2 ] ]. clear IHt1 IHt2. revert pos. generalize (dnf t2). generalize (dnf t1). clear t1 t2. intro sop. induction sop; intros sop' pos; simpl.
unfold tswaps at 1. rewrite (tinvariant_eq _ bottom). simpl. apply le_0_n.
induction sop'; simpl.
unfold tswaps at 1. rewrite (tinvariant_eq _ bottom). simpl. apply le_0_n.
unfold tswaps at 1. rewrite (tinvariant_eq _ (intersection _ _)). simpl. reflexivity.
unfold tswaps at 1 3. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. apply max_lub.
etransitivity; [ apply IHsop'1 | ]. apply max_lub.
apply le_max_l.
etransitivity; [ | apply le_max_r ]. apply le_max_l.
etransitivity; [ apply IHsop'2 | ]. apply max_lub.
apply le_max_l.
etransitivity; [ | apply le_max_r ]. apply le_max_r.
unfold tswaps at 1 2. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. fold (tswaps (generic (meet sop1 sop'))). fold (tswaps (generic (meet sop2 sop'))). fold (tswaps (generic sop1)). fold (tswaps (generic sop2)). apply max_lub.
etransitivity; [ apply IHsop1 | ]. apply max_lub.
etransitivity; [ | apply le_max_l ]. apply le_max_l.
apply le_max_r.
etransitivity; [ apply IHsop2 | ]. apply max_lub.
etransitivity; [ | apply le_max_l ]. apply le_max_r.
apply le_max_r.
unfold tswaps. repeat rewrite (tinvariant_eq _ (union _ _)). simpl. apply max_mono; [ apply IHt1 | apply IHt2 ].
Qed.
Lemma i_wf (R : T -> T -> Type) : (forall t1 t2 : T, (forall (con : DCon t1 t2) (req : DReq con), R (Ass req left) (Ass req right)) -> R t1 t2) -> forall t t' : T, R t t'.
intros rec t t'. pose proof (decrease_acc t t') as acc. induction acc as [ t t' _ ind ]. apply rec. clear rec. intros con req. apply ind; clear ind. destruct con; try (destruct req; fail); simpl in *.
apply dheightl.
unfold tswaps at 3. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold (tswaps l). fold (tswaps r). apply plus_le_compat_r. apply le_max_l.
reflexivity.
simpl. apply le_n_S. apply le_max_l.
apply dheightl.
unfold tswaps at 3. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold (tswaps l). fold (tswaps r). apply plus_le_compat_r. apply le_max_r.
reflexivity.
simpl. apply le_n_S. apply le_max_r.
apply dheightr.
unfold tswaps at 4. rewrite (tinvariant_eq _ (intersection l r)). simpl. fold (tswaps l). fold (tswaps r). destruct req; apply plus_le_compat_l; [ apply le_max_l | apply le_max_r ].
destruct req; apply le_n_S; [ apply le_max_l | apply le_max_r ].
apply dheightr.
unfold tswaps at 4. rewrite (tinvariant_eq _ (union l r)). simpl. fold (tswaps l). fold (tswaps r). apply plus_le_compat_l. apply le_max_l.
apply le_n_S. apply le_max_l.
apply dheightr.
unfold tswaps at 4. rewrite (tinvariant_eq _ (union l r)). simpl. fold (tswaps l). fold (tswaps r). apply plus_le_compat_l. apply le_max_r.
apply le_n_S. apply le_max_r.
apply dheightl.
unfold tswaps at 3. rewrite (tinvariant_eq _ (union l r)). simpl. fold (tswaps l). fold (tswaps r). destruct req; apply plus_le_compat_r; [ apply le_max_l | apply le_max_r ].
destruct req; reflexivity.
simpl. apply le_n_S. destruct req; [ apply le_max_l | apply le_max_r ].
destruct req.
apply dheightr.
etransitivity; [ apply plus_le_compat_r; apply tswaps_i | ]. unfold tswaps at 3 4. repeat rewrite (tinvariant_eq _ (class _ _ _)). simpl. rename i0 into i. fold (tswaps i). fold (tswaps o). fold (tswaps i'). fold (tswaps o'). fold cswaps. apply plus_le_compat.
clear i' o'. revert i o. induction p; intros i o; simpl.
unfold cswaps. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh _ _ ]. induction linh; simpl.
apply le_max_r.
etransitivity; [ | apply le_max_l ]. apply IHlinh.
unfold cswaps. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh fin _ ]. apply fin in H. rename H into inl. clear fin. induction linh; simpl; [ destruct inl | ]. destruct inl as [ e | inl ].
subst. clear IHlinh. simpl. etransitivity; [ | apply le_max_r ]. rewrite fill_fill. etransitivity; [ apply IHp | ]. clear IHp c''t linh p c c''. fold cswaps. rewrite <- (tswaps_fill _ _ _ left). rewrite <- (tswaps_fill _ _ _ right). reflexivity.
etransitivity; [ | apply le_max_l ]. apply IHlinh.
assumption.
apply (le_max_r (S _) _).
simpl. apply le_n_S. apply le_max_r.
apply dswaps. unfold lt. etransitivity; [ apply le_n_S; apply plus_le_compat_r; apply tswaps_i | ]. unfold tswaps at 3 4. repeat rewrite (tinvariant_eq _ (class _ _ _)). simpl. rename i0 into i. fold (tswaps i). fold (tswaps o). fold (tswaps i'). fold (tswaps o'). fold cswaps. pose proof (max_S (tswaps i' left) (tswaps o' right)) as m. destruct m as [ m e ]. simpl in e. rewrite e. rewrite <- plus_Snm_nSm. simpl. apply le_n_S. rewrite (plus_comm _ m). apply plus_le_compat.
destruct (tswaps o' right).
inversion e. reflexivity.
inversion e. apply le_max_l.
clear e i' o'. revert i o. induction p; intros i o; simpl.
unfold cswaps. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh _ _ ]. induction linh; simpl.
apply le_max_l.
etransitivity; [ | apply le_max_l ]. apply IHlinh.
unfold cswaps. rewrite cinvariant_eq. simpl. destruct (pinh_finite c) as [ linh fin _ ]. apply fin in H. rename H into inl. clear fin. induction linh; simpl; [ destruct inl | ]. destruct inl as [ e | inl ].
subst. clear IHlinh. simpl. etransitivity; [ | apply le_max_r ]. rewrite fill_fill. etransitivity; [ apply IHp | ]. clear IHp c''t linh p c c''. fold cswaps. rewrite <- (tswaps_fill _ _ _ left). rewrite <- (tswaps_fill _ _ _ right). reflexivity.
etransitivity; [ | apply le_max_l ]. apply IHlinh.
assumption.
Qed.
End WFI.
Import WFI.
Module Preprocessing := Preprocessing T DRule ORule DDRule I WFI.
Lemma distributive (l r t : T) : Decidable (i (intersection (union l r) t)) (union (intersection l t) (intersection r t)).
unfold i. apply transposel; [ apply Decidable.Proof.proof_admits | ]. simpl. apply tforall_branch.
apply sub_unionl. apply uintersect_counitd.
apply sub_unionr. apply uintersect_counitd.
Qed.
End Distributive.
This page has been generated by coqdoc