Infrastructure
At this point, there are a few definitions and lemmas that are not central to understanding the proofs and in some sense self-explanatory, and therefore omitted from this document. Please see Section3_Infrastructure.v for those definitions and lemmas.Require Import List.
Require Import Nat.
Require Import Util.
Require Import Wf.
Require Import Plus.
Require Import Wellfounded.Transitive_Closure.
Require Import Wellfounded.Inverse_Image.
Require Import Relation_Definitions.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Import Relation_Operators.
Import List.
Import ListNotations.
Proof of Decidability of Subtyping (Section3_Proofs.v)
The single theorem of Section 3 is as follows: For every set of literals Lit, set of declarative rules (DRule, DPremise), and set of reductive rules (RRule, RPremise) satisfying Requirements 1 through 6, proof search for reductive subtyping as defined in Figure 2 (rsub) is a decision procedure for declarative subtyping as defined in Figure 1 (dsub).- We prove that rsub is decidable (rsub_dec)
- We prove that rsub is reflexive (rsub_refl) and transitive (rsub_trans)
- We prove that rsub is equivalent to dsub (rsub_dsub)
- We prove that dsub is decidable by using the decidability of rsub and its equivalence to dsub (DecidabilityOfDeclarativeSubtyping)
Deciability of rsub
The decidability of rsub is established using a well-founded measure and proving that every recursive step of rsub reduces the size of that measure. The particular measure used here, progress_measure, is based on the lexicographic ordering of the measure mlt (or more precisely, its transitive closure mltt) provided by the user and the syntactic depth of literals within a given type (syntactic_literal_depth). The former guarantees that the measure is reduced when recursively stepping into the premises of the literal subtyping rule, whereas the latter guarantees that the measure is reduced when union or intersection rules are applied, where mlt is only required to be less-than-or-equal. We first define the measure and its components, establish its well-foundedness (progress_measure_wf) and transitivity (progress_measure_trans, for convenience), and finally prove that rsubf is decidable for any set of premises that reduce the measure in the literal step (rsubf_dec). This is then easily applied to rsub, because RPremise by Requirement 2 (in particular, m_lit) has this property, which gives us rsub_dec.Module TraditionalDec (M_Traditional : Traditional).
Import M_Traditional.
Module M_Infrastructure := UIType_Infrastructure(M_Traditional).
Import M_Infrastructure.
Fixpoint syntactic_literal_depth (t : T) :=
match t with
| TTop => 0
| TBot => 0
| TUni l r => 1 + (max (syntactic_literal_depth l) (syntactic_literal_depth r))
| TIsect l r => 1 + (max (syntactic_literal_depth l) (syntactic_literal_depth r))
| TLit l => 0
end.
Definition mltt: M -> M -> Prop := clos_trans M mlt.
Definition mltt_wf : well_founded mltt := wf_clos_trans M mlt mltwf.
Lemma mltt_trans : forall ml mm mr : M, mltt ml mm -> mltt mm mr -> mltt ml mr.
intros ml mm mr Hlm Hmr. apply t_trans with mm; assumption.
Qed.
Definition PM : Type := M * nat.
Definition pm (tp : T * T) : PM := (m (fst tp) (snd tp), ((syntactic_literal_depth (fst tp)) + (syntactic_literal_depth (snd tp)))).
Definition pmlt (pml pmr : PM) : Prop := mltt (fst pml) (fst pmr) \/ (fst pml = fst pmr /\ snd pml < snd pmr).
Definition progress_measure (tpl tpr : T * T) : Prop := pmlt (pm tpl) (pm tpr).
Lemma lt_Acc_pmlt_acc : forall pmr : PM, (forall pml : PM, mltt (fst pml) (fst pmr) -> Acc pmlt pml) -> Acc lt (snd pmr) -> Acc pmlt pmr.
intros pmr Haccl Hacc. destruct pmr. simpl in *. induction Hacc. constructor. intros pml Hlt. destruct Hlt as [Hlt | [Hltm Hltnat]].
apply Haccl; assumption.
apply H0 in Hltnat. destruct pml. simpl in *. subst. assumption.
Qed.
Lemma mltt_Acc_pmlt_acc : forall pmr : PM, Acc mltt (fst pmr) -> Acc pmlt pmr.
intros [mr nr] Hacc. simpl in *. generalize dependent nr. induction Hacc. constructor. intros [ml nl] [Hlt | [Hltm Hltn]].
apply lt_Acc_pmlt_acc. intros pml Hltt. destruct pml as [ml' nl']. simpl in *. apply H0. apply t_trans with ml; assumption. apply PeanoNat.Nat.lt_wf_0.
apply lt_Acc_pmlt_acc. intros pml Hltt. destruct pml as [ml' nl']. simpl in *. apply H0. subst. assumption. apply PeanoNat.Nat.lt_wf_0.
Qed.
Lemma pmlt_wf : well_founded pmlt.
intros pm. apply mltt_Acc_pmlt_acc. apply mltt_wf.
Qed.
Lemma progress_measure_wf : well_founded progress_measure.
unfold progress_measure. apply wf_inverse_image. apply pmlt_wf.
Qed.
Ltac solve_lt := match goal with
| [|- ?n <= ?n] => reflexivity
| [|- ?n <= S ?n] => apply PeanoNat.Nat.le_succ_diag_r
| [|- _ \/ _] => left; solve_lt
| [|- _ \/ _] => right; solve_lt
| [|- ?n < S ?n] => apply PeanoNat.Nat.lt_succ_diag_r
| [|- ?n < S (max _ _)] => rewrite -> PeanoNat.Nat.succ_max_distr; solve_lt
| [|- max _ _ < ?n] => apply PeanoNat.Nat.max_lub_lt; solve_lt
| [|- ?n < max _ _] => apply PeanoNat.Nat.max_lt_iff; solve_lt
| [|- ?n < match ?x with | _ => _ end] => destruct x; try solve_lt
| [|- 0 < S _] => apply PeanoNat.Nat.lt_0_succ
| [|- context C [S (_ + _)]] => rewrite <- PeanoNat.Nat.add_succ_r; solve_lt
| [|- context C [S (_ + _)]] => rewrite <- PeanoNat.Nat.add_succ_l; solve_lt
| [|- _ + _ < _ + _] => apply plus_lt_le_compat; solve_lt
| [|- _ + _ < _ + _] => apply plus_le_lt_compat; solve_lt
| [H : ?n < ?m |- ?n < ?p] => apply PeanoNat.Nat.lt_trans with m; [assumption|clear H]; solve_lt
| [H : ?m < ?p |- ?n < ?p] => apply PeanoNat.Nat.lt_trans with m; [clear H | assumption]; solve_lt
| [H : ?a |- ?a] => apply H
end.
Lemma progress_measure_trans : forall tpl tpm tpr : T * T, progress_measure tpl tpm -> progress_measure tpm tpr -> progress_measure tpl tpr.
intros tpl tpm tpr Hlm Hmr. destruct Hlm as [Hlm | [Hlmeq Hlms]]; destruct Hmr as [Hmr | [Hmreq Hmrs]].
left. apply mltt_trans with (fst (pm (tpm))); assumption.
left. rewrite -> Hmreq in Hlm. assumption.
left. rewrite <- Hlmeq in Hmr. assumption.
right. split.
rewrite -> Hlmeq. assumption.
apply PeanoNat.Nat.lt_trans with (snd (pm tpm)); assumption.
Qed.
Ltac solve_progress_measure_step := match goal with
| [H : progress_measure _ _ |- _] => let H' := fresh H in destruct H as [H | [H H']]; simpl in *
| [tp : T * T |- _] => let tpr := fresh tp in destruct tp as [tp tpl]; simpl in *
| [|- progress_measure (?tl, ?tr) (?tl, ?trx)] => unfold progress_measure; unfold pmlt; simpl
| [|- progress_measure (?tl, ?tr) (?tlx, ?tr)] => unfold progress_measure; unfold pmlt; simpl
| [|- progress_measure (?tl, ?tr) ((_ ?tl _), ?trx)] => apply progress_measure_trans with (tl, trx); unfold progress_measure; unfold pmlt; simpl
| [|- progress_measure (?tl, ?tr) ((_ _ ?tl), ?trx)] => apply progress_measure_trans with (tl, trx); unfold progress_measure; unfold pmlt; simpl
| [|- progress_measure (?tl, ?tr) (?tlx, (_ ?tr _))] => apply progress_measure_trans with (tlx, tr); unfold progress_measure; unfold pmlt; simpl
| [|- progress_measure (?tl, ?tr) (?tlx, (_ _ ?tr))] => apply progress_measure_trans with (tlx, tr); unfold progress_measure; unfold pmlt; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) ((_ ?tlx _), (_ ?trx _))] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) (?tlx, (_ ?trx _))] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) ((_ ?tlx _), ?trx)] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) ((_ _ ?tlx), (_ _ ?trx))] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) (?tlx, (_ _ ?trx))] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [H : mltt (m ?tl ?tr) (m ?tlx ?trx) |- progress_measure (?tl, ?tr) ((_ _ ?tlx), ?trx)] => left; apply clos_t_rt with (m tlx trx); [assumption|]; simpl
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m (_ ?tl _) ?trx)] => apply rt_trans with (m tl trx); [apply m_ui_r; constructor |]
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m (_ ?tl _) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m ?tlx (_ ?tr _))] => apply rt_trans with (m tlx tr); [|apply m_ui_l; constructor]
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m ?tl (_ ?tr _))] => apply m_ui_r; constructor
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m (_ _ ?tl) ?trx)] => apply rt_trans with (m tl trx); [apply m_ui_r; constructor |]
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m (_ _ ?tl) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m ?tlx (_ _ ?tr))] => apply rt_trans with (m tlx tr); [|apply m_ui_l; constructor]
| [|- clos_refl_trans M mlt (m ?tl ?tr) (m ?tl (_ _ ?tr))] => apply m_ui_r; constructor
| [H : m ?tl ?tr = m _ _ |- progress_measure (?tl, ?tr) _] => unfold progress_measure; unfold pmlt; simpl; rewrite -> H in *; clear H
| [|- mltt (m ?tl ?tr) (m ?tlx ?tr) \/ (_ = _ /\ _ < _)] => missing (subui tl tlx); let H:= fresh in assert (H : subui tl tlx) by constructor ; apply (m_ui_l _ _ tr) in H ;apply clos_refl_trans_refl_or_trans in H; destruct H as [H | H]; [right; split; [assumption| try solve_lt] | left; assumption]
| [|- mltt (m ?tl ?tr) (m ?tl ?trx) \/ (_ = _ /\ _ < _)] => missing (subui tr trx); let H:= fresh in assert (H : subui tr trx) by constructor ; apply (m_ui_r tl) in H ;apply clos_refl_trans_refl_or_trans in H; destruct H as [H | H]; [right; split; [assumption|try solve_lt] | left; assumption]
end.
Ltac solve_progress_measure := repeat solve_progress_measure_step.
Ltac tac_rsub_dec := match goal with
| [|- {rsubf _ ?tl ?tr} + {~ rsubf _ ?tl ?tr}] => right; let Hcontra := fresh in intros Hcontra; apply rsubf_uisub in Hcontra; inversion Hcontra; fail
| [|- {rsubf _ ?tl ?tr} + {~ rsubf _ ?tl ?tr}] => left; repeat constructor; assumption
| [IH : forall y : T * T, progress_measure y (?tl, ?tr) -> {rsubf _ (fst y) (snd y)} + {~ rsubf _ (fst y) (snd y)}, H : (forall y : T * T, progress_measure y (?tl', ?tr') -> {rsubf _ (fst y) (snd y)} + {~ rsubf _ (fst y) (snd y)}) -> ?a |- _] => let H' := fresh H in assert (H' : a) by (apply H; intros; apply IH; solve_progress_measure); clear H
| [IH : forall y : T * T, progress_measure y (?tl, ?tr) -> {rsubf ?Prem (fst y) (snd y)} + {~ rsubf _ (fst y) (snd y)}, H : ~ rsubf _ ?tl' ?tr' -> ?a |- _] => let H' := fresh H in assert (H' : {rsubf Prem (fst (tl', tr')) (snd (tl', tr'))} + {~rsubf Prem (fst (tl', tr')) (snd (tl', tr'))}) by (apply IH; solve_progress_measure); destruct H' as [H' | H']; [|let H'' := fresh H' in pose proof (H H') as H'']; clear H; simpl in *
| [Hsub : {rsubf _ ?tl ?tr} + {~ rsubf _ ?tl ?tr} |- _] => destruct Hsub as [Hsub | Hsub]
| [Hl : rsubf _ ?t ?tl |- {rsubf _ ?t (TUni ?tl ?tr)} + {~rsubf _ ?t (TUni ?tl ?tr)}] => left ; constructor; apply rsubf_uisub in Hl; apply ui_uni_rl; apply Hl
| [Hr : rsubf _ ?t ?tr |- {rsubf _ ?t (TUni ?tl ?tr)} + {~rsubf _ ?t (TUni ?tl ?tr)}] => left ; constructor; apply rsubf_uisub in Hr; apply ui_uni_rr; apply Hr
| [Hn : ~ rsubf _ ?tl ?tr, Hc : uisub (lsub _ (rsubf _)) ?tl ?tr |- _] => apply Rsubf in Hc; contradiction
| [Hl : ~ rsubf _ ?t ?tl, Hr : ~rsubf _ ?t ?tr |- {rsubf _ ?t (TUni ?tl ?tr)} + {~rsubf _ ?t (TUni ?tl ?tr)}] => let Hcontra := fresh Hl in right ; intros Hcontra; apply rsubf_uisub in Hcontra; inversion Hcontra; subst
| [Hl : rsubf _ ?t ?tl, Hr : rsubf _ ?t ?tr |- {rsubf _ ?t (TIsect ?tl ?tr)} + {~rsubf _ ?t (TIsect ?tl ?tr)}] => left ; constructor; apply rsubf_uisub in Hl; apply rsubf_uisub in Hr; apply ui_int_r; assumption
| [Hl : ~rsubf _ ?t ?tl |- {rsubf _ ?t (TIsect ?tl ?tr)} + {~rsubf _ ?t (TIsect ?tl ?tr)}] => let Hcontra := fresh Hl in right ; intros Hcontra; apply rsubf_uisub in Hcontra; apply uisub_int_r in Hcontra; let Hc' := fresh Hcontra in destruct Hcontra as [Hcontra Hc']; apply Rsubf in Hcontra; apply Rsubf in Hc'; contradiction
| [Hr : ~rsubf _ ?t ?tr |- {rsubf _ ?t (TIsect ?tl ?tr)} + {~rsubf _ ?t (TIsect ?tl ?tr)}] => let Hcontra := fresh Hr in right ; intros Hcontra; apply rsubf_uisub in Hcontra; apply uisub_int_r in Hcontra; let Hc' := fresh Hcontra in destruct Hcontra as [Hcontra Hc']; apply Rsubf in Hcontra; apply Rsubf in Hc'; contradiction
| [Hl : rsubf _ ?tl ?t, Hr : rsubf _ ?tr ?t |- {rsubf _ (TUni ?tl ?tr) ?t} + {~ rsubf _ (TUni ?tl ?tr) ?t}] => left; constructor; apply ui_uni_l; apply rsubf_uisub; assumption
| [Hl : ~ rsubf _ ?tl ?t |- {rsubf _ (TUni ?tl ?tr) ?t} + {~ rsubf _ (TUni ?tl ?tr) ?t}] => right; let Hcontra := fresh Hl in intros Hcontra; apply rsubf_uisub in Hcontra; apply uisub_uni_l in Hcontra; let Hc' := fresh Hcontra in destruct Hcontra as [Hcontra Hc']; apply Rsubf in Hcontra; apply Rsubf in Hc'; contradiction
| [Hr : ~ rsubf _ ?tr ?t |- {rsubf _ (TUni ?tl ?tr) ?t} + {~ rsubf _ (TUni ?tl ?tr) ?t}] => right; let Hcontra := fresh Hr in intros Hcontra; apply rsubf_uisub in Hcontra; apply uisub_uni_l in Hcontra; let Hc' := fresh Hcontra in destruct Hcontra as [Hcontra Hc']; apply Rsubf in Hcontra; apply Rsubf in Hc'; contradiction
| [Hl : rsubf _ ?tl ?t |- {rsubf _ (TIsect ?tl ?tr) ?t} + {~ rsubf _ (TIsect ?tl ?tr) ?t}] => left; constructor; apply ui_int_ll; apply rsubf_uisub; assumption
| [Hr : rsubf _ ?tr ?t |- {rsubf _ (TIsect ?tl ?tr) ?t} + {~ rsubf _ (TIsect ?tl ?tr) ?t}] => left; constructor; apply ui_int_lr; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- {rsubf _ (TIsect ?tl _) (TUni ?tr _)} + {~ rsubf _ (TIsect ?tl _) (TUni ?tr _)}] => left; constructor; apply ui_int_ll; apply ui_uni_rl; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- {rsubf _ (TIsect _ ?tl) (TUni ?tr _)} + {~ rsubf _ (TIsect _ ?tl) (TUni ?tr _)}] => left; constructor; apply ui_int_lr; apply ui_uni_rl; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- {rsubf _ (TIsect ?tl _) (TUni _ ?tr)} + {~ rsubf _ (TIsect ?tl _) (TUni _ ?tr)}] => left; constructor; apply ui_int_ll; apply ui_uni_rr; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- {rsubf _ (TIsect _ ?tl) (TUni _ ?tr)} + {~ rsubf _ (TIsect _ ?tl) (TUni _ ?tr)}] => left; constructor; apply ui_int_lr; apply ui_uni_rr; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- uisub _ (TIsect ?tl _) ?tr] => apply ui_int_ll; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- uisub _ (TIsect _ ?tl) ?tr] => apply ui_int_lr; apply rsubf_uisub; assumption
| [H : rsubf _ ?tl ?tr |- uisub _ ?tl ?tr] => apply rsubf_uisub; assumption
| [|- {rsubf _ _ (TIsect _ _)} + {~rsubf _ _ (TIsect _ _)}] => left; constructor; apply ui_int_r
end.
Lemma rsubf_dec {Premise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} (Hpremsd : forall {ll lr : Lit} (r : RRule ll lr), { rpremises : list (prod (T) (T)) | forall pl pr : T, Premise ll lr r pl pr <-> In (pair pl pr) rpremises }) (HMlit : forall {ll lr : Lit} (r : RRule ll lr) (tl tr : T), Premise ll lr r tl tr -> progress_measure (tl, tr) (TLit ll, TLit lr)) : forall tl tr : T, {rsubf Premise tl tr} + {~ rsubf Premise tl tr}.
intros tl tr. change ({rsubf Premise (fst (tl, tr)) (snd (tl, tr))} + {~ rsubf Premise (fst (tl, tr)) (snd (tl, tr))}). apply (well_founded_induction progress_measure_wf (fun tp : T * T => {rsubf Premise (fst tp) (snd tp)} + {~ rsubf Premise (fst tp) (snd tp)})); clear tl tr.
intros [tl tr] IH. simpl in *. induction tl.
induction tr; repeat tac_rsub_dec.
induction tr; repeat tac_rsub_dec.
repeat tac_rsub_dec.
repeat tac_rsub_dec. induction tr.
right. intros Hcontra. apply IHtl0. repeat constructor.
right. intros Hcontra. apply rsubf_uisub in Hcontra. inversion Hcontra; subst; apply Rsubf in H2; contradiction.
repeat tac_rsub_dec.
repeat tac_rsub_dec.
right. intros Hcontra. apply rsubf_uisub in Hcontra. inversion Hcontra; subst; apply Rsubf in H2; contradiction.
induction tr; repeat tac_rsub_dec.
pose proof (SyntaxDirectedness_Rules l l0) as [rules Hrules]. assert (Hrapp : {r : RRule l l0 | In r rules /\ forall tl tr : T, Premise l l0 r tl tr -> rsubf Premise tl tr} + {forall r : RRule l l0, In r rules -> exists tp : T * T, Premise l l0 r (fst tp) (snd tp) /\ ~ rsubf Premise (fst tp) (snd tp)}).
clear Hrules. induction rules; [right; intros r HIn; inversion HIn |]. destruct IHrules as [[r [HIn Hprem]] | Hnrule]; [left; apply (exist (fun r' => In r' (a :: rules) /\ forall tl tr : T, Premise l l0 r' tl tr -> rsubf Premise tl tr) r); split; [apply in_cons|]; assumption|]. pose proof (Hpremsd _ _ a) as [premises Hpremises]; clear Hpremsd. assert (Hpdec : {forall tl tr : T, In (tl, tr) premises -> rsubf Premise tl tr} + {exists tp : T * T, Premise l l0 a (fst tp) (snd tp) /\ ~ rsubf Premise (fst tp) (snd tp)}). clear Hnrule. assert (Hpremises' : forall pl pr : T, In (pl, pr) premises -> Premise l l0 a pl pr) by (apply Hpremises). clear Hpremises. induction premises; [left; intros tl tr HIn; inversion HIn|]. assert (Hpremdec: {forall tl tr : T, In (tl, tr) premises -> rsubf Premise tl tr} + {exists tp : T * T, Premise l l0 a (fst tp) (snd tp) /\ ~ rsubf Premise (fst tp) (snd tp)}) by (apply IHpremises; intros; apply Hpremises'; apply in_cons; assumption); clear IHpremises. destruct Hpremdec as [Hprem | Hnprem]; [|right; assumption]. destruct a0 as [tl tr]. pose proof (Hpremises' tl tr (in_eq (tl, tr) premises)) as Hp. apply HMlit in Hp. apply IH in Hp. simpl in Hp. destruct Hp as [Hp | Hnp]; [left; intros tl' tr' [HIn | HIn]; [inversion HIn;subst| apply Hprem in HIn]; assumption |]. right. exists (tl, tr). split; [|assumption]. apply Hpremises'; apply in_eq.
destruct Hpdec as [Hpdec | Hpdec].
left. exists a. split; [apply in_eq |]. intros tl tr Hp. apply Hpremises in Hp. apply Hpdec in Hp. assumption.
right. intros r HIn. inversion HIn; subst; [|apply Hnrule]; assumption.
destruct Hrapp as [[r [HIn Hprem]] | Hn].
left. constructor. constructor. apply Lsub with r. assumption.
right. intros Hsub. apply rsubf_uisub in Hsub. inversion Hsub; subst. destruct H1 as [r Hr]. pose proof (Hn r (Hrules r)) as [tp [Hp Hsub']]. apply Hr in Hp. contradiction.
Qed.
Lemma rsub_dec : forall tl tr : T, {rsub tl tr} + {~ rsub tl tr}.
apply rsubf_dec.
intros ll lr. apply SyntaxDirectedness_Premises.
intros ll lr r tl tr Hp. pose proof (m_lit r tl tr Hp). left. apply t_step. assumption.
Qed.
An induction principle and Reflexivity
Next, we use the progress_measure to prove a mutual induction principle on types T and literals Lit: uirec_alt. The only part of it that so far has not been mentioned is the predicate uirec, defined in Section3_Infrastructure.v, which specifies that, for two given types, a given relation on Literals holds for all pairs of literals contained in the cross product of the literals contained somewhere in each of the two types. This induction principle is used to prove most of the following Lemmas, starting with reflexivity (rsub_refl), which is otherwise straightforward, using Requirement 3 LiteralReflexivity.Lemma uirec_alt (RL : Lit -> Lit -> Prop) (RT : T -> T -> Prop) : (forall {ll lr : Lit} , (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> (RT tl tr)) -> RL ll lr) -> (forall (tl tr : T), uirec RL tl tr -> RT tl tr) -> forall (tl tr : T), RT tl tr.
intros Hlits Hrec tl tr. apply Hrec. change (uirec RL (fst (tl, tr)) (snd (tl, tr))). apply (well_founded_ind progress_measure_wf (fun tp => uirec RL (fst tp) (snd tp))).
clear tl tr. intros [ tl tr ] IH. pose proof (fun tl' tr' => IH (pair tl' tr')) as IH'. clear IH. simpl in *. unfold uirec. destruct tl; destruct tr; simpl; try (apply ForallCrossPairs_nil_l || apply ForallCrossPairs_app_l; split); try (apply ForallCrossPairs_nil_r || apply ForallCrossPairs_app_r; split); try apply IH'; try apply (fun l => IH' (TLit l)); try apply (fun tl lr => IH' tl (TLit lr)); solve_progress_measure.
apply ForallCrossPairs_singleton. apply Hlits. intros r tl tr p. apply Hrec. apply IH'. apply m_lit in p. left. apply t_step. assumption.
Qed.
Lemma rsub_refl : forall t : T, rsub t t.
intros t. constructor. apply (uirec_alt (fun ll lr => ll = lr -> uisub (lsub (@RPremise) rsub) (TLit ll) (TLit lr)) (fun tl tr => tl = tr -> uisub (lsub (@RPremise) rsub) tl tr)); [| | reflexivity]; clear t.
intros ll lr IH Heq. subst. pose proof (LiteralReflexivity lr) as [r Hrule]. constructor. apply Lsub with r. intros tl tr Hp. pose proof (Hrule _ _ Hp) as Heq. constructor. apply IH with r; assumption.
intros tl tr Hrec Heq; subst. induction tr; try (repeat constructor; assumption).
apply ui_uni_l; [apply ui_uni_rl; apply IHtr1 | apply ui_uni_rr; apply IHtr2] ; apply uirec_uni_r in Hrec; destruct Hrec as [Hrecl Hrecr]; [apply uirec_uni_l in Hrecl; apply Hrecl | apply uirec_uni_l in Hrecr; apply Hrecr].
apply ui_int_r; [apply ui_int_ll; apply IHtr1 | apply ui_int_lr; apply IHtr2] ; apply uirec_int_r in Hrec; destruct Hrec as [Hrecl Hrecr]; [apply uirec_int_l in Hrecl; apply Hrecl | apply uirec_int_l in Hrecr; apply Hrecr].
unfold uirec in Hrec. simpl in Hrec. apply ForallCrossPairs_singleton_forward in Hrec. apply Hrec; reflexivity.
Qed.
Transitivity
First, it is relatively easy to see that the rules for union and intersection types alone (i.e. uisub) are transitive if the literal subtyping relation they use is transitive (see uisub_trans). That last part, however, depends on being able to build a reductive subtyping proof using Requirement 6 (LiteralTransitivity). Requirement 6 is specified using reductive subtyping proofs with assumptions and monotonicity (rsubam), which are not easily translated to regular subtyping proofs. The key trick in the proof here is defining the relation rsubt, which is essentially like rsub, except that it has an explicit transitivity rule. The nice thing about this relation is that it exactly expresses transitivity of rsub and has a nice translation from rsubam (rsubam_rsubt), which we can use to compose the assumptions given by Requirement 6 and therefore proof that rsubt implies rsub (rsubt_rsub) and therefore rsub is transitive (rsub_trans).Lemma uisub_trans {R R' R'' : Lit -> Lit -> Prop} (Htrans: forall ll lm lr : Lit, R ll lm -> R' lm lr -> R'' ll lr) : forall tl tm tr : T, uisub R tl tm -> uisub R' tm tr -> uisub R'' tl tr.
intros tl tm tr Hlm Hmr. generalize dependent tr. induction Hlm; intros trx Hmr.
remember (TLit lr) as tl. induction Hmr; try (inversion Heqtl; fail); try (constructor; auto; fail). constructor. inversion Heqtl; clear Heqtl; subst. apply Htrans with lr; assumption.
apply (uisub_top _ _ Hmr).
apply ui_int_ll; apply IHHlm; assumption.
apply ui_int_lr; apply IHHlm; assumption.
remember (TIsect il ir) as ti. induction Hmr; try (inversion Heqti; fail); try (constructor; auto; fail).
apply IHHlm1. inversion Heqti; clear Heqti; subst. assumption.
apply IHHlm2. inversion Heqti; clear Heqti; subst. assumption.
constructor.
apply uisub_uni_l in Hmr. apply IHHlm; apply Hmr.
apply uisub_uni_l in Hmr. apply IHHlm; apply Hmr.
apply ui_uni_l; [apply IHHlm1 | apply IHHlm2]; assumption.
Qed.
Inductive rsubt : T -> T -> Prop :=
| rt_transitivity (tl tm tr : T) : rsubt tl tm -> rsubt tm tr -> rsubt tl tr
| rt_lit (ll lr : Lit) (r : RRule ll lr) : (forall pl pr : T, RPremise r pl pr -> rsubt pl pr) -> rsubt (TLit ll) (TLit lr)
| rt_top (tl : T) : rsubt tl TTop
| rt_int_ll (il ir tr : T) : rsubt il tr -> rsubt (TIsect il ir) tr
| rt_int_lr (il ir tr : T) : rsubt ir tr -> rsubt (TIsect il ir) tr
| rt_int_r (tl il ir : T) : rsubt tl il -> rsubt tl ir -> rsubt tl (TIsect il ir)
| rt_bot (tr : T) : rsubt TBot tr
| rt_uni_rl (tl ul ur : T) : rsubt tl ul -> rsubt tl (TUni ul ur)
| rt_uni_rr (tl ul ur : T) : rsubt tl ur -> rsubt tl (TUni ul ur)
| rt_uni_l (ul ur tr : T) : rsubt ul tr -> rsubt ur tr -> rsubt (TUni ul ur) tr.
Arguments rsubt : clear implicits.
Lemma rsub_rsubt : forall tl tr : T, rsub tl tr -> rsubt tl tr.
apply (uirec_alt (fun ll lr => lsub (@RPremise) rsub ll lr -> lsub (@RPremise) rsubt ll lr) (fun tl tr => rsub tl tr -> rsubt tl tr)).
intros ll lr IH [r Hr]. apply Lsub with r. intros tl tr Hp. apply IH with r; [| apply Hr]; assumption.
intros tl tr ind tltr. assert (uisub (lsub (@RPremise) rsubt) tl tr).
destruct tltr. revert ind H. apply uirec_uisub_uisub. trivial.
clear tltr ind. rename H into tltr. induction tltr; try (constructor; auto; fail). destruct H as [ r p ]. apply rt_lit with r. assumption.
Qed.
Lemma rsubam_rsubt (A : T -> T -> Prop) : (forall tl tr : T, A tl tr -> rsubt tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubt tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
apply Himpl; assumption.
apply rt_transitivity with tl'.
apply rsub_rsubt in H. assumption.
apply rt_transitivity with tr'.
assumption.
apply rsub_rsubt in H0. assumption.
apply rt_lit with r. assumption.
Qed.
Lemma rsubt_rsub : forall tl tr : T, rsubt tl tr -> rsub tl tr.
intros tl tr Hsub. constructor. revert Hsub. apply (uirec_alt (fun (ll lr : Lit) => lsub (@RPremise) (rsubt) ll lr -> lsub (@RPremise) (uisub (lsub (@RPremise) rsub)) ll lr) (fun tl tr => rsubt tl tr -> uisub (lsub (@RPremise) (rsub)) tl tr)); clear.
intros ll lr IH Hsub. destruct Hsub as [r Hsub]. apply Lsub with r. intros ptl ptr Hp. apply (IH r ptl ptr Hp). apply Hsub. apply Hp.
intros tl tr Huir Hsub. eapply uirec_uisub_uisub with (R' := lsub (@RPremise) (rsubt)); try apply Huir; clear Huir.
clear. intros ll lr Hrec [r Hprem]. simpl in Hrec. pose proof (Lsub (@RPremise) (rsubt) ll lr r Hprem) as Hasub. apply Hrec in Hasub. inversion Hasub. apply Lsub with r0. intros tl tr Hprem'. apply H in Hprem'. constructor. assumption.
induction Hsub; try (constructor; assumption).
revert IHHsub1 IHHsub2. apply uisub_trans. intros ll lm lr [ rlm plm ] [ rmr pmr ]. pose proof (LiteralTransitivity rlm rmr) as [rt Hrt]. apply Lsub with rt. intros tl' tr' Hp. pose proof (Hrt _ _ Hp) as [tm' [[Hl Hr] | [Hl Hr]]]; clear Hrt; apply rsubam_rsubt in Hl; apply rsubam_rsubt in Hr; try assumption; apply rt_transitivity with tm'; assumption.
constructor. apply Lsub with r. assumption.
Qed.
Lemma rsub_trans : forall tl tm tr : T, rsub tl tm -> rsub tm tr -> rsub tl tr.
intros tl tm tr Hlm Hmr. apply rsubt_rsub. apply rt_transitivity with tm; apply rsub_rsubt; assumption.
Qed.
Two corollaries of rsub's transitivity are that proofs with assumptions and monotonicity can be converted into regular subtyping proofs if the assumptions can be proven (rsubam_rsub), and that literal subtyping proofs can be composed when the relation used for the premises is rsub (lsub_rsub_trans)
Lemma rsubam_rsub {A : T -> T -> Prop}: (forall tl tr: T, A tl tr -> rsub tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsub tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (repeat constructor; assumption); try ((apply rsubf_uisub in IHHsub || (apply rsubf_uisub in IHHsub1; apply rsubf_uisub in IHHsub2)); repeat constructor; assumption).
apply Himpl. assumption.
apply rsub_trans with tl'; [assumption |]. apply rsub_trans with tr'; assumption.
repeat constructor. apply Lsub with r; assumption.
Qed.
Lemma lsub_rsub_trans : forall ll lm lr : Lit, lsub (@RPremise) rsub ll lm -> lsub (@RPremise) rsub lm lr -> lsub (@RPremise) rsub ll lr.
intros ll lm lr Hlm Hmr. destruct Hlm as [rlm Hlm]. destruct Hmr as [rmr Hmr]. pose proof (LiteralTransitivity rlm rmr) as [rt Ht]. apply Lsub with rt. intros tl tr Hp. pose proof (Ht _ _ Hp) as [tm [[Hl Hr] | [Hl Hr]]]; clear Ht; (apply rsubam_mono with (A' := rsub) in Hl; [|assumption]); (apply rsubam_mono with (A' := rsub) in Hr; [|assumption]); apply rsubam_rsub in Hl; apply rsubam_rsub in Hr; (trivial || apply rsub_trans with tm; assumption).
Qed.
intros Himpl tl tr Hsub. induction Hsub; try (repeat constructor; assumption); try ((apply rsubf_uisub in IHHsub || (apply rsubf_uisub in IHHsub1; apply rsubf_uisub in IHHsub2)); repeat constructor; assumption).
apply Himpl. assumption.
apply rsub_trans with tl'; [assumption |]. apply rsub_trans with tr'; assumption.
repeat constructor. apply Lsub with r; assumption.
Qed.
Lemma lsub_rsub_trans : forall ll lm lr : Lit, lsub (@RPremise) rsub ll lm -> lsub (@RPremise) rsub lm lr -> lsub (@RPremise) rsub ll lr.
intros ll lm lr Hlm Hmr. destruct Hlm as [rlm Hlm]. destruct Hmr as [rmr Hmr]. pose proof (LiteralTransitivity rlm rmr) as [rt Ht]. apply Lsub with rt. intros tl tr Hp. pose proof (Ht _ _ Hp) as [tm [[Hl Hr] | [Hl Hr]]]; clear Ht; (apply rsubam_mono with (A' := rsub) in Hl; [|assumption]); (apply rsubam_mono with (A' := rsub) in Hr; [|assumption]); apply rsubam_rsub in Hl; apply rsubam_rsub in Hr; (trivial || apply rsub_trans with tm; assumption).
Qed.
Equivalence
Since rsub has been shown reflexive (rsub_refl) and transitive (rsub_trans), we can now show that declarative and reductive subtyping are equivalent. The reflexivity and transitivity rules are already taken care of, the rules for unions, intersections, top and bottom are trivial, and the rules for literals can be proven equivalent using Requirements 4 (RRuleToDProof) and 5 (DRuleToRProof).Lemma rsub_dsub : forall tl tr : T, rsub tl tr <-> dsub tl tr.
intros tl tr. split; intros H; [destruct H|].
revert H. apply (uirec_alt (fun ll lr => lsub (@RPremise) (rsub) ll lr -> dsub (TLit ll) (TLit lr)) (fun tl tr => uisub (lsub (@RPremise) (rsub)) tl tr -> dsub tl tr)); clear tl tr.
intros ll lr IH Hsub. destruct Hsub as [r Hsub]. pose proof (RRuleToDProof r) as H. apply (@dsuba_dsubf (RPremise r)); [|assumption]. intros tl tr Hp. apply IH with r; [|apply rsubf_uisub; apply Hsub]; assumption.
intros tl tr IH Hsub. induction Hsub; try (constructor; assumption).
unfold uirec in IH. simpl in IH. rewrite -> ForallCrossPairs_singleton in IH. apply (IH H).
apply uirec_int_l in IH. apply dsuba_trans with il; [apply dsuba_int_ll|]; apply IHHsub; apply IH.
apply uirec_int_l in IH. apply dsuba_trans with ir; [apply dsuba_int_lr|]; apply IHHsub; apply IH.
apply uirec_int_r in IH. apply dsuba_int_r; [apply IHHsub1|apply IHHsub2]; apply IH.
apply uirec_uni_r in IH. apply dsuba_trans with ul; [|apply dsuba_uni_rl]; apply IHHsub; apply IH.
apply uirec_uni_r in IH. apply dsuba_trans with ur; [|apply dsuba_uni_rr]; apply IHHsub; apply IH.
apply uirec_uni_l in IH. apply dsuba_uni_l; [apply IHHsub1|apply IHHsub2]; apply IH.
induction H; try (repeat constructor; assumption).
apply rsub_refl.
apply rsub_trans with tm; assumption.
contradiction.
pose proof (DRuleToRProof r) as Hconv. apply rsubam_mono with (A' := rsub) in Hconv; [|assumption]. apply rsubam_rsub in Hconv; [|trivial]. assumption.
apply rsubf_uisub in IHdsuba1. apply rsubf_uisub in IHdsuba2. repeat constructor; assumption.
constructor. apply ui_uni_rl. apply rsubf_uisub. apply rsub_refl.
constructor. apply ui_uni_rr. apply rsubf_uisub. apply rsub_refl.
apply rsubf_uisub in IHdsuba1. apply rsubf_uisub in IHdsuba2. repeat constructor; assumption.
constructor. apply ui_int_ll. apply rsubf_uisub. apply rsub_refl.
constructor. apply ui_int_lr. apply rsubf_uisub. apply rsub_refl.
Qed.
Theorem : Decidability of Declarative Subtyping
Now we just stitch the previous lemmas together. Given two types, we use the decider for rsub to see whether they are subtypes under reductive subtyping, and then use the equivalence of reductive and declarative subtyping to produce the corresponding result for declarative subtyping.Theorem DecidabilityOfDeclarativeSubtyping : forall tl tr : T, {dsub tl tr} + {~ dsub tl tr}.
intros tl tr. destruct (rsub_dec tl tr) as [H | Hn]; [left | right; intros H; apply Hn] ; apply rsub_dsub ; assumption.
Qed.
End TraditionalDec.
This page has been generated by coqdoc