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.
Import Relation_Operators.
Import List.
Import ListNotations.
Section UIType_Infra_Global.
Variable Lit : Type.
Notation T := (UIType Lit).
Fixpoint lits (t : T) : list Lit :=
match t with
| TLit l => [l]
| TTop => []
| TIsect tl tr => lits tl ++ lits tr
| TBot => []
| TUni tl tr => lits tl ++ lits tr
end.
End UIType_Infra_Global.
Arguments lits {Lit}.
Module UIType_Infrastructure (M_Traditional : Traditional).
Import M_Traditional.
Notation T := (UIType Lit).
Lemma rsubf_uisub {Premise : forall (l r : Lit), RRule l r -> T -> T -> Prop} {tl tr : T} : rsubf Premise tl tr -> uisub (lsub Premise (rsubf Premise)) tl tr.
intro tltr. inversion tltr. assumption.
Qed.
Inductive InType : T -> T -> Prop :=
| it_eq : forall t : T, InType t t
| it_uni_l : forall t tl tr : T, InType (TUni tl tr) t -> InType tl t
| it_uni_r : forall t tl tr : T, InType (TUni tl tr) t -> InType tr t
| it_isect_l : forall t tl tr : T, InType (TIsect tl tr) t -> InType tl t
| it_isect_r : forall t tl tr : T, InType (TIsect tl tr) t -> InType tr t
.
Lemma InType_trans : forall tl tm tr : T, InType tl tm -> InType tm tr -> InType tl tr.
intros tl tm tr Hlm. generalize dependent tr. induction Hlm; intros tr' Hmr.
assumption.
apply IHHlm in Hmr. apply it_uni_l in Hmr. assumption.
apply IHHlm in Hmr. apply it_uni_r in Hmr. assumption.
apply IHHlm in Hmr. apply it_isect_l in Hmr. assumption.
apply IHHlm in Hmr. apply it_isect_r in Hmr. assumption.
Qed.
Lemma InType_TUni : forall t tl tr : T, InType t (TUni tl tr) <-> t = (TUni tl tr) \/ InType t tl \/ InType t tr.
intros t tl tr; split; intros HIT.
remember (TUni tl tr) as tuni. generalize dependent tl. generalize dependent tr. induction HIT; intros tr' tl' Heq.
left. reflexivity.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst. inversion Heq'; subst. right. left. constructor.
apply it_uni_l in HIT'. right. left. assumption.
apply it_uni_l in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst. inversion Heq'; subst. right. right. constructor.
apply it_uni_r in HIT'. right. left. assumption.
apply it_uni_r in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst; inversion Heq'.
apply it_isect_l in HIT'. right. left. assumption.
apply it_isect_l in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst; inversion Heq'.
apply it_isect_r in HIT'. right. left. assumption.
apply it_isect_r in HIT'. right. right. assumption.
destruct HIT as [Heq | [Hl | Hr]].
subst. apply it_eq.
pose proof (it_uni_l _ _ _ (it_eq (TUni tl tr))). apply InType_trans with tl; assumption.
pose proof (it_uni_r _ _ _ (it_eq (TUni tl tr))). apply InType_trans with tr; assumption.
Qed.
Lemma InType_TIsect : forall t tl tr : T, InType t (TIsect tl tr) <-> t = (TIsect tl tr) \/ InType t tl \/ InType t tr.
intros t tl tr; split; intros HIT.
remember (TIsect tl tr) as tuni. generalize dependent tl. generalize dependent tr. induction HIT; intros tr' tl' Heq.
left. reflexivity.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst; inversion Heq'.
apply it_uni_l in HIT'. right. left. assumption.
apply it_uni_l in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst; inversion Heq'.
apply it_uni_r in HIT'. right. left. assumption.
apply it_uni_r in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst. inversion Heq'; subst. right. left. constructor.
apply it_isect_l in HIT'. right. left. assumption.
apply it_isect_l in HIT'. right. right. assumption.
pose proof (IHHIT _ _ Heq) as H. destruct H as [Heq' | [HIT' | HIT']].
subst. inversion Heq'; subst. right. right. constructor.
apply it_isect_r in HIT'. right. left. assumption.
apply it_isect_r in HIT'. right. right. assumption.
destruct HIT as [Heq | [Hl | Hr]].
subst. apply it_eq.
pose proof (it_isect_l _ _ _ (it_eq (TIsect tl tr))). apply InType_trans with tl; assumption.
pose proof (it_isect_r _ _ _ (it_eq (TIsect tl tr))). apply InType_trans with tr; assumption.
Qed.
Definition uirec (R : Lit -> Lit -> Prop) (tl tr : T) : Prop
:= ForallCrossPairs R (lits tl) (lits tr).
Lemma uirec_int_l : forall (P : Lit -> Lit -> Prop) (tl tr t' : T), uirec P (TIsect tl tr) t' -> uirec P tl t' /\ uirec P tr t'.
intros P t tl tr Huirec. apply ForallCrossPairs_app_l. assumption.
Qed.
Lemma uirec_int_r : forall (P : Lit -> Lit -> Prop) (t tl tr : T), uirec P t (TIsect tl tr) -> uirec P t tl /\ uirec P t tr.
intros P t tl tr Huirec. apply ForallCrossPairs_app_r. assumption.
Qed.
Lemma uirec_uni_l : forall (P : Lit -> Lit -> Prop) (tl tr t' : T), uirec P (TUni tl tr) t' -> uirec P tl t' /\ uirec P tr t'.
intros P t tl tr Huirec. apply ForallCrossPairs_app_l. assumption.
Qed.
Lemma uirec_uni_r : forall (P : Lit -> Lit -> Prop) (t tl tr : T), uirec P t (TUni tl tr) -> uirec P t tl /\ uirec P t tr.
intros P t tl tr Huirec. apply ForallCrossPairs_app_r. assumption.
Qed.
Ltac tac_uirec_uisub_uisub := match goal with
| [H : ?a |- ?a] => apply H
| [H : _ /\ _ |- _] => let H' := fresh H in destruct H as [H H']; tac_uirec_uisub_uisub
| [|- uisub _ _ _] => constructor; tac_uirec_uisub_uisub
| [H : uirec _ _ _ |- _] => unfold uirec in *; simpl in *; tac_uirec_uisub_uisub
| [H : ForallCrossPairs ?R [_] [_] |- _] => apply (ForallCrossPairs_singleton R) in H; tac_uirec_uisub_uisub
| [H : ForallCrossPairs ?R (_ ++ _) _ |- _] => apply ForallCrossPairs_app_l in H; tac_uirec_uisub_uisub
| [H : ForallCrossPairs ?R _ (_ ++ _) |- _] => apply ForallCrossPairs_app_r in H; tac_uirec_uisub_uisub
| [H : Forall _ [_] |- _] => apply Forall_singleton in H; tac_uirec_uisub_uisub
| [IH : forall ll lr, ?R ll lr -> ?R' ll lr -> ?R'' ll lr |- _] => apply IH; tac_uirec_uisub_uisub
| [H : ?a -> ?g |- ?g] => apply H; tac_uirec_uisub_uisub
end.
Lemma uirec_uisub_uisub : forall (R R' R'' : Lit -> Lit -> Prop) (tl tr : T), (forall ll lr : Lit, R ll lr -> R' ll lr -> R'' ll lr) -> uirec R tl tr -> uisub R' tl tr -> uisub R'' tl tr.
intros R R' R'' tl tr Himpl Hrec Hsub. induction Hsub; try tac_uirec_uisub_uisub.
Qed.
Lemma InType_lit_In_lits : forall (l : Lit) (t : T), In l (lits t) -> InType (TLit l) t.
intros l t HIn. induction t; simpl in *; try inversion HIn; subst; try (constructor; assumption); try contradiction.
apply in_app_or in HIn. apply InType_TUni. right. destruct HIn as [HIn | HIn]; [left; apply IHt1 | right; apply IHt2]; apply HIn.
apply in_app_or in HIn. apply InType_TIsect. right. destruct HIn as [HIn | HIn]; [left; apply IHt1 | right; apply IHt2]; apply HIn.
Qed.
Lemma uisub_int_r {R : Lit -> Lit -> Prop} {t tl tr : T} : uisub R t (TIsect tl tr) -> uisub R t tl /\ uisub R t tr.
intros Hsub. induction t; inversion Hsub; subst; try (split; try (constructor; assumption); assumption).
apply IHt1 in H1. apply IHt2 in H3. split; (constructor; [apply H1 | apply H3]).
apply IHt1 in H2. split; apply ui_int_ll; apply H2.
apply IHt2 in H2. split; apply ui_int_lr; apply H2.
Qed.
Lemma uisub_uni_l {R : Lit -> Lit -> Prop} {tl tr t : T} : uisub R (TUni tl tr) t -> uisub R tl t /\ uisub R tr t.
intros Hsub. induction t; inversion Hsub; subst; try (split; try (constructor; assumption); assumption).
apply IHt1 in H1. split; apply ui_uni_rl; apply H1.
apply IHt2 in H1. split; apply ui_uni_rr; apply H1.
apply IHt1 in H2. apply IHt2 in H3. split; (constructor; [apply H2 | apply H3]).
Qed.
Lemma uisub_top {R R' : Lit -> Lit -> Prop} (t t' : T) : uisub R TTop t -> uisub R' t' t.
intros Hsub. remember TTop as ttop. induction Hsub; subst; try inversion Heqttop; repeat remove_eq_implications; try (constructor; assumption).
Qed.
Lemma uisub_top_trans {R R' R'' : Lit -> Lit -> Prop} (t t' : T) : uisub R TTop t -> uisub R' t t' -> uisub R'' TTop t'.
intros Hsubl Hsubr. induction Hsubr; try (inversion Hsubl; subst; constructor; assumption).
apply uisub_int_r in Hsubl. apply IHHsubr. apply Hsubl.
apply uisub_int_r in Hsubl. apply IHHsubr. apply Hsubl.
constructor; [apply IHHsubr1 | apply IHHsubr2]; assumption.
apply ui_uni_rl; apply IHHsubr; assumption.
apply ui_uni_rr; apply IHHsubr; assumption.
inversion Hsubl; subst; [apply IHHsubr1 | apply IHHsubr2]; assumption.
Qed.
Lemma uisub_bot {R R' : Lit -> Lit -> Prop} (t t' : T) : uisub R t TBot -> uisub R' t t'.
intros Hsub. remember TBot as tbot. induction Hsub; subst; try inversion Heqtbot; repeat remove_eq_implications; try (constructor; assumption).
Qed.
Lemma uisub_bot_trans {R R' R'' : Lit -> Lit -> Prop} (t t' : T) : uisub R t TBot -> uisub R' t' t -> uisub R'' t' TBot.
intros Hsubl Hsubr. induction Hsubr; try (inversion Hsubl; subst; constructor; assumption).
apply ui_int_ll. apply IHHsubr. apply Hsubl.
apply ui_int_lr. apply IHHsubr. apply Hsubl.
inversion Hsubl; subst; [apply IHHsubr1 | apply IHHsubr2]; assumption.
inversion Hsubl; subst; apply IHHsubr; assumption.
inversion Hsubl; subst; apply IHHsubr; assumption.
constructor; [apply IHHsubr1 | apply IHHsubr2]; assumption.
Qed.
Lemma rsub_top : forall t : T, rsub TTop t -> forall t' : T, rsub t' t.
intros t Hsub t'. apply rsubf_uisub in Hsub. constructor. apply (uisub_top _ _ Hsub).
Qed.
Lemma rsub_bot : forall t : T, rsub t TBot -> forall t' : T, rsub t t'.
intros t Hsub t'. apply rsubf_uisub in Hsub. constructor. apply (uisub_bot _ _ Hsub).
Qed.
Lemma uisub_refl {R : Lit -> Lit -> Prop} (Hrefl: forall l : Lit, R l l) : forall t : T, uisub R t t.
induction t; try (constructor; assumption).
apply ui_uni_l; [apply ui_uni_rl | apply ui_uni_rr]; assumption.
apply ui_int_r; [apply ui_int_ll | apply ui_int_lr]; assumption.
constructor. apply Hrefl.
Qed.
Lemma lsub_refl {R : (forall {ll lr : Lit} (r : RRule ll lr), T -> T -> Prop) -> T -> T -> Prop} (Hrefl : forall t : T, R (@RPremise) t t) : forall l : Lit, lsub (@RPremise) (R (@RPremise)) l l.
intros l. pose proof (LiteralReflexivity l) as [r Hprem]. apply Lsub with r. intros tl tr Hp. apply Hprem in Hp. subst. apply Hrefl.
Qed.
Lemma rsubam_bind (A A' : T -> T -> Prop) : (forall tl tr : T, A tl tr -> rsubam (@RPremise) A' tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubam (@RPremise) A' tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
apply Himpl; assumption.
apply (ram_mono tl tl' tr' tr); assumption.
apply ram_lit with r. apply H0.
Qed.
Lemma rsubam_mono (A A' : T -> T -> Prop) : (forall tl tr : T, A tl tr -> A' tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubam (@RPremise) A' tl tr.
intros aa'. apply rsubam_bind. intros tl tr a. apply ram_assumption. apply aa'. assumption.
Qed.
Lemma uisub_mono : forall (A A' : Lit -> Lit -> Prop), (forall (ll lr : Lit), A ll lr -> A' ll lr) -> forall tl tr : T, uisub A tl tr -> uisub A' tl tr.
intros A A' Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
constructor. apply Himpl. assumption.
Qed.
Lemma lsub_mono : forall {Rule : Lit -> Lit -> Type} (Premise : forall (ll lr : Lit), Rule ll lr -> T -> T -> Prop) (R R' : T -> T -> Prop), (forall (tl tr : T), R tl tr -> R' tl tr) -> forall ll lr : Lit, lsub Premise R ll lr -> lsub Premise R' ll lr.
intros Rule Premise R R' Himpl ll lr Hsub. inversion Hsub. apply Lsub with r. intros tl tr Hprem. apply Himpl. apply H. assumption.
Qed.
Lemma dsuba_mono {A A' : T -> T -> Prop} : (forall tl tr : T, A tl tr -> A' tl tr) -> forall tl tr : T, dsuba (@DPremise) A tl tr -> dsuba (@DPremise) A' tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
apply dsuba_trans with tm; assumption.
apply dsuba_assume. apply Himpl; assumption.
apply dsuba_lit with r. assumption.
Qed.
Lemma dsuba_dsubf {A : T -> T -> Prop} : (forall tl tr : T, A tl tr -> dsub tl tr) -> forall tl tr : T, dsuba (@DPremise) A tl tr -> dsub tl tr.
intros Himpl tl tr Hsub. induction Hsub; try (constructor; assumption).
apply dsuba_trans with tm; assumption.
apply Himpl. assumption.
apply dsuba_lit with r; assumption.
Qed.
End UIType_Infrastructure.
This page has been generated by coqdoc