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.

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