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