Generic Classes with Unions and Intersections (Class.v)
This file contains an example of how to use the framework to formalize a type system for the purposes of Section 3. We'll specifically call out the definitions that implement things required by the framework. The type system we specify here is a simplified model for the programming language Ceylon as discussed in the paper. That is, its types Generic consist of single-argument generic types without constraints, unions, intersections, a Top type, and a Bottom type. The system is parameterized over the relations Inh and pInh. pInh is the actual inheritance relation in that it specifies the immediate inheritance declarations of classes. That is, a class declaration likeModule Generics.
Parameter Class : Type.
Parameter class_deq : forall c c' : Class, { c = c' } + { c = c' -> False }.
Inductive Generic
:= parameter : Generic
| top : Generic
| intersection : Generic -> Generic -> Generic
| bottom : Generic
| union : Generic -> Generic -> Generic
| class : Class -> Generic -> Generic -> Generic.
Lemma deq (t t' : Generic) : {t = t'} + {t = t' -> False}.
Module Deq <: DecidableType.
Definition U := Generic.
Definition eq_dec := deq.
End Deq.
Module UIP := DecidableEqDep Deq.
Fixpoint fill (i o t : Generic) : Generic
:= match t with
| parameter => o
| top => top
| intersection l r => intersection (fill i o l) (fill i o r)
| bottom => bottom
| union l r => union (fill i o l) (fill i o r)
| class c i' o' => class c (fill o i i') (fill i o o')
end.
Parameter Inh : Class -> Class -> Prop.
Parameter pInh : Class -> Class -> Generic -> Prop.
The Type Instantiation
This is the first part of where we fill in one part of our framework, defining Generic to be the type of types that the framework is reasoning about
PreInh is the reflexive, transitive closure of pInh, with appropriate subsitutions for generic type arguments.
It is not required by the framework per se.
Inductive PreInh (c : Class) : Class -> T -> Prop
:= rinh : PreInh c c parameter
| tinh (c' c'' : Class) (c't c''t : T) : pInh c c' c't -> PreInh c' c'' c''t -> PreInh c c'' (fill c't c't c''t).
Decidable/Reductive Subtyping Rules
This part is required by the framework. The inductive DCon specifies the set of subtyping rules like in Sections 3.1 and 3.2 in the paper, i.e. their constructors and components. The two argument types to DCon are the types in the conclusion, i.e. a DCon t1 t2 is a rule about when t1 is a subtype of t2. Each rule has some number of premises, but that number may vary from rule to rule. For any given rule, DReq gives us a type that lets us index into that rule's premises.- Rules like dtop are axioms, so their premise index type is Empty.
- Rules like dintersectionl have one premise, so their premise index type is unit.
- Rules like dintersection or dclass have two premises, so they have two-valued premise index types. We chose different ones for different kinds of rules, but that was not actually necessary.
Module DRule <: Rules T.
Inductive DCon : T -> T -> Type
:= dparameter : DCon parameter parameter
| dtop (t : T) : DCon t top
| dintersectionl (l r t' : T) : DCon (intersection l r) t'
| dintersectionr (l r t' : T) : DCon (intersection l r) t'
| dintersection (t l r : T) : DCon t (intersection l r)
| dbottom (t' : T) : DCon bottom t'
| dunionl (t l r : T) : DCon t (union l r)
| dunionr (t l r : T) : DCon t (union l r)
| dunion (l r t' : T) : DCon (union l r) t'
| dclass (c : Class) (i o : T) (c' : Class) (i' o' c't : T) : PreInh c c' c't -> DCon (class c i o) (class c' i' o').
Definition DReq {t t' : T} (con : DCon t t') : Type
:= match con in DCon t t' return Type with
| dparameter => Empty
| dtop _ => Empty
| dintersectionl _ _ _ => unit
| dintersectionr _ _ _ => unit
| dintersection _ _ _ => Position
| dbottom _ => Empty
| dunionl _ _ _ => unit
| dunionr _ _ _ => unit
| dunion _ _ _ => Position
| dclass _ _ _ _ _ _ _ _ => Variance
end.
Definition DAss {t t' : T} {con : DCon t t'}
:= match con as con in DCon t t' return DReq con -> Position -> T with
| dparameter => fun req => match req with end
| dtop _ => fun req => match req with end
| dintersectionl l _ t' => fun _ pos => match pos with left => l | right => t' end
| dintersectionr _ r t' => fun _ pos => match pos with left => r | right => t' end
| dintersection t l r => fun req pos => match req, pos with _, left => t | left, right => l | right, right => r end
| dbottom _ => fun req => match req with end
| dunionl t l _ => fun _ pos => match pos with left => t | right => l end
| dunionr t _ r => fun _ pos => match pos with left => t | right => r end
| dunion l r t' => fun req pos => match req, pos with _, right => t' | left, left => l | right, left => r end
| dclass c i o c' i' o' c't _ => fun req pos => match req, pos with
| covariant, left => fill i o c't
| covariant, right => o'
| contravariant, left => i'
| contravariant, right => fill o i c't
end
end.
End DRule.
Variances for Premises
In the paper, we introduced premises as having variances already. In the formalization, this is more step-by-step, so Var is a separate function that, like Ass, takes a rule and a value of its premise index type, and returns the variance of the corresponding premise. This is required by the framework.Module ORule <: OrientedRules T DRule.
Definition Var {t t' : T} {con : DCon t t'} : DReq con -> Variance
:= match con as con in DCon t t' return DReq con -> Variance with
| dparameter => fun _ => covariant
| dtop _ => fun _ => covariant
| dintersectionl l _ t' => fun _ => covariant
| dintersectionr _ r t' => fun _ => covariant
| dintersection t l r => fun _ => covariant
| dbottom _ => fun _ => covariant
| dunionl t l _ => fun _ => covariant
| dunionr t _ r => fun _ => covariant
| dunion l r t' => fun _ => covariant
| dclass c i o c' i' o' c't _ => fun req => req
end.
End ORule.
Parameter pinh_finite : forall c : Class, { l : list (prod Class T) | forall (c' : Class) (c't : T), pInh c c' c't -> In (pair c' c't) l & forall (c' : Class) (c't : T), In (pair c' c't) l -> pInh c c' c't}.
Section WF.
Inductive Mentioned (c : Class) : T -> Prop
:= mintersectionl (l r : T) : Mentioned c l -> Mentioned c (intersection l r)
| mintersectionr (l r : T) : Mentioned c r -> Mentioned c (intersection l r)
| munionl (l r : T) : Mentioned c l -> Mentioned c (union l r)
| munionr (l r : T) : Mentioned c r -> Mentioned c (union l r)
| mclassc (i o : T) : Mentioned c (class c i o)
| mclassi (c' : Class) (i o : T) : Mentioned c i -> Mentioned c (class c' i o)
| mclasso (c' : Class) (i o : T) : Mentioned c o -> Mentioned c (class c' i o).
Parameter inh_wf : well_founded Inh.
Parameter pinh_inh : forall {c c' : Class} {c't : T}, pInh c c' c't -> Inh c' c.
Parameter pinh_wf : forall (c c' : Class) (c't : T), pInh c c' c't -> forall c'' : Class, Mentioned c'' c't -> Inh c'' c.
Definition Inherited (I : T -> Type) (J : Class -> Type) (c' : prod Class T) : Type
:= prod (J (fst c')) (I parameter -> I (snd c')).
Record Invariant {I : T -> Type} {J : Class -> Type} : Type := invariant {
itop : I top;
iintersection : forall {l r : T}, I l -> I r -> I (intersection l r);
ibottom : I bottom;
iunion : forall {l r : T}, I l -> I r -> I (union l r);
iclass : forall {c : Class} {i o : T}, J c -> I i -> I o -> I (class c i o);
iinh : forall (c : Class), (let (linh, _, _) := pinh_finite c in Prod (Inherited I J) linh) -> J c
}.
Definition pinvariant (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) : forall t : T, (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t
:= fix pinvariant (t : T) : (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t
:= match t as t return (forall c : Class, Mentioned c t -> J c) -> I parameter -> I t with
| parameter => fun _ ip => ip
| top => fun _ _ => itop inv
| intersection l r => fun mc ip => iintersection inv (pinvariant l (fun c m => mc c (mintersectionl c l r m)) ip) (pinvariant r (fun c m => mc c (mintersectionr c l r m)) ip)
| bottom => fun _ _ => ibottom inv
| union l r => fun mc ip => iunion inv (pinvariant l (fun c m => mc c (munionl c l r m)) ip) (pinvariant r (fun c m => mc c (munionr c l r m)) ip)
| class c i o => fun mc' ip => let mc := mc' c (mclassc c i o)
in let mi := pinvariant i (fun c' m => mc' c' (mclassi c' c i o m)) ip
in let mo := pinvariant o (fun c' m => mc' c' (mclasso c' c i o m)) ip
in iclass inv mc mi mo
end.
Definition in_prod {A : Type} {B : A -> Type} : forall l : list A, (forall a : A, In a l -> B a) -> Prod B l
:= fix in_prod (l : list A) : (forall a : A, In a l -> B a) -> Prod B l
:= match l as l return (forall a : A, In a l -> B a) -> Prod B l with
| nil => fun _ => prod_nil _
| cons a l => fun f => prod_cons _ a l (f a (or_introl eq_refl)) (in_prod l (fun a i => f a (or_intror i)))
end.
Definition in_prod_eq {A : Type} {B : A -> Type} (l : list A) (f f' : forall a : A, In a l -> B a) : (forall (a : A) (inl : In a l), f a inl = f' a inl) -> in_prod l f = in_prod l f'.
Qed.
Definition iinvariant (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) : forall c : Class, Acc Inh c -> J c
:= fix iinvariant (c : Class) (acc : Acc Inh c) : J c
:= match acc with
| Acc_intro _ rec => iinh inv c match pinh_finite c as fin return let (linh, _, _) := fin in Prod (Inherited I J) linh with
| exist2 _ _ linh _ fin => in_prod linh (fun (c' : prod Class T) => match c' as c' return In c' linh -> Inherited I J c' with
| pair c' c't => fun i => pair (iinvariant c' (rec c' (pinh_inh (fin c' c't i)))) (pinvariant _ _ inv c't (fun c'' m => iinvariant c'' (rec c'' (pinh_wf c c' c't (fin c' c't i) c'' m))))
end)
end
end.
Definition cinvariant {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (c : Class) : J c
:= iinvariant I J inv c (inh_wf c).
Definition tinvariant {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (t : T) : I parameter -> I t
:= pinvariant I J inv t (fun c _ => cinvariant inv c).
Lemma tinvariant_eq {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (t : T) (ip : I parameter)
: tinvariant inv t ip
= match t with
| parameter => ip
| top => itop inv
| intersection l r => iintersection inv (tinvariant inv l ip) (tinvariant inv r ip)
| bottom => ibottom inv
| union l r => iunion inv (tinvariant inv l ip) (tinvariant inv r ip)
| class c i o => iclass inv (cinvariant inv c) (tinvariant inv i ip) (tinvariant inv o ip)
end.
Definition pinvariant_eq (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) (t : T) (mc mc' : forall c : Class, Mentioned c t -> J c) : (forall (c : Class) (m : Mentioned c t), mc c m = mc' c m) -> pinvariant I J inv t mc = pinvariant I J inv t mc'.
Qed.
Definition map_prod {A : Type} {B : A -> Type} (f : forall a : A, B a) : forall l : list A, Prod B l
:= fix in_prod (l : list A) : Prod B l
:= match l as l return Prod B l with
| nil => prod_nil _
| cons a l => prod_cons _ a l (f a) (in_prod l)
end.
Lemma iinvariant_eq (I : T -> Type) (J : Class -> Type) (inv : Invariant I J) (c : Class) (acc acc' : Acc Inh c) : iinvariant I J inv c acc = iinvariant I J inv c acc'.
Lemma cinvariant_eq {I : T -> Type} {J : Class -> Type} (inv : Invariant I J) (c : Class)
: cinvariant inv c
= iinh inv c match pinh_finite c as fin return let (linh, _, _) := fin in Prod (Inherited I J) linh with
| exist2 _ _ linh _ _ => map_prod (fun (c' : prod Class T) => match c' as c' return Inherited I J c' with
| pair c' c't => pair (cinvariant inv c') (tinvariant inv c't)
end) linh
end.
Definition prod_list {A : Type} {B : Type} : forall {l : list A}, Prod (fun _ => B) l -> list B
:= fix prod_list (l : list A) (p : Prod (fun _ => B) l) : list B
:= match p with
| prod_nil _ => nil
| prod_cons _ _ l b p => cons b (prod_list l p)
end.
Definition Measure (M N : Type) : Type
:= Invariant (fun _ => M) (fun _ => N).
Definition measure (M N : Type)
(mtop : M)
(mintersection : M -> M -> M)
(mbottom : M)
(munion : M -> M -> M)
(mclass : N -> M -> M -> M)
(minh_init : N)
(minh_iter : N -> N -> (M -> M) -> N)
: Measure M N.
Defined.
Definition expansion : Measure nat (nat -> nat -> nat).
Defined.
Definition texpansion := tinvariant expansion.
Definition cexpansion := cinvariant expansion.
Lemma max_mono (l l' r r' : nat) : l <= l' -> r <= r' -> max l r <= max l' r'.
Lemma expansion_mono : Invariant (fun t => forall mp mp' : nat, mp <= mp' -> texpansion t mp <= texpansion t mp') (fun c => forall mi mi' mo mo' : nat, mi <= mi' -> mo <= mo' -> cexpansion c mi mo <= cexpansion c mi' mo').
Lemma texpansion_mono (mp mp' : nat) (t : T) : mp <= mp' -> texpansion t mp <= texpansion t mp'.
Lemma cexpansion_mono (c : Class) (mi mi' mo mo' : nat) : mi <= mi' -> mo <= mo' -> cexpansion c mi mo <= cexpansion c mi' mo'.
Lemma cexpansion_i (c : Class) (mi mo : nat) : mi <= cexpansion c mi mo.
Lemma cexpansion_o (c : Class) (mi mo : nat) : mo <= cexpansion c mi mo.
Lemma cexpansion_inh (c : Class) (mi mo : nat) (c' : Class) (c't : T) (pinh : pInh c c' c't) : cexpansion c' (texpansion c't (max mo mi)) (texpansion c't (max mi mo)) <= cexpansion c mi mo.
Lemma fexpansion (i o t : T) (mp : nat) : texpansion (fill i o t) mp <= texpansion t (max (texpansion i mp) (texpansion o mp)).
Lemma fill_fill (i o i' o' t : T) : fill i o (fill i' o' t) = fill (fill o i i') (fill i o o') t.
Lemma wf (R : T -> T -> Type) : (forall t1 t2 : T, (forall (con : DCon t1 t2) (req : DReq con), R (DAss req left) (DAss req right)) -> R t1 t2) -> forall t t' : T, R t t'.
End WF.
Reflexivity and Transitivity
The next part in specifying decidable/reductive subtyping in our framework are the requirements that have to do with reflexivity, transitivity, and well-foundedness. In this module refl, Red, finite_con, and wf (the last of which was just defined above and will basically be imported here) are required by the framework. Their correspondences are explained in Decide.v, and their meaning is straightforward. The defintions of everything but refl are somewhat tedious, but that is to be expected of formalizing a type system with a medium amount of complexity in Coq. The point of our framework is that all of this proof-work can be reused for extensions to the type system.Module DDRule <: DecidableRules T DRule ORule.
Module Reduction := Reduction T DRule ORule.
Module Proof := Reduction.Proof .
Module ProofPV := Reduction.ProofPV.
Lemma refl (t : T) : Proof t t.
Lemma fill_parameter (t : T) : fill parameter parameter t = t.
Lemma fill_Rv (R : Variance -> T -> T -> Prop) (admits : AdmitsPV R) {v : Variance} {i o i' o' t : T} : R (invert v) i' i -> R v o o' -> R v (fill i o t) (fill i' o' t).
Lemma Red {t1 t2 t3 : T} (lcon : DCon t1 t2) (rcon : DCon t2 t3) : Reduction lcon rcon.
Lemma preinh_finite : forall c : Class, { l : list (prod Class T) | forall (c' : Class) (c't : T), PreInh c c' c't -> In (pair c' c't) l & forall (c' : Class) (c't : T), In (pair c' c't) l -> PreInh c c' c't}.
Definition map_filter {A B : Type} (f : A -> option B) : list A -> list B
:= fix map_filter (l : list A) : list B
:= match l with
| nil => nil
| cons a l => match f a with
| None => map_filter l
| Some b => cons b (map_filter l)
end
end.
Lemma exists_map_filter {A B : Type} (f : A -> option B) (l : list A) (a : A) (b : B) : f a = Some b -> In a l -> In b (map_filter f l).
Lemma map_filter_exists {A B : Type} (f : A -> option B) (l : list A) (b : B) : In b (map_filter f l) -> exists2 a : A, f a = Some b & In a l.
Lemma preinh_dec (c c' : Class) : { linh : list T | forall t : T, In t linh -> PreInh c c' t & forall t : T, PreInh c c' t -> In t linh }.
Definition in_map {A B : Type} : forall l : list A, (forall a : A, In a l -> B) -> list B
:= fix in_map (l : list A) : (forall a : A, In a l -> B) -> list B
:= match l as l return (forall a : A, In a l -> B) -> list B with
| nil => fun _ => nil
| cons a l => fun f => cons (f a (or_introl eq_refl)) (in_map l (fun a i => f a (or_intror i)))
end.
Definition FiniteCon (t t' : T) : Type := { lcon : list (DCon t t')
& Prod (fun con : DCon t t' => { lreq : list (DReq con) | forall req : DReq con, In req lreq }) lcon
& forall R : T -> T -> Prop, Admits R -> (forall {t1 t2 t3 t4 : T}, Proof t1 t2 -> R t2 t3 -> Proof t3 t4 -> R t1 t4) -> forall con' : DCon t t', (forall req : DReq con', R (DAss req left) (DAss req right)) -> Exists (fun con : DCon t t' => forall req : DReq con, R (DAss req left) (DAss req right)) lcon }.
Lemma finite_con {t t' : T} : FiniteCon t t'.
Definition wf := wf.
End DDRule.
Module Decidable := Decidable T DRule ORule DDRule.
Definition Decidable := Decidable.Decidable.
Traditional/Declarative Subtyping
In reverse order for the paper, we now define traditional/declarative subtyping. The rules are specified just the same as the declarative ones, but with the expectation that the framework will add explicit reflexivity and transitvity rules to them (see Tradition.v). All in all, those rules formalize the declarative literal subtyping rules for Ceylon from Figure 10 in the paper, combined with the declarative subtyping rules for unions and intersections in Figure 1.Module TRule <: Rules T.
Inductive TCon : T -> T -> Type
:= tparameter : TCon parameter parameter
| ttop (t : T) : TCon t top
| tintersectionl (l r : T) : TCon (intersection l r) l
| tintersectionr (l r : T) : TCon (intersection l r) r
| tintersection (t l r : T) : TCon t (intersection l r)
| tbottom (t' : T) : TCon bottom t'
| tunionl (l r : T) : TCon l (union l r)
| tunionr (l r : T) : TCon r (union l r)
| tunion (l r t' : T) : TCon (union l r) t'
| tinherit (c : Class) (i o : T) (c' : Class) (c't : T) : pInh c c' c't -> TCon (class c i o) (class c' (fill o i c't) (fill i o c't))
| tclass (c : Class) (i o i' o' : T) : TCon (class c i o) (class c i' o').
Definition TReq {t t' : T} (con : Con t t')
:= match con in TCon t t' return Type with
| tparameter => Empty
| ttop _ => Empty
| tintersectionl _ _ => Empty
| tintersectionr _ _ => Empty
| tintersection _ _ _ => Position
| tbottom _ => Empty
| tunionl _ _ => Empty
| tunionr _ _ => Empty
| tunion _ _ _ => Position
| tinherit _ _ _ _ _ _ => Empty
| tclass _ _ _ _ _ => Variance
end.
Definition TAss {t t' : T} {con : Con t t'}
:= match con as con in TCon t t' return TReq con -> Position -> T with
| tparameter => fun req => match req with end
| ttop _ => fun req => match req with end
| tintersectionl _ _ => fun req => match req with end
| tintersectionr _ _ => fun req => match req with end
| tintersection t l r => fun req pos => match req, pos with _, left => t | left, right => l | right, right => r end
| tbottom _ => fun req => match req with end
| tunionl _ _ => fun req => match req with end
| tunionr _ _ => fun req => match req with end
| tunion l r t' => fun req pos => match req, pos with _, right => t' | left, left => l | right, left => r end
| tinherit c i o c' c't _ => fun req => match req with end
| tclass c i o i' o' => fun req pos => match req, pos with
| covariant, left => o
| covariant, right => o'
| contravariant, left => i'
| contravariant, right => i
end
end.
End TRule.
Module Traditional := Traditional T TRule.
Translating Rules
Lastly, we need a way to translate between the traditional/declarative and the decidable/reductive subtyping rules. The two lemmas in this module are required by the framework, see Convert.v. This produces a proof that traditional/declarative and decidable/reductive subtyping in our system here are equivalent and decidable, just as in the end of Section 3 in the paper. The decidability result stems from decidable/reductive subtyping is decidable, see Decide.v.Module CRule <: Converter T TRule DRule ORule DDRule.
Module Decidable := Decidable.
Module Basic := Proofs T TRule.
Module Traditional := Traditional.
Lemma decidable_traditional_R (R : T -> T -> Prop) : Traditional.Proof.Admits R -> Decidable.Proof.Admits R.
Lemma traditional_decidable_R (R : T -> T -> Prop) : (forall t : T, R t t)
-> (forall t1 t2 t3 t4 : T, Decidable.Decidable t1 t2 -> R t2 t3 -> Decidable.Decidable t3 t4 -> R t1 t4)
-> Decidable.Proof.Admits R
-> Basic.Admits R.
End CRule.
Module Conversion := Conversion T TRule DRule ORule DDRule.
End Generics.
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).Module SumOfProducts.
Inductive Tree (A : Type) : Type
:= leaf
| node (a : A)
| branch (l r : Tree 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.
Lemma branch_tforall {A : Type} (P : A -> Prop) {l r : Tree A} : TForall P (branch l r) -> TForall P l /\ TForall P r.
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).
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.
Lemma node_texists {A : Type} (P : A -> Prop) {a : A} : TExists P (node a) -> P a.
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.
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.
Lemma sub_intersectionr (l r p : Tree CT) : SubProd r p -> SubProd (branch l r) p.
Lemma subprod_refl (refl : forall t : CT, R t t) (p : Tree CT) : SubProd p p.
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.
Lemma sub_node (sop : SoP) (p' : Tree CT) : TForall (fun p => SubProd CTR p p') sop -> Sub sop (node p').
Lemma sub_unionl (sop l r : SoP) : Sub sop l -> Sub sop (branch l r).
Lemma sub_unionr (sop l r : SoP) : Sub sop r -> Sub sop (branch l r).
Lemma sub_refl (refl : forall t : T, R t t) (sop : SoP) : Sub sop sop.
Lemma bottom_sub (sop : SoP) : Sub sop leaf -> TForall (fun p => False) sop.
Lemma node_sub (sop : SoP) (p' : Tree CT) : Sub sop (node p') -> TForall (fun p => SubProd CTR p p') sop.
Lemma sub_meet (sop l r : SoP) : Sub sop l -> Sub sop r -> Sub sop (meet l r).
Lemma sub_meetl (l r sop : SoP) : Sub l sop -> Sub (meet l r) sop.
Lemma sub_meetr (l r sop : SoP) : Sub r sop -> Sub (meet l r) sop.
Lemma sub_meet_l (sop l r : SoP) : Sub sop (meet l r) -> Sub sop l.
Lemma sub_meet_r (sop l r : SoP) : Sub sop (meet l r) -> Sub sop r.
End Sub.
Definition sub_transd (sop1 sop2 sop3 : SoP) : Sub Decidable sop1 sop2 -> Sub Decidable sop2 sop3 -> Sub Decidable sop1 sop3.
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.
Lemma top_generic (sop : SoP) : top = generic sop -> node leaf = sop.
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.
Lemma bottom_generic (sop : SoP) : bottom = generic sop -> leaf = sop.
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.
Lemma class_generic (c : Class) (i o : T) (sop : SoP) : class c i o = generic sop -> node (node (cclass c i o)) = sop.
Lemma transposel (R : T -> T -> Prop) (admits : AdmitsD R) (sop : SoP) (t' : T) : Sub R sop (dnf t') -> R (generic sop) t'.
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').
Definition swaps : Measure (Position -> nat) (nat -> nat -> nat).
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.
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.
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).
Definition UIntersected : SoP -> Prop
:= TForall Intersected.
Definition uintersect : SoP -> SoP
:= tbind intersect.
Lemma uintersected (sop : SoP) : UIntersected (uintersect sop).
Lemma uintersect_counitd (sop : SoP) : Sub Decidable (uintersect sop) sop.
Lemma uintersect_derelictd (sop sop' : SoP) : Sub Decidable sop sop' -> Sub Decidable (uintersect sop) sop'.
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.
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').
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').
Lemma uintersect_monod (sop sop' : SoP) : Sub Decidable sop sop' -> Sub Decidable (uintersect sop) (uintersect sop').
End UIntersector.
Module Distributive (II : Intersector).
Module UIntersector := UIntersector II.
Module I <: Comonad T DRule ORule DDRule.
Module Decidable := Decidable.
Definition i (t : T) := generic (uintersect (dnf t)).
Lemma counit (t : T) : Decidable (i t) t.
Qed.
Qed.
Definition Preprocessed := DNF Intersected.
Lemma i_preprocessed (t : T) : Preprocessed (i t).
Definition Opt {t t' : T} {con : DCon t t'} (req : DReq con) : option (Preprocessed t -> Preprocessed (DAss req left)).
Defined.
Lemma sub_admits (R : T -> T -> Prop) (admits : AdmitsD R) (sop sop' : SoP) : Sub R sop sop' -> R (generic sop) (generic sop').
Lemma dnf_generic (sop : SoP) : dnf (generic sop) = sop.
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').
End I.
Module WFI <: WellFoundedComonad T DRule ORule DDRule I.
Module Decidable := Decidable.
Module PRule := PreprocessingRules T DRule ORule DDRule I.
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.
Lemma max_S (l r : nat) : exists m : nat, max (S l) r = S m.
Lemma uintersect_swaps (sop : SoP) (pos : Position) : tswaps (generic (uintersect sop)) pos <= tswaps (generic sop) pos.
Lemma tswaps_i (t : T) (pos : Position) : tswaps (i t) pos <= tswaps t pos.
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'.
End 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)).
End Distributive.
Compositionality (ClassCompose.v)
Once all the machinery of ClassDistribute.v is in place, it is surprisingly simple to show how instantiations of that framework compose. The reasoning for composition is just like in Section 5 in the paper, that is, all we require is a proof that given two intersectors, applying the second one does not affect the intersected-predicate of the first one. When that is the case, all the other parts of two intersector modules easily compose.Module Type Composable (LI : Intersector) (RI : Intersector).
Parameter composable_intersect : forall t : Tree CT, LI.Intersected t -> TForall LI.Intersected (RI.intersect t).
End Composable.
Module Composor (LI : Intersector) (RI : Intersector) (c : Composable LI RI) <: Intersector.
Module RUIntersector := UIntersector RI.
Definition intersect : Tree CT -> SoP := fun (t : Tree CT) => (tbind RI.intersect) (LI.intersect t).
Lemma project : forall p : Tree CT, Sub Decidable (intersect p) (node p).
Definition Intersected : Tree CT -> Prop := fun (t : Tree CT) => LI.Intersected t /\ RI.Intersected t.
Lemma tforall_bind : forall {A B : Type} (P : Tree B -> Prop) (f : Tree A -> Tree (Tree B)) (t : Tree (Tree A)), (TForall (fun tt : Tree A => TForall P (f tt)) t) -> TForall P (tbind f t).
Lemma tforall_split : forall {A : Type} (P Q : A -> Prop) (t : Tree A), TForall P t /\ TForall Q t -> TForall (fun tt => (P tt) /\ (Q tt)) t.
Lemma tforall_split2 : forall {A : Type} (P Q : A -> Prop) (t : Tree A), TForall (fun tt => (P tt) /\ (Q tt)) t -> TForall P t /\ TForall Q t.
Lemma intersected : forall p : Tree CT, TForall Intersected (intersect p).
Lemma intersectedl : forall l r : Tree CT, Intersected (branch l r) -> Intersected l.
Lemma intersectedr : forall l r : Tree CT, Intersected (branch l r) -> Intersected r.
Lemma texists_bind : forall {A B : Type} (P : B -> Prop) (f : A -> Tree B) (t : Tree A), TExists (fun (tt : A) => TExists P (f tt)) t -> TExists P (tbind f t).
Lemma dnf_split_right : forall (P Q : Tree CT -> Prop) (t : T), DNF (fun (tt : Tree CT) => (P tt) /\ (Q tt)) t -> ((DNF P t) /\ (DNF Q t)).
Lemma sub_bind : forall (R : T -> T -> Prop) (f : Tree CT -> Tree (Tree CT)) (p : SoP) (t : Tree (Tree CT)), TExists (fun (tt : Tree CT) => Sub R p (f tt)) t -> Sub R p (tbind f t).
Lemma CTR_mono : forall (R S : T -> T -> Prop), (forall (t1 t2 : T), R t1 t2 -> S t1 t2) -> (forall (ct1 ct2 : CT), (CTR R) ct1 ct2 -> (CTR S) ct1 ct2).
Lemma sub_prod_mono : forall (R S : CT -> CT -> Prop) (l r : Tree CT), (forall (t1 t2 : CT), R t1 t2 -> S t1 t2) -> SubProd R l r -> SubProd S l r.
Lemma sub_mono : forall (R S : T -> T -> Prop) (l r : SoP), (forall (t1 t2 : T), R t1 t2 -> S t1 t2) -> Sub R l r -> Sub S l r.
Lemma intersect_promote_R : forall (R : T -> T -> Prop), AdmitsD R -> forall (p p' : Tree CT), (forall p' : Tree CT, SubProd (CTR R) p p' -> SubProd (CTInversion R) p p') -> Intersected p -> SubProd (CTR R) p p' -> Sub R (node p) (intersect p').
Lemma tswaps_union : forall (lsop rsop : SoP) (pos : Position), tswaps (union (generic lsop) (generic rsop)) pos = Nat.max (tswaps (generic lsop) pos) (tswaps (generic rsop) pos).
Lemma intersect_swaps : forall (p : Tree CT) (pos : Position), tswaps (generic (intersect p)) pos <= tswaps (generic (node p)) pos.
End Composor.
Disjointness (ClassDisjoint.v)
This file shows a simple extension implemented in the framework of ClassDistribute.v. The module type disjointness makes some assumption about a given disjointness predicate, the implementation of the intersector is straightforward from there. An interesting fact that we can prove at the end: disjointness is in fact composable after ANY other extension.Module Type Disjointness.
Parameter Disjointness : Class -> Class -> Prop.
Parameter Disjointness_symm : forall c1 c2 : Class, Disjointness c1 c2 -> Disjointness c2 c1.
Parameter Disjointness_antirefl : forall c : Class, Disjointness c c -> False.
Parameter Disjointness_inh : forall (c1 c2 c3 : Class) (t : T), Disjointness c1 c2 -> pInh c3 c1 t -> Disjointness c3 c2.
Parameter Disjointness_dec : forall c1 c2 : Class, {Disjointness c1 c2} + {~ Disjointness c1 c2}.
End Disjointness.
Module DsjIntersect (Disjointness : Disjointness) <: Intersector.
Lemma Disjointness_trans : forall (c1 c2 c3 : Class) (t : T), Disjointness c1 c2 -> PreInh c3 c1 t -> Disjointness c3 c2.
Inductive CTdsj : CT -> CT -> Prop :=
ct_dsj : forall (c1 c2 : Class) (ti1 to1 ti2 to2 : T), Disjointness c1 c2 -> CTdsj (cclass c1 ti1 to1) (cclass c2 ti2 to2).
Lemma CTdsj_dec : forall ct1 ct2 : CT, {CTdsj ct1 ct2} + {~ CTdsj ct1 ct2}.
Lemma CTdsj_symm : forall ct1 ct2 : CT, CTdsj ct1 ct2 -> CTdsj ct2 ct1.
Inductive ICTdsj : Tree CT -> CT -> Prop :=
| ict_dsj_node : forall ct ct', CTdsj ct' ct -> ICTdsj (node ct') ct
| ict_dsj_left : forall (t1 t2 : Tree CT) (ct : CT), ICTdsj t1 ct -> ICTdsj (branch t1 t2) ct
| ict_dsj_right : forall (t1 t2 : Tree CT) (ct : CT), ICTdsj t2 ct -> ICTdsj (branch t1 t2) ct
.
Lemma ICTdsj_dec : forall (t : Tree CT) (ct : CT), {ICTdsj t ct} + {~ ICTdsj t ct}.
Inductive Idsj : Tree CT -> Tree CT -> Prop :=
| i_dsj_node : forall (ct : CT) (t : Tree CT), ICTdsj t ct -> Idsj (node ct) t
| i_dsj_left : forall (t11 t12 t2 : Tree CT), Idsj t11 t2 -> Idsj (branch t11 t12) t2
| i_dsj_right : forall (t11 t12 t2 : Tree CT), Idsj t12 t2 -> Idsj (branch t11 t12) t2
.
Lemma Idsj_dec : forall t1 t2 : Tree CT, {Idsj t1 t2} + {~ Idsj t1 t2}.
Lemma Idsj_symm : forall t1 t2 : Tree CT, Idsj t1 t2 -> Idsj t2 t1.
Inductive IIntersected : Tree CT -> Prop :=
| ileaf : IIntersected leaf
| inode : forall ct : CT, IIntersected (node ct)
| ibranch : forall (t1 t2 : Tree CT), IIntersected t1 -> IIntersected t2 -> ~Idsj t1 t2 -> IIntersected (branch t1 t2).
Definition Intersected : Tree CT -> Prop := IIntersected.
Inductive NotIntersected : Tree CT -> Prop :=
| ni_left : forall (t1 t2 : Tree CT), NotIntersected t1 -> NotIntersected (branch t1 t2)
| ni_right : forall (t1 t2 : Tree CT), NotIntersected t2 -> NotIntersected (branch t1 t2)
| ni_branch : forall (t1 t2 : Tree CT), Idsj t1 t2 -> NotIntersected (branch t1 t2).
Lemma Intersected_dec : forall t : Tree CT, {Intersected t} + {~ Intersected t}.
Lemma NotIntersected_dec : forall t : Tree CT, {NotIntersected t} + {~ NotIntersected t}.
Lemma Intersected_NotIntersected : forall t : Tree CT, Intersected t <-> ~ NotIntersected t.
Lemma NotIntersected_Intersected : forall t : Tree CT, NotIntersected t <-> ~ Intersected t.
Definition intersect (t : Tree CT) : SoP :=
match (Intersected_dec t) with
| Specif.left _ => node t
| Specif.right _ => leaf
end.
Lemma project : forall p : Tree CT, Sub Decidable (intersect p) (node p).
Lemma intersected : forall p : Tree CT, TForall Intersected (intersect p).
Lemma intersectedl : forall l r : Tree CT, Intersected (branch l r) -> Intersected l.
Lemma intersectedr : forall l r : Tree CT, Intersected (branch l r) -> Intersected r.
Lemma dsj_exists : forall t1 t2 : Tree CT, Idsj t1 t2 -> TExists (fun (ct1 : CT) => TExists (fun (ct2 : CT) => CTdsj ct1 ct2) t2) t1.
Lemma ICTdsj_exists : forall (t : Tree CT) (ct : CT), ICTdsj t ct <-> TExists (fun (ct' : CT) => CTdsj ct' ct) t.
Lemma intersection_dsj_CT : forall (R : T -> T -> Prop) (ct1 ct2 : CT) (t : Tree CT), CTdsj ct1 ct2 -> TExists (fun l : CT => CTInversion R l ct1) t -> ICTdsj t ct2.
Lemma dsj_CTinversion_dsj : forall (R : T -> T -> Prop) (ct1 ct2 ct3 : CT), CTdsj ct1 ct2 -> CTInversion R ct3 ct1 -> CTdsj ct2 ct3.
Lemma Idsj_exists_ICTdsj : forall (R : T -> T -> Prop) (ct : CT) (t1 t2 : Tree CT), ICTdsj t2 ct -> TExists (fun l : CT => CTInversion R l ct) t1 -> Idsj t1 t2.
Lemma Idsj_refl_NotIntersected : forall t : Tree CT, Idsj t t -> NotIntersected t.
Lemma intersect_Idsj_sub : forall (R : T -> T -> Prop), AdmitsD R -> forall (p t1 t2 : Tree CT), SubProd (CTInversion R) p (branch t1 t2) -> Idsj t1 t2 -> NotIntersected p.
Lemma intersect_swaps : forall (p : Tree CT) (pos : Position), tswaps (generic (intersect p)) pos <= tswaps (generic (node p)) pos.
Lemma intersect_promote_R : forall (R : T -> T -> Prop), AdmitsD R -> forall (p p' : Tree CT), (forall p' : Tree CT, SubProd (CTR R) p p' -> SubProd (CTInversion R) p p') -> Intersected p -> SubProd (CTR R) p p' -> Sub R (node p) (intersect p').
End DsjIntersect.
Module DsjIntersectComposable (D : Disjointness).
Module DsjIntersect := (DsjIntersect D).
Module Type DsjComposable (I : Intersector) <: (Composable I DsjIntersect).
Lemma composable_intersect : forall t : Tree CT, I.Intersected t -> TForall I.Intersected (DsjIntersect.intersect t).
End DsjComposable.
End DsjIntersectComposable.
Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (336 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
C
Class [library]ClassCompose [library]
ClassDisjoint [library]
ClassDistribute [library]
Composable [module, in ClassCompose]
Composable.composable_intersect [axiom, in ClassCompose]
Composor [module, in ClassCompose]
Composor.CTR_mono [lemma, in ClassCompose]
Composor.dnf_split_right [lemma, in ClassCompose]
Composor.intersect [definition, in ClassCompose]
Composor.intersected [lemma, in ClassCompose]
Composor.Intersected [definition, in ClassCompose]
Composor.intersectedl [lemma, in ClassCompose]
Composor.intersectedr [lemma, in ClassCompose]
Composor.intersect_swaps [lemma, in ClassCompose]
Composor.intersect_promote_R [lemma, in ClassCompose]
Composor.project [lemma, in ClassCompose]
Composor.RUIntersector [module, in ClassCompose]
Composor.sub_mono [lemma, in ClassCompose]
Composor.sub_prod_mono [lemma, in ClassCompose]
Composor.sub_bind [lemma, in ClassCompose]
Composor.texists_bind [lemma, in ClassCompose]
Composor.tforall_split2 [lemma, in ClassCompose]
Composor.tforall_split [lemma, in ClassCompose]
Composor.tforall_bind [lemma, in ClassCompose]
Composor.tswaps_union [lemma, in ClassCompose]
D
Disjointness [module, in ClassDisjoint]Disjointness.Disjointness [axiom, in ClassDisjoint]
Disjointness.Disjointness_dec [axiom, in ClassDisjoint]
Disjointness.Disjointness_inh [axiom, in ClassDisjoint]
Disjointness.Disjointness_antirefl [axiom, in ClassDisjoint]
Disjointness.Disjointness_symm [axiom, in ClassDisjoint]
Distributive [module, in ClassDistribute]
Distributive.distributive [lemma, in ClassDistribute]
Distributive.I [module, in ClassDistribute]
Distributive.I.counit [lemma, in ClassDistribute]
Distributive.I.Decidable [module, in ClassDistribute]
Distributive.I.dnf_generic [lemma, in ClassDistribute]
Distributive.I.generic_tprod_r [lemma, in ClassDistribute]
Distributive.I.generic_tprod_l [lemma, in ClassDistribute]
Distributive.I.i [definition, in ClassDistribute]
Distributive.I.i_promote_R [lemma, in ClassDistribute]
Distributive.I.i_preprocessed [lemma, in ClassDistribute]
Distributive.I.Opt [definition, in ClassDistribute]
Distributive.I.Preprocessed [definition, in ClassDistribute]
Distributive.I.sub_admits [lemma, in ClassDistribute]
Distributive.Preprocessing [module, in ClassDistribute]
Distributive.UIntersector [module, in ClassDistribute]
Distributive.WFI [module, in ClassDistribute]
Distributive.WFI.acc2 [constructor, in ClassDistribute]
Distributive.WFI.Acc2 [inductive, in ClassDistribute]
Distributive.WFI.Decidable [module, in ClassDistribute]
Distributive.WFI.Decrease [inductive, in ClassDistribute]
Distributive.WFI.decrease_acc [lemma, in ClassDistribute]
Distributive.WFI.dheightl [constructor, in ClassDistribute]
Distributive.WFI.dheightr [constructor, in ClassDistribute]
Distributive.WFI.dswaps [constructor, in ClassDistribute]
Distributive.WFI.height [definition, in ClassDistribute]
Distributive.WFI.i_wf [lemma, in ClassDistribute]
Distributive.WFI.max_S [lemma, in ClassDistribute]
Distributive.WFI.PRule [module, in ClassDistribute]
Distributive.WFI.tswaps_i [lemma, in ClassDistribute]
Distributive.WFI.uintersect_swaps [lemma, in ClassDistribute]
DsjIntersect [module, in ClassDisjoint]
DsjIntersectComposable [module, in ClassDisjoint]
DsjIntersectComposable.DsjComposable [module, in ClassDisjoint]
DsjIntersectComposable.DsjComposable.composable_intersect [lemma, in ClassDisjoint]
DsjIntersectComposable.DsjIntersect [module, in ClassDisjoint]
DsjIntersect.CTdsj [inductive, in ClassDisjoint]
DsjIntersect.CTdsj_symm [lemma, in ClassDisjoint]
DsjIntersect.CTdsj_dec [lemma, in ClassDisjoint]
DsjIntersect.ct_dsj [constructor, in ClassDisjoint]
DsjIntersect.Disjointness_trans [lemma, in ClassDisjoint]
DsjIntersect.dsj_CTinversion_dsj [lemma, in ClassDisjoint]
DsjIntersect.dsj_exists [lemma, in ClassDisjoint]
DsjIntersect.ibranch [constructor, in ClassDisjoint]
DsjIntersect.ICTdsj [inductive, in ClassDisjoint]
DsjIntersect.ICTdsj_exists [lemma, in ClassDisjoint]
DsjIntersect.ICTdsj_dec [lemma, in ClassDisjoint]
DsjIntersect.ict_dsj_right [constructor, in ClassDisjoint]
DsjIntersect.ict_dsj_left [constructor, in ClassDisjoint]
DsjIntersect.ict_dsj_node [constructor, in ClassDisjoint]
DsjIntersect.Idsj [inductive, in ClassDisjoint]
DsjIntersect.Idsj_refl_NotIntersected [lemma, in ClassDisjoint]
DsjIntersect.Idsj_exists_ICTdsj [lemma, in ClassDisjoint]
DsjIntersect.Idsj_symm [lemma, in ClassDisjoint]
DsjIntersect.Idsj_dec [lemma, in ClassDisjoint]
DsjIntersect.IIntersected [inductive, in ClassDisjoint]
DsjIntersect.ileaf [constructor, in ClassDisjoint]
DsjIntersect.inode [constructor, in ClassDisjoint]
DsjIntersect.intersect [definition, in ClassDisjoint]
DsjIntersect.intersected [lemma, in ClassDisjoint]
DsjIntersect.Intersected [definition, in ClassDisjoint]
DsjIntersect.intersectedl [lemma, in ClassDisjoint]
DsjIntersect.intersectedr [lemma, in ClassDisjoint]
DsjIntersect.Intersected_NotIntersected [lemma, in ClassDisjoint]
DsjIntersect.Intersected_dec [lemma, in ClassDisjoint]
DsjIntersect.intersection_dsj_CT [lemma, in ClassDisjoint]
DsjIntersect.intersect_promote_R [lemma, in ClassDisjoint]
DsjIntersect.intersect_swaps [lemma, in ClassDisjoint]
DsjIntersect.intersect_Idsj_sub [lemma, in ClassDisjoint]
DsjIntersect.i_dsj_right [constructor, in ClassDisjoint]
DsjIntersect.i_dsj_left [constructor, in ClassDisjoint]
DsjIntersect.i_dsj_node [constructor, in ClassDisjoint]
DsjIntersect.ni_branch [constructor, in ClassDisjoint]
DsjIntersect.ni_right [constructor, in ClassDisjoint]
DsjIntersect.ni_left [constructor, in ClassDisjoint]
DsjIntersect.NotIntersected [inductive, in ClassDisjoint]
DsjIntersect.NotIntersected_Intersected [lemma, in ClassDisjoint]
DsjIntersect.NotIntersected_dec [lemma, in ClassDisjoint]
DsjIntersect.project [lemma, in ClassDisjoint]
G
Generics [module, in Class]Generics.bottom [constructor, in Class]
Generics.cexpansion [definition, in Class]
Generics.cexpansion_inh [lemma, in Class]
Generics.cexpansion_o [lemma, in Class]
Generics.cexpansion_i [lemma, in Class]
Generics.cexpansion_mono [lemma, in Class]
Generics.cinvariant [definition, in Class]
Generics.cinvariant_eq [lemma, in Class]
Generics.class [constructor, in Class]
Generics.Class [axiom, in Class]
Generics.class_deq [axiom, in Class]
Generics.Conversion [module, in Class]
Generics.CRule [module, in Class]
Generics.CRule.Basic [module, in Class]
Generics.CRule.Decidable [module, in Class]
Generics.CRule.decidable_traditional_R [lemma, in Class]
Generics.CRule.Traditional [module, in Class]
Generics.CRule.traditional_decidable_R [lemma, in Class]
Generics.DDRule [module, in Class]
Generics.DDRule.exists_map_filter [lemma, in Class]
Generics.DDRule.fill_Rv [lemma, in Class]
Generics.DDRule.fill_parameter [lemma, in Class]
Generics.DDRule.FiniteCon [definition, in Class]
Generics.DDRule.finite_con [lemma, in Class]
Generics.DDRule.in_map [definition, in Class]
Generics.DDRule.map_filter_exists [lemma, in Class]
Generics.DDRule.map_filter [definition, in Class]
Generics.DDRule.preinh_dec [lemma, in Class]
Generics.DDRule.preinh_finite [lemma, in Class]
Generics.DDRule.Proof [module, in Class]
Generics.DDRule.ProofPV [module, in Class]
Generics.DDRule.Red [lemma, in Class]
Generics.DDRule.Reduction [module, in Class]
Generics.DDRule.refl [lemma, in Class]
Generics.DDRule.wf [definition, in Class]
Generics.Decidable [definition, in Class]
Generics.Decidable [module, in Class]
Generics.Deq [module, in Class]
Generics.deq [lemma, in Class]
Generics.Deq.eq_dec [definition, in Class]
Generics.Deq.U [definition, in Class]
Generics.DRule [module, in Class]
Generics.DRule.Ass [definition, in Class]
Generics.DRule.Con [definition, in Class]
Generics.DRule.DAss [definition, in Class]
Generics.DRule.dbottom [constructor, in Class]
Generics.DRule.dclass [constructor, in Class]
Generics.DRule.DCon [inductive, in Class]
Generics.DRule.dintersection [constructor, in Class]
Generics.DRule.dintersectionl [constructor, in Class]
Generics.DRule.dintersectionr [constructor, in Class]
Generics.DRule.dparameter [constructor, in Class]
Generics.DRule.DReq [definition, in Class]
Generics.DRule.dtop [constructor, in Class]
Generics.DRule.dunion [constructor, in Class]
Generics.DRule.dunionl [constructor, in Class]
Generics.DRule.dunionr [constructor, in Class]
Generics.DRule.Req [definition, in Class]
Generics.expansion [definition, in Class]
Generics.expansion_mono [lemma, in Class]
Generics.fexpansion [lemma, in Class]
Generics.fill [definition, in Class]
Generics.fill_fill [lemma, in Class]
Generics.Generic [inductive, in Class]
Generics.ibottom [projection, in Class]
Generics.iclass [projection, in Class]
Generics.iinh [projection, in Class]
Generics.iintersection [projection, in Class]
Generics.iinvariant [definition, in Class]
Generics.iinvariant_eq [lemma, in Class]
Generics.Inh [axiom, in Class]
Generics.Inherited [definition, in Class]
Generics.inh_wf [axiom, in Class]
Generics.intersection [constructor, in Class]
Generics.Invariant [record, in Class]
Generics.invariant [constructor, in Class]
Generics.in_prod_eq [definition, in Class]
Generics.in_prod [definition, in Class]
Generics.itop [projection, in Class]
Generics.iunion [projection, in Class]
Generics.map_prod [definition, in Class]
Generics.max_mono [lemma, in Class]
Generics.mclassc [constructor, in Class]
Generics.mclassi [constructor, in Class]
Generics.mclasso [constructor, in Class]
Generics.measure [definition, in Class]
Generics.Measure [definition, in Class]
Generics.Mentioned [inductive, in Class]
Generics.mintersectionl [constructor, in Class]
Generics.mintersectionr [constructor, in Class]
Generics.munionl [constructor, in Class]
Generics.munionr [constructor, in Class]
Generics.ORule [module, in Class]
Generics.ORule.Var [definition, in Class]
Generics.parameter [constructor, in Class]
Generics.pInh [axiom, in Class]
Generics.pinh_wf [axiom, in Class]
Generics.pinh_inh [axiom, in Class]
Generics.pinh_finite [axiom, in Class]
Generics.pinvariant [definition, in Class]
Generics.pinvariant_eq [definition, in Class]
Generics.PreInh [inductive, in Class]
Generics.prod_list [definition, in Class]
Generics.rinh [constructor, in Class]
Generics.T [module, in Class]
Generics.texpansion [definition, in Class]
Generics.texpansion_mono [lemma, in Class]
Generics.tinh [constructor, in Class]
Generics.tinvariant [definition, in Class]
Generics.tinvariant_eq [lemma, in Class]
Generics.top [constructor, in Class]
Generics.Traditional [module, in Class]
Generics.TRule [module, in Class]
Generics.TRule.Ass [definition, in Class]
Generics.TRule.Con [definition, in Class]
Generics.TRule.Req [definition, in Class]
Generics.TRule.TAss [definition, in Class]
Generics.TRule.tbottom [constructor, in Class]
Generics.TRule.tclass [constructor, in Class]
Generics.TRule.TCon [inductive, in Class]
Generics.TRule.tinherit [constructor, in Class]
Generics.TRule.tintersection [constructor, in Class]
Generics.TRule.tintersectionl [constructor, in Class]
Generics.TRule.tintersectionr [constructor, in Class]
Generics.TRule.tparameter [constructor, in Class]
Generics.TRule.TReq [definition, in Class]
Generics.TRule.ttop [constructor, in Class]
Generics.TRule.tunion [constructor, in Class]
Generics.TRule.tunionl [constructor, in Class]
Generics.TRule.tunionr [constructor, in Class]
Generics.T.T [definition, in Class]
Generics.UIP [module, in Class]
Generics.union [constructor, in Class]
Generics.wf [lemma, in Class]
Generics.WF [section, in Class]
I
Intersector [module, in ClassDistribute]Intersector.intersect [axiom, in ClassDistribute]
Intersector.intersected [axiom, in ClassDistribute]
Intersector.Intersected [axiom, in ClassDistribute]
Intersector.intersectedl [axiom, in ClassDistribute]
Intersector.intersectedr [axiom, in ClassDistribute]
Intersector.intersect_swaps [axiom, in ClassDistribute]
Intersector.intersect_promote_R [axiom, in ClassDistribute]
Intersector.project [axiom, in ClassDistribute]
S
SumOfProducts [module, in ClassDistribute]SumOfProducts.bottom_generic [lemma, in ClassDistribute]
SumOfProducts.bottom_sub [lemma, in ClassDistribute]
SumOfProducts.branch [constructor, in ClassDistribute]
SumOfProducts.branch_tforall [lemma, in ClassDistribute]
SumOfProducts.cclass [constructor, in ClassDistribute]
SumOfProducts.class_generic [lemma, in ClassDistribute]
SumOfProducts.cparameter [constructor, in ClassDistribute]
SumOfProducts.cswaps [definition, in ClassDistribute]
SumOfProducts.CT [inductive, in ClassDistribute]
SumOfProducts.ctclass [constructor, in ClassDistribute]
SumOfProducts.CTInversion [inductive, in ClassDistribute]
SumOfProducts.ctot [definition, in ClassDistribute]
SumOfProducts.ctparameter [constructor, in ClassDistribute]
SumOfProducts.CTR [definition, in ClassDistribute]
SumOfProducts.DNF [definition, in ClassDistribute]
SumOfProducts.dnf [definition, in ClassDistribute]
SumOfProducts.generic [definition, in ClassDistribute]
SumOfProducts.intersection_generic [lemma, in ClassDistribute]
SumOfProducts.leaf [constructor, in ClassDistribute]
SumOfProducts.meet [definition, in ClassDistribute]
SumOfProducts.node [constructor, in ClassDistribute]
SumOfProducts.node_sub [lemma, in ClassDistribute]
SumOfProducts.node_texists [lemma, in ClassDistribute]
SumOfProducts.node_tforall [lemma, in ClassDistribute]
SumOfProducts.parameter_generic [lemma, in ClassDistribute]
SumOfProducts.SoP [definition, in ClassDistribute]
SumOfProducts.Sub [definition, in ClassDistribute]
SumOfProducts.Sub [section, in ClassDistribute]
SumOfProducts.SubProd [definition, in ClassDistribute]
SumOfProducts.SubProd [section, in ClassDistribute]
SumOfProducts.subprod_refl [lemma, in ClassDistribute]
SumOfProducts.SubProd.R [variable, in ClassDistribute]
SumOfProducts.sub_transd [definition, in ClassDistribute]
SumOfProducts.sub_meet_r [lemma, in ClassDistribute]
SumOfProducts.sub_meet_l [lemma, in ClassDistribute]
SumOfProducts.sub_meetr [lemma, in ClassDistribute]
SumOfProducts.sub_meetl [lemma, in ClassDistribute]
SumOfProducts.sub_meet [lemma, in ClassDistribute]
SumOfProducts.sub_refl [lemma, in ClassDistribute]
SumOfProducts.sub_unionr [lemma, in ClassDistribute]
SumOfProducts.sub_unionl [lemma, in ClassDistribute]
SumOfProducts.sub_node [lemma, in ClassDistribute]
SumOfProducts.sub_bottom [lemma, in ClassDistribute]
SumOfProducts.sub_intersectionr [lemma, in ClassDistribute]
SumOfProducts.sub_intersectionl [lemma, in ClassDistribute]
SumOfProducts.Sub.R [variable, in ClassDistribute]
SumOfProducts.swaps [definition, in ClassDistribute]
SumOfProducts.tbind [definition, in ClassDistribute]
SumOfProducts.TExists [inductive, in ClassDistribute]
SumOfProducts.texists_mono [lemma, in ClassDistribute]
SumOfProducts.texists_right [constructor, in ClassDistribute]
SumOfProducts.texists_left [constructor, in ClassDistribute]
SumOfProducts.texists_node [constructor, in ClassDistribute]
SumOfProducts.tfold [definition, in ClassDistribute]
SumOfProducts.TForall [inductive, in ClassDistribute]
SumOfProducts.tforall_mono [lemma, in ClassDistribute]
SumOfProducts.tforall_map [lemma, in ClassDistribute]
SumOfProducts.tforall_branch [constructor, in ClassDistribute]
SumOfProducts.tforall_node [constructor, in ClassDistribute]
SumOfProducts.tforall_leaf [constructor, in ClassDistribute]
SumOfProducts.tmap [definition, in ClassDistribute]
SumOfProducts.top_generic [lemma, in ClassDistribute]
SumOfProducts.tprod [definition, in ClassDistribute]
SumOfProducts.transposel [lemma, in ClassDistribute]
SumOfProducts.transposer [lemma, in ClassDistribute]
SumOfProducts.Tree [inductive, in ClassDistribute]
SumOfProducts.tswaps [definition, in ClassDistribute]
SumOfProducts.tswaps_fill [lemma, in ClassDistribute]
SumOfProducts.union_generic [lemma, in ClassDistribute]
U
UIntersector [module, in ClassDistribute]UIntersector.sub_trans_R [definition, in ClassDistribute]
UIntersector.uintersect [definition, in ClassDistribute]
UIntersector.uintersected [lemma, in ClassDistribute]
UIntersector.UIntersected [definition, in ClassDistribute]
UIntersector.uintersect_monod [lemma, in ClassDistribute]
UIntersector.uintersect_derelictd [lemma, in ClassDistribute]
UIntersector.uintersect_counitd [lemma, in ClassDistribute]
UIntersector.upromote [lemma, in ClassDistribute]
UIntersector.upromote' [lemma, in ClassDistribute]
Module Index
C
Composable [in ClassCompose]Composor [in ClassCompose]
Composor.RUIntersector [in ClassCompose]
D
Disjointness [in ClassDisjoint]Distributive [in ClassDistribute]
Distributive.I [in ClassDistribute]
Distributive.I.Decidable [in ClassDistribute]
Distributive.Preprocessing [in ClassDistribute]
Distributive.UIntersector [in ClassDistribute]
Distributive.WFI [in ClassDistribute]
Distributive.WFI.Decidable [in ClassDistribute]
Distributive.WFI.PRule [in ClassDistribute]
DsjIntersect [in ClassDisjoint]
DsjIntersectComposable [in ClassDisjoint]
DsjIntersectComposable.DsjComposable [in ClassDisjoint]
DsjIntersectComposable.DsjIntersect [in ClassDisjoint]
G
Generics [in Class]Generics.Conversion [in Class]
Generics.CRule [in Class]
Generics.CRule.Basic [in Class]
Generics.CRule.Decidable [in Class]
Generics.CRule.Traditional [in Class]
Generics.DDRule [in Class]
Generics.DDRule.Proof [in Class]
Generics.DDRule.ProofPV [in Class]
Generics.DDRule.Reduction [in Class]
Generics.Decidable [in Class]
Generics.Deq [in Class]
Generics.DRule [in Class]
Generics.ORule [in Class]
Generics.T [in Class]
Generics.Traditional [in Class]
Generics.TRule [in Class]
Generics.UIP [in Class]
I
Intersector [in ClassDistribute]S
SumOfProducts [in ClassDistribute]U
UIntersector [in ClassDistribute]Variable Index
S
SumOfProducts.SubProd.R [in ClassDistribute]SumOfProducts.Sub.R [in ClassDistribute]
Library Index
C
ClassClassCompose
ClassDisjoint
ClassDistribute
Lemma Index
C
Composor.CTR_mono [in ClassCompose]Composor.dnf_split_right [in ClassCompose]
Composor.intersected [in ClassCompose]
Composor.intersectedl [in ClassCompose]
Composor.intersectedr [in ClassCompose]
Composor.intersect_swaps [in ClassCompose]
Composor.intersect_promote_R [in ClassCompose]
Composor.project [in ClassCompose]
Composor.sub_mono [in ClassCompose]
Composor.sub_prod_mono [in ClassCompose]
Composor.sub_bind [in ClassCompose]
Composor.texists_bind [in ClassCompose]
Composor.tforall_split2 [in ClassCompose]
Composor.tforall_split [in ClassCompose]
Composor.tforall_bind [in ClassCompose]
Composor.tswaps_union [in ClassCompose]
D
Distributive.distributive [in ClassDistribute]Distributive.I.counit [in ClassDistribute]
Distributive.I.dnf_generic [in ClassDistribute]
Distributive.I.generic_tprod_r [in ClassDistribute]
Distributive.I.generic_tprod_l [in ClassDistribute]
Distributive.I.i_promote_R [in ClassDistribute]
Distributive.I.i_preprocessed [in ClassDistribute]
Distributive.I.sub_admits [in ClassDistribute]
Distributive.WFI.decrease_acc [in ClassDistribute]
Distributive.WFI.i_wf [in ClassDistribute]
Distributive.WFI.max_S [in ClassDistribute]
Distributive.WFI.tswaps_i [in ClassDistribute]
Distributive.WFI.uintersect_swaps [in ClassDistribute]
DsjIntersectComposable.DsjComposable.composable_intersect [in ClassDisjoint]
DsjIntersect.CTdsj_symm [in ClassDisjoint]
DsjIntersect.CTdsj_dec [in ClassDisjoint]
DsjIntersect.Disjointness_trans [in ClassDisjoint]
DsjIntersect.dsj_CTinversion_dsj [in ClassDisjoint]
DsjIntersect.dsj_exists [in ClassDisjoint]
DsjIntersect.ICTdsj_exists [in ClassDisjoint]
DsjIntersect.ICTdsj_dec [in ClassDisjoint]
DsjIntersect.Idsj_refl_NotIntersected [in ClassDisjoint]
DsjIntersect.Idsj_exists_ICTdsj [in ClassDisjoint]
DsjIntersect.Idsj_symm [in ClassDisjoint]
DsjIntersect.Idsj_dec [in ClassDisjoint]
DsjIntersect.intersected [in ClassDisjoint]
DsjIntersect.intersectedl [in ClassDisjoint]
DsjIntersect.intersectedr [in ClassDisjoint]
DsjIntersect.Intersected_NotIntersected [in ClassDisjoint]
DsjIntersect.Intersected_dec [in ClassDisjoint]
DsjIntersect.intersection_dsj_CT [in ClassDisjoint]
DsjIntersect.intersect_promote_R [in ClassDisjoint]
DsjIntersect.intersect_swaps [in ClassDisjoint]
DsjIntersect.intersect_Idsj_sub [in ClassDisjoint]
DsjIntersect.NotIntersected_Intersected [in ClassDisjoint]
DsjIntersect.NotIntersected_dec [in ClassDisjoint]
DsjIntersect.project [in ClassDisjoint]
G
Generics.cexpansion_inh [in Class]Generics.cexpansion_o [in Class]
Generics.cexpansion_i [in Class]
Generics.cexpansion_mono [in Class]
Generics.cinvariant_eq [in Class]
Generics.CRule.decidable_traditional_R [in Class]
Generics.CRule.traditional_decidable_R [in Class]
Generics.DDRule.exists_map_filter [in Class]
Generics.DDRule.fill_Rv [in Class]
Generics.DDRule.fill_parameter [in Class]
Generics.DDRule.finite_con [in Class]
Generics.DDRule.map_filter_exists [in Class]
Generics.DDRule.preinh_dec [in Class]
Generics.DDRule.preinh_finite [in Class]
Generics.DDRule.Red [in Class]
Generics.DDRule.refl [in Class]
Generics.deq [in Class]
Generics.expansion_mono [in Class]
Generics.fexpansion [in Class]
Generics.fill_fill [in Class]
Generics.iinvariant_eq [in Class]
Generics.max_mono [in Class]
Generics.texpansion_mono [in Class]
Generics.tinvariant_eq [in Class]
Generics.wf [in Class]
S
SumOfProducts.bottom_generic [in ClassDistribute]SumOfProducts.bottom_sub [in ClassDistribute]
SumOfProducts.branch_tforall [in ClassDistribute]
SumOfProducts.class_generic [in ClassDistribute]
SumOfProducts.intersection_generic [in ClassDistribute]
SumOfProducts.node_sub [in ClassDistribute]
SumOfProducts.node_texists [in ClassDistribute]
SumOfProducts.node_tforall [in ClassDistribute]
SumOfProducts.parameter_generic [in ClassDistribute]
SumOfProducts.subprod_refl [in ClassDistribute]
SumOfProducts.sub_meet_r [in ClassDistribute]
SumOfProducts.sub_meet_l [in ClassDistribute]
SumOfProducts.sub_meetr [in ClassDistribute]
SumOfProducts.sub_meetl [in ClassDistribute]
SumOfProducts.sub_meet [in ClassDistribute]
SumOfProducts.sub_refl [in ClassDistribute]
SumOfProducts.sub_unionr [in ClassDistribute]
SumOfProducts.sub_unionl [in ClassDistribute]
SumOfProducts.sub_node [in ClassDistribute]
SumOfProducts.sub_bottom [in ClassDistribute]
SumOfProducts.sub_intersectionr [in ClassDistribute]
SumOfProducts.sub_intersectionl [in ClassDistribute]
SumOfProducts.texists_mono [in ClassDistribute]
SumOfProducts.tforall_mono [in ClassDistribute]
SumOfProducts.tforall_map [in ClassDistribute]
SumOfProducts.top_generic [in ClassDistribute]
SumOfProducts.transposel [in ClassDistribute]
SumOfProducts.transposer [in ClassDistribute]
SumOfProducts.tswaps_fill [in ClassDistribute]
SumOfProducts.union_generic [in ClassDistribute]
U
UIntersector.uintersected [in ClassDistribute]UIntersector.uintersect_monod [in ClassDistribute]
UIntersector.uintersect_derelictd [in ClassDistribute]
UIntersector.uintersect_counitd [in ClassDistribute]
UIntersector.upromote [in ClassDistribute]
UIntersector.upromote' [in ClassDistribute]
Constructor Index
D
Distributive.WFI.acc2 [in ClassDistribute]Distributive.WFI.dheightl [in ClassDistribute]
Distributive.WFI.dheightr [in ClassDistribute]
Distributive.WFI.dswaps [in ClassDistribute]
DsjIntersect.ct_dsj [in ClassDisjoint]
DsjIntersect.ibranch [in ClassDisjoint]
DsjIntersect.ict_dsj_right [in ClassDisjoint]
DsjIntersect.ict_dsj_left [in ClassDisjoint]
DsjIntersect.ict_dsj_node [in ClassDisjoint]
DsjIntersect.ileaf [in ClassDisjoint]
DsjIntersect.inode [in ClassDisjoint]
DsjIntersect.i_dsj_right [in ClassDisjoint]
DsjIntersect.i_dsj_left [in ClassDisjoint]
DsjIntersect.i_dsj_node [in ClassDisjoint]
DsjIntersect.ni_branch [in ClassDisjoint]
DsjIntersect.ni_right [in ClassDisjoint]
DsjIntersect.ni_left [in ClassDisjoint]
G
Generics.bottom [in Class]Generics.class [in Class]
Generics.DRule.dbottom [in Class]
Generics.DRule.dclass [in Class]
Generics.DRule.dintersection [in Class]
Generics.DRule.dintersectionl [in Class]
Generics.DRule.dintersectionr [in Class]
Generics.DRule.dparameter [in Class]
Generics.DRule.dtop [in Class]
Generics.DRule.dunion [in Class]
Generics.DRule.dunionl [in Class]
Generics.DRule.dunionr [in Class]
Generics.intersection [in Class]
Generics.invariant [in Class]
Generics.mclassc [in Class]
Generics.mclassi [in Class]
Generics.mclasso [in Class]
Generics.mintersectionl [in Class]
Generics.mintersectionr [in Class]
Generics.munionl [in Class]
Generics.munionr [in Class]
Generics.parameter [in Class]
Generics.rinh [in Class]
Generics.tinh [in Class]
Generics.top [in Class]
Generics.TRule.tbottom [in Class]
Generics.TRule.tclass [in Class]
Generics.TRule.tinherit [in Class]
Generics.TRule.tintersection [in Class]
Generics.TRule.tintersectionl [in Class]
Generics.TRule.tintersectionr [in Class]
Generics.TRule.tparameter [in Class]
Generics.TRule.ttop [in Class]
Generics.TRule.tunion [in Class]
Generics.TRule.tunionl [in Class]
Generics.TRule.tunionr [in Class]
Generics.union [in Class]
S
SumOfProducts.branch [in ClassDistribute]SumOfProducts.cclass [in ClassDistribute]
SumOfProducts.cparameter [in ClassDistribute]
SumOfProducts.ctclass [in ClassDistribute]
SumOfProducts.ctparameter [in ClassDistribute]
SumOfProducts.leaf [in ClassDistribute]
SumOfProducts.node [in ClassDistribute]
SumOfProducts.texists_right [in ClassDistribute]
SumOfProducts.texists_left [in ClassDistribute]
SumOfProducts.texists_node [in ClassDistribute]
SumOfProducts.tforall_branch [in ClassDistribute]
SumOfProducts.tforall_node [in ClassDistribute]
SumOfProducts.tforall_leaf [in ClassDistribute]
Axiom Index
C
Composable.composable_intersect [in ClassCompose]D
Disjointness.Disjointness [in ClassDisjoint]Disjointness.Disjointness_dec [in ClassDisjoint]
Disjointness.Disjointness_inh [in ClassDisjoint]
Disjointness.Disjointness_antirefl [in ClassDisjoint]
Disjointness.Disjointness_symm [in ClassDisjoint]
G
Generics.Class [in Class]Generics.class_deq [in Class]
Generics.Inh [in Class]
Generics.inh_wf [in Class]
Generics.pInh [in Class]
Generics.pinh_wf [in Class]
Generics.pinh_inh [in Class]
Generics.pinh_finite [in Class]
I
Intersector.intersect [in ClassDistribute]Intersector.intersected [in ClassDistribute]
Intersector.Intersected [in ClassDistribute]
Intersector.intersectedl [in ClassDistribute]
Intersector.intersectedr [in ClassDistribute]
Intersector.intersect_swaps [in ClassDistribute]
Intersector.intersect_promote_R [in ClassDistribute]
Intersector.project [in ClassDistribute]
Inductive Index
D
Distributive.WFI.Acc2 [in ClassDistribute]Distributive.WFI.Decrease [in ClassDistribute]
DsjIntersect.CTdsj [in ClassDisjoint]
DsjIntersect.ICTdsj [in ClassDisjoint]
DsjIntersect.Idsj [in ClassDisjoint]
DsjIntersect.IIntersected [in ClassDisjoint]
DsjIntersect.NotIntersected [in ClassDisjoint]
G
Generics.DRule.DCon [in Class]Generics.Generic [in Class]
Generics.Mentioned [in Class]
Generics.PreInh [in Class]
Generics.TRule.TCon [in Class]
S
SumOfProducts.CT [in ClassDistribute]SumOfProducts.CTInversion [in ClassDistribute]
SumOfProducts.TExists [in ClassDistribute]
SumOfProducts.TForall [in ClassDistribute]
SumOfProducts.Tree [in ClassDistribute]
Projection Index
G
Generics.ibottom [in Class]Generics.iclass [in Class]
Generics.iinh [in Class]
Generics.iintersection [in Class]
Generics.itop [in Class]
Generics.iunion [in Class]
Section Index
G
Generics.WF [in Class]S
SumOfProducts.Sub [in ClassDistribute]SumOfProducts.SubProd [in ClassDistribute]
Definition Index
C
Composor.intersect [in ClassCompose]Composor.Intersected [in ClassCompose]
D
Distributive.I.i [in ClassDistribute]Distributive.I.Opt [in ClassDistribute]
Distributive.I.Preprocessed [in ClassDistribute]
Distributive.WFI.height [in ClassDistribute]
DsjIntersect.intersect [in ClassDisjoint]
DsjIntersect.Intersected [in ClassDisjoint]
G
Generics.cexpansion [in Class]Generics.cinvariant [in Class]
Generics.DDRule.FiniteCon [in Class]
Generics.DDRule.in_map [in Class]
Generics.DDRule.map_filter [in Class]
Generics.DDRule.wf [in Class]
Generics.Decidable [in Class]
Generics.Deq.eq_dec [in Class]
Generics.Deq.U [in Class]
Generics.DRule.Ass [in Class]
Generics.DRule.Con [in Class]
Generics.DRule.DAss [in Class]
Generics.DRule.DReq [in Class]
Generics.DRule.Req [in Class]
Generics.expansion [in Class]
Generics.fill [in Class]
Generics.iinvariant [in Class]
Generics.Inherited [in Class]
Generics.in_prod_eq [in Class]
Generics.in_prod [in Class]
Generics.map_prod [in Class]
Generics.measure [in Class]
Generics.Measure [in Class]
Generics.ORule.Var [in Class]
Generics.pinvariant [in Class]
Generics.pinvariant_eq [in Class]
Generics.prod_list [in Class]
Generics.texpansion [in Class]
Generics.tinvariant [in Class]
Generics.TRule.Ass [in Class]
Generics.TRule.Con [in Class]
Generics.TRule.Req [in Class]
Generics.TRule.TAss [in Class]
Generics.TRule.TReq [in Class]
Generics.T.T [in Class]
S
SumOfProducts.cswaps [in ClassDistribute]SumOfProducts.ctot [in ClassDistribute]
SumOfProducts.CTR [in ClassDistribute]
SumOfProducts.DNF [in ClassDistribute]
SumOfProducts.dnf [in ClassDistribute]
SumOfProducts.generic [in ClassDistribute]
SumOfProducts.meet [in ClassDistribute]
SumOfProducts.SoP [in ClassDistribute]
SumOfProducts.Sub [in ClassDistribute]
SumOfProducts.SubProd [in ClassDistribute]
SumOfProducts.sub_transd [in ClassDistribute]
SumOfProducts.swaps [in ClassDistribute]
SumOfProducts.tbind [in ClassDistribute]
SumOfProducts.tfold [in ClassDistribute]
SumOfProducts.tmap [in ClassDistribute]
SumOfProducts.tprod [in ClassDistribute]
SumOfProducts.tswaps [in ClassDistribute]
U
UIntersector.sub_trans_R [in ClassDistribute]UIntersector.uintersect [in ClassDistribute]
UIntersector.UIntersected [in ClassDistribute]
Record Index
G
Generics.Invariant [in Class]Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (336 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
This page has been generated by coqdoc