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.Concept from Paper | Corresponding Proof Part | Comment |
---|---|---|
Literals & Types | Typ.T in Common.v | Generalized to arbitrary types, all user-provided |
User-Defined Subtyping Rules | Rules.Con, Rules.Req, Rules.Ass in Common.v | |
Declarative Subtyping Rules | Traditional.TransRefl.TRCon etc. in Tradition.v | in our original formalization, we used the term "Traditional" instead of "Declarative" |
Reductive Subtyping Rules | see User-Defined Typing Rules | While Declarative Rules add reflexivity and transitivity, Reductive Rules are all user-supplied in this more general framework |
Requirement 1: Syntax-Directedness | DecidableRules.finite_con in Decide.v | |
Requirement 2: Well-Foundedness | DecidableRules.wf in Decide.v | |
Requirement 3: Literal Reflexivity | DecidableRules.refl in Decide.v | Since everything is a literal/type, this captures all types |
Subtyping Rules with Assumptions | ProofPV.ProofPV etc. in Common.v | |
Requirement 4: R-to-D Literal Conversion | Converter.decidable_traditional_R in Convert.v | |
Requirement 5: D-to-R Literal Conversion | Converter.traditional_decidable_R in Convert.v | |
Requirement 6: Literal Transitivity | DecidableRules.Red in Decide.v | See also Reduction.Reduction in Common.v |
Decidability of Declarative Subtyping Theorem | Conversion.decidable_traditional and Conversion.traditional_decidable in Convert.v | Together with Decider.decider in Decide.v |
Extended Subtyping | Extension.Con and ExtendedRules.ECon etc. in Extend.v | |
Intersector/Integrator | Comonad.i in Preprocess.v | Since everything is a literal/type, there is no distinction between intersector and integrator |
Requirement 7: Intersector Completeness | Equivocator.iextended in Equate.v | |
Requirement 8: Intersector Soundness | Equivocator.unit in Equate.v | |
Lemma 1: Integrated Soundness | Equivalence.ipreprocessing_extended in Equate.v | |
Requirement 9: Measure Preservation | WellFoundedComonad.i_wf in Preprocess.v | Requires full well-foundedness proof instead of measure preservation |
Lemma 2: Integrated Decidability | Decider.decider in Preprocess.v | |
Requirement 10: Literal Dereliction | Comonad.counit in Preprocess.v | |
Lemma 3: Dereliction | Comonad.counit in Preprocess.v | Same as Requirement 10 due to missing type/literal distinction |
Intersected Predicate | Comonad.Preprocessed in Preprocess.v | |
Requirement 11: Intersector Integrated | Comonad.i_Preprocessed in Preprocess.v | |
Lemma 4: Integrator Integrated | Comonad.i_Preprocessed in Preprocess.v | Same as Requirement 11 due to missing type/literal distinction |
Requirement 12: Literal Promotion | Comonad.i_promote_R in Preprocess.v | |
Lemma 5: Promotion | Preprocessing.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 Promotion | Preprocessing.promote in Preprocess.v | |
Lemma 9: Integrated Reflexivity | Comonad.derelict and Comonad.refl in Preprocess.v | |
Lemma 10: D-to-I Literal Conversion | Equivalence.iadmitst in Equate.v | |
Lemma 11: Integrated Transitivity | Preprocessing.itrans in Preprocess.v | |
Lemma 12: Integrated Completeness | Equivalence.extended_ipreprocessing in Equate.v | |
Decidability of Extended Subtyping Theorem | Equivalence.decider in Equate.v |
Common Definitions (Common.v)
This module defines our formalization of subtyping proof rules and proofs that lie at the heart of our system.User-Defined Types
With modules of this type, a user provides the syntactic representation of types in the system at handUser-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.
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.
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.
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.
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.
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.
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.
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.
Section Decider.
Lemma decider (t t' : T) : { Decidable t t' } + { Decidable t t' -> False }.
End Decider.
End Decidable.
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.
- 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
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
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
CommonConvert
D
DecideE
EquateExtend
I
IntroductionP
PreprocessT
TraditionLemma 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