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.Require Import Common.
Require Import Tradition.
Require Import Decide.
Module Type Converter (T : Typ) (TRule DRule : Rules T) (ORule : OrientedRules T DRule) (DDRule : DecidableRules T DRule ORule).
Import T.
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).
Import T.
Import CRule.
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'.
intro d. induction d as [ t t' con _ req ]. apply (decidable_traditional_R Traditional Traditional.Proof.proof_admits _ _ con). assumption.
Qed.
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.
intros R d_R R_trans R_admits t t' con ass. destruct con as [ t | t1 t2 t3 | t t' con ].
apply d_R. apply DDRule.refl.
apply R_trans with t2.
apply (ass left).
apply (ass right).
apply traditional_decidable_R with con; try assumption; clear t t' con ass.
intro t. apply d_R. apply DDRule.refl.
intros t1 t2 t3 t4 d r d'. apply d_R in d. apply d_R in d'. apply R_trans with t2; try assumption. apply R_trans with t3; assumption.
Qed.
Lemma dadmitst : Traditional.Proof.Admits Decidable.
apply traditional_decidable_R_trans.
intros t t' d. assumption.
exact @Decidable.trans.
apply Decidable.Proof.proof_admits.
Qed.
Lemma traditional_decidable {t t' : T} : Traditional t t' -> Decidable t t'.
intro tr. induction tr as [ t t' con _ rec ]. apply (dadmitst _ _ con). assumption.
Qed.
End Conversion.
This page has been generated by coqdoc