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).
Import T.
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.
Import T.
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).
Import T.
Import Rule.
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.
Arguments proof [t1 t2].
Lemma proof_admits : Admits Proof.
intros t1 t2 con rec. apply (proof con). assumption.
Qed.
Import T.
Import Rule.
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.
Arguments proof [t1 t2].
Lemma proof_admits : Admits Proof.
intros t1 t2 con rec. apply (proof con). assumption.
Qed.
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'.
intros ra rr t1' t2' trace. induction trace.
assumption.
apply IHtrace. apply rr. assumption.
Qed.
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''.
intros trace trace'. induction trace'.
assumption.
apply recursion with _ req. assumption.
Qed.
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''.
intros trace trace'. revert trace' trace. apply trace_comp.
Qed.
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'.
intros ra rr t1' t2' trace. induction trace.
assumption.
apply IHtrace. apply rr. assumption.
Qed.
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''.
intros trace trace'. induction trace'.
assumption.
apply recursion with _ req. assumption.
Qed.
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''.
intros trace trace'. revert trace' trace. apply trace_comp.
Qed.
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).
Arguments permit [P t t'].
Arguments proofP [P t t'].
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'.
intros imp t t' p. induction p as [ t t' p | t t' con _ rec ].
apply permit. apply imp. assumption.
apply (proofP con). assumption.
Qed.
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'.
intro d. induction d as [ t t' p | t t' con ass rec ].
apply bind. assumption.
apply (proofP con). assumption.
Qed.
Lemma proof_proofP {t t' : T} : Proof t t' -> ProofP (fun t t' => False) t t'.
intro p. induction p as [ t t' con _ rec ]. apply proofP with con. intro req. apply rec.
Qed.
Lemma proofP_proof {t t' : T} : ProofP (fun t t' => False) t t' -> Proof t t'.
intro p. induction p as [ t t' f | t t' con _ rec ].
destruct f.
apply proof with con. assumption.
Qed.
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. destruct v; reflexivity. Qed.
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'). destruct v; destruct v'; reflexivity. Qed.
Lemma multiply_covariant (v : Variance) : multiply v covariant = v. destruct v; reflexivity. Qed.
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).
Import T.
Import Rule.
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).
Import T.
Import Rule.
Import ORule.
Module Proof := Proofs T Rule.
Import Proof.
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).
Arguments permitV [P v t t'].
Arguments proofPV [P] v [t t'].
Lemma proof_admitsPV (P : Variance -> T -> T -> Prop) : AdmitsPV (ProofPV P).
intros v t t' con ass. apply proofPV with con. assumption.
Qed.
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'.
intros imp v t t' p. induction p as [ v t t' p | v t t' con _ rec ].
apply permitV. apply imp. assumption.
apply (proofPV _ con). assumption.
Qed.
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'.
intros t t' d. induction d as [ v t t' p | v t t' con ass rec ].
apply permitV. rewrite invert_invert. assumption.
apply (proofPV _ con). intro req. pose proof (rec req) as rec. rewrite multiply_invert. assumption.
Qed.
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'.
intros sub t t' p. apply invertPV in p. revert p. apply monoV. clear v t t'. intro v. destruct v; apply sub.
Qed.
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'.
intro d. induction d as [ v t t' p | v t t' con ass rec ].
apply bind. assumption.
apply (proofPV _ con). assumption.
Qed.
Lemma proofP_proofPV (v : Variance) {P : T -> T -> Prop} {t t' : T} : ProofP P t t' -> ProofPV (fun v => P) v t t'.
intro p. revert v. induction p as [ t t' p | t t' con _ rec ].
intro v. apply permitV. assumption.
intro v. apply proofPV with con. intro req. apply rec.
Qed.
Lemma proofPV_proofP {v : Variance} {P : T -> T -> Prop} {t t' : T} : ProofPV (fun v => P) v t t' -> ProofP P t t'.
intro p. induction p as [ v t t' f | v t t' con _ rec ].
apply permit. assumption.
apply proofP with con. assumption.
Qed.
Lemma proof_proofPV (v : Variance) {t t' : T} : Proof t t' -> ProofPV (fun v t t' => False) v t t'.
intro p. apply proofP_proofPV. revert p. apply proof_proofP.
Qed.
Lemma proofPV_proof {v : Variance} {t t' : T} : ProofPV (fun v t t' => False) v t t' -> Proof t t'.
intro p. apply proofPV_proofP in p. revert p. apply proofP_proof.
Qed.
End ProofPV.
Definition invert (v : Variance) : Variance
:= match v with covariant => contravariant | contravariant => covariant end.
Lemma invert_invert (v : Variance) : invert (invert v) = v. destruct v; reflexivity. Qed.
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'). destruct v; destruct v'; reflexivity. Qed.
Lemma multiply_covariant (v : Variance) : multiply v covariant = v. destruct v; reflexivity. Qed.
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).
Import T.
Import Rule.
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).
Import T.
Import Rule.
Import ORule.
Module Proof := Proofs T Rule.
Import Proof.
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).
Arguments permitV [P v t t'].
Arguments proofPV [P] v [t t'].
Lemma proof_admitsPV (P : Variance -> T -> T -> Prop) : AdmitsPV (ProofPV P).
intros v t t' con ass. apply proofPV with con. assumption.
Qed.
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'.
intros imp v t t' p. induction p as [ v t t' p | v t t' con _ rec ].
apply permitV. apply imp. assumption.
apply (proofPV _ con). assumption.
Qed.
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'.
intros t t' d. induction d as [ v t t' p | v t t' con ass rec ].
apply permitV. rewrite invert_invert. assumption.
apply (proofPV _ con). intro req. pose proof (rec req) as rec. rewrite multiply_invert. assumption.
Qed.
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'.
intros sub t t' p. apply invertPV in p. revert p. apply monoV. clear v t t'. intro v. destruct v; apply sub.
Qed.
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'.
intro d. induction d as [ v t t' p | v t t' con ass rec ].
apply bind. assumption.
apply (proofPV _ con). assumption.
Qed.
Lemma proofP_proofPV (v : Variance) {P : T -> T -> Prop} {t t' : T} : ProofP P t t' -> ProofPV (fun v => P) v t t'.
intro p. revert v. induction p as [ t t' p | t t' con _ rec ].
intro v. apply permitV. assumption.
intro v. apply proofPV with con. intro req. apply rec.
Qed.
Lemma proofPV_proofP {v : Variance} {P : T -> T -> Prop} {t t' : T} : ProofPV (fun v => P) v t t' -> ProofP P t t'.
intro p. induction p as [ v t t' f | v t t' con _ rec ].
apply permit. assumption.
apply proofP with con. assumption.
Qed.
Lemma proof_proofPV (v : Variance) {t t' : T} : Proof t t' -> ProofPV (fun v t t' => False) v t t'.
intro p. apply proofP_proofPV. revert p. apply proof_proofP.
Qed.
Lemma proofPV_proof {v : Variance} {t t' : T} : ProofPV (fun v t t' => False) v t t' -> Proof t t'.
intro p. apply proofPV_proofP in p. revert p. apply proofP_proof.
Qed.
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).
Import T.
Import Rule.
Import ORule.
Module ProofPV := ProofPV T Rule ORule.
Import ProofPV.
Module Proof := ProofPV.Proof.
Import 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.
Import T.
Import Rule.
Import ORule.
Module ProofPV := ProofPV T Rule ORule.
Import ProofPV.
Module Proof := ProofPV.Proof.
Import 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.
This page has been generated by coqdoc