Set Implicit Arguments.

Require Import RelSub.
Require Import ListUtil.
Require Import ListRepeatFree.
Require Import Arith.
Require Import RelUtil.
Require Import LogicUtil.
Require Import ListShrink.
Require Import RelMidex.

Section S.

Variable A : Type.

Section Path.

Variable R : relation A.

Fixpoint is_path (x y : A) (l : list A) {struct l} : Prop :=
  match l with
    | nil ⇒ R x y
    | z::l' ⇒ R x z ∧ is_path z y l'
  end.

Lemma path_clos_trans : ∀ y l x,
  is_path x y l → clos_trans R x y.

Proof.
induction l; simpl; intros. constructor. assumption.
constructor 2 with a. constructor. tauto. apply IHl. tauto.
Qed.

Lemma path_app : ∀ y z l' l x,
  is_path x y l → is_path y z l' → is_path x z (l++y::l').

Proof.
induction l; simpl; intros. tauto. split. tauto. apply IHl; tauto.
Qed.

Lemma clos_trans_path : ∀ x y,
  clos_trans R x y → ∃ l, is_path x y l.

Proof.
intros. induction H. ∃ (nil : list A). simpl. assumption.
destruct IHclos_trans1. destruct IHclos_trans2. ∃ (x0++y::x1).
apply path_app; assumption.
Qed.

Lemma path_app_elim_right : ∀ y z l l' x,
  is_path x z (l++y::l') → is_path y z l'.

Proof.
induction l; simpl; intros. tauto. apply IHl with a. tauto.
Qed.

Lemma path_repeat_free_length :
  eq_midex A → ∀ y l x, is_path x y l →
    ∃ l', ¬In x l' ∧ ¬In y l' ∧ repeat_free l'
      ∧ length l'≤ length l ∧ incl l' l ∧ is_path x y l'.

Proof.
induction l; intros; simpl in H0. ∃ (nil : list A). simpl.
pose (incl_nil (nil : list A)). pose (le_O_n 0). tauto.
destruct (IHl a). tauto.
destruct (H y a). ∃ (nil : list A). simpl.
pose (le_O_n (S (length l))). pose (incl_nil (a::l)). rewrite H2. tauto.
destruct (In_midex H x x0). destruct (In_elim_right H x x0). assumption.
destruct H4. ∃ x2. split. tauto. split. intro. absurd (In y x0). tauto.
rewrite (proj1 H4). apply in_or_app. simpl. tauto. rewrite (proj1 H4) in H1.
split.
destruct (repeat_free_app_elim_right x1 (x::x2)). tauto. tauto.
split. rewrite (length_app x1 (x::x2)) in H1. simpl in H1|-* . omega. split.
apply incl_tran with (x::x2). apply incl_tl. apply incl_refl.
apply incl_tran with (x1++(x::x2)). apply incl_appr. apply incl_refl.
apply incl_tran with l.
tauto. apply incl_tl. apply incl_refl. apply path_app_elim_right with x1 a.
tauto.
destruct (H x a). ∃ x0. rewrite H4. simpl.
assert (length x0 ≤ S (length l)). omega.
assert (incl x0 (a :: l)). apply incl_tl. tauto. tauto. ∃ (a::x0). simpl.
assert (S (length x0) ≤ S (length l)). omega.
assert (incl (a :: x0) (a :: l)). apply incl_double_cons. tauto.
assert (a≠x). intro. rewrite H7 in H4. tauto.
assert (a≠y). intro. rewrite H8 in H2. tauto. tauto.
Qed.

Lemma path_restricted_incl : ∀ y l l' x,
  is_restricted R l → is_path x y l' → incl l' l.

Proof.
unfold is_restricted. induction l'; simpl; intros. intro. simpl. tauto.
apply incl_cons. pose (H x a). tauto. apply IHl' with a; tauto.
Qed.

Inductive bound_path (n : nat) : relation A :=
  | bp_intro : ∀ x y l,
    length l≤ n → is_path x y l → bound_path n x y.

Lemma bound_path_clos_trans : ∀ n,
  bound_path n << clos_trans R.

Proof.
repeat intro. inversion H. apply path_clos_trans with l. assumption.
Qed.

Lemma clos_trans_bound_path : eq_midex A → ∀ l,
  is_restricted R l → (clos_trans R) << (bound_path (length l)).

Proof.
do 6 intro. destruct (clos_trans_path H1).
destruct (path_repeat_free_length H y x0 x H2). apply bp_intro with x1.
apply repeat_free_incl_length. assumption. tauto.
apply path_restricted_incl with y x;tauto. tauto.
Qed.

Lemma bound_path_n_Sn : ∀ n x y,
  bound_path n x y → bound_path (S n) x y.

Proof.
intros. inversion H. apply bp_intro with l. apply le_trans with n. assumption.
apply le_n_Sn. assumption.
Qed.

Lemma bound_path_Sn_n_or_Rn : ∀ n x y,
  bound_path (S n) x y →
  bound_path n x y ∨ ∃ z : A, R x z ∧ bound_path n z y.

Proof.
intros. inversion H. destruct (le_le_S_dec (length l) n).
constructor. apply bp_intro with l; assumption. constructor 2.
destruct l. simpl in l0. pose (le_Sn_O n l0). tauto. ∃ a. simpl in H0, H1.
split. tauto. apply bp_intro with l. apply le_S_n. assumption. tauto.
Qed.

Lemma R_bound_path_n_Sn : ∀ x y z n,
  R x y → bound_path n y z → bound_path (S n) x z.

Proof.
intros. inversion H0. apply bp_intro with (y::l). simpl. apply le_n_S.
assumption.
simpl. tauto.
Qed.

End Path.

Lemma path_preserved : ∀ R R' y l x,
  R << R' → is_path R x y l → is_path R' x y l.

Proof.
induction l; repeat intro; simpl in H0 |- × . apply H. assumption.
split. pose (H x a). tauto. pose (IHl a). tauto.
Qed.

Lemma path_restriction : ∀ R y l x,
  is_path R x y l → is_path (restriction R (x::y::l)) x y l.

Proof.
unfold restriction. induction l; simpl; intros. tauto. split. tauto.
simpl in IHl.
apply path_preserved with (fun x0 y0 : A ⇒ (a = x0 ∨ y = x0 ∨ In x0 l) ∧
(a = y0 ∨ y = y0 ∨ In y0 l) ∧ R x0 y0). repeat intro. tauto.
apply IHl. tauto.
Qed.

End S.

Section S2.

Variable A : Type.
Variable eqdec : eq_dec A.
Variable R : relation A.

Lemma path_app_elim : ∀ l x y z m,
  is_path R x y (l ++ z :: m) → is_path R x z l ∧ is_path R z y m.

Proof.
induction l; simpl; intros. exact H. destruct H. ded (IHl _ _ _ _ H0).
intuition.
Qed.

Lemma sub_path : ∀ l x y x' y' l' m p,
  x :: l ++ y :: nil = m ++ x' :: l' ++ y' :: p →
  is_path R x y l → is_path R x' y' l'.

Proof.
induction l; simpl; intros.
destruct m; simpl in H.
injection H; intros. subst x'. destruct l'; simpl in H1.
injection H1; intros. subst y'. exact H0.
injection H1; intros. destruct l'; discriminate.
injection H; intros. destruct m; simpl in H1.
injection H1; intros. destruct l'; discriminate.
injection H1; intros. destruct m; discriminate.
destruct H0. destruct m; simpl in H.
injection H; intros. subst x'. destruct l'; simpl in H2; simpl in H.
injection H2; intros. subst a. exact H0.
simpl. injection H2; intros. subst a0. intuition.
apply (IHl a y a y' l' (@nil A) p). simpl. exact H2. exact H1.
injection H; intros. subst a0. eapply IHl. apply H2. exact H1.
Qed.

Lemma path_suffix : ∀ (y z : A) l' l'' (x : A),
  is_path R x y l' → suffix (z::l'') l' → is_path R z y l''.

Proof.
induction l'; intros. assert (rev (z :: l'')=nil). apply prefix_nil. hyp.
simpl in H1. symmetry in H1. pose (app_cons_not_nil (rev l'') nil z H1). tauto.
destruct (List.list_eq_dec eqdec (z :: l'')(a :: l')). inversion e. simpl in H.
tauto. simpl in H.
apply IHl' with a. tauto. apply suffix_smaller with a; assumption.
Qed.

Lemma path_cut : ∀ (y : A) l' (x : A),
  In x l' → is_path R x y l' → is_path R x y (tail(cut eqdec x l')).

Proof.
intros. apply path_suffix with l' x. assumption.
rewrite <- (cut_head eqdec x l' H). apply suffix_cut.
Qed.

Lemma path_cut_bis : ∀ l' (x y z : A),
  In z l' → R x z → is_path R z y l' → is_path R x y (cut eqdec z l').

Proof.
intros. rewrite (cut_head eqdec z l'). simpl.
assert (is_path R z y (tail (cut eqdec z l'))).
apply path_cut; assumption. destruct l'. pose (in_nil H).
contradiction. tauto. assumption.
Qed.

Lemma path_shrink : ∀ (y : A) l' (x : A),
  is_path R x y l' → is_path R x y (shrink eqdec l').

Proof.
induction l'; simpl; intros. assumption.
assert (is_path R a y (shrink eqdec l')).
apply IHl'; tauto. destruct (In_dec eqdec a (shrink eqdec l')).
apply path_cut_bis; tauto. simpl. tauto.
Qed.

Require Import Arith.

Section sub_Rel2.

Variable l : list A.

Lemma restricted_path_incl : is_restricted R l →
  ∀ m x y, is_path R x y m → incl (x :: m ++ y :: nil) l.

Proof.
induction m; simpl; intros.
ded (H _ _ H0). unfold is_restricted in H. unfold incl. simpl. intuition.
subst a. exact H2. subst a. exact H3.
destruct H0. apply incl_cons. ded (H _ _ H0). unfold is_restricted in H2.
intuition.
apply IHm. exact H1.
Qed.

Require Import ListOccur.

Notation occur := (occur eqdec).

Lemma long_path_occur : is_restricted R l →
  ∀ x y m, is_path R x y m → length m ≥ length l - 1 →
    ∃ z, occur z (x :: m ++ y :: nil) ≥ 2.

Proof.
intros. apply pigeon_hole with l. apply restricted_path_incl.
apply H. apply H0. simpl. rewrite length_app. simpl. omega.
Qed.

Lemma path_restriction_In_left : ∀ (x y : A) l',
is_path (restriction R l) x y l' → In x l.

Proof.
unfold restriction. intros; destruct l'; simpl in H; tauto.
Qed.

End sub_Rel2.

End S2.

Implicit Arguments path_app_elim [A R l x y z m].
Implicit Arguments restricted_path_incl [A R l m x y].