Proof of the more general integration process

Introduction 

This document gives an overview of the Coq formalization we have created for our more general framework that handles Integrated Subtyping for general type systems, not just those with union and intersection types, as discussed in section 7 of the paper.
In case you are not familiar with Coq's module system: we implemented this formalization as a library for people to use. A "Module Type" specifies a signature that a user needs to implement; "Parameter"s within that module type are the specific things a user needs to provide/proof. Once a user instantiated a module type in a module of their own, they can use that to instantiate our "Module"s, which provide the extended systems/proofs based on the user's input.
This file contains only the signatures of the various components of our proof, but for each file (.v), there is a link at the beginning of the section corresponding to that file that leads to the coqdoc for the full file including the actual proof code. The .v-files themselves are also included and can be used to verify the proofs in Coq. The files should be compiled in the order in which they appear in this file.
The following table gives an outline of the parts of our paper and where to find their corresponding counterpart in this formalization:
Concept from PaperCorresponding Proof PartComment
Literals & TypesTyp.T in Common.vGeneralized to arbitrary types, all user-provided
User-Defined Subtyping RulesRules.Con, Rules.Req, Rules.Ass in Common.v
Declarative Subtyping RulesTraditional.TransRefl.TRCon etc. in Tradition.vin our original formalization, we used the term "Traditional" instead of "Declarative"
Reductive Subtyping Rulessee User-Defined Typing RulesWhile Declarative Rules add reflexivity and transitivity, Reductive Rules are all user-supplied in this more general framework
Requirement 1: Syntax-DirectednessDecidableRules.finite_con in Decide.v
Requirement 2: Well-FoundednessDecidableRules.wf in Decide.v
Requirement 3: Literal ReflexivityDecidableRules.refl in Decide.vSince everything is a literal/type, this captures all types
Subtyping Rules with AssumptionsProofPV.ProofPV etc. in Common.v
Requirement 4: R-to-D Literal ConversionConverter.decidable_traditional_R in Convert.v
Requirement 5: D-to-R Literal ConversionConverter.traditional_decidable_R in Convert.v
Requirement 6: Literal TransitivityDecidableRules.Red in Decide.vSee also Reduction.Reduction in Common.v
Decidability of Declarative Subtyping TheoremConversion.decidable_traditional and Conversion.traditional_decidable in Convert.vTogether with Decider.decider in Decide.v
Extended SubtypingExtension.Con and ExtendedRules.ECon etc. in Extend.v
Intersector/IntegratorComonad.i in Preprocess.vSince everything is a literal/type, there is no distinction between intersector and integrator
Requirement 7: Intersector CompletenessEquivocator.iextended in Equate.v
Requirement 8: Intersector SoundnessEquivocator.unit in Equate.v
Lemma 1: Integrated SoundnessEquivalence.ipreprocessing_extended in Equate.v
Requirement 9: Measure PreservationWellFoundedComonad.i_wf in Preprocess.vRequires full well-foundedness proof instead of measure preservation
Lemma 2: Integrated DecidabilityDecider.decider in Preprocess.v
Requirement 10: Literal DerelictionComonad.counit in Preprocess.v
Lemma 3: DerelictionComonad.counit in Preprocess.vSame as Requirement 10 due to missing type/literal distinction
Intersected PredicateComonad.Preprocessed in Preprocess.v
Requirement 11: Intersector IntegratedComonad.i_Preprocessed in Preprocess.v
Lemma 4: Integrator IntegratedComonad.i_Preprocessed in Preprocess.vSame as Requirement 11 due to missing type/literal distinction
Requirement 12: Literal PromotionComonad.i_promote_R in Preprocess.v
Lemma 5: PromotionPreprocessing.dpromote' in Preprocess.v
Lemma 6: Integrated Monotonicity-Helper Lemmas, established in various different forms in Preprocess.v
Lemma 7: Integrated Assumptions-
Lemma 8: Integrated PromotionPreprocessing.promote in Preprocess.v
Lemma 9: Integrated ReflexivityComonad.derelict and Comonad.refl in Preprocess.v
Lemma 10: D-to-I Literal ConversionEquivalence.iadmitst in Equate.v
Lemma 11: Integrated TransitivityPreprocessing.itrans in Preprocess.v
Lemma 12: Integrated CompletenessEquivalence.extended_ipreprocessing in Equate.v
Decidability of Extended Subtyping TheoremEquivalence.decider in Equate.v
All of this was generated using coqdoc, whose approach to links in the face of modules is not the most helpful one. However, other syntax highlighting features depend on the same information as link generation, so the code should still be a lot more readable than without links. We made sure that links in standard HTML rendering (blue underlined) lead to where they should, and most of the links should get you at least closer to where the definition you wanted to was.

Common Definitions (Common.v)

This module defines our formalization of subtyping proof rules and proofs that lie at the heart of our system.

Inductive Empty : Type :=.
Inductive Position : Type := left | right.

User-Defined Types

With modules of this type, a user provides the syntactic representation of types in the system at hand
Module Type Typ.
Parameter T : Type.
End Typ.

User-Defined Proof Rules

Each proof rule has two components:
  • A conclusion Con, which here both identifies the proof rule in question and relates the sub- and supertype in the conclusion
  • A set of requirements Req (also known as Premises). Each requirement specifies a subtyping that needs to hold, and so for each Req, Ass provides the left (subtype) or right (supertype) component of that subtyping.
Thus, typically, Con is an inductive type specifying the subtyping rules by just their conclusions. Then, Req is a function matching on Con, returning a type that can be used to index into the premises. For example, Empty is defined above for convenience for those rules that do not have any premises. Similarly unit can be used for rules with one premise, and Position for rules with two premises. This only really comes in in the definition of Ass, which, for a given Con, matches on a Req for that con to find the right premis, and then matches on Position to return either the sub- or supertype of that premise.
Module Type Rules (T : Typ).
Parameter Con : T -> T -> Type.
Parameter Req : forall {t t' : T}, Con t t' -> Type.
Parameter Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T.
End Rules.

Proofs

Formalizes proofs constructed using the user-defined proof rules above. An arbitrary relation on types is said to admit (Admits) the user-defined proof rules if, for each rule, if the parts of all its premises are related, the parts of the conclusion are also related. Some proofs are just parameterized over relations that Admit some other relation; in the paper, we cover all these cases via proofs with assumptions. The inductive Proof represents full subtyping proofs between its two arguments.
Module Proofs (T : Typ) (Rule : Rules T).

Definition Admits (R : T -> T -> Type) : Type
:= forall (t1 t2 : T) (con : Con t1 t2), (forall (req : Req con), R (Ass req left) (Ass req right)) -> R t1 t2.

Inductive Proof : T -> T -> Prop
:= proof : Admits Proof.
Lemma proof_admits : Admits Proof.

Traces

Traces let us reason about a specific path from a conclusion to an axiom/assumption in a subtytping proof. They are used in some internal proofs of the system and do not show up in the paper at all.
Section Trace.

Inductive Trace (t t' : T) : T -> T -> Type
:= assumption : Trace t t' t t'
 | recursion (t1 t2 : T) (con : Con t1 t2) (req : Req con) : Trace t t' (Ass req left) (Ass req right) -> Trace t t' t1 t2.

Lemma trace_ind (R : T -> T -> Type) (t1 t2 : T) : R t1 t2 -> (forall (t1' t2' : T) (con : Con t1' t2') (req : Req con), R t1' t2' -> R (Ass req left) (Ass req right)) -> forall t1' t2' : T, Trace t1' t2' t1 t2 -> R t1' t2'.

Lemma trace_comp {t1 t2 t1' t2' t1'' t2'' : T} : Trace t1 t2 t1' t2' -> Trace t1' t2' t1'' t2'' -> Trace t1 t2 t1'' t2''.
Lemma trace_comp' {t1 t2 t1' t2' t1'' t2'' : T} : Trace t1' t2' t1'' t2'' -> Trace t1 t2 t1' t2' -> Trace t1 t2 t1'' t2''.

End Trace.

Inversion

Since we often accept a general relation of types that just Admits a known one (usually Decidable, i.e. reductive subtyping), we can usually not examine how a particular subtyping relation was proven. This section characterizes relations that are invertible up to a certain point, namely up to where the left-hand side stops satisfying a given predicate on types, usually Preprocessed, i.e. "integrated". In the paper, we did not need this, because we could always induct over the union/intersection-part of subtyping proof until we got to applications of the literal subtyping rule, which is the intuition for what inversion does here.
Section Inversion.

Inductive Inversion (P : T -> Prop) (R : T -> T -> Prop) : T -> T -> Prop
:= inversion (t t' : T) (con : Con t t') : (forall req : Req con, R (Ass req left) (Ass req right)) -> (forall req : Req con, P (Ass req left) -> Inversion P R (Ass req left) (Ass req right)) -> Inversion P R t t'.

Definition Inverts (P : T -> Prop) (R : T -> T -> Prop) : Prop := forall t t' : T, P t -> R t t' -> Inversion P R t t'.

End Inversion.

Proofs with Assumptions (but not variance)

Formalizes proofs that allow a certain set of additional subtyping relations to be given as assumptions, i.e. these proofs are proof trees based on the user-defined rules with some additional axioms based on a given relation. This is a first step towards the subtyping relations with variance and assumptions in the paper; as we mention there, the variance part is not actually necessary to formalize translations between declarative and reductive rules, so the two are separated out in the formal proof.

Section ProofP.

Definition AdmitsP (R : T -> T -> Prop) : Prop
:= forall (t t' : T) (con : Con t t'), (forall (req : Req con), R (Ass req left) (Ass req right)) -> R t t'.

Inductive ProofP (P : T -> T -> Prop) : T -> T -> Prop
:= permit (t t' : T) : P t t' -> ProofP P t t'
 | proofP : AdmitsP (ProofP P).

Lemma mono {P P' : T -> T -> Prop} : (forall (t t' : T), P t t' -> P' t t') -> forall {t t' : T}, ProofP P t t' -> ProofP P' t t'.

Lemma bind (P P' : T -> T -> Prop) (bind : forall (t t' : T), P t t' -> ProofP P' t t') {t t' : T} : ProofP P t t' -> ProofP P' t t'.

Lemma proof_proofP {t t' : T} : Proof t t' -> ProofP (fun t t' => False) t t'.

Lemma proofP_proof {t t' : T} : ProofP (fun t t' => False) t t' -> Proof t t'.

End ProofP.

End Proofs.

Full Proofs with Assumptions and Variance

Corresponds to the extensions we make to subtyping rules to get subtyping rules with assumptions in the paper. Variances are added to each premise via OrientedRules.Var (in the paper, we formalized premises to have a variance component from the start). ProofPV.AdmitsPV contains the multiplication of variances for literal (here: all) rules, and ProofPV.ProofPV patches in the possiblity to match on given assumptions P.
Inductive Variance : Type := covariant | contravariant.
Definition invert (v : Variance) : Variance
:= match v with covariant => contravariant | contravariant => covariant end.
Lemma invert_invert (v : Variance) : invert (invert v) = v.
Definition multiply (v v' : Variance) : Variance
:= match v with covariant => v' | contravariant => invert v' end.
Lemma multiply_invert (v v' : Variance) : multiply (invert v) v' = invert (multiply v v').
Lemma multiply_covariant (v : Variance) : multiply v covariant = v.

Inductive Prod {A : Type} (B : A -> Type) : list A -> Type
:= prod_nil : Prod B nil
 | prod_cons (a : A) (l : list A) : B a -> Prod B l -> Prod B (cons a l).

Module Type OrientedRules (T : Typ) (Rule : Rules T).
Parameter Var : forall {t t' : T} {con : Con t t'}, Req con -> Variance.
End OrientedRules.

Module ProofPV (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule).
Module Proof := Proofs T Rule.

Definition AdmitsPV (R : Variance -> T -> T -> Prop) : Prop
:= forall (v : Variance) {t t' : T} (con : Con t t'), (forall (req : Req con), R (multiply v (Var req)) (Ass req left) (Ass req right)) -> R v t t'.

Inductive ProofPV (P : Variance -> T -> T -> Prop) : Variance -> T -> T -> Prop
:= permitV (v : Variance) (t t' : T) : P v t t' -> ProofPV P v t t'
 | proofPV : AdmitsPV (ProofPV P).

Lemma proof_admitsPV (P : Variance -> T -> T -> Prop) : AdmitsPV (ProofPV P).

Lemma monoV {P P' : Variance -> T -> T -> Prop} : (forall (v : Variance) (t t' : T), P v t t' -> P' v t t') -> forall {v : Variance} {t t' : T}, ProofPV P v t t' -> ProofPV P' v t t'.

Lemma invertPV (v : Variance) {P : Variance -> T -> T -> Prop} : forall {t t' : T}, ProofPV P v t t' -> ProofPV (fun v t t' => P (invert v) t t') (invert v) t t'.

Lemma invertPV' (v : Variance) {P P' : Variance -> T -> T -> Prop} : (forall (v : Variance) (t t' : T), P v t t' -> P' (invert v) t t') -> forall {t t' : T}, ProofPV P v t t' -> ProofPV P' (invert v) t t'.

Lemma bindV (P P' : Variance -> T -> T -> Prop) (bind : forall (v : Variance) (t t' : T), P v t t' -> ProofPV P' v t t') {v : Variance} {t t' : T} : ProofPV P v t t' -> ProofPV P' v t t'.

Lemma proofP_proofPV (v : Variance) {P : T -> T -> Prop} {t t' : T} : ProofP P t t' -> ProofPV (fun v => P) v t t'.

Lemma proofPV_proofP {v : Variance} {P : T -> T -> Prop} {t t' : T} : ProofPV (fun v => P) v t t' -> ProofP P t t'.

Lemma proof_proofPV (v : Variance) {t t' : T} : Proof t t' -> ProofPV (fun v t t' => False) v t t'.

Lemma proofPV_proof {v : Variance} {t t' : T} : ProofPV (fun v t t' => False) v t t' -> Proof t t'.

End ProofPV.

Reduction

This module expresses the core component of the decidability proof for Reductive Subtpying: Reduction encodes essentially the requirements of Literal transitivity that there must be a way to make progress by somehow combining two proof rules that have a middle type in common. Requires is a convenience predicate to get at all the components of all the premises of a rule easily. Transitivity and CoXposition encode the possibility that assumptions switch sides due to contravariance.
Module Reduction (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule).
Module ProofPV := ProofPV T Rule ORule.
Module Proof := ProofPV.Proof.

Inductive Composition (L R : Variance -> T -> T -> Prop) (t1 t3 : T) : Prop
:= compose (t2 : T) : L covariant t1 t2 -> R covariant t2 t3 -> Composition L R t1 t3.
Inductive Contraposition (L R : Variance -> T -> T -> Prop) (t1 t3 : T) : Prop
:= contrapose (t2 : T) : R contravariant t1 t2 -> L contravariant t2 t3 -> Contraposition L R t1 t3.

Definition Comaposition (L R : Variance -> T -> T -> Prop) (v : Variance) : T -> T -> Prop
:= match v with covariant => Composition L R | contravariant => Contraposition L R end.

Inductive Transitivity (L R : Variance -> T -> T -> Prop) (v : Variance) (t1 t3 : T) : Prop
:= transl : Comaposition L (ProofPV R) v t1 t3 -> Transitivity L R v t1 t3
 | transr : Comaposition (ProofPV L) R v t1 t3 -> Transitivity L R v t1 t3.

Inductive Requires {t t' : T} (con : Con t t') : Variance -> T -> T -> Prop
:= requires (req : Req con) : Requires con (Var req) (Ass req left) (Ass req right).

Inductive Reduction {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3) : Prop
:= simplify (rreq : Req rcon) : Var rreq = covariant -> ProofPV (Requires lcon) covariant t1 (Ass rreq left) -> Ass rreq right = t3 -> Reduction lcon rcon
 | progress (con : Con t1 t3) : (forall req : Req con, ProofPV (Transitivity (Requires lcon) (Requires rcon)) (Var req) (Ass req left) (Ass req right)) -> Reduction lcon rcon.

End Reduction.

Declarative Subtyping (Tradition.v)

Given some user-defined subtyping rules as defined in Common.v, this module adds reflexivity and transitivity rules, and, based in them provides (straightforward) proofs of reflexivity and transitivity of the resulting subtyping relation Traditional. This corresponds to the definition of Declarative Subtyping in the paper.


Module Traditional (T : Typ) (Rule : Rules T).

Module TransRefl <: Rules T.
Inductive TRCon : T -> T -> Type
:= refl (t : T) : TRCon t t
 | trans (t1 t2 t3 : T) : TRCon t1 t3
 | tcon (t t' : T) : Rule.Con t t' -> TRCon t t'.
Definition Con := TRCon.
Definition Req : forall {t t' : T}, Con t t' -> Type
:= fun t t' con => match con with
                   | refl t => Empty
                   | trans t1 t2 t3 => Position
                   | tcon con => Rule.Req con
                   end.
Definition Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T
:= fun t t' con => match con as con in TRCon t t' return Req con -> Position -> T with
                   | refl t => fun req => match req with end
                   | trans t1 t2 t3 => fun req => match req with
                                                  | left => fun p => match p with left => t1 | right => t2 end
                                                  | right => fun p => match p with left => t2 | right => t3 end
                                                  end
                   | @tcon t t' con => @Rule.Ass t t' con
                   end.
End TransRefl.

Module Proof := Proofs T TransRefl.
Definition Traditional := Proof.

Lemma refl (t : T) : Traditional t t.
Lemma trans {t1 t2 t3 : T} : Traditional t1 t2 -> Traditional t2 t3 -> Traditional t1 t3.

End Traditional.

Reductive Subtyping (Decide.v)

For reductive subtyping, the user needs to supply proofs of a few more properties in the module type DecidableRules in order to prove transitivity, decidability and, later (in Convert.v), equivalence to declarative subtyping:
  • refl: A proof of reflexivity of subtyping, corresponding to the Literal Reflexivity requirement in the paper
  • Red: A proof that for all pairs of subtyping rules, where the LHS type of one is equal to the RHS type of the other, there is a way to admit a combined rule. This is corresponds to the Literal Transitivity requirement in the paper
  • wf: A well-foundedness proof for the subtyping rules. This corresponds to the Well-Foundedness requirement in the paper
  • finite_con: A proof that for every two types, there is a finite number of rules that may apply - this is needed for the proof search algorithm for decidability. This corresponds to the Syntax-Directedness requirement in the paper.

Module Type DecidableRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule).
Module Reduction := Reduction T Rule ORule.
Module Proof := Reduction.Proof .
Module ProofPV := Reduction.ProofPV.

Parameter refl : forall t : T, Proof t t.
Parameter Red : forall {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3), Reduction lcon rcon.
Parameter wf : forall (R : T -> T -> Type), (forall t1 t2 : T, (forall (con : Con t1 t2) (req : Req con), R (Ass req left) (Ass req right)) -> R t1 t2) -> forall t t' : T, R t t'.
Parameter finite_con : forall t t' : T, { lcon : list (Con t t')
                                        & Prod (fun con : Con t t' => { lreq : list (Req con) | forall req : Req 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 : Con t t', (forall req : Req con, R (Ass req left) (Ass req right)) -> Exists (fun con' : Con t t' => forall req' : Req con', R (Ass req' left) (Ass req' right)) lcon }.

End DecidableRules.

Module Decidable (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Module Proof := DRule.Proof .
Module ProofPV := DRule.ProofPV.
Module Reduction := DRule.Reduction.

Definition Decidable := Proof.
Definition dproof := proof.
Definition AdmitsD := Admits.

Lemma drefl_R (R : T -> T -> Prop) : AdmitsD R -> forall t : T, R t t.

Lemma Red' {t1 t2 t3 : T} (lcon : Con t1 t2) (rcon : Con t2 t3) : ProofPV (Transitivity (Requires lcon) (Requires rcon)) covariant t1 t3.

Lemma d_trace_ind (R : T -> T -> Type) : (forall t t' : T, (forall (con : Con t t') (req : Req con) (t t' : T), Trace t t' (Ass req left) (Ass req right) -> R t t') -> R t t') -> forall t t' : T, R t t'.

Section Transitivity.

Lemma proofPV_invert_trans (v : Variance) {P P' : Variance -> T -> T -> Prop} : forall {t t' : T}, ProofPV (Transitivity (fun v => P (invert v)) (fun v => P' (invert v))) v t t' -> ProofPV (Transitivity P' P) (invert v) t t'.

Lemma transPV {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV (Transitivity P P') covariant t1 t3.

Lemma transPV' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.

Lemma trans_bindV {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P P' v t t' -> ProofPV Pt v t t') -> ProofPV P covariant t1 t2 -> ProofPV P' covariant t2 t3 -> ProofPV Pt covariant t1 t3.

Lemma trans_contra {P P' : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV (Transitivity P' P) contravariant t1 t3.

Lemma trans_contra' {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.

Lemma trans_bind_contra {P P' Pt : Variance -> T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity P' P v t t' -> ProofPV Pt v t t') -> ProofPV P contravariant t1 t2 -> ProofPV P' contravariant t2 t3 -> ProofPV Pt contravariant t1 t3.

Lemma trans_bind {P P' Pt : T -> T -> Prop} {t1 t2 t3 : T} : (forall (v : Variance) (t t' : T), Transitivity (fun v => P) (fun v => P') v t t' -> ProofP Pt t t') -> ProofP P t1 t2 -> ProofP P' t2 t3 -> ProofP Pt t1 t3.

Lemma trans {t1 t2 t3 : T} : Proof t1 t2 -> Proof t2 t3 -> Proof t1 t3.

End Transitivity.

Decidability

The proof that Reductive subtyping is decidable
Section Decider.

Lemma decider (t t' : T) : { Decidable t t' } + { Decidable t t' -> False }.

End Decider.

End Decidable.

Equivalence between Declarative and Reductive Subtyping (Convert.v)

This module takes the subtyping systems defined in "Tradition.v" and "Decide.v" and user-supplied proofs that each of the systems essentially admits the user-supplied rules of the other (this correspons to the literal conversion requirements in the paper). It then produces proofs of equivalence between Traditional and Decidable (decidable_traditional and traditional_decidable), which, together with decider in "Decide.v" mean that declarative subtyping is decidable.


Module Type Converter (T : Typ) (TRule DRule : Rules T) (ORule : OrientedRules T DRule) (DDRule : DecidableRules T DRule ORule).
Module Traditional := Traditional T TRule.
Module Decidable := Decidable T DRule ORule DDRule.
Module Basic := Proofs T TRule.

Parameter decidable_traditional_R : forall R : T -> T -> Prop, Traditional.Proof.Admits R -> Decidable.Proof.Admits R.

Parameter traditional_decidable_R : forall 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 Converter.

Module Conversion (T : Typ) (TRule DRule : Rules T) (ORule : OrientedRules T DRule) (DDRule : DecidableRules T DRule ORule) (CRule : Converter T TRule DRule ORule DDRule).
Module Basic := Basic.
Module Traditional := Traditional.
Module Decidable := Decidable.

Definition Traditional := Traditional.Traditional.
Definition Decidable := Decidable.Decidable.

Lemma decidable_traditional {t t' : T} : Decidable t t' -> Traditional t t'.

Lemma traditional_decidable_R_trans : forall R : T -> T -> Prop,
                                      (forall {t t' : T}, Decidable t t' -> R t t')
                                   -> (forall {t1 t2 t3 : T}, R t1 t2 -> R t2 t3 -> R t1 t3)
                                   -> Decidable.Proof.Admits R
                                   -> Traditional.Proof.Admits R.

Lemma dadmitst : Traditional.Proof.Admits Decidable.

Lemma traditional_decidable {t t' : T} : Traditional t t' -> Decidable t t'.

End Conversion.

Extending Declarative Subtyping (Extend.v)

This module takes a user-supplied extension relation and a declarative subtyping relation and creates an extended subtyping relation. Due to the explicit reflexivity and transitivity rules of the declarative subtyping relation, extended subtyping is still easily provably reflexive and transitive. This corresponds to Extended Subtyping in the paper.


Module Type Extension (T : Typ) (Rule : Rules T).
Parameter Con : T -> T -> Prop.
End Extension.

Module ExtendedRules (T : Typ) (Rule : Rules T) (ERule : Extension T Rule) <: Rules T.
Module Traditional := Traditional T Rule.

Inductive ECon (t t' : T) : Type
:= traditional : Traditional.TransRefl.Con t t' -> ECon t t'
 | extended : ERule.Con t t' -> ECon t t'.
Definition Con := ECon.
Definition Req {t t' : T} (con : Con t t') : Type
:= match con with
   | traditional con => Traditional.TransRefl.Req con
   | extended con => Empty
   end.
Definition Ass {t t' : T} {con : Con t t'} : Req con -> Position -> T
:= match con as con return Req con -> Position -> T with
   | traditional con => @Traditional.TransRefl.Ass _ _ con
   | extended con => fun e => match e with end
   end.

End ExtendedRules.

Module Extended (T : Typ) (Rule : Rules T) (ERule : Extension T Rule).
Module ExtendedRules := ExtendedRules T Rule ERule.
Module Traditional := ExtendedRules.Traditional.
Module Proof := Proofs T ExtendedRules.

Definition Extended := Proof.

Lemma traditional_extended {t t' : T} : Traditional t t' -> Extended t t'.

Lemma refl (t : T) : Extended t t.
Lemma trans {t1 t2 t3 : T} : Extended t1 t2 -> Extended t2 t3 -> Extended t1 t3.

End Extended.

Integrated Subtyping (Preprocess.v)

To specify integrated subtyping, the user supplies an integrator i, and integrated-predicate Preprocessed, subject to a few requirements:
  • counit: the result of integrating a type must be a reductive subtype of the original type. This corresponds to the "Literal Dereliction" requirement in the paper. The full "Dereliction" Lemma easily follows from transitivity.
  • i_preprocessed: the result of integrating a type must be integrated according to the integrated-predicate Preprocessed. This corresponds to the "Integrator Integrated" Lemma in the paper; which just lifts the "Intersector Integrated" requirement to dnf and unions/intersection types.
  • Opt: Intuitively, integrated subtyping integrates the LHS type at every recursive step in subtyping. However, there are many subtyping rules that have premises whose LHS is integrated if the LHS of the conclusion is integrated. In this case, we can optimize those subtyping rules to not integrate the LHS (see the definition of Ass in PreprocessingRules). In the paper, we use this insight to only apply the integrator at the beginning of subtyping, and then the intersector whenever we recurse trough literals. This is because for the intersection and union subtyping rules, the LHS is essentially always integrated. In order for this to be true for LHS-intersection rule, the formalization here would require that if an intersection is integrated, so are both of its components. For the system in the paper, we relaxed this requirement - this is the small relaxation we allude to in section 7.
  • i_promote_R: a proof of promotion, corresponding roughly to the "Literal Promotion" requirement in the paper, but using a general relation R that just admits the decidable rules, reflexivity, and monotonicity (as we alluded to in section 7) in order to model proofs with assumptions.
We define a new set of subtyping rules PreprocessingRules, expressing Integrated Subtyping, and with those rules express the final requirement:
  • i_wf: the new subtyping relation must still be well-founded. In the paper, we prove this from the "Measure Preservation" requirement, which in this case comes down to proving well-foundedness of the subtyping relation altogether
Given these, the rest of the section proves full promotion (dpromote'), transitivity (itrans), and eventually decidability (decider) of Integrated Subtyping. This relation corresponds to ≤ in the paper, i.e. the subtyping relation that integrates the left-hand side in recursive steps, but does not do so for its original inputs. From that, the full integrated subtyping relation ≤ is defined just like in the paper, except using i instead of DNF.

Module Type Comonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule).
Module Decidable := Decidable T Rule ORule DRule.

Parameter i : T -> T.
Parameter counit : forall t : T, Decidable (i t) t.

Parameter Preprocessed : T -> Prop.
Parameter i_preprocessed : forall t : T, Preprocessed (i t).

Parameter Opt : forall {t t' : T} {con : Con t t'} (req : Req con), option (Preprocessed t -> Preprocessed (Ass req left)).

Parameter i_promote_R : forall 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 -> Decidable.Proof.Inverts Preprocessed R -> forall (t t' : T) (con : Con t t'), Preprocessed t -> (forall req : Req con, R (Rule.Ass req left) (Rule.Ass req right)) -> (forall req : Req con, Preprocessed (Ass req left) -> R (Ass req left) (i (Ass req right))) -> R t (i t').

End Comonad.

Module PreprocessingRules (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) <: Rules T.

Definition Con := Rule.Con.
Definition Req : forall {t t' : T}, Con t t' -> Type
:= @Rule.Req.
Definition Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T
:= fun t t' con req pos => match pos with
                           | left => match Opt req with
                                     | None => i (Rule.Ass req left)
                                     | Some _ => Rule.Ass req left
                                     end
                           | right => Rule.Ass req right
                           end.
Definition Var : forall {t t' : T} {con : Con t t'}, Req con -> Variance := @ORule.Var.

End PreprocessingRules.

Module Type WellFoundedComonad (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule).
Module PRule := PreprocessingRules T Rule ORule DRule I.

Parameter i_wf : forall (R : T -> T -> Type), (forall t1 t2 : T, (forall (con : Con t1 t2) (req : Req con), R (Ass req left) (Ass req right)) -> R t1 t2) -> forall t t' : T, R t t'.

End WellFoundedComonad.

Module Preprocessing (T : Typ) (Rule : Rules T) (ORule : OrientedRules T Rule) (DRule : DecidableRules T Rule ORule) (I : Comonad T Rule ORule DRule) (WFI : WellFoundedComonad T Rule ORule DRule I).
Module PRule := WFI.PRule.
Module ProofPV := ProofPV T PRule PRule.
Module Proof := ProofPV.Proof.
Module Decidable := I.Decidable.

Definition Preprocessing := Proof.

Section PreprocessingDecidable.

Lemma dderelict {t t' : T} : Decidable t t' -> Decidable (i t) t'.

Lemma dpromote' {t t' : T} : Preprocessed t -> Decidable t t' -> Decidable t (i t').

Corollary dpromote {t t' : T} : Decidable (i t) t' -> Decidable (i t) (i t').

Corollary dpreprocessed {t : T} : Preprocessed t -> Decidable t (i t).

Corollary dmap {t t' : T} : Decidable t t' -> Decidable (i t) (i t').

End PreprocessingDecidable.

Section PreprocessingDecidableTrans.
Lemma decidableP_preprocessing {t1 t4 : T} : Preprocessed t1 -> DecidableP (fun t2 t3 => forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4) t1 t4 -> Preprocessing t1 t4.

Theorem decidable_trans {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> Preprocessing t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.

End PreprocessingDecidableTrans.

Section Comonad.

Lemma derelict {t t' : T} : Preprocessing t t' -> Preprocessing (i t) t'.

Lemma admitsd : AdmitsD Preprocessing.

Definition iPreprocessing (t2 t3 : T) := forall t1 t4 : T, Preprocessed t1 -> Decidable t1 t2 -> Decidable t3 t4 -> Preprocessing t1 t4.

Lemma iadmitsd : AdmitsD iPreprocessing.

Lemma decidable_preprocessing {t t' : T} : Decidable t t' -> Preprocessing t t'.

Lemma refl (t : T) : Preprocessing t t.

Lemma iiinverts : Decidable.Proof.Inverts Preprocessed iPreprocessing.

Lemma ipromote {t2 t3 : T} : Preprocessing t2 t3 -> Preprocessed t2 -> iPreprocessing t2 (i t3).

Corollary promote' {t t' : T} : Preprocessed t -> Preprocessing t t' -> Preprocessing t (i t').

Corollary promote {t t' : T} : Preprocessing (i t) t' -> Preprocessing (i t) (i t').

Corollary map {t t' : T} : Preprocessing t t' -> Preprocessing (i t) (i t').

End Comonad.

Section Transitivity.

Theorem decidable_transPV' {tc tc' : T} {bcon : Con tc tc'} (bind : forall req : Req bcon, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t1 t2 t3 t4 : T} : Preprocessed t1 -> Decidable t1 t2 -> DecidablePV (Requires bcon) v t2 t3 -> Decidable t3 t4 -> Preprocessing t1 t4.

Lemma decidable_ipreprocessingPV' {t1 t2 : T} {con : Con t1 t2} (bind : forall req : Req con, Preprocessing (Ass req left) (Ass req right)) {v : Variance} {t t' : T} : DecidablePV (Requires con) v t t' -> Preprocessing (i t) t'.

Lemma decidable_preprocessingPV (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : (forall (v : Variance) (t1 t2 t3 t4 : T), Decidable t1 t2 -> P v t2 t3 -> Decidable t3 t4 -> P v t1 t4) -> DecidablePV P v t t' -> ProofPV P v t t'.

Lemma decidable_preprocessingPV' (P : Variance -> T -> T -> Prop) (v : Variance) (t t' : T) : DecidablePV P v t t' -> ProofPV (Comaposition (fun v => Decidable) (Comaposition P (fun v => Decidable))) v t t'.

Lemma trans {t1 t2 t3 : T} : Preprocessed t1 -> Preprocessing t1 t2 -> Preprocessing t2 t3 -> Preprocessing t1 t3.

Corollary itrans {t1 t2 t3 : T} : iPreprocessing t1 t2 -> iPreprocessing t2 t3 -> iPreprocessing t1 t3.

End Transitivity.

Section Decider.

Theorem decider' (t t' : T) : Preprocessed t -> { Preprocessing t t' } + { Preprocessing t t' -> False }.

Corollary decider (t t' : T) : { Preprocessing (i t) t' } + { Preprocessing (i t) t' -> False }.

End Decider.

End Preprocessing.

Equivalence between Extended and Integrated Subtyping (Equate.v)

In a final step, we show that Extended and Integrated Subtyping are equivalent and the decision procedure for Integrated Subtyping is also a decision procedure for Extended Subtyping. In order to do that, the user of our framework needs to show the two last missing pieces, which are
  • unit: this corresponds to the Intersector Soundness requirement from the paper
  • iextended: this corresponds to the Intersector Completeness requirement from the paper
The final two theorems extended_ipreprocessing and ipreprocessing_extended establish the equivalence. Recall that Preprocessing is only the "inner" part of Integrated Subtyping, to the LHS type has to be integrated using o before turning it over to Preprocessing to fully express Integrated Subtyping. The final theorem decider corresponds to the main theorem in the paper: Decidability of Extended Subtyping.


Module Type Equivocator (T : Typ) (TRule DRule : Rules T) (ERule : Extension T TRule) (ORule : OrientedRules T DRule) (DDRule : DecidableRules T DRule ORule) (I : Comonad T DRule ORule DDRule) (WFI : WellFoundedComonad T DRule ORule DDRule I).
Module Basic := Proofs T TRule.
Module Extended := Extended T TRule ERule.
Module Traditional := Extended.Traditional.
Module Preprocessing := Preprocessing T DRule ORule DDRule I WFI.
Module Decidable := Preprocessing.Decidable.
Parameter unit : forall t : T, Extended.Extended t (i t).

Parameter iextended : forall {t t' : T}, ERule.Con t t' -> Traditional.Traditional (i t) t'.

End Equivocator.

Module Equivalence (T : Typ) (TRule DRule : Rules T) (ERule : Extension T TRule) (ORule : OrientedRules T DRule) (DDRule : DecidableRules T DRule ORule) (I : Comonad T DRule ORule DDRule) (WFI : WellFoundedComonad T DRule ORule DDRule I) (Eq : Equivocator T TRule DRule ERule ORule DDRule I WFI).
Module Basic := Eq.Basic.
Module Traditional := Eq.Traditional.
Module Extended := Eq.Extended.
Module Decidable := Eq.Decidable.
Module Preprocessing := Eq.Preprocessing.

Definition Traditional := Traditional.Traditional.
Definition Decidable := Decidable.Decidable.
Definition Extended := Extended.Extended.
Definition Preprocessing := Preprocessing.Preprocessing.
Definition iPreprocessing := Preprocessing.iPreprocessing.


Section Equivalence.

Lemma iextended_extended {t t' : T} : Extended (i t) t' -> Extended t t'.

Lemma iadmitsb : Basic.Admits iPreprocessing.

Lemma iadmitst : Traditional.Proof.Admits iPreprocessing.

Theorem extended_ipreprocessing' {t t' : T} : Extended t t' -> iPreprocessing t t'.

Theorem extended_ipreprocessing {t t' : T} : Extended t t' -> Preprocessing (i t) t'.

Theorem ipreprocessing_extended {t t' : T} : Preprocessing (i t) t' -> Extended t t'.

End Equivalence.

Section Decider.

Theorem decider : forall t t' : T, {Extended t t'} + {~ Extended t t'}.

End Decider.

End Equivalence.
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 (267 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 (57 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 (8 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 (81 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 (23 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 (26 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 (16 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 (14 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 (42 entries)

Global Index

C

Common [library]
Comonad [module, in Preprocess]
Comonad.counit [axiom, in Preprocess]
Comonad.Decidable [module, in Preprocess]
Comonad.i [axiom, in Preprocess]
Comonad.i_promote_R [axiom, in Preprocess]
Comonad.i_preprocessed [axiom, in Preprocess]
Comonad.Opt [axiom, in Preprocess]
Comonad.Preprocessed [axiom, in Preprocess]
contravariant [constructor, in Common]
Conversion [module, in Convert]
Conversion.Basic [module, in Convert]
Conversion.dadmitst [lemma, in Convert]
Conversion.Decidable [definition, in Convert]
Conversion.Decidable [module, in Convert]
Conversion.decidable_traditional [lemma, in Convert]
Conversion.Traditional [definition, in Convert]
Conversion.Traditional [module, in Convert]
Conversion.traditional_decidable [lemma, in Convert]
Conversion.traditional_decidable_R_trans [lemma, in Convert]
Convert [library]
Converter [module, in Convert]
Converter.Basic [module, in Convert]
Converter.Decidable [module, in Convert]
Converter.decidable_traditional_R [axiom, in Convert]
Converter.Traditional [module, in Convert]
Converter.traditional_decidable_R [axiom, in Convert]
covariant [constructor, in Common]


D

Decidable [module, in Decide]
DecidableRules [module, in Decide]
DecidableRules.finite_con [axiom, in Decide]
DecidableRules.Proof [module, in Decide]
DecidableRules.ProofPV [module, in Decide]
DecidableRules.Red [axiom, in Decide]
DecidableRules.Reduction [module, in Decide]
DecidableRules.refl [axiom, in Decide]
DecidableRules.wf [axiom, in Decide]
Decidable.AdmitsD [definition, in Decide]
Decidable.Decidable [definition, in Decide]
Decidable.decider [lemma, in Decide]
Decidable.Decider [section, in Decide]
Decidable.dproof [definition, in Decide]
Decidable.drefl_R [lemma, in Decide]
Decidable.d_trace_ind [lemma, in Decide]
Decidable.Proof [module, in Decide]
Decidable.ProofPV [module, in Decide]
Decidable.proofPV_invert_trans [lemma, in Decide]
Decidable.Reduction [module, in Decide]
Decidable.Red' [lemma, in Decide]
Decidable.trans [lemma, in Decide]
Decidable.Transitivity [section, in Decide]
Decidable.transPV [lemma, in Decide]
Decidable.transPV' [lemma, in Decide]
Decidable.trans_bind [lemma, in Decide]
Decidable.trans_bind_contra [lemma, in Decide]
Decidable.trans_contra' [lemma, in Decide]
Decidable.trans_contra [lemma, in Decide]
Decidable.trans_bindV [lemma, in Decide]
Decide [library]


E

Empty [inductive, in Common]
Equate [library]
Equivalence [module, in Equate]
Equivalence.Basic [module, in Equate]
Equivalence.Conversion [section, in Equate]
Equivalence.dadmitst [lemma, in Equate]
Equivalence.Decidable [definition, in Equate]
Equivalence.Decidable [module, in Equate]
Equivalence.decidable_traditional [lemma, in Equate]
Equivalence.decider [lemma, in Equate]
Equivalence.Decider [section, in Equate]
Equivalence.Equivalence [section, in Equate]
Equivalence.Extended [definition, in Equate]
Equivalence.Extended [module, in Equate]
Equivalence.extended_ipreprocessing [lemma, in Equate]
Equivalence.extended_ipreprocessing' [lemma, in Equate]
Equivalence.iadmitsb [lemma, in Equate]
Equivalence.iadmitst [lemma, in Equate]
Equivalence.iextended_extended [lemma, in Equate]
Equivalence.iPreprocessing [definition, in Equate]
Equivalence.ipreprocessing_extended [lemma, in Equate]
Equivalence.Preprocessing [definition, in Equate]
Equivalence.Preprocessing [module, in Equate]
Equivalence.Traditional [definition, in Equate]
Equivalence.Traditional [module, in Equate]
Equivalence.traditional_decidable [lemma, in Equate]
Equivalence.traditional_decidable_R_trans [lemma, in Equate]
Equivocator [module, in Equate]
Equivocator.Basic [module, in Equate]
Equivocator.Converter [section, in Equate]
Equivocator.Decidable [module, in Equate]
Equivocator.decidable_traditional_R [axiom, in Equate]
Equivocator.Extended [module, in Equate]
Equivocator.iextended [axiom, in Equate]
Equivocator.Preprocessing [module, in Equate]
Equivocator.Traditional [module, in Equate]
Equivocator.traditional_decidable_R [axiom, in Equate]
Equivocator.unit [axiom, in Equate]
Extend [library]
Extended [module, in Extend]
ExtendedRules [module, in Extend]
ExtendedRules.Ass [definition, in Extend]
ExtendedRules.Con [definition, in Extend]
ExtendedRules.ECon [inductive, in Extend]
ExtendedRules.extended [constructor, in Extend]
ExtendedRules.Req [definition, in Extend]
ExtendedRules.traditional [constructor, in Extend]
ExtendedRules.Traditional [module, in Extend]
Extended.Extended [definition, in Extend]
Extended.ExtendedRules [module, in Extend]
Extended.Proof [module, in Extend]
Extended.refl [lemma, in Extend]
Extended.Traditional [module, in Extend]
Extended.traditional_extended [lemma, in Extend]
Extended.trans [lemma, in Extend]
Extension [module, in Extend]
Extension.Con [axiom, in Extend]


I

Introduction [library]
invert [definition, in Common]
invert_invert [lemma, in Common]


L

left [constructor, in Common]


M

multiply [definition, in Common]
multiply_covariant [lemma, in Common]
multiply_invert [lemma, in Common]


O

OrientedRules [module, in Common]
OrientedRules.Var [axiom, in Common]


P

Position [inductive, in Common]
Preprocess [library]
Preprocessing [module, in Preprocess]
PreprocessingRules [module, in Preprocess]
PreprocessingRules.Ass [definition, in Preprocess]
PreprocessingRules.Con [definition, in Preprocess]
PreprocessingRules.Req [definition, in Preprocess]
PreprocessingRules.Var [definition, in Preprocess]
Preprocessing.admitsd [lemma, in Preprocess]
Preprocessing.Comonad [section, in Preprocess]
Preprocessing.dbindV [definition, in Preprocess]
Preprocessing.dderelict [lemma, in Preprocess]
Preprocessing.Decidable [module, in Preprocess]
Preprocessing.DecidableP [definition, in Preprocess]
Preprocessing.DecidablePV [definition, in Preprocess]
Preprocessing.decidablePV_decidableP [definition, in Preprocess]
Preprocessing.decidablePV_decidable [definition, in Preprocess]
Preprocessing.decidableP_preprocessing [lemma, in Preprocess]
Preprocessing.decidableP_decidablePV [definition, in Preprocess]
Preprocessing.decidable_preprocessingPV' [lemma, in Preprocess]
Preprocessing.decidable_preprocessingPV [lemma, in Preprocess]
Preprocessing.decidable_ipreprocessingPV' [lemma, in Preprocess]
Preprocessing.decidable_transPV' [lemma, in Preprocess]
Preprocessing.decidable_preprocessing [lemma, in Preprocess]
Preprocessing.decidable_trans [lemma, in Preprocess]
Preprocessing.decidable_decidablePV [definition, in Preprocess]
Preprocessing.decider [lemma, in Preprocess]
Preprocessing.Decider [section, in Preprocess]
Preprocessing.decider' [lemma, in Preprocess]
Preprocessing.derelict [lemma, in Preprocess]
Preprocessing.dmap [lemma, in Preprocess]
Preprocessing.dmonoV [definition, in Preprocess]
Preprocessing.dpermitV [definition, in Preprocess]
Preprocessing.dpreprocessed [lemma, in Preprocess]
Preprocessing.dpromote [lemma, in Preprocess]
Preprocessing.dpromote' [lemma, in Preprocess]
Preprocessing.drefl [definition, in Preprocess]
Preprocessing.dtrans [definition, in Preprocess]
Preprocessing.iadmitsd [lemma, in Preprocess]
Preprocessing.iiinverts [lemma, in Preprocess]
Preprocessing.iPreprocessing [definition, in Preprocess]
Preprocessing.ipromote [lemma, in Preprocess]
Preprocessing.itrans [lemma, in Preprocess]
Preprocessing.i_trace_ind [lemma, in Preprocess]
Preprocessing.map [lemma, in Preprocess]
Preprocessing.Preprocessing [definition, in Preprocess]
Preprocessing.PreprocessingDecidable [section, in Preprocess]
Preprocessing.PreprocessingDecidableTrans [section, in Preprocess]
Preprocessing.promote [lemma, in Preprocess]
Preprocessing.promote' [lemma, in Preprocess]
Preprocessing.Proof [module, in Preprocess]
Preprocessing.ProofPV [module, in Preprocess]
Preprocessing.PRule [module, in Preprocess]
Preprocessing.refl [lemma, in Preprocess]
Preprocessing.trans [lemma, in Preprocess]
Preprocessing.Transitivity [section, in Preprocess]
Preprocessing.trans_decider [lemma, in Preprocess]
Preprocessing.trans_decidel [lemma, in Preprocess]
Prod [inductive, in Common]
prod_cons [constructor, in Common]
prod_nil [constructor, in Common]
ProofPV [module, in Common]
ProofPV.AdmitsPV [definition, in Common]
ProofPV.bindV [lemma, in Common]
ProofPV.invertPV [lemma, in Common]
ProofPV.invertPV' [lemma, in Common]
ProofPV.monoV [lemma, in Common]
ProofPV.permitV [constructor, in Common]
ProofPV.Proof [module, in Common]
ProofPV.proofPV [constructor, in Common]
ProofPV.ProofPV [inductive, in Common]
ProofPV.proofPV_proof [lemma, in Common]
ProofPV.proofPV_proofP [lemma, in Common]
ProofPV.proofP_proofPV [lemma, in Common]
ProofPV.proof_proofPV [lemma, in Common]
ProofPV.proof_admitsPV [lemma, in Common]
Proofs [module, in Common]
Proofs.Admits [definition, in Common]
Proofs.AdmitsP [definition, in Common]
Proofs.assumption [constructor, in Common]
Proofs.bind [lemma, in Common]
Proofs.inversion [constructor, in Common]
Proofs.Inversion [inductive, in Common]
Proofs.Inversion [section, in Common]
Proofs.Inverts [definition, in Common]
Proofs.mono [lemma, in Common]
Proofs.permit [constructor, in Common]
Proofs.proof [constructor, in Common]
Proofs.Proof [inductive, in Common]
Proofs.proofP [constructor, in Common]
Proofs.ProofP [inductive, in Common]
Proofs.ProofP [section, in Common]
Proofs.proofP_proof [lemma, in Common]
Proofs.proof_proofP [lemma, in Common]
Proofs.proof_admits [lemma, in Common]
Proofs.recursion [constructor, in Common]
Proofs.Trace [inductive, in Common]
Proofs.Trace [section, in Common]
Proofs.trace_comp' [lemma, in Common]
Proofs.trace_comp [lemma, in Common]
Proofs.trace_ind [lemma, in Common]


R

Reduction [module, in Common]
Reduction.Comaposition [definition, in Common]
Reduction.compose [constructor, in Common]
Reduction.Composition [inductive, in Common]
Reduction.contrapose [constructor, in Common]
Reduction.Contraposition [inductive, in Common]
Reduction.progress [constructor, in Common]
Reduction.Proof [module, in Common]
Reduction.ProofPV [module, in Common]
Reduction.Reduction [inductive, in Common]
Reduction.requires [constructor, in Common]
Reduction.Requires [inductive, in Common]
Reduction.simplify [constructor, in Common]
Reduction.Transitivity [inductive, in Common]
Reduction.transl [constructor, in Common]
Reduction.transr [constructor, in Common]
right [constructor, in Common]
Rules [module, in Common]
Rules.Ass [axiom, in Common]
Rules.Con [axiom, in Common]
Rules.Req [axiom, in Common]


T

Tradition [library]
Traditional [module, in Tradition]
Traditional.Proof [module, in Tradition]
Traditional.refl [lemma, in Tradition]
Traditional.Traditional [definition, in Tradition]
Traditional.trans [lemma, in Tradition]
Traditional.TransRefl [module, in Tradition]
Traditional.TransRefl.Ass [definition, in Tradition]
Traditional.TransRefl.Con [definition, in Tradition]
Traditional.TransRefl.refl [constructor, in Tradition]
Traditional.TransRefl.Req [definition, in Tradition]
Traditional.TransRefl.tcon [constructor, in Tradition]
Traditional.TransRefl.trans [constructor, in Tradition]
Traditional.TransRefl.TRCon [inductive, in Tradition]
Typ [module, in Common]
Typ.T [axiom, in Common]


V

Variance [inductive, in Common]


W

WellFoundedComonad [module, in Preprocess]
WellFoundedComonad.i_wf [axiom, in Preprocess]
WellFoundedComonad.PRule [module, in Preprocess]



Module Index

C

Comonad [in Preprocess]
Comonad.Decidable [in Preprocess]
Conversion [in Convert]
Conversion.Basic [in Convert]
Conversion.Decidable [in Convert]
Conversion.Traditional [in Convert]
Converter [in Convert]
Converter.Basic [in Convert]
Converter.Decidable [in Convert]
Converter.Traditional [in Convert]


D

Decidable [in Decide]
DecidableRules [in Decide]
DecidableRules.Proof [in Decide]
DecidableRules.ProofPV [in Decide]
DecidableRules.Reduction [in Decide]
Decidable.Proof [in Decide]
Decidable.ProofPV [in Decide]
Decidable.Reduction [in Decide]


E

Equivalence [in Equate]
Equivalence.Basic [in Equate]
Equivalence.Decidable [in Equate]
Equivalence.Extended [in Equate]
Equivalence.Preprocessing [in Equate]
Equivalence.Traditional [in Equate]
Equivocator [in Equate]
Equivocator.Basic [in Equate]
Equivocator.Decidable [in Equate]
Equivocator.Extended [in Equate]
Equivocator.Preprocessing [in Equate]
Equivocator.Traditional [in Equate]
Extended [in Extend]
ExtendedRules [in Extend]
ExtendedRules.Traditional [in Extend]
Extended.ExtendedRules [in Extend]
Extended.Proof [in Extend]
Extended.Traditional [in Extend]
Extension [in Extend]


O

OrientedRules [in Common]


P

Preprocessing [in Preprocess]
PreprocessingRules [in Preprocess]
Preprocessing.Decidable [in Preprocess]
Preprocessing.Proof [in Preprocess]
Preprocessing.ProofPV [in Preprocess]
Preprocessing.PRule [in Preprocess]
ProofPV [in Common]
ProofPV.Proof [in Common]
Proofs [in Common]


R

Reduction [in Common]
Reduction.Proof [in Common]
Reduction.ProofPV [in Common]
Rules [in Common]


T

Traditional [in Tradition]
Traditional.Proof [in Tradition]
Traditional.TransRefl [in Tradition]
Typ [in Common]


W

WellFoundedComonad [in Preprocess]
WellFoundedComonad.PRule [in Preprocess]



Library Index

C

Common
Convert


D

Decide


E

Equate
Extend


I

Introduction


P

Preprocess


T

Tradition



Lemma Index

C

Conversion.dadmitst [in Convert]
Conversion.decidable_traditional [in Convert]
Conversion.traditional_decidable [in Convert]
Conversion.traditional_decidable_R_trans [in Convert]


D

Decidable.decider [in Decide]
Decidable.drefl_R [in Decide]
Decidable.d_trace_ind [in Decide]
Decidable.proofPV_invert_trans [in Decide]
Decidable.Red' [in Decide]
Decidable.trans [in Decide]
Decidable.transPV [in Decide]
Decidable.transPV' [in Decide]
Decidable.trans_bind [in Decide]
Decidable.trans_bind_contra [in Decide]
Decidable.trans_contra' [in Decide]
Decidable.trans_contra [in Decide]
Decidable.trans_bindV [in Decide]


E

Equivalence.dadmitst [in Equate]
Equivalence.decidable_traditional [in Equate]
Equivalence.decider [in Equate]
Equivalence.extended_ipreprocessing [in Equate]
Equivalence.extended_ipreprocessing' [in Equate]
Equivalence.iadmitsb [in Equate]
Equivalence.iadmitst [in Equate]
Equivalence.iextended_extended [in Equate]
Equivalence.ipreprocessing_extended [in Equate]
Equivalence.traditional_decidable [in Equate]
Equivalence.traditional_decidable_R_trans [in Equate]
Extended.refl [in Extend]
Extended.traditional_extended [in Extend]
Extended.trans [in Extend]


I

invert_invert [in Common]


M

multiply_covariant [in Common]
multiply_invert [in Common]


P

Preprocessing.admitsd [in Preprocess]
Preprocessing.dderelict [in Preprocess]
Preprocessing.decidableP_preprocessing [in Preprocess]
Preprocessing.decidable_preprocessingPV' [in Preprocess]
Preprocessing.decidable_preprocessingPV [in Preprocess]
Preprocessing.decidable_ipreprocessingPV' [in Preprocess]
Preprocessing.decidable_transPV' [in Preprocess]
Preprocessing.decidable_preprocessing [in Preprocess]
Preprocessing.decidable_trans [in Preprocess]
Preprocessing.decider [in Preprocess]
Preprocessing.decider' [in Preprocess]
Preprocessing.derelict [in Preprocess]
Preprocessing.dmap [in Preprocess]
Preprocessing.dpreprocessed [in Preprocess]
Preprocessing.dpromote [in Preprocess]
Preprocessing.dpromote' [in Preprocess]
Preprocessing.iadmitsd [in Preprocess]
Preprocessing.iiinverts [in Preprocess]
Preprocessing.ipromote [in Preprocess]
Preprocessing.itrans [in Preprocess]
Preprocessing.i_trace_ind [in Preprocess]
Preprocessing.map [in Preprocess]
Preprocessing.promote [in Preprocess]
Preprocessing.promote' [in Preprocess]
Preprocessing.refl [in Preprocess]
Preprocessing.trans [in Preprocess]
Preprocessing.trans_decider [in Preprocess]
Preprocessing.trans_decidel [in Preprocess]
ProofPV.bindV [in Common]
ProofPV.invertPV [in Common]
ProofPV.invertPV' [in Common]
ProofPV.monoV [in Common]
ProofPV.proofPV_proof [in Common]
ProofPV.proofPV_proofP [in Common]
ProofPV.proofP_proofPV [in Common]
ProofPV.proof_proofPV [in Common]
ProofPV.proof_admitsPV [in Common]
Proofs.bind [in Common]
Proofs.mono [in Common]
Proofs.proofP_proof [in Common]
Proofs.proof_proofP [in Common]
Proofs.proof_admits [in Common]
Proofs.trace_comp' [in Common]
Proofs.trace_comp [in Common]
Proofs.trace_ind [in Common]


T

Traditional.refl [in Tradition]
Traditional.trans [in Tradition]



Axiom Index

C

Comonad.counit [in Preprocess]
Comonad.i [in Preprocess]
Comonad.i_promote_R [in Preprocess]
Comonad.i_preprocessed [in Preprocess]
Comonad.Opt [in Preprocess]
Comonad.Preprocessed [in Preprocess]
Converter.decidable_traditional_R [in Convert]
Converter.traditional_decidable_R [in Convert]


D

DecidableRules.finite_con [in Decide]
DecidableRules.Red [in Decide]
DecidableRules.refl [in Decide]
DecidableRules.wf [in Decide]


E

Equivocator.decidable_traditional_R [in Equate]
Equivocator.iextended [in Equate]
Equivocator.traditional_decidable_R [in Equate]
Equivocator.unit [in Equate]
Extension.Con [in Extend]


O

OrientedRules.Var [in Common]


R

Rules.Ass [in Common]
Rules.Con [in Common]
Rules.Req [in Common]


T

Typ.T [in Common]


W

WellFoundedComonad.i_wf [in Preprocess]



Constructor Index

C

contravariant [in Common]
covariant [in Common]


E

ExtendedRules.extended [in Extend]
ExtendedRules.traditional [in Extend]


L

left [in Common]


P

prod_cons [in Common]
prod_nil [in Common]
ProofPV.permitV [in Common]
ProofPV.proofPV [in Common]
Proofs.assumption [in Common]
Proofs.inversion [in Common]
Proofs.permit [in Common]
Proofs.proof [in Common]
Proofs.proofP [in Common]
Proofs.recursion [in Common]


R

Reduction.compose [in Common]
Reduction.contrapose [in Common]
Reduction.progress [in Common]
Reduction.requires [in Common]
Reduction.simplify [in Common]
Reduction.transl [in Common]
Reduction.transr [in Common]
right [in Common]


T

Traditional.TransRefl.refl [in Tradition]
Traditional.TransRefl.tcon [in Tradition]
Traditional.TransRefl.trans [in Tradition]



Inductive Index

E

Empty [in Common]
ExtendedRules.ECon [in Extend]


P

Position [in Common]
Prod [in Common]
ProofPV.ProofPV [in Common]
Proofs.Inversion [in Common]
Proofs.Proof [in Common]
Proofs.ProofP [in Common]
Proofs.Trace [in Common]


R

Reduction.Composition [in Common]
Reduction.Contraposition [in Common]
Reduction.Reduction [in Common]
Reduction.Requires [in Common]
Reduction.Transitivity [in Common]


T

Traditional.TransRefl.TRCon [in Tradition]


V

Variance [in Common]



Section Index

D

Decidable.Decider [in Decide]
Decidable.Transitivity [in Decide]


E

Equivalence.Conversion [in Equate]
Equivalence.Decider [in Equate]
Equivalence.Equivalence [in Equate]
Equivocator.Converter [in Equate]


P

Preprocessing.Comonad [in Preprocess]
Preprocessing.Decider [in Preprocess]
Preprocessing.PreprocessingDecidable [in Preprocess]
Preprocessing.PreprocessingDecidableTrans [in Preprocess]
Preprocessing.Transitivity [in Preprocess]
Proofs.Inversion [in Common]
Proofs.ProofP [in Common]
Proofs.Trace [in Common]



Definition Index

C

Conversion.Decidable [in Convert]
Conversion.Traditional [in Convert]


D

Decidable.AdmitsD [in Decide]
Decidable.Decidable [in Decide]
Decidable.dproof [in Decide]


E

Equivalence.Decidable [in Equate]
Equivalence.Extended [in Equate]
Equivalence.iPreprocessing [in Equate]
Equivalence.Preprocessing [in Equate]
Equivalence.Traditional [in Equate]
ExtendedRules.Ass [in Extend]
ExtendedRules.Con [in Extend]
ExtendedRules.Req [in Extend]
Extended.Extended [in Extend]


I

invert [in Common]


M

multiply [in Common]


P

PreprocessingRules.Ass [in Preprocess]
PreprocessingRules.Con [in Preprocess]
PreprocessingRules.Req [in Preprocess]
PreprocessingRules.Var [in Preprocess]
Preprocessing.dbindV [in Preprocess]
Preprocessing.DecidableP [in Preprocess]
Preprocessing.DecidablePV [in Preprocess]
Preprocessing.decidablePV_decidableP [in Preprocess]
Preprocessing.decidablePV_decidable [in Preprocess]
Preprocessing.decidableP_decidablePV [in Preprocess]
Preprocessing.decidable_decidablePV [in Preprocess]
Preprocessing.dmonoV [in Preprocess]
Preprocessing.dpermitV [in Preprocess]
Preprocessing.drefl [in Preprocess]
Preprocessing.dtrans [in Preprocess]
Preprocessing.iPreprocessing [in Preprocess]
Preprocessing.Preprocessing [in Preprocess]
ProofPV.AdmitsPV [in Common]
Proofs.Admits [in Common]
Proofs.AdmitsP [in Common]
Proofs.Inverts [in Common]


R

Reduction.Comaposition [in Common]


T

Traditional.Traditional [in Tradition]
Traditional.TransRefl.Ass [in Tradition]
Traditional.TransRefl.Con [in Tradition]
Traditional.TransRefl.Req [in Tradition]



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 (267 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 (57 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 (8 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 (81 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 (23 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 (26 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 (16 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 (14 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 (42 entries)

This page has been generated by coqdoc