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