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. In particular, there are many relatively obvious equivalences and other relationships between previously defined functions and predicates on Ts and their sop-equivalents. Please see Section4_Infrastructure.v for those definitions and lemmas.
Require Import List.
Require Import Nat.
Require Import Util.
Require Import Wf.
Require Import Wellfounded.Inverse_Image.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Require Import Section4_Infrastructure.
Import Relation_Operators.
Import List.
Import ListNotations.
Require Import Nat.
Require Import Util.
Require Import Wf.
Require Import Wellfounded.Inverse_Image.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Require Import Section4_Infrastructure.
Import Relation_Operators.
Import List.
Import ListNotations.
Proof of Decidability of Extended Subtyping (Section4_Proofs.v)
The main Theorem of this section (Decidability of Extended Subtyping) is proven along the path set out in the paper, though due to the use of the SOP representation the formulation of some of the intermediate Lemmas has changed (all Lemmas in the paper are proven here, but they may not be part of the final proof in their form in the paper). The proof proceeds roughly as follows:- We define sop versions of most things given by an Intersector module
- We prove induction principles for sops that include integrating the LHS of premises of literal rules.
- We define integrated subtyping and prove Lemmas similar to those in the paper about it
- We prove equivalence of integrated subtyping and extended subtyping
- We prove decidability of integrated subtyping
- We prove that if an equivalent decidable relation exists, extended subtyping is decidable, and instantiate this lemma with integrated subtyping and the above proofs, proving the main Theorem.
SOP Intersectors
We define sopintersect as simply the user-defined intersector combined with ui2sop. Because any result of intersect is required to be in DNF, we can proof that the sopof relation holds between the results of sopintersect and intersect (sopintersect_sopof_intersect). Several intermediate lemmas build up to suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect, which lets us translate subtyping proofs involving the SOP Integrator to subtyping proofs involving the Integrator as presented in the paper, and vice versa. This is a quite central part of moving between the two representations in the rest of this section's proofs.Module Integrated (M_traditional : Traditional) (M_intersector : Intersector M_traditional).
Import M_traditional.
Import M_intersector.
Module M_sopinfrastructure := SOP_Infrastructure M_traditional.
Import M_sopinfrastructure.
Import M_sopinfrastructure.M_TraditionalDec.
Import M_sopinfrastructure.M_TraditionalDec.M_Infrastructure.
Definition sopintersect : list Lit -> list (list Lit) := fun ls => ui2sop (intersect ls).
Lemma sopintersect_sopof_intersect : forall ls : list Lit, sopof (sopintersect ls) (intersect ls).
intros ls. unfold sopintersect. apply ui2sop_sopof_ui. apply (Integrated_SumOfProducts _ _ (IntersectorIntegrated ls)).
Qed.
Lemma suisub_sopof_uisub (R : Lit -> Lit -> Prop) : forall (sl : sop) (tl t : T), sopof sl tl -> (suisub R sl t <-> uisub R tl t).
intros sl tl t Hsop. split; intros Hsub.
generalize dependent t. induction Hsop; intros tx Hsub; try (constructor; assumption).
generalize dependent tx. induction H; intros tx Hsub; try (constructor; assumption).
apply suisub_uisub in Hsub. simpl in Hsub. apply uisub_uni_l in Hsub. destruct Hsub as [Hsub _]. remember (TIsect (TLit l) TTop) as tisect. induction Hsub; inversion Heqtisect; subst; repeat remove_eq_implications; try (try constructor; try assumption; fail).
apply (uisub_top _ _ Hsub).
apply suisub_uisub in Hsub. simpl in Hsub. apply uisub_uni_l in Hsub. apply Hsub.
unfold suisub in Hsub. apply Forall_singleton in Hsub. induction Hsub; try (constructor; assumption).
apply Exists_app_or in H1. destruct H1 as [Hex | Hex]; [apply ui_int_ll; apply IHpolof1 | apply ui_int_lr; apply IHpolof2]; apply ruisub_suisub; apply rui_lit; assumption.
apply Forall_app in Hsub. apply ui_uni_l; [apply IHHsop1 | apply IHHsop2]; apply Hsub.
generalize dependent t. induction Hsop; intros tx Hsub; try (constructor; assumption).
generalize dependent tx. induction H; intros tx Hsub; try (constructor; assumption).
apply uisub_suisub'. apply ui_uni_l; [apply ui_int_ll | apply ui_bot]. assumption.
apply uisub_suisub'. apply ui_uni_l; [assumption | apply ui_bot].
remember (TIsect tl tr) as tisect. induction Hsub; inversion Heqtisect; subst; repeat remove_eq_implications; apply ruisub_suisub; try (repeat constructor; assumption).
apply Forall_singleton in IHpolof1. eapply (ruisub_mono _ _ _ _ IHpolof1). Unshelve. 6: simpl; intros l Hex; apply Exists_app_or; left; assumption.
apply Forall_singleton in IHpolof2. eapply (ruisub_mono _ _ _ _ IHpolof2). Unshelve. 5: simpl; intros l Hex; apply Exists_app_or; right; assumption.
apply Forall_singleton in IHHsub0. apply Forall_singleton in IHHsub1. apply rui_int; assumption.
apply Forall_singleton in IHHsub0. apply rui_uni_l; assumption.
apply Forall_singleton in IHHsub0. apply rui_uni_r; assumption.
apply uisub_uni_l in Hsub. apply Forall_app; split; [apply IHHsop1 | apply IHHsop2]; apply Hsub.
Qed.
Lemma SopIntegrate_sopof_Integrate (f : list Lit -> sop) (g : list Lit -> T) (Hfg : forall ls : list Lit, sopof (f ls) (g ls)) : forall t : T, sopof (SopIntegrate f t) (Integrate g t).
intros t; generalize dependent g; generalize dependent f; induction t; intros f g Hfg; simpl; try apply Hfg; try (constructor; assumption).
apply sopof_uni; [apply IHt1 | apply IHt2]; assumption.
apply IHt1. intros ls. apply IHt2. intros ls'. apply Hfg.
Qed.
Lemma suisub_SopIntegrate_uisub_Integrate (R : Lit -> Lit -> Prop) (f : list Lit -> sop) (g : list Lit -> T) (Hfg : forall ls : list Lit, sopof (f ls) (g ls)) : forall (tl t : T), suisub R (SopIntegrate f tl) t <-> uisub R (Integrate g tl) t.
intros tl t. apply suisub_sopof_uisub. apply SopIntegrate_sopof_Integrate. apply Hfg.
Qed.
Lemma suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect (R : Lit -> Lit -> Prop) : forall tl t : T, suisub R (SopIntegrate sopintersect tl) t <-> uisub R (Integrate intersect tl) t.
apply suisub_SopIntegrate_uisub_Integrate. apply sopintersect_sopof_intersect.
Qed.
Lemma SopIntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (sop2ui (SopIntegrate sopintersect tl)) tr.
intros tl tr Hext. pose proof (IntersectorCompleteness tl tr Hext) as H. apply dsuba_trans with (Integrate intersect tl); [|assumption]. apply rsub_dsub. constructor. apply suisub_uisub. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply rsubf_uisub. apply rsub_refl.
Qed.
Lemma rssub_refl : forall s : sop, ssub (lsub (@RPremise) rsub) s s.
intros s. rewrite <- (ui2sop_sop2ui s). apply suisub_ssub. apply uisub_suisub. apply rsubf_uisub. apply rsub_refl.
Qed.
Lemma SopIntersectorSoundness : forall ls : list Lit, esub (Intersect ls) (sop2ui (sopintersect ls)).
intros t. pose proof (IntersectorSoundness t) as H. apply dsubda_trans with (intersect t); [assumption|]. apply dsuba_dsubda. apply @dsuba_mono with (A := fun _ _ => False); [intros; contradiction|]. apply rsub_dsub. clear H. pose proof (sopintersect_sopof_intersect t). constructor. apply (suisub_sopof_uisub _ _ _ _ (sopintersect_sopof_intersect t)). apply ssub_suisub. apply rssub_refl.
Qed.
Requirement 9: Measure Preservation (No SOP Version)
The requirements on the behavior of the measure function m are very weak - we expect that in most cases, the measures of unions and intersections will be joins of the measures of their components, but that is not required. Hence, the connections of measures of a type in DNF with their original are hard to establish, even more so if additionally, and intersector mangles types. We can avoid all of this by simply using the original measure preservation requirement whenever we need to prove that some recursion terminates.Requirement 10: Literal Derelicton (SOP Version)
Lemma SopLiteralDereliction : forall ls : list Lit, rsub (sop2ui (sopintersect ls)) (Intersect ls).
intros ls. pose proof (LiteralDereliction ls) as H. apply rsub_trans with (intersect ls); [clear H|apply H]. constructor. apply suisub_uisub. apply (suisub_sopof_uisub _ _ _ _ (sopintersect_sopof_intersect ls)). apply rsubf_uisub. apply rsub_refl.
Qed.
Lemma SopIntersectorIntegrated : forall ls : list Lit, SopIntegrated intersected (sopintersect ls).
intros ls. pose proof (IntersectorIntegrated ls) as H. unfold sopintersect. unfold ui2sop. revert H. generalize intersected. induction (intersect ls); intros P Hint.
simpl. constructor. apply Hint.
constructor.
constructor.
simpl. apply Forall_app; split; [apply IHu1 | apply IHu2]; apply Hint.
simpl in *. apply Integrated_int_Integrated in Hint. apply IHu1 in Hint. rewrite -> SopIntegrate_flat_map. apply SopIntegrated_flat_map. revert Hint. apply SopIntegrated_mono. intros ls' Hint. apply Integrated_int_Integrated in Hint. apply IHu2 in Hint. rewrite -> SopIntegrate_flat_map. apply SopIntegrated_flat_map. revert Hint. apply SopIntegrated_mono. intros l'' Hp. constructor; [assumption | constructor].
simpl. repeat constructor. apply Hint.
Qed.
Lemma SopLiteralPromotion : forall ls : list Lit, intersected ls -> forall rs : list (sig2T RRule), incl (map proj2T1 rs) ls -> Exists (fun ls' => Forall (fun lr => Exists (fun ll => lsub (@RPremise) (rsubam (@RPremise) (fun tl tr : T => Exists (fun r => RPremise (proj2V r) tl tr) rs)) ll lr) ls) ls') (sopintersect (map proj2T2 rs)).
intros ls Hint rs Hincl. pose proof (LiteralPromotion ls (map proj2T2 rs) rs) as Hpromo. promotehyp Hpromo; [apply Forall_forall; intros l HIn; apply in_map_iff in HIn; apply Exists_exists; destruct HIn as [x [Hx HIn]]; exists x; split; assumption|]. promotehyp Hpromo. promotehyp Hpromo. unfold sopintersect. destruct Hpromo as [rs' Hpromo]. induction (intersect (map proj2T2 rs)).
repeat constructor.
simpl in Hpromo. contradiction Hpromo.
destruct Hpromo as [Hpromo | Hpromo]; [apply IHu1 in Hpromo | apply IHu2 in Hpromo]; clear IHu1 IHu2; unfold ui2sop; simpl; apply Exists_app_or; [left | right]; assumption.
clear IHu1 IHu2. apply Exists_Intersection_int_exists in Hpromo. destruct Hpromo as [Hpos Hfa]. rewrite <- (Tlits_ui2sop Hpos). constructor. destruct Hfa as [Heqrs' [Hinclrs' Hfa]]. rewrite -> Heqrs'. apply Forall_map. mono. intros r' HInr' Hprem. apply Exists_exists. exists (proj2T1 r'). split; [apply Hinclrs'; apply in_map_iff; exists r'; split; [reflexivity|assumption]|]. apply Lsub with (proj2V r'). assumption.
simpl in *. unfold ui2sop. simpl. repeat constructor. apply Exists_exists. destruct Hpromo as [Heqrs' [Hinclrs' Hfa]]. destruct rs' as [|r' rs']; [inversion Heqrs'|]. destruct rs' as [|r'' rs']; [|inversion Heqrs']. exists (proj2T1 r'). split; [apply Hinclrs'; apply in_eq|]. apply Forall_singleton in Hfa. simpl in Heqrs'. inversion Heqrs'; subst. apply Lsub with (proj2V r'). assumption.
Qed.
Lemma suirec_suisub_suisub (R R' R'' : Lit -> Lit -> Prop) (sl : sop) (tr : T) : (forall ll lr : Lit, R ll lr -> R' ll lr -> R'' ll lr) -> suirec R sl tr -> suisub R' sl tr -> suisub R'' sl tr.
intros imp srec sltr. induction sltr as [ | il sl iltr sltr ].
constructor.
inversion srec; clear srec; subst. rename H1 into irec. rename H2 into srec. constructor; [ clear sl srec sltr IHsltr | apply IHsltr; assumption ]. induction iltr; try (constructor; assumption).
constructor. mono. intros l' HIn HR'; apply imp; [|assumption]. unfold ruirec in irec. apply Forall_singleton in irec. rewrite -> Forall_forall in irec. apply irec; assumption.
apply ruirec_isect in irec; destruct irec as [irecl irecr]; repeat remove_eq_implications. constructor; assumption.
apply ruirec_uni in irec; destruct irec as [irecl irecr]; repeat remove_eq_implications. constructor; assumption.
apply ruirec_uni in irec; destruct irec as [irecl irecr]; repeat remove_eq_implications. constructor; assumption.
Qed.
Induction Principles
Next, we prove the induction principles irec and irec_alt. irec is really only used to prove irec_alt, which is simliar to uirec_alt, except that it includes the Integrator and is (partially) about sops. As sops make it easy to recurse down to pairings of literals, the measure litlt we use to prove these induction principles is a measure between pairs of literals; and essentially defined as the restriction of (the transitive closure of) mlt to just the literal cases. Since lrec and irec are defined largely using a mixed sop/T relation, we define the intermediate lemma mlt_recurse, which, together with a number of other straightforward lemmas about the relationship between InType and sops also lets us drill down to the literal cases in Ts.
Definition litlt (lpl lpr : Lit * Lit) : Prop := mltt (m (TLit (fst lpl)) (TLit (snd lpl))) (m (TLit (fst lpr)) (TLit (snd lpr))).
Lemma litlt_wf : well_founded litlt.
unfold litlt. apply wf_inverse_image. apply mltt_wf.
Qed.
Ltac tac_mlt_recurse := repeat match goal with
| [|- clos_refl_trans _ _ ?m ?m] => apply rt_refl
| [H : clos_refl_trans _ _ ?ml ?mm |- clos_refl_trans _ _ ?ml ?mr] => apply rt_trans with mm; [assumption|]; clear H
| [H : clos_refl_trans _ _ ?mm ?mr |- clos_refl_trans _ _ ?ml ?mr] => apply rt_trans with mm; [|assumption]; clear H
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m (_ ?tl ?tlr) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m (_ ?tll ?tl) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m ?tl (_ ?tr ?trr))] => apply m_ui_r; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m ?tl (_ ?trl ?tr))] => apply m_ui_r; constructor
end.
Lemma mlt_recurse : forall (tl tr : T) (tl' tr' : T), InType tl' tl -> InType tr' tr -> clos_refl_trans M mlt (m tl' tr') (m tl tr).
intros tl tr tl' tr' Hitl Hitr. generalize dependent tr. generalize dependent tr'. induction Hitl; intros tr' rtr Hitr; induction Hitr; tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
Qed.
Lemma irec (R : Lit -> Lit -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> suirec R (SopIntegrate sopintersect tl) tr) -> R ll lr) -> forall ll lr : Lit, R ll lr.
intros IH ll lr. rewrite -> uncurry_eq. apply (well_founded_ind litlt_wf). clear ll lr. intros [ll lr] IHlt. unfold uncurry. simpl. apply IH. intros r tl tr Hprem.
unfold suirec. apply Forall_forall. intros lsl HInlsl.
apply Forall_forall. intros llr HInllr. apply Forall_forall. intros lll HInlll. rewrite -> uncurry_eq. apply IHlt. unfold litlt. simpl. apply Operators_Properties.clos_rt_t with (m tl tr).
unfold sopintersect in HInlsl. rewrite -> SopIntegrate_flat_map in HInlsl. apply in_flat_map in HInlsl. destruct HInlsl as [lsli [HInlsli HInlsl]].
apply rt_trans with (m (Integrate intersect tl) tr).
apply mlt_recurse.
apply InType_lit_In. exists lsl. fold (ui2sop (Integrate intersect tl)). split; [|assumption]. unfold ui2sop. rewrite -> (SopIntegrate_Integrate _ sopintersect); [|intros; reflexivity]. rewrite -> SopIntegrate_flat_map. apply in_flat_map. exists lsli. split; assumption.
apply InType_lit_In_lits; assumption.
apply (MeasurePreservation tl tr).
apply t_step. apply (m_lit r _ _ Hprem).
Qed.
Lemma irec_alt (RL : Lit -> Lit -> Prop) (RT : sop -> T -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> RT (SopIntegrate sopintersect tl) tr) -> RL ll lr) -> (forall (sl : sop) (tr : T), suirec RL sl tr -> RT sl tr) -> forall (sl : sop) (tr : T), RT sl tr.
intros Hlit Hrec sl tr. apply Hrec. apply Forall_forall. intros lsl HInlsl. apply Forall_forall. intros lr HInlr. apply Forall_forall. intros ll HInll. apply irec. clear lsl ll lr HInlsl HInlr HInll sl tr.
intros ll lr IH. apply Hlit. intros r tl tr Hp. apply Hrec. apply IH with r; assumption.
Qed.
Lemma litlt_wf : well_founded litlt.
unfold litlt. apply wf_inverse_image. apply mltt_wf.
Qed.
Ltac tac_mlt_recurse := repeat match goal with
| [|- clos_refl_trans _ _ ?m ?m] => apply rt_refl
| [H : clos_refl_trans _ _ ?ml ?mm |- clos_refl_trans _ _ ?ml ?mr] => apply rt_trans with mm; [assumption|]; clear H
| [H : clos_refl_trans _ _ ?mm ?mr |- clos_refl_trans _ _ ?ml ?mr] => apply rt_trans with mm; [|assumption]; clear H
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m (_ ?tl ?tlr) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m (_ ?tll ?tl) ?tr)] => apply m_ui_l; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m ?tl (_ ?tr ?trr))] => apply m_ui_r; constructor
| [|- clos_refl_trans _ _ (m ?tl ?tr) (m ?tl (_ ?trl ?tr))] => apply m_ui_r; constructor
end.
Lemma mlt_recurse : forall (tl tr : T) (tl' tr' : T), InType tl' tl -> InType tr' tr -> clos_refl_trans M mlt (m tl' tr') (m tl tr).
intros tl tr tl' tr' Hitl Hitr. generalize dependent tr. generalize dependent tr'. induction Hitl; intros tr' rtr Hitr; induction Hitr; tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
pose proof (IHHitl _ _ (it_eq t0)). tac_mlt_recurse.
Qed.
Lemma irec (R : Lit -> Lit -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> suirec R (SopIntegrate sopintersect tl) tr) -> R ll lr) -> forall ll lr : Lit, R ll lr.
intros IH ll lr. rewrite -> uncurry_eq. apply (well_founded_ind litlt_wf). clear ll lr. intros [ll lr] IHlt. unfold uncurry. simpl. apply IH. intros r tl tr Hprem.
unfold suirec. apply Forall_forall. intros lsl HInlsl.
apply Forall_forall. intros llr HInllr. apply Forall_forall. intros lll HInlll. rewrite -> uncurry_eq. apply IHlt. unfold litlt. simpl. apply Operators_Properties.clos_rt_t with (m tl tr).
unfold sopintersect in HInlsl. rewrite -> SopIntegrate_flat_map in HInlsl. apply in_flat_map in HInlsl. destruct HInlsl as [lsli [HInlsli HInlsl]].
apply rt_trans with (m (Integrate intersect tl) tr).
apply mlt_recurse.
apply InType_lit_In. exists lsl. fold (ui2sop (Integrate intersect tl)). split; [|assumption]. unfold ui2sop. rewrite -> (SopIntegrate_Integrate _ sopintersect); [|intros; reflexivity]. rewrite -> SopIntegrate_flat_map. apply in_flat_map. exists lsli. split; assumption.
apply InType_lit_In_lits; assumption.
apply (MeasurePreservation tl tr).
apply t_step. apply (m_lit r _ _ Hprem).
Qed.
Lemma irec_alt (RL : Lit -> Lit -> Prop) (RT : sop -> T -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> RT (SopIntegrate sopintersect tl) tr) -> RL ll lr) -> (forall (sl : sop) (tr : T), suirec RL sl tr -> RT sl tr) -> forall (sl : sop) (tr : T), RT sl tr.
intros Hlit Hrec sl tr. apply Hrec. apply Forall_forall. intros lsl HInlsl. apply Forall_forall. intros lr HInlr. apply Forall_forall. intros ll HInll. apply irec. clear lsl ll lr HInlsl HInlr HInll sl tr.
intros ll lr IH. apply Hlit. intros r tl tr Hp. apply Hrec. apply IH with r; assumption.
Qed.
Integrated Subtyping
The recursive part of Integrated Subtyping in the paper is defined to be like reductive subtyping, except that the literal rule applies the Integrator to the LHS of every premise. We model this by giving rsubf a different Premise argument, IPremise, which applies the Integrator to the LHS of every RPremise. isub' is therefore the recursive part of Integrated Subtyping (≤⊓), and isub the outer part (≤⊓). rssub and issub are the sop counterparts of rsub and isub', respectively.Inductive IPremise {ll lr : Lit} (r : RRule ll lr) : T -> T -> Prop :=
ipremise (tl tr : T) : RPremise r tl tr -> IPremise r (Integrate intersect tl) tr.
Definition isub' : T -> T -> Prop :=
rsubf (@IPremise).
Definition isub (tl : T) : T -> Prop :=
isub' (Integrate intersect tl).
Definition rssub : sop -> sop -> Prop :=
ssub (lsub (@RPremise) (rsub)).
Definition issub : sop -> sop -> Prop :=
ssub (lsub (@IPremise) isub').
Lemma 1: Integrated Soundness
Integrated Subtyping implies Extended Subtyping (proven using helper Lemma IntegratorSoundness, which in turn extends the IntersectorSoundness Requirement to Integrators)Lemma IntegratorSoundness : forall t : T, esub t (Integrate intersect t).
intros t. apply dsubda_trans with (Integrate Intersect t) ; [apply dsubda_dnf|]. apply dsubda_trans with (Integrate intersect (Integrate Intersect t)).
pose proof (Integrated_SumOfProducts _ _ (Intersect_Integrated t)) as Hsop. remember (Integrate Intersect t) as ti. clear Heqti. induction Hsop.
constructor; fail.
apply dsubda_uni_l; simpl; [apply dsubda_trans with (Integrate intersect tl) | apply dsubda_trans with (Integrate intersect tr)]; assumption || (constructor; fail).
rewrite -> (Integrate_ProductOfLiterals _ _ H). apply dsubda_trans with (Intersect (Tlits t0 H)); [|apply IntersectorSoundness]. rewrite -> Tlits_lits. induction H.
apply dsubda_refl.
simpl. apply dsubda_int_r; constructor; fail.
simpl. induction (lits tl).
apply dsubda_trans with tr; [constructor; fail|assumption].
simpl in *. apply dsubda_isect_r in IHProductOfLiterals1. destruct IHProductOfLiterals1 as [IH1a IH1l]. apply dsubda_int_r; [apply dsubda_trans with tl; [constructor|]| apply IHl]; assumption.
rewrite <- Integrate_Integrate_dnf. apply dsubda_refl.
Qed.
Lemma IntegratedSoundness : forall tl tr : T, isub tl tr -> esub tl tr.
intros tl tr Hsub.
unfold isub in Hsub. unfold isub' in Hsub. apply dsubda_trans with (Integrate intersect tl).
apply IntegratorSoundness.
apply dsubda_trans with (sop2ui (SopIntegrate sopintersect tl)).
clear Hsub. apply dsubda_sopof. apply SopIntegrate_sopof_Integrate. apply sopintersect_sopof_intersect.
apply rsubf_uisub in Hsub. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in Hsub. apply suisub_uisub in Hsub. apply Rsubf in Hsub. revert Hsub. apply (irec_alt (fun ll lr => lsub (@IPremise) (rsubf (@IPremise)) ll lr -> esub (TLit ll) (TLit lr)) (fun sl tr => rsubf (@IPremise) (sop2ui sl) tr -> esub (sop2ui sl) tr)); clear tl tr; simpl in *.
intros ll lr IH [r Hsub]. pose proof (RRuleToDProof r) as Hp. induction Hp; try (constructor; assumption).
apply dsubda_trans with tm; assumption.
apply dsubda_trans with (sop2ui (SopIntegrate sopintersect tl)).
apply dsubda_trans with (Integrate intersect tl); [apply IntegratorSoundness|]. apply dsubda_sopof. apply SopIntegrate_sopof_Integrate. apply sopintersect_sopof_intersect.
apply IH with r; [assumption|]. constructor. apply suisub_uisub. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply rsubf_uisub. apply Hsub. constructor. assumption.
apply dsubda_lit with r0; assumption.
intros tl tr IH Hsub. apply rsubf_uisub in Hsub. apply uisub_suisub in Hsub. rewrite -> ui2sop_sop2ui in Hsub. induction Hsub.
constructor; fail.
simpl. apply dsubda_uni_l; [|apply IHHsub; inversion IH; assumption]; clear IHHsub Hsub. inversion IH; subst. clear IH H3. rename H2 into IH. induction H; try (constructor; assumption).
inversion IH; subst. apply Exists_exists in H. destruct H as [l' [HIn Hsub]]. rewrite -> Forall_forall in H2; pose proof (H2 _ HIn) as Himpl. apply in_split in HIn. destruct HIn as [l1 [l2 Heq]]. subst. induction l1.
simpl. apply dsubda_trans with (TLit l'); [apply dsubda_int_ll|]. apply Himpl. apply Hsub.
simpl. apply dsubda_trans with (Intersect (l1 ++ l' :: l2)); [apply dsubda_int_lr|]. apply IHl1; [constructor | intros ; apply H2; try apply in_cons; assumption|]. clear IHl1 Himpl H2 Hsub. inversion IH; subst. constructor; [|constructor]. simpl in H1. inversion H1; assumption.
apply ruirec_isect in IH; destruct IH as [IHl IHr]; apply dsubda_int_r; [apply IHruisub1 | apply IHruisub2]; assumption.
apply ruirec_uni in IH; destruct IH as [IHl IHr];apply dsubda_trans with tl; [|apply dsubda_uni_rl]; apply IHruisub; assumption.
apply ruirec_uni in IH; destruct IH as [IHl IHr];apply dsubda_trans with tr; [|apply dsubda_uni_rr]; apply IHruisub; assumption.
Qed.
Lemma 2: Integrated Decidability
The Integrated Subtyping Relation relation ≤⊓ is decidable.Lemma IntegratedDecidability : forall tl tr : T, {isub tl tr} + {~ isub tl tr}.
pose proof (@rsubf_dec (@IPremise)) as Hdec. assert (H : forall tl tr : T, {rsubf (@IPremise) tl tr} + {~ rsubf (@IPremise) tl tr}).
apply Hdec.
intros ll lr r. pose proof (SyntaxDirectedness_Premises r) as [rpremises Hpr]. exists (map (fun tp => (Integrate intersect (fst tp), snd tp)) rpremises). intros tl tr. split; intros H.
destruct H as [tl tr H]. apply Hpr in H. apply in_map_iff. exists (tl, tr). split; [reflexivity | assumption].
apply in_map_iff in H. destruct H as [[tl' tr'] [Heq HIn]]; simpl in *. inversion Heq; subst. constructor. apply Hpr. assumption.
intros ll lr r tl tr Hp. destruct Hp as [tl tr Hp]. apply m_lit in Hp. left. apply Operators_Properties.clos_rt_t with (m tl tr); [apply MeasurePreservation|apply t_step; assumption].
clear Hdec. intros tl tr. pose proof (H (Integrate intersect tl) tr) as [Hsub | Hnsub]; [left | right]; unfold isub; unfold isub'; assumption.
Qed.
Lemma 3: Dereliction
The result of integrating a type is a subtype of the original type. After a few straightforward intermediate Lemmas, we first proof dereliction on sops (sopdereliction, and then based on that, the Dereliction Lemma as in the paper.Lemma suisub_uisub_trans (Rl Rm Rr : Lit -> Lit -> Prop) {sl : sop} (tm : T) {tr : T} : (forall ll lm lr : Lit, Rl ll lm -> Rr lm lr -> Rm ll lr) -> suisub Rl sl tm -> uisub Rr tm tr -> suisub Rm sl tr.
intros Hltrans Hlm Hmr. unfold suisub in *. unfold ssub in Hlm. mono. intros lsl HInlsl Hsub. induction Hmr; try (constructor; assumption).
inversion Hsub; subst. apply Exists_exists in H1. destruct H1 as [l [HInl HR]]. constructor. apply Exists_exists. exists l. split; [| apply Hltrans with ll]; assumption.
apply IHHmr. inversion Hsub. assumption.
apply IHHmr. inversion Hsub. assumption.
constructor; [apply IHHmr1 | apply IHHmr2]; assumption.
inversion Hsub.
apply rui_uni_l; apply IHHmr; assumption.
apply rui_uni_r; apply IHHmr; assumption.
inversion Hsub; [apply IHHmr1 | apply IHHmr2]; assumption.
Qed.
Lemma dereliction_lits : forall (ls ls' : list Lit), rssub [ls] [ls'] -> suisub (lsub (@RPremise) rsub) (sopintersect ls) (sop2ui [ls']).
intros ls ls' Hsub. unfold rssub in Hsub. apply ssub_suisub in Hsub. apply suisub_uisub in Hsub. eapply (@suisub_uisub_trans (lsub (@RPremise) rsub) _ _ (sopintersect ls) (sop2ui [ls]) (sop2ui [ls']) lsub_rsub_trans _ Hsub). Unshelve.
clear Hsub. rewrite <- (ui2sop_sop2ui (sopintersect ls)). apply uisub_suisub. unfold sop2ui. simpl. apply ui_uni_rl. apply rsubf_uisub. apply SopLiteralDereliction.
Qed.
Lemma sopdereliction (tl tr : T) : rsub tl tr -> rsub (sop2ui (SopIntegrate sopintersect tl)) tr.
intros Hsub. apply rsub_trans with tl; [|assumption]. clear Hsub. constructor. apply suisub_uisub. apply (@suisub_uisub_trans (lsub (@RPremise) rsub) _ _ (SopIntegrate sopintersect tl) (sop2ui (ui2sop tl)) tl lsub_rsub_trans).
rewrite -> SopIntegrate_flat_map. fold (ui2sop tl). induction (ui2sop tl) as [| lsl sl].
constructor.
simpl. apply Forall_app; split.
clear IHsl. pose proof (dereliction_lits lsl lsl (rssub_refl [lsl])). unfold suisub in H. mono. intros ls HInls Hsub. simpl in Hsub. inversion Hsub; subst.
apply rui_uni_l. assumption.
inversion H0.
unfold suisub in IHsl. mono. intros ls HInls Hex. apply rui_uni_r. assumption.
apply uisub_dnf.
Qed.
Lemma Dereliction (tl tr : T) : rsub tl tr -> rsub (Integrate intersect tl) tr.
intros Hsub. pose proof (sopdereliction tl tr Hsub) as Hsopder. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply rsubf_uisub in Hsopder. apply uisub_suisub'. assumption.
Qed.
Lemma 4: Integrator Integrated
Proofs of both the sop and regular version of Lemma 4. None of these proofs depend on each other, but we mostly use the sop version in the rest of the proof.Lemma SopIntegratorIntegrated : forall (t : T), SopIntegrated intersected (SopIntegrate sopintersect t).
induction t; try apply SopIntersectorIntegrated.
simpl. constructor.
simpl. apply Forall_app; split; assumption.
simpl. rewrite -> SopIntegrate_flat_map. apply Forall_forall. intros ls HIn. apply in_flat_map in HIn. destruct HIn as [ls' [HInls' HIn]]. rewrite -> SopIntegrate_flat_map in HIn. apply in_flat_map in HIn. destruct HIn as [ls'' [HInls'' HIn]]. pose proof (SopIntersectorIntegrated (ls' ++ ls'')). unfold SopIntegrated in H. rewrite -> Forall_forall in H. apply H. assumption.
Qed.
Lemma IntegratorIntegrated : forall t : T, Integrated intersected (Integrate intersect t).
intros t. apply IntegrateIntegrated_P. apply IntersectorIntegrated.
Qed.
Lemma 5: Promotion
If the LHS of a reductive subtyping proof is Integrated, then the reductive subtyping also holds after Integrating the RHS.Lemma LiteralPromotion' : forall ls : list Lit, intersected ls -> forall rs : list (sig2T RRule), incl (map proj2T1 rs) ls -> rsubam (@RPremise) (fun pl pr => Exists (fun r => match r with exist2T rl rr r => RPremise r pl pr end) rs) (Intersect ls) (sop2ui (sopintersect (map proj2T2 rs))).
intros ls Hint rs Hincl. pose proof (SopLiteralPromotion ls Hint rs Hincl) as HLP. clear Hint Hincl. apply Exists_exists in HLP. destruct HLP as [ls' [HIn HLP]]. apply in_split in HIn. destruct HIn as [l1 [l2 Heq]]. rewrite -> Heq. clear Heq. induction l1.
simpl. apply ram_uni_rl. induction HLP.
simpl. apply ram_top.
simpl. apply ram_int_r.
clear IHHLP HLP. apply Exists_exists in H. destruct H as [l' [HIn Hsub]]. apply in_split in HIn. destruct HIn as [l1 [l2' Heq]]. subst. induction l1.
simpl. apply ram_int_ll. destruct Hsub as [r Hsub]. apply ram_lit with r. intros tl tr Hp. pose proof (Hsub tl tr Hp) as H. remember (fun _ _ => Exists _ rs) as f. apply rsubam_mono with (A := f); [|assumption]. subst. intros tl0 tr0 Hex. mono. intros rt HIn Hprem. destruct rt. apply Hprem.
simpl. apply ram_int_lr. assumption.
assumption.
simpl. apply ram_uni_rr. assumption.
Qed.
Lemma ssub_isects_litrules : forall (lsl lsr : list Lit), rssub [lsl] [lsr] -> exists lrt : list (sig2T RRule), map proj2T2 lrt = lsr /\ incl (map proj2T1 lrt) lsl /\ Forall (fun rt => forall tl tr : T, RPremise (proj2V rt) tl tr -> rsub tl tr) lrt.
intros lsl lsr Hsub. unfold rssub in Hsub. unfold ssub in Hsub. apply Forall_singleton in Hsub. apply Exists_singleton_forward in Hsub. induction lsr.
exists []. split; [reflexivity | split; [intros H HIn; inversion HIn | constructor]].
inversion Hsub; subst. apply IHlsr in H2. destruct H2 as [lrt [Hmap [HIncl Hfa]]]. apply Exists_exists in H1. destruct H1 as [l [HIn Hlsub]]. destruct Hlsub as [r Hlsub]. exists ((exist2T l a r) :: lrt). subst; split; [reflexivity | split; [intros x [HIn' | HIn']; subst; [simpl|apply HIncl in HIn']; assumption| constructor; assumption]].
Defined.
Lemma sui_promotion (sl : sop) (tr : T) : SopIntegrated intersected sl -> suisub (lsub (@RPremise) (rsub)) sl tr -> ssub (lsub (@RPremise) (rsub)) sl (SopIntegrate sopintersect tr).
intros Hint Hsub. apply suisub_ssub in Hsub. unfold ssub in *. mono. intros lsl HInlsl Hex. apply Exists_exists in Hex. destruct Hex as [lsr [HInlsr Hfa]]. apply Exists_singleton in Hfa. assert (Hsub : forall ls, In ls [lsl] -> Exists (Forall (fun lr : Lit => Exists (fun ll : Lit => lsub (@RPremise) (rsub) ll lr) ls)) [lsr]) by (intros ls HIn; inversion HIn; subst; [apply Hfa | contradiction]). apply Forall_forall in Hsub. apply ssub_isects_litrules in Hsub. destruct Hsub as [lrt [Hprojr [Hprojl Hprem]]]. unfold SopIntegrated in Hint. rewrite -> Forall_forall in Hint. apply Hint in HInlsl. pose proof (LiteralPromotion' lsl HInlsl lrt Hprojl) as Hpromo. rewrite -> Hprojr in Hpromo. apply rsubam_mono with (A' := rsub) in Hpromo.
apply rsubam_rsub in Hpromo; [|trivial]. apply rsubf_uisub in Hpromo. apply uisub_suisub in Hpromo. unfold ui2sop in Hpromo. rewrite -> integrate_intersect in Hpromo. apply suisub_ssub in Hpromo. apply Forall_singleton in Hpromo. rewrite -> ui2sop_sop2ui in Hpromo. rewrite -> SopIntegrate_flat_map. fold (ui2sop tr). apply in_split in HInlsr. destruct HInlsr as [l1 [l2 Heq]]. rewrite -> Heq. clear Heq Hfa Hprojr Hprojl Hprem. induction l1.
simpl. apply Exists_app_or. left. assumption.
simpl. apply Exists_app_or. right. assumption.
intros tl' tr' Hex. apply Exists_exists in Hex. destruct Hex as [rt [HInrt Hrtp]]. rewrite -> Forall_forall in Hprem. destruct rt. apply (Hprem (exist2T a b c) HInrt tl' tr' Hrtp).
Qed.
Lemma Promotion : forall tl tr : T, Integrated intersected tl -> rsub tl tr -> rsub tl (Integrate intersect tr).
intros tl tr Hint Hsub. apply rsubf_uisub in Hsub. apply uisub_suisub in Hsub. apply sui_promotion in Hsub. apply ssub_suisub in Hsub. apply rsub_trans with (sop2ui (SopIntegrate sopintersect tr)); [| constructor; apply suisub_uisub; apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect; apply rsubf_uisub; apply rsub_refl]. pose proof (ui2sop_sopof_ui tl (Integrated_SumOfProducts _ _ Hint)) as Hsopof. apply (suisub_sopof_uisub _ _ _ _ Hsopof) in Hsub. constructor; assumption.
clear Hsub. remember intersected as f. clear Heqf. generalize dependent f. induction tl; intros f Hint; try (simpl in *; repeat constructor; assumption).
apply Forall_app. split; [apply IHtl1 | apply IHtl2]; apply Hint.
simpl in Hint. apply Integrated_int_Integrated in Hint. apply IHtl1 in Hint. unfold ui2sop. rewrite -> SopIntegrate_flat_map. apply SopIntegrated_flat_map. simpl. rewrite -> SopIntegrate_flat_map. fold (ui2sop tl1). apply SopIntegrated_flat_map. unfold SopIntegrated in *. mono. intros ls HInls Hint. apply Integrated_int_Integrated in Hint. apply IHtl2 in Hint. rewrite -> SopIntegrate_flat_map. apply SopIntegrated_flat_map. fold (ui2sop tl2). unfold SopIntegrated. mono. intros ls' Hinls' Hf. constructor; [|constructor]. constructor; [assumption | constructor].
Qed.
Lemmas 6 and 7: Integrated Monotonicity and Integrated Assumptions
The first three lemmas ssub_suisub_trans, lsub_rsubam_rsubf_trans, and lsub_rsubf_rsubam_trans are concerned with composing subtyping proofs, of various kinds, which is necessary for proving Monotonicity. Since rsubam is reductive subtyping with Assumptions and Monotonicity, integrated_assumptions' and IntegratedAssumptions already integrate the Integrated Monotonicity Lemma; thus the surface-level Lemma IntegratedMonotonicity follows from IntegratedAssumptions in this proof, while at the core, monotonicity is required to prove IntegratedAssumptions.Lemma ssub_suisub_trans (Rl Rm Rr : Lit -> Lit -> Prop) {sl : sop} (sm : sop) {tr : T} : (forall ll lm lr : Lit, Rl ll lm -> Rr lm lr -> Rm ll lr) -> ssub Rl sl sm -> suisub Rr sm tr -> suisub Rm sl tr.
intros Hltrans Hlm Hmr. unfold suisub in *. unfold ssub in Hlm. mono. intros lsl HInlsl Hexm. apply Exists_exists in Hexm. destruct Hexm as [lsm [HInlsm Hfam]]. rewrite -> Forall_forall in Hmr. apply Hmr in HInlsm. clear Hmr. induction HInlsm; try (constructor; assumption). apply Exists_exists in H. destruct H as [l' [HInl' HR]]. rewrite -> Forall_forall in Hfam. apply Hfam in HInl'. apply Exists_exists in HInl'. destruct HInl' as [l'' [HInl'' HR']]. constructor. apply Exists_exists. exists l''. split; [assumption | apply Hltrans with l'; assumption].
Qed.
Lemma lsub_rsubam_rsubf_trans (A : T -> T -> Prop) (ll lm lr : Lit) : lsub (@RPremise) (rsubam (@RPremise) A) ll lm -> lsub (@RPremise) (rsub) lm lr -> lsub (@RPremise) (rsubam (@RPremise) A) ll lr.
intros [ rlm plm ] [ rmr pmr ]. destruct (LiteralTransitivity rlm rmr) as [ rlr plr ]. apply Lsub with rlr. intros tl tr p. pose proof (plr tl tr p) as plr. clear rlr p. destruct plr as [ tm [ [ tltm tmtr ] | [ tltm tmtr ] ] ].
apply ram_mono with tl tm.
apply rsub_refl.
revert tltm. apply rsubam_bind. assumption.
revert tmtr. apply rsubam_rsub. assumption.
apply ram_mono with tm tr.
revert tltm. apply rsubam_rsub. assumption.
revert tmtr. apply rsubam_bind. assumption.
apply rsub_refl.
Qed.
Lemma lsub_rsubf_rsubam_trans (A : T -> T -> Prop) (ll lm lr : Lit) : lsub (@RPremise) (rsub) ll lm -> lsub (@RPremise) (rsubam (@RPremise) A) lm lr -> lsub (@RPremise) (rsubam (@RPremise) A) ll lr.
intros [ rlm plm ] [ rmr pmr ]. destruct (LiteralTransitivity rlm rmr) as [ rlr plr ]. apply Lsub with rlr. intros tl tr p. pose proof (plr tl tr p) as plr. clear rlr p. destruct plr as [ tm [ [ tltm tmtr ] | [ tltm tmtr ] ] ].
apply ram_mono with tm tr.
revert tltm. apply rsubam_rsub. assumption.
revert tmtr. apply rsubam_bind. assumption.
apply rsub_refl.
apply ram_mono with tl tm.
apply rsub_refl.
revert tltm. apply rsubam_bind. assumption.
revert tmtr. apply rsubam_rsub. assumption.
Qed.
Lemma integrated_assumptions' (A : T -> T -> Prop) (sl : sop) (tl tr : T) : SopIntegrated intersected sl -> rsub (sop2ui sl) tl -> rsubam (@RPremise) A tl tr -> (forall tl tr : T, A tl tr -> isub tl tr) -> isub' (sop2ui sl) tr.
intros isl sltl tlr asub. apply rsubam_mono with (A' := isub) in tlr; try assumption. clear A asub. constructor. apply suisub_uisub. apply rsubf_uisub in sltl. apply uisub_suisub' in sltl. revert tl isl sltl tlr. apply (irec_alt (fun ll lr => lsub (@IPremise) (rsubam (@RPremise) isub) ll lr -> lsub (@IPremise) isub' ll lr)) with (sl := sl) (tr := tr); clear sl tr.
intros ll lr srec [ r plr ]. apply Lsub with r. intros tl tr p. pose proof (plr tl tr p) as plr. destruct p as [ tl tr p ]. pose proof (srec r tl tr p) as srec. clear r p. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply srec with (sop2ui (SopIntegrate sopintersect tl)); try assumption.
apply SopIntegratorIntegrated.
apply uisub_suisub'. apply rsubf_uisub. apply rsub_refl.
eapply (ram_mono _ _ _ _ _ plr (rsub_refl tr)). Unshelve. 2: (constructor; apply suisub_uisub; apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect; apply rsubf_uisub; apply rsub_refl).
intros sl tr lrec tl isl sltl tltr. eapply suirec_suisub_suisub with (R' := lsub (@RPremise) (rsubam (@RPremise) isub)); try apply lrec; clear lrec.
clear sl tr tl isl sltl tltr. intros ll lr lrec [ r plr ]. apply lrec. apply Lsub with r. intros tl tr p. destruct p. apply ram_mono with tl tr; [apply Dereliction; apply rsub_refl | |apply rsub_refl]. apply plr. assumption.
revert sl isl sltl. induction tltr; intros sl isl sltl.
rename H into tlr. apply rsubf_uisub in tlr. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in tlr. apply sui_promotion in sltl; try assumption. clear isl. revert sltl tlr. apply ssub_suisub_trans. clear tl tr sl. intros ll lm lr [ rlm plm ] [ rmr pmr ]. destruct (LiteralTransitivity rlm rmr) as [ rlr plr ]. apply Lsub with rlr. intros tl tr p. pose proof (plr tl tr p) as plr. clear p. destruct plr as [ tm [ [ tltm tmtr ] | [ tltm tmtr ] ] ].
apply ram_mono with tm tr.
revert tltm. apply rsubam_rsub. assumption.
revert tmtr. apply rsubam_mono. clear tl tm tr tltm. intros tl tr p. unfold isub. unfold isub'. apply pmr. constructor. assumption.
apply rsub_refl.
apply ram_mono with tl tm.
apply rsub_refl.
revert tltm. apply rsubam_mono. clear tl tm tr tmtr. intros tl tr p. unfold isub. unfold isub'. apply pmr. constructor. assumption.
revert tmtr. apply rsubam_rsub. assumption.
rename H into tltl'. rename H0 into tr'tr. clear tltr. apply suisub_uisub in sltl. apply Rsubf in sltl. pose proof (rsub_trans _ tl _ sltl tltl') as sltl'. clear tl sltl tltl'. apply rsubf_uisub in sltl'. apply uisub_suisub' in sltl'. pose proof (IHtltr sl isl sltl') as IHtltr. clear tl' isl sltl'. apply rsubf_uisub in tr'tr. revert IHtltr tr'tr. apply suisub_uisub_trans. clear sl tr' tr. apply lsub_rsubam_rsubf_trans.
clear H0. assert (uisub (lsub (@RPremise) (rsubam (@RPremise) isub)) (TLit ll) (TLit lr)) as llr; [ constructor; apply Lsub with r; assumption | clear H ]. revert sltl llr. apply suisub_uisub_trans. clear ll lr r sl isl. apply lsub_rsubf_rsubam_trans.
unfold suisub. apply Forall_forall. intros. constructor.
apply IHtltr; [assumption|]. clear IHtltr. unfold suisub in *. mono. intros ls HIn Hsub. inversion Hsub; subst; assumption.
apply IHtltr; [assumption|]. clear IHtltr. unfold suisub in *. mono. intros ls HIn Hsub. inversion Hsub; subst; assumption.
pose proof (IHtltr1 _ isl sltl) as IH1. pose proof (IHtltr2 _ isl sltl) as IH2. clear IHtltr1 IHtltr2 sltl isl tltr1 tltr2. unfold suisub in *. forall_and IH. mono. intros ls HIn [Hsubl Hsubr]. constructor; assumption.
inversion sltl; [constructor | inversion H].
pose proof (IHtltr _ isl sltl) as IH. clear IHtltr isl sltl tltr. unfold suisub in *. mono. intros ls HIn Hsub. constructor; assumption.
pose proof (IHtltr _ isl sltl) as IH. clear IHtltr isl sltl tltr. unfold suisub in *. mono. intros ls HIn Hsub. constructor; assumption.
induction sltl; constructor; inversion isl; subst; [|apply IHsltl; assumption]. inversion H; subst; apply ruisub_suisub in H1; pose proof (Forall_cons _ H2 (Forall_nil intersected)) as Hint; [pose proof IHtltr1 _ Hint H1 as Hsub|pose proof IHtltr2 _ Hint H1 as Hsub]; inversion Hsub; assumption.
Qed.
Lemma IntegratedAssumptions (A : T -> T -> Prop) (tl tr : T) : rsubam (@RPremise) A tl tr -> (forall tl tr : T, A tl tr -> isub tl tr) -> isub tl tr.
intros lr Himpl. pose proof (integrated_assumptions' A (SopIntegrate sopintersect tl) tl tr) as H'. unfold isub. unfold isub'. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply uisub_suisub'. apply rsubf_uisub. apply H'; try assumption.
apply SopIntegratorIntegrated.
apply sopdereliction. apply rsub_refl.
Qed.
Lemma IntegratedMonotonicity : forall t1 t2 t3 t4 : T, rsub t1 t2 -> isub t2 t3 -> rsub t3 t4 -> isub t1 t4.
intros t1 t2 t3 t4 H12 H23 H34. apply IntegratedAssumptions with (A:=fun tl tr => isub tl tr); [| intros; assumption]; apply ram_mono with (tl' := t2) (tr' := t3); [| apply ram_assumption |]; assumption.
Qed.
Lemma 8: Integrated Promotion
If Integrated Subtyping holds between two types, it also holds after applying the Integrator to the RHS.Lemma issub_promotion (sl sr : sop) : Forall intersected sl -> issub sl sr -> issub sl (flat_map sopintersect sr).
intros isl slr. induction slr as [ | il sl ilr slr ].
constructor.
inversion isl; clear isl; subst. rename H1 into iil. rename H2 into isl. constructor.
clear sl slr isl IHslr. induction ilr as [ ir sr ilr | ir sr ilr ]; simpl; apply Exists_app_or.
left. clear sr. assert (exists2 rs : list (sig2T RRule), incl (map proj2T1 rs) il /\ map proj2T2 rs = ir & Forall (fun r => match r with exist2T ll lr r => forall pl pr : T, IPremise r pl pr -> isub' pl pr end) rs) as [ rs [ irs e ] ps ].
clear iil. induction ilr as [ | lr ir llr ilr ].
apply ex_intro2 with nil; repeat constructor. simpl. intros ll i. destruct i.
clear ilr. destruct IHilr as [ rs [ ril e ] ps ]. destruct e. apply Exists_exists in llr. destruct llr as [ ll [ llil r ] ]. destruct r as [ r p ]. apply ex_intro2 with (cons (exist2T ll lr r) rs); simpl.
split; try reflexivity. intros l i. destruct i.
subst. assumption.
apply ril. assumption.
constructor; assumption.
clear ilr. destruct e. apply LiteralPromotion' in irs; try assumption. apply integrated_assumptions' with (sl := [il]) in irs.
clear iil ps. apply rsubf_uisub in irs. apply uisub_suisub' in irs. apply suisub_ssub' in irs. inversion irs; clear irs; subst. rename H1 into ilrs. clear H2. assumption.
repeat constructor. assumption.
simpl. repeat constructor. apply rsubf_uisub. apply rsub_refl.
clear il iil irs. intros tl tr ers. induction ers as [ r rs p | r rs ers ].
inversion ps; clear ps; subst. rename H1 into ilr. clear H2. destruct r as [ pl pr r ]. unfold isub. unfold isub'. apply ilr. constructor. assumption.
inversion ps; clear ps; subst. apply IHers. assumption.
right. assumption.
apply IHslr. assumption.
Qed.
Lemma isuisub_promotion (sl : sop) (tr : T) : Forall intersected sl -> suisub (lsub (@IPremise) isub') sl tr -> issub sl (SopIntegrate sopintersect tr).
intros isl slr. rewrite -> SopIntegrate_flat_map. fold (ui2sop tr). apply issub_promotion; try assumption. apply suisub_ssub. assumption.
Qed.
Lemma integrated_promotion (tl tr : T) : isub tl tr -> isub tl (sop2ui (SopIntegrate sopintersect tr)).
intro ilr. apply rsubf_uisub in ilr. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in ilr. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply ssub_suisub. apply isuisub_promotion; try assumption. apply SopIntegratorIntegrated.
Qed.
Lemma uisub_dnf_r {R : Lit -> Lit -> Prop}: forall tl tr : T, uisub R tl (sop2ui (ui2sop tr)) -> uisub R tl tr.
intros tl tr Hsub. generalize dependent tl; induction tr; intros tl Hsub.
apply ui_top.
simpl in Hsub. assumption.
unfold ui2sop in Hsub. simpl in Hsub. fold (ui2sop tr1) in *. fold (ui2sop tr2) in *. apply uisub_sop2ui_app in Hsub. remember (TUni (sop2ui _) (sop2ui _)) as tuni. induction Hsub; try (inversion Heqtuni; fail); try (repeat remove_eq_implications; constructor; assumption); clear IHHsub; inversion Heqtuni; subst; clear Heqtuni; [apply IHtr1 in Hsub | apply IHtr2 in Hsub]; constructor; assumption.
apply ui_int_r; [apply IHtr1 | apply IHtr2]; clear IHtr1 IHtr2.
unfold ui2sop in Hsub. simpl in Hsub. rewrite -> SopIntegrate_flat_map in Hsub. fold (ui2sop tr1) in Hsub. remember (flat_map _ (ui2sop tr1)) as s'. apply ui2sop_sop2ui_sublists with s'; [assumption|subst; clear Hsub]. induction (ui2sop tr1).
constructor.
simpl. apply Forall_app; split.
apply Forall_forall. intros ls HIn. rewrite -> SopIntegrate_flat_map in HIn. apply in_flat_map in HIn. destruct HIn as [ls' [HIn' HInls']]. inversion HInls'; [|contradiction]; subst. apply Exists_cons_hd. intros ls HInls; apply in_app_iff; left; assumption.
apply Forall_forall. intros ls HIn. apply in_flat_map in HIn. destruct HIn as [ls' [HInls' HIn]]. rewrite -> Forall_forall in IHl. apply Exists_cons_tl. apply IHl. apply in_flat_map. exists ls'; split; assumption.
unfold ui2sop in Hsub. simpl in Hsub. rewrite -> SopIntegrate_flat_map in Hsub. fold (ui2sop tr1) in Hsub. remember (flat_map _ (ui2sop tr1)) as s'. apply ui2sop_sop2ui_sublists with s'; [assumption|subst; clear Hsub]. induction (ui2sop tr1).
constructor.
simpl. apply Forall_app; split.
apply Forall_forall. intros ls HIn. rewrite -> SopIntegrate_flat_map in HIn. apply in_flat_map in HIn. destruct HIn as [ls' [HIn' HInls']]. inversion HInls'; [|contradiction]; subst. fold (ui2sop tr2) in HIn'. apply Exists_exists. exists ls'. split; [assumption|]. intros ls HIn; apply in_app_iff; right; assumption.
apply Forall_forall. intros ls HIn. apply in_flat_map in HIn. destruct HIn as [ls' [HInls' HIn]]. rewrite -> Forall_forall in IHl. apply IHl. apply in_flat_map. exists ls'; split; assumption.
unfold ui2sop in Hsub. simpl in Hsub. remember (TUni (TIsect _ _) TBot) as tuni. induction Hsub; try (inversion Heqtuni; fail); try (repeat remove_eq_implications; constructor; assumption); clear IHHsub; inversion Heqtuni; subst; clear Heqtuni.
apply uisub_int_r in Hsub. apply Hsub.
apply (uisub_bot _ _ Hsub).
Qed.
Lemma IntegratedPromotion : forall tl tr : T, isub tl tr -> isub tl (Integrate intersect tr).
intros tl tr Hsub. apply integrated_promotion in Hsub. rewrite <- SopIntegrate_Integrate with (f:= intersect) in Hsub; [| intros ls; reflexivity]. fold (ui2sop (Integrate intersect tr)) in Hsub. constructor. apply rsubf_uisub in Hsub. revert Hsub. apply uisub_dnf_r.
Qed.
Lemma IntegratedReflexivity : forall t : T, isub t t.
intros t. apply IntegratedAssumptions with (A := fun _ _ => False); [|intros; contradiction]. apply rsub_rsubam. apply rsub_refl.
Qed.
Lemma 10: Declarative-to-Integrated Literal Conversion
Straightforward proof based on IntegratedAssumptions.Lemma DeclarativeToIntegratedLiteralConversion : forall {ll lr : Lit} (r : DRule ll lr), (forall tl tr : T, DPremise r tl tr -> isub tl tr) -> isub (TLit ll) (TLit lr).
intros ll lr r Hprem. pose proof (DRuleToRProof r). apply IntegratedAssumptions with (A := DPremise r); assumption.
Qed.
Lemma 11: Integrated Transitivity
As before, we need to be able to compose assumptions of literal subtyping. The complication here is that the the LHS of the RHS premise is integrated, while the RHS of the LHS premise is not. Thus, we need to promote the LHS premise. Lastly, IntegratedAssumptions lets us convert the rsubam proofs of LiteralTransitivity into the isub proofs we need.Lemma IntegratedTransitivity (t1 t2 t3 : T) : isub t1 t2 -> isub t2 t3 -> isub t1 t3.
intros i12 i23. apply rsubf_uisub in i12. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in i12. apply isuisub_promotion in i12; try apply SopIntegratorIntegrated. apply rsubf_uisub in i23. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in i23. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. revert i12 i23. generalize (SopIntegrate sopintersect t2). clear t2. revert t3. generalize (SopIntegrate sopintersect t1). clear t1. apply (irec_alt (fun ll lr => forall lm, lsub (@IPremise) isub' ll lm -> lsub (@IPremise) isub' lm lr -> lsub (@IPremise) isub' ll lr) (fun tl tr => forall tm, _ -> _ -> suisub _ _ _)).
intros ll lr lrec lm llm lmr. destruct llm as [ rlm alm ]. destruct lmr as [ rmr amr ]. destruct (LiteralTransitivity rlm rmr) as [ rlr alr ]. apply Lsub with rlr. intros tl tr plr. destruct plr as [ pl pr plr ]. pose proof (lrec rlr pl pr plr) as lrec. pose proof (alr pl pr plr) as alr. destruct alr as [ pm alr ]. assert (isub pl pm /\ isub pm pr) as [ plm pmr ].
destruct alr as [ [ plm pmr ] | [ plm pmr ] ].
apply IntegratedAssumptions in plm.
apply IntegratedAssumptions in pmr.
split; assumption.
intros tl tr p. unfold isub. unfold isub'. apply amr. constructor. assumption.
intros tl tr p. unfold isub. unfold isub'. apply alm. constructor. assumption.
apply IntegratedAssumptions in plm.
apply IntegratedAssumptions in pmr.
split; assumption.
intros tl tr p. unfold isub. unfold isub'. apply alm. constructor. assumption.
intros tl tr p. unfold isub. unfold isub'. apply amr. constructor. assumption.
clear rlr plr alr. unfold isub'. constructor. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect. apply lrec with (SopIntegrate sopintersect pm).
apply isuisub_promotion; try apply SopIntegratorIntegrated. apply rsubf_uisub in plm. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in plm. assumption.
apply rsubf_uisub in pmr. apply suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect in pmr. assumption.
intros sl tr srec sm slsm smtr. eapply suirec_suisub_suisub with (R' := fun ll lr => exists2 lm, lsub (@IPremise) isub' ll lm & lsub (@IPremise) isub' lm lr); try apply srec; clear srec.
clear sl tr sm slsm smtr. simpl. intros ll lr lrec [ lm llm lmr ]. apply lrec with lm; assumption.
revert slsm smtr. apply ssub_suisub_trans. intros ll lm lr llm lmr. apply ex_intro2 with lm; assumption.
Qed.
Lemma 12: Integrated Completeness
Mostly applying the previous lemmas, some extra work to cover distributivity.Lemma IntegratedCompleteness : forall tl tr : T, esub tl tr -> isub tl tr.
intros tl tr Hsub. induction Hsub; try (try apply rsubf_uisub in IHHsub; try apply rsubf_uisub in IHHsub1; try apply rsubf_uisub in IHHsub2; repeat constructor; assumption); try (apply IntegratedAssumptions with (A := fun _ _ => False); [|intros; contradiction]; constructor ; apply rsub_rsubam; apply rsub_refl).
apply IntegratedReflexivity.
apply IntegratedTransitivity with tm; assumption.
apply IntersectorCompleteness in H. apply rsub_dsub in H. unfold isub. unfold isub'. revert H. generalize (Integrate intersect tl) as t. intros t H. apply rsubf_uisub in H. constructor. induction H; try (constructor; assumption). destruct H as [r H]. constructor; apply Lsub with r. intros tlx trx [tlx' trx' Hprem]. clear tlx trx. fold (isub' (Integrate intersect tlx') trx'). fold (isub tlx' trx'). apply IntegratedAssumptions with (A:= fun _ _ => False); [|intros; contradiction]. apply rsub_rsubam. apply H. assumption.
apply DeclarativeToIntegratedLiteralConversion with r. assumption.
apply IntegratedTransitivity with (TIsect (TUni trl trr) tl).
apply IntegratedAssumptions with (A := fun _ _ => False); [|intros; contradiction]. apply ram_int_r; constructor; apply rsub_rsubam; apply rsub_refl.
unfold isub. unfold isub'. constructor. simpl. apply ui_uni_l; [apply ui_uni_rl | apply ui_uni_rr]; apply rsubf_uisub; [remember (Integrate intersect (TIsect trl tl)) as x | remember (Integrate intersect (TIsect trr tl)) as x]; assert (Hii := Heqx); simpl in Hii; rewrite -> Heqx in Hii; rewrite <- Hii; (apply IntegratedAssumptions with (A := fun _ _ => False); [|intros; contradiction]); apply ram_int_r; constructor; apply rsub_rsubam; apply rsub_refl.
Qed.
Equivalence of Integrated and Extended Subtyping
Simply combines IntegratedSoundness and IntegratedCompleteness.Lemma isub_esub : forall tl tr : T, isub tl tr <-> esub tl tr.
intros tl tr. split; intros Hsub.
apply IntegratedSoundness; assumption.
apply IntegratedCompleteness; assumption.
Qed.
MAIN THEOREM, Part 1: Decidability of Extended Subtyping
We first prove the Lemma dsub_ext_dec, which says that if there is a relation that is equivalent to Extended Subtyping and decidable, then Extended Subtyping is decidable. We instantiate this Lemma with isub in dsuba_ext_dec_isub' and use that to prove the main theorem, namely that Integrated Subtyping provides a decision procedure for Extended Subtyping.Lemma dsuba_ext_dec : forall (R : T -> T -> Prop), (forall tl tr : T, R tl tr <-> esub tl tr) -> (forall tl tr : T, {R tl tr} + {~ R tl tr}) -> forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
intros R Hequiv Hdec tl tr. destruct (Hdec tl tr) as [H | Hn]; [left | right; intros H; apply Hn]; apply Hequiv; assumption.
Qed.
Definition dsuba_ext_dec_isub' : forall tl tr : T, {esub tl tr} + {~ esub tl tr} := dsuba_ext_dec isub isub_esub IntegratedDecidability.
Theorem DecidabilityOfExtendedSubtyping : forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
apply dsuba_ext_dec_isub'.
Qed.
Beginning of MAIN THEOREM, Part 2: Optimized Decision Procedure for Extended Subtyping
The decision procedure for isub is somewhat inefficient. As it is defined, it first tries to recurse down into the LHS type as far as possible before ever touching the RHS type. However, it is well-known that a subtyping algorithm for union and intersection types can prioritize certain rules over others. In particular, the LHS-union and RHS-intersection rules can (and should) always be applied before any other rules, because none of these rules makes a choice that might have to be back-tracked later. The LHS-intersection and RHS-union rules, on the other hand, need to make a choice and might have to back-track later because we tried the wrong subtyping first. This means that normally, one might have to try out all four combinations of of potential subtypings if one needs to decide whether τ1∩τ2 <: τ3∪τ4. However, because we know that the LHS is in DNF, we know that all we can do on the LHS is to find a number of matching Literals for whatever is on the RHS. That is, there is no way that the proof search will branch in a way such that different branches will choose differently between τ3 and τ4 on the RHS. This means that we can prioritize the RHS-union rule in those cases. The result is a deterministic algorithm that minimizes the search space for subtyping proofs.- ouisub says all subtyping proofs need to descend through all unions on the LHS down to either bottom or a ProductOfLiterals (i.e. a TIsect, TTop, or TLit) first.
- Then, ouisub_r says all subtyping proofs needs to descend through the RHS down to either a TTop or a literal TLit
- Only then, ouisub_l allows recursing through intersections on the LHS until we find a literal that is in a literal subtyping relation with an RHS literal
Inductive ouisub_l {R : Lit -> Lit -> Prop} : T -> Lit -> Prop :=
| oui_lit (ll lr : Lit) : R ll lr -> ouisub_l (TLit ll) lr
| oui_int_l (tl tr : T) (l : Lit) : ouisub_l tl l -> ouisub_l (TIsect tl tr) l
| oui_int_r (tl tr : T) (l : Lit) : ouisub_l tr l -> ouisub_l (TIsect tl tr) l
.
Arguments ouisub_l : clear implicits.
Inductive ouisub_r {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| oui_poll (tl : T) (lr : Lit) : ouisub_l R tl lr -> ouisub_r tl (TLit lr)
| oui_top (t : T) : ouisub_r t TTop
| oui_int (t tl tr : T) : ouisub_r t tl -> ouisub_r t tr -> ouisub_r t (TIsect tl tr)
| oui_uni_l (t tl tr : T) : ouisub_r t tl -> ouisub_r t (TUni tl tr)
| oui_uni_r (t tl tr : T) : ouisub_r t tr -> ouisub_r t (TUni tl tr)
.
Arguments ouisub_r : clear implicits.
Inductive ouisub {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| oui_polr (tl tr : T) : ProductOfLiterals tl -> ouisub_r R tl tr -> ouisub tl tr
| oui_bot (t : T) : ouisub TBot t
| oui_uni (tl tr t : T) : ouisub tl t -> ouisub tr t -> ouisub (TUni tl tr) t
.
Arguments ouisub : clear implicits.
Inductive orsubf (RPremise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop) : T -> T -> Prop :=
| ORsubf : forall tl tr : T, ouisub (lsub RPremise (orsubf RPremise)) tl tr -> orsubf RPremise tl tr
.
orsubf_ouisub is equivalent to rsubf_uisub
Lemma orsubf_ouisub {RPremise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} : forall tl tr : T, orsubf RPremise tl tr -> ouisub (lsub RPremise (orsubf RPremise)) tl tr.
intros tl tr Hsub. inversion Hsub; subst. assumption.
Qed.
Some helper Lemmas
Lemma ouisub_int_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub R (TIsect tl tr) t -> ouisub_r R (TIsect tl tr) t.
intros tl tr t Hsub. inversion Hsub; assumption.
Qed.
Lemma ouisub_top_l {R : Lit -> Lit -> Prop} : forall t : T, ouisub R TTop t -> ouisub_r R TTop t.
intros t Hsub. inversion Hsub; assumption.
Qed.
Lemma ouisub_r_top_lit {R : Lit -> Lit -> Prop} : forall l : Lit, ouisub_r R TTop (TLit l) -> False.
intros t Hsub. inversion Hsub; subst. inversion H1.
Qed.
Lemma ouisub_r_uni_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub_r R (TUni tl tr) t -> ouisub_r R tl t /\ ouisub_r R tr t.
intros tl tr t Hsub. remember (TUni tl tr) as tuni; induction Hsub; inversion Heqtuni; subst; repeat remove_eq_implications.
inversion H.
split; apply oui_top.
split; apply oui_int; (apply IHHsub0 || apply IHHsub1).
split; apply oui_uni_l; apply IHHsub0.
split; apply oui_uni_r; apply IHHsub0.
Qed.
Lemma ouisub_uni_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub R (TUni tl tr) t -> ouisub R tl t /\ ouisub R tr t.
intros tl tr t Hsub. inversion Hsub; subst; [|split; assumption]. inversion H.
Qed.
Lemma ouisub_ProductOfLiterals {R : Lit -> Lit -> Prop} : forall tl tr : T, ProductOfLiterals tl -> ouisub R tl tr -> ouisub_r R tl tr.
intros tl tr Hpol Hsub. inversion Hsub; subst; try (inversion Hpol; fail); subst; assumption.
Qed.
Lemma ouisub_r_lit_r {R : Lit -> Lit -> Prop} : forall (tl : T) (lr : Lit), ouisub_r R tl (TLit lr) -> ouisub_l R tl lr.
intros tl lr Hsub. inversion Hsub; subst; assumption.
Qed.
Ltac solve_SumOfProducts := match goal with
| [H : ?g |- ?g] => apply H
| [H : ProductOfLiterals ?t |- SumOfProducts ?t] => apply SOP_prod; apply H
| [H : SumOfProducts (TUni ?tl ?tr) |- _] => let H' := fresh H in pose proof (SumOfProducts_uni_l H) as H'; apply H'
| [H : SumOfProducts (TUni ?tl ?tr) |- _] => let H' := fresh H in pose proof (SumOfProducts_uni_r H) as H'; apply H'
| [H : ProductOfLiterals (TIsect ?tl ?tr) |- _] => apply ProductOfLiterals_int_l in H; solve_SumOfProducts
| [H : ProductOfLiterals (TIsect ?tl ?tr) |- _] => apply ProductOfLiterals_int_r in H; solve_SumOfProducts
| [H : SumOfProducts (TIsect ?tl ?tr) |- _] => apply SumOfProducts_int in H; try solve_SumOfProducts
| [H : SumOfProducts (TIsect ?tl ?tr) |- _] => apply SumOfProducts_int in H; solve_SumOfProducts
| [|- ProductOfLiterals _] => constructor; assumption
end.
The definition of ouisub_dec follows the prioritized proof-search method description above.
Recursive calls have the form (destruct IH _ _ _), and prioritize in order
In the last case, there are inner recursions to go over all possible rules between the two literals, and for each such rule (while no applicable one has been found), all of its premses.
For a somewhat easier-to-read version of the algorithm, check the result of extracting this function to ML, listed below (or check "OptimizedSubtyping.ml" after compiling/running this file once).
Definition ouisub_dec {Premise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} (premises_for_rule : 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) /\ SumOfProducts tl) : forall tl tr : T, SumOfProducts tl -> {orsubf Premise tl tr} + {~ orsubf Premise tl tr}.
intros tl tr. change (SumOfProducts (fst (tl, tr)) -> {orsubf Premise (fst (tl, tr)) (snd (tl, tr))} + {~ (orsubf Premise (fst (tl, tr)) (snd (tl, tr)))}). apply (Fix progress_measure_wf (fun tp => SumOfProducts (fst tp) -> {orsubf Premise (fst tp) (snd tp)} + {~ orsubf Premise (fst tp) (snd tp)})). clear tl tr. intros [tl tr] IH Hsop; simpl in *.
destruct tl as [| | tll tlr | tll tlr | ll].
destruct tr as [| | trl trr | trl trr | lr].
left. repeat constructor; fail.
right. intros Hnsub. inversion Hnsub; subst. inversion H; subst. inversion H1.
assert (Hpml : progress_measure (TTop, trl) (TTop, TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsub | Hnsubl].
left. constructor. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|constructor]. apply oui_polr; constructor ; assumption.
assert (Hpmr : progress_measure (TTop, trr) (TTop, TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsub | Hnsubr].
left. constructor. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|constructor]. apply oui_polr; constructor ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; [apply Hnsubl | apply Hnsubr]; constructor; constructor; assumption.
assert (Hpml : progress_measure (TTop, trl) (TTop, TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsubl | Hnsub].
assert (Hpmr : progress_measure (TTop, trr) (TTop, TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsubr | Hnsub].
left. constructor. apply orsubf_ouisub in Hsubl. apply orsubf_ouisub in Hsubr. simpl in *. apply ouisub_ProductOfLiterals in Hsubl; [|constructor]. apply ouisub_ProductOfLiterals in Hsubr; [|constructor]. apply oui_polr; constructor ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst; inversion H1; subst. inversion H4; subst.
left. repeat constructor; fail.
assert (Hpml : progress_measure (tll, tr) ((TUni tll tlr), tr)) by solve_progress_measure. destruct (IH _ Hpml (SumOfProducts_uni_l Hsop)) as [Hsubl | Hnsub].
assert (Hpmr : progress_measure (tlr, tr) ((TUni tll tlr), tr)) by solve_progress_measure. destruct (IH _ Hpmr (SumOfProducts_uni_r Hsop)) as [Hsubr | Hnsub].
left. constructor. apply orsubf_ouisub in Hsubl. apply orsubf_ouisub in Hsubr. constructor; assumption.
right. intros Hn. inversion Hn; subst; apply Hnsub. apply ouisub_uni_l in H. constructor; apply H.
right. intros Hn. inversion Hn; subst; apply Hnsub. apply ouisub_uni_l in H. constructor; apply H.
destruct tr as [| | trl trr | trl trr | lr].
left. constructor. apply SumOfProducts_int in Hsop. apply oui_polr; [assumption | constructor; fail].
right. intros Hn. inversion Hn; subst. inversion H; subst; inversion H1; subst.
assert (Hpml : progress_measure (TIsect tll tlr, trl) (TIsect tll tlr, TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsub | Hnsubl].
left. constructor. apply SumOfProducts_int in Hsop. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|assumption]. apply oui_polr ; [| constructor] ; assumption.
assert (Hpmr : progress_measure (TIsect tll tlr, trr) (TIsect tll tlr, TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsub | Hnsubr].
left. constructor. apply SumOfProducts_int in Hsop. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|assumption]. apply oui_polr; [|constructor] ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; [apply Hnsubl | apply Hnsubr]; constructor; constructor; assumption.
assert (Hpml : progress_measure (TIsect tll tlr, trl) (TIsect tll tlr, TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsubl | Hnsub].
assert (Hpmr : progress_measure (TIsect tll tlr, trr) (TIsect tll tlr, TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsubr | Hnsub].
left. constructor. apply SumOfProducts_int in Hsop. apply orsubf_ouisub in Hsubl. apply orsubf_ouisub in Hsubr. simpl in *. apply ouisub_ProductOfLiterals in Hsubl; [|assumption]. apply ouisub_ProductOfLiterals in Hsubr; [|assumption]. apply oui_polr; [|constructor] ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
assert (Hpml : progress_measure (tll, (TLit lr)) (TIsect tll tlr, (TLit lr))) by solve_progress_measure. apply SumOfProducts_int in Hsop. destruct (IH _ Hpml (SOP_prod _ (ProductOfLiterals_int_l Hsop))) as [Hsub | Hnsubl].
left. constructor. pose proof (ProductOfLiterals_int_l Hsop) as Hpoll. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|assumption]. apply ouisub_r_lit_r in Hsub. apply oui_polr ; [| constructor; constructor] ; assumption.
assert (Hpmr : progress_measure (tlr, (TLit lr)) (TIsect tll tlr, (TLit lr))) by solve_progress_measure. destruct (IH _ Hpmr (SOP_prod _ (ProductOfLiterals_int_r Hsop))) as [Hsub | Hnsubr].
left. constructor. pose proof (ProductOfLiterals_int_r Hsop) as Hpoll. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|assumption]. apply ouisub_r_lit_r in Hsub; apply oui_polr ; [| constructor; constructor] ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. simpl in *. inversion H1 ; subst; inversion H4; subst; [apply Hnsubl | apply Hnsubr].
constructor ; constructor; [apply (ProductOfLiterals_int_l H0)|]; constructor; assumption.
constructor ; constructor; [apply (ProductOfLiterals_int_r H0)|]; constructor; assumption.
destruct tr as [| | trl trr | trl trr | lr].
left. constructor. apply oui_polr; constructor; fail.
right. intros Hn. inversion Hn; subst. inversion H; subst; inversion H1; subst.
assert (Hpml : progress_measure ((TLit ll), trl) ((TLit ll), TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsub | Hnsubl].
left. constructor. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|constructor]. apply oui_polr ; constructor ; assumption.
assert (Hpmr : progress_measure ((TLit ll), trr) ((TLit ll), TUni trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsub | Hnsubr].
left. constructor. apply orsubf_ouisub in Hsub. simpl in Hsub. apply ouisub_ProductOfLiterals in Hsub; [|constructor]. apply oui_polr; constructor ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; [apply Hnsubl | apply Hnsubr]; constructor; constructor; assumption.
assert (Hpml : progress_measure ((TLit ll), trl) ((TLit ll), TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpml Hsop) as [Hsubl | Hnsub].
assert (Hpmr : progress_measure ((TLit ll), trr) ((TLit ll), TIsect trl trr)) by solve_progress_measure. destruct (IH _ Hpmr Hsop) as [Hsubr | Hnsub].
left. constructor. apply orsubf_ouisub in Hsubl. apply orsubf_ouisub in Hsubr. simpl in *. apply ouisub_ProductOfLiterals in Hsubl; [|constructor]. apply ouisub_ProductOfLiterals in Hsubr; [|constructor]. apply oui_polr; constructor ; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
right. intros Hn; inversion Hn; subst. inversion H; subst. inversion H1; subst; apply Hnsub; constructor; constructor; assumption.
pose proof (SyntaxDirectedness_Rules ll lr) as [rules Hrules]. assert (exists_applicable_rule : {r : RRule ll lr | In r rules /\ forall tl tr : T, Premise ll lr r tl tr -> orsubf Premise tl tr} + {forall r : RRule ll lr, In r rules -> exists tp : T * T, Premise ll lr r (fst tp) (snd tp) /\ ~ orsubf Premise (fst tp) (snd tp)}).
clear Hrules. induction rules as [| r rules]; [right; intros r HIn; inversion HIn |]. pose proof (premises_for_rule _ _ r) as [premises Hpremises]; clear premises_for_rule. assert (all_premises_hold : {forall tl tr : T, In (tl, tr) premises -> orsubf Premise tl tr} + {exists tp : T * T, Premise ll lr r (fst tp) (snd tp) /\ ~ orsubf Premise (fst tp) (snd tp)}). assert (Hpremises' : forall pl pr : T, In (pl, pr) premises -> Premise ll lr r pl pr) by (apply Hpremises). clear Hpremises. induction premises as [|p premises]; [left; intros tl tr HIn; inversion HIn|]. destruct p as [tl tr]. pose proof (Hpremises' tl tr (in_eq (tl, tr) premises)) as Hp. apply HMlit in Hp. destruct Hp as [current_premise_holds Hsoptl]. apply (IH) in current_premise_holds; [|apply Hsoptl]; simpl in current_premise_holds. destruct current_premise_holds as [Hp | Hnp]; [|right; exists (tl, tr); split; [apply Hpremises'; apply in_eq|assumption]]. assert (Hpremises_rest : forall pl pr : T, In (pl, pr) premises -> Premise ll lr r pl pr) by (intros pl pr HIn; apply Hpremises'; apply in_cons; assumption). destruct (IHpremises Hpremises_rest) as [Hprem | Hnprem]; [|right; assumption]. left. intros tlx trx HIn. inversion HIn; subst; [inversion H; subst|apply Hprem] ; assumption.
destruct all_premises_hold as [Hpdec | Hpdec].
left. exists r. split; [apply in_eq |]. intros tl tr Hp. apply Hpremises in Hp. apply Hpdec in Hp. assumption.
destruct IHrules as [[r' [HIn Hprem]] | Hnrule]; [left | right; intros r' HIn; inversion HIn; subst; [| apply Hnrule]; assumption]. exists r'; split; [apply in_cons|]; assumption.
destruct exists_applicable_rule as [[r [HIn Hprem]] | Hn].
left. repeat constructor. apply Lsub with r. assumption.
right. intros Hsub. apply orsubf_ouisub in Hsub. inversion Hsub; subst. inversion H0; subst. inversion H3; subst. destruct H2 as [r Hr]. pose proof (Hn r (Hrules r)) as [tp [Hp Hsub']]. apply Hr in Hp. contradiction.
Defined.
Extraction Language Ocaml.
Extraction "OptimizedSubtyping.ml" ouisub_dec.
The result of the above extraction is shown below (check "OptimizedSubtyping.ml" after compiling/running this file once).
The inner recursive function that is defined on pairs because that is how the recursion principle works - the pair consists of the two arguments to the subtyping algorithm.
What we can see in this definition is that we first match on the left argument and then potentially match on the right argument, recursing into first Unions on the left, then Unions and Intersections on the right, and finally Intersections on the right, until we either find an easy case involving Top or Bottom or two Literals.
In the latter case, we find all the rules that might apply for the two literals in question, and try to see if we can find one for which all premises hold.
The return values Left and Inleft _ here represent true, while the return values Right and Inright represent false.
Similar to the definition of isub based on rsubf, we define oisub based on orsubf, and prove it's decidability (oisub_dec).
let ouisub_dec premises_for_rule tl tr = let rec fix_F = function | Pair (tl0, tr0) -> (match tl0 with | TTop -> (match tr0 with | TTop -> Left | TUni (trl, trr) -> let s = fix_F (Pair (TTop, trl)) in (match s with | Left -> Left | Right -> fix_F (Pair (TTop, trr))) | TIsect (trl, trr) -> let s = fix_F (Pair (TTop, trl)) in (match s with | Left -> fix_F (Pair (TTop, trr)) | Right -> Right) | _ -> Right) | TBot -> Left | TUni (tll, tlr) -> let s = fix_F (Pair (tll, tr0)) in (match s with | Left -> fix_F (Pair (tlr, tr0)) | Right -> Right) | TIsect (tll, tlr) -> (match tr0 with | TTop -> Left | TBot -> Right | TUni (trl, trr) -> let s = fix_F (Pair ((TIsect (tll, tlr)), trl)) in (match s with | Left -> Left | Right -> fix_F (Pair ((TIsect (tll, tlr)), trr))) | TIsect (trl, trr) -> let s = fix_F (Pair ((TIsect (tll, tlr)), trl)) in (match s with | Left -> fix_F (Pair ((TIsect (tll, tlr)), trr)) | Right -> Right) | TLit lr -> let s = fix_F (Pair (tll, (TLit lr))) in (match s with | Left -> Left | Right -> fix_F (Pair (tlr, (TLit lr))))) | TLit ll -> (match tr0 with | TTop -> Left | TBot -> Right | TUni (trl, trr) -> let s = fix_F (Pair ((TLit ll), trl)) in (match s with | Left -> Left | Right -> fix_F (Pair ((TLit ll), trr))) | TIsect (trl, trr) -> let s = fix_F (Pair ((TLit ll), trl)) in (match s with | Left -> fix_F (Pair ((TLit ll), trr)) | Right -> Right) | TLit lr -> let x0 = M_traditional.coq_SyntaxDirectedness_Rules ll lr in let exists_applicable_rule = let rec f = function | Nil -> Inright | Cons (y, l0) -> let x1 = premises_for_rule ll lr y in let all_premises_hold = let rec f0 = function | Nil -> Left | Cons (y0, l2) -> let current_premise_holds = fix_F y0 in (match current_premise_holds with | Left -> f0 l2 | Right -> Right) in f0 x1 in (match all_premises_hold with | Left -> Inleft y | Right -> f l0) in f x0 in (match exists_applicable_rule with | Inleft _ -> Left | Inright -> Right))) in fix_F (Pair (tl, tr))
Definition oisub (tl tr : T) := orsubf (@IPremise) (Integrate intersect tl) tr.
Lemma oisub_dec : forall tl tr : T, {oisub tl tr} + {~ oisub tl tr}.
intros tl tr. unfold oisub. apply ouisub_dec.
intros ll lr r. pose proof (SyntaxDirectedness_Premises r) as [prems Hprems]. exists (map (fun tp => (Integrate intersect (fst tp), snd tp)) prems). intros pl pr. split; intros H.
inversion H; subst. apply Hprems in H0. apply in_map_iff. exists (tl0, pr); split; [reflexivity | assumption].
apply in_map_iff in H. destruct H as [[tlx trx] [Heq HIn]]. inversion Heq; subst. constructor. apply Hprems. assumption.
intros ll lr r tlx trx Hprem. inversion Hprem; subst. split.
apply m_lit in H. left. apply Operators_Properties.clos_rt_t with (m tl0 trx); [apply MeasurePreservation|apply t_step; assumption].
apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
Qed.
If the LHS type is in DNF, uisub and ouisub are equivalent (uisub_ouisub).
This is a helper lemma for proving the equivalence of isub and oisub in oisub_isub
Lemma uisub_ouisub {R : Lit -> Lit -> Prop} : forall tl tr : T, SumOfProducts tl -> (uisub R tl tr <-> ouisub R tl tr).
intros tl tr; split; intros Hsub.
induction Hsub; repeat remove_eq_implications; try (repeat constructor; assumption).
induction H; try (constructor; assumption).
repeat constructor; assumption.
apply SumOfProducts_int in H. clear Hsub. pose proof (SOP_prod _ (ProductOfLiterals_int_l H)) as Hsub. apply IHHsub in Hsub. clear IHHsub. apply (oui_polr _ _ H). apply ProductOfLiterals_int_l in H. inversion Hsub; subst; try (inversion H; fail). induction H1; repeat remove_eq_implications; try (repeat constructor; assumption).
rename IHouisub_r2 into IHr. rename IHouisub_r1 into IHl. repeat (promotehyp IHl). repeat (promotehyp IHr). constructor; assumption.
rename IHouisub_r into IH. repeat (promotehyp IH). constructor; assumption.
rename IHouisub_r into IH. repeat (promotehyp IH). constructor; assumption.
apply SumOfProducts_int in H. clear Hsub. pose proof (SOP_prod _ (ProductOfLiterals_int_r H)) as Hsub. apply IHHsub in Hsub. clear IHHsub. apply (oui_polr _ _ H). apply ProductOfLiterals_int_r in H. inversion Hsub; subst; try (inversion H; fail). induction H1; repeat remove_eq_implications; try (repeat constructor; assumption).
rename IHouisub_r2 into IHr. rename IHouisub_r1 into IHl. repeat (promotehyp IHl). repeat (promotehyp IHr). constructor; assumption.
rename IHouisub_r into IH. repeat (promotehyp IH). constructor; assumption.
rename IHouisub_r into IH. repeat (promotehyp IH). constructor; assumption.
clear Hsub1 Hsub2. induction H; try (constructor; assumption).
apply ouisub_uni_l in IHHsub1. apply ouisub_uni_l in IHHsub2. constructor; [apply IHSumOfProducts1 | apply IHSumOfProducts2]; (apply IHHsub1 || apply IHHsub2).
apply oui_polr; [assumption|]. inversion IHHsub1; subst; try (inversion H; fail). inversion IHHsub2; subst; try (inversion H; fail). constructor; assumption.
clear Hsub. induction H; try (constructor; assumption).
apply ouisub_uni_l in IHHsub. constructor; [apply IHSumOfProducts1 | apply IHSumOfProducts2]; apply IHHsub.
apply oui_polr; [assumption|]. inversion IHHsub; subst; try (inversion H; fail). constructor; assumption.
clear Hsub. induction H; try (constructor; assumption).
apply ouisub_uni_l in IHHsub. constructor; [apply IHSumOfProducts1 | apply IHSumOfProducts2]; apply IHHsub.
apply oui_polr; [assumption|]. inversion IHHsub; subst; try (inversion H; fail). constructor; assumption.
constructor; [apply IHHsub1; apply SumOfProducts_uni_l in H | apply IHHsub2; apply SumOfProducts_uni_r in H]; assumption.
clear H. induction Hsub; try (constructor; assumption).
clear H. induction H0; try (constructor; assumption).
induction H; try (constructor; assumption).
Qed.
Ltac tac_oisub_isub_right := match goal with
| [IH : forall tp : T * T, progress_measure tp _ -> _, H : uisub (lsub _ (orsubf _)) ?tl ?tr |- uisub (lsub ?p (rsubf ?p)) ?tl ?tr] => change (uisub (lsub p (rsubf p)) (fst (tl, tr)) (snd (tl, tr))); apply IH; [solve_progress_measure | simpl; solve_SumOfProducts | apply H]
end.
Ltac tac_oisub_isub_left := match goal with
| [IH : forall tp : T * T, progress_measure tp _ -> _, H : uisub (lsub _ (rsubf _)) ?tl ?tr |- uisub (lsub ?p (orsubf ?p)) ?tl ?tr] => change (uisub (lsub p (orsubf p)) (fst (tl, tr)) (snd (tl, tr))); apply IH; [solve_progress_measure | simpl; solve_SumOfProducts | apply H]
end.
Lemma oisub_isub : forall tl tr : T, oisub tl tr <-> isub tl tr.
intros tl tr; split; intros Hsub.
unfold isub. unfold isub'. constructor. unfold oisub in Hsub. apply orsubf_ouisub in Hsub. assert (Hsop : SumOfProducts (Integrate intersect tl)) by (apply (Integrated_SumOfProducts intersected); apply IntegrateIntegrated_P; intros ls; apply IntersectorIntegrated). apply uisub_ouisub in Hsub; [|assumption]. revert Hsop Hsub. generalize (Integrate intersect tl). clear tl. intros tl. change (SumOfProducts (fst (tl, tr)) -> uisub (lsub (@IPremise) (orsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr)) -> uisub (lsub (@IPremise) (rsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr))). apply (well_founded_ind progress_measure_wf (fun tp : T * T => SumOfProducts (fst tp) -> uisub (lsub (@IPremise) (orsubf (@IPremise))) (fst tp) (snd tp) -> uisub (lsub (@IPremise) (rsubf (@IPremise))) (fst tp) (snd tp))); clear tl tr.
intros [tl tr] IH Hsop Hsub; simpl in *. inversion Hsub; subst; try (constructor; tac_oisub_isub_right; fail).
destruct H as [r Hprem]. apply ui_lit. apply Lsub with r. intros tl tr Hp. constructor. change (uisub (lsub (@IPremise) (rsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr))). apply IH.
destruct Hp as [tl tr Hp]. apply m_lit in Hp. left. apply Operators_Properties.clos_rt_t with (m tl tr); [apply MeasurePreservation|apply t_step; assumption].
destruct Hp as [tl tr Hp]. simpl. apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
apply uisub_ouisub.
destruct Hp as [tl tr Hp]. simpl. apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
apply orsubf_ouisub. apply Hprem. assumption.
unfold isub in Hsub. unfold isub' in Hsub. unfold oisub. constructor. apply rsubf_uisub in Hsub. assert (Hsop : SumOfProducts (Integrate intersect tl)) by (apply (Integrated_SumOfProducts intersected); apply IntegrateIntegrated_P; intros ls; apply IntersectorIntegrated). apply uisub_ouisub; [assumption|]. revert Hsop Hsub. generalize (Integrate intersect tl). clear tl. intros tl. change (SumOfProducts (fst (tl, tr)) -> uisub (lsub (@IPremise) (rsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr)) -> uisub (lsub (@IPremise) (orsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr))). apply (well_founded_ind progress_measure_wf (fun tp : T * T => SumOfProducts (fst tp) -> uisub (lsub (@IPremise) (rsubf (@IPremise))) (fst tp) (snd tp) -> uisub (lsub (@IPremise) (orsubf (@IPremise))) (fst tp) (snd tp))); clear tl tr.
intros [tl tr] IH Hsop Hsub; simpl in *. inversion Hsub; subst; try (constructor; tac_oisub_isub_left; fail).
destruct H as [r Hprem]. apply ui_lit. apply Lsub with r. intros tl tr Hp. constructor. apply uisub_ouisub.
destruct Hp as [tl tr Hp]. simpl. apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
change (uisub (lsub (@IPremise) (orsubf (@IPremise))) (fst (tl, tr)) (snd (tl, tr))). apply IH.
destruct Hp as [tl tr Hp]. apply m_lit in Hp. left. apply Operators_Properties.clos_rt_t with (m tl tr); [apply MeasurePreservation|apply t_step; assumption].
destruct Hp as [tl tr Hp]. simpl. apply Integrated_SumOfProducts with intersected. apply IntegrateIntegrated_P. intros ls. apply IntersectorIntegrated.
apply rsubf_uisub. apply Hprem. assumption.
Qed.
From the equivalence of oisub and isub, and the equivalence of isub and esub, it follows that oisub and esub are equivalent, too
Lemma oisub_esub : forall tl tr : T, oisub tl tr <-> esub tl tr.
intros tl tr. split; intros H.
apply isub_esub. apply oisub_isub; assumption.
apply oisub_isub; apply isub_esub; assumption.
Qed.
Actual MAIN THEOREM, Part 2: Optimized Decidability of Extended Subtyping
As oisub is decidable and equivalent to esub, esub is decidable.Theorem OptimizedDecidabilityOfExtendedSubtyping : forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
apply (dsuba_ext_dec oisub oisub_esub oisub_dec).
Qed.
End Integrated.
This page has been generated by coqdoc