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
Require Import Common.
Require Import Tradition.
Require Import Decide.
Require Import Convert.
Require Import Extend.
Require Import Preprocess.
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).
Import T.
Import 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).
Import T.
Import I.
Import Eq.
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'.
apply Extended.trans. apply unit.
Qed.
Lemma iadmitsb : Basic.Admits iPreprocessing.
apply traditional_decidable_R.
intros t t1 t4 pre d. eapply Preprocessing.decidable_trans; [ exact pre | exact d | ]. apply Preprocessing.refl.
intros t1 t2 t3 t4 id ed id' t0 t5 pre d d'. apply ed; try assumption.
revert d id. apply Decidable.trans.
revert id' d'. apply Decidable.trans.
exact Preprocessing.iadmitsd.
Qed.
Lemma iadmitst : Traditional.Proof.Admits iPreprocessing.
apply traditional_decidable_R_trans.
intros t t' d t1 t4 pre d' d''. apply Preprocessing.decidable_preprocessing in d. revert pre d' d d''. apply Preprocessing.decidable_trans.
intros t1 t2 t3 ed ed' t0 t5 pre d d'. apply @Preprocessing.trans with (i t2); try assumption.
apply Preprocessing.promote'; try assumption. apply ed; try assumption. apply DDRule.refl.
apply ed'; try assumption.
apply i_preprocessed.
apply counit.
exact Preprocessing.iadmitsd.
Qed.
Theorem extended_ipreprocessing' {t t' : T} : Extended t t' -> iPreprocessing t t'.
intro ei. induction ei as [ t t' con _ rec ]. destruct con as [ con | con ].
apply (iadmitst t t' con). assumption.
clear rec. apply iextended in con. apply traditional_decidable in con. intros t1 t4 pre d d'. apply Preprocessing.decidable_preprocessing. revert d'. apply Decidable.trans. revert con. apply Decidable.trans. apply Preprocessing.dpromote'; assumption.
Qed.
Theorem extended_ipreprocessing {t t' : T} : Extended t t' -> Preprocessing (i t) t'.
intro ei. apply extended_ipreprocessing' in ei. apply ei.
apply i_preprocessed.
apply counit.
apply DDRule.refl.
Qed.
Theorem ipreprocessing_extended {t t' : T} : Preprocessing (i t) t' -> Extended t t'.
intro ed. apply iextended_extended. revert ed. unfold iPreprocessing. unfold Preprocessing.iPreprocessing. generalize (i t). clear t. intros t ed. induction ed as [ t t' con _ rec ]. apply (fun A => decidable_traditional_R Extended A t t' con).
clear t t' con rec. intros t t' con ass. apply (Extended.Proof.proof (Extended.ExtendedRules.traditional con)). assumption.
simpl in rec. intro req. pose proof (rec req) as rec. destruct (Opt req) as [ _ | ].
assumption.
apply iextended_extended. assumption.
Qed.
End Equivalence.
Section Decider.
Theorem decider : forall t t' : T, {Extended t t'} + {~ Extended t t'}.
intros t t'. destruct (Preprocessing.decider t t').
left. apply ipreprocessing_extended. assumption.
right. intros H. apply f. apply extended_ipreprocessing. assumption.
Qed.
End Decider.
End Equivalence.
This page has been generated by coqdoc