Require Import List.
Require Import Wf.
Require Import Relations.

Import ListNotations.

Section TD2_wf.



 (* Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y}).
  Variable R : A -> A -> Prop.
  Variable l: list A.
  Variable l': list A.*)


Inductive suffix_spec (A:Set) : list A -> list A -> Prop :=
 | suffix_nil : forall (l:list A), suffix_spec A l l
 | suffix_cons : forall (s l:list A) (a:A), suffix_spec A s l-> suffix_spec A s (a::l).

Hint Constructors suffix_spec : suffix.


Section demo_suffix.
Variable A : Set.
Variable a b c : A.

Goal suffix_spec A [] [].
auto with suffix.
Qed.

Goal suffix_spec A [] [a; b].
auto with suffix.
Qed.

Goal suffix_spec A [b; c] [a; b; c].
auto with suffix.
Qed.
End demo_suffix.

Lemma suffix_app_l : forall (X: Set) (xs ys: list X),
  suffix_spec X xs ys ->  exists ws, ys = ws ++ xs.
Proof.
intros X xs ys; induction ys as [|y ys IHys]; intros H; inversion_clear H as [| ? ? ? Hxsys ]; [exists []| exists []| ]; trivial.
 apply IHys in Hxsys as [zs Hzs].
 exists (y::zs).
 rewrite Hzs.
 trivial.
Qed.

Lemma suffix_app_r : forall (X: Set) (ws ys: list X), suffix_spec X ys (ws ++ ys) .
Proof.
intros.
induction ws; simpl; auto with suffix.
Qed.


Lemma suffix_nil_implies_nil : forall (A: Set) (xs : list A), suffix_spec A xs [] -> xs = [].
Proof.
induction xs.
auto with suffix.
intros H; inversion H.
Qed.

Lemma suffix_app_nil : forall (X: Set) (xs: list X), suffix_spec X [] xs .
Proof.
intros. induction xs; auto with suffix.
Qed.


Theorem suffix_app : forall (X: Set) (xs ys: list X), suffix_spec X xs ys <->  exists ws, ys = ws ++ xs.
Proof.
intros X xs ys.
split.
 - apply suffix_app_l.
 - intros [ws H].
   rewrite H.
   apply suffix_app_r.
Qed.

Hint Resolve suffix_nil_implies_nil suffix_app_l suffix_app_r suffix_app_nil : suffix.

Lemma suffix_strict_or_same : forall (A:Set) (xs:list A) (ys:list A) (y:A),
   suffix_spec A xs (y::ys) -> (suffix_spec A xs ys \/ xs = y::ys).
Proof.
intros.
inversion_clear H; auto.
Qed.

Theorem suffix_spec_antisymmetric : forall (A:Set), antisymmetric (list A) (suffix_spec A).
Proof.
unfold antisymmetric.
intros A xs ys Hxy Hyx.
apply (suffix_app_l A) in Hxy; destruct Hxy as [ws Hxy].
apply (suffix_app_l A) in Hyx; destruct Hyx as [ws' Hyx].
rewrite Hxy in Hyx.
assert (xs = [] ++ xs); auto.
rewrite H in Hyx at 1.
rewrite app_assoc in Hyx.
apply app_inv_tail in Hyx.
symmetry in Hyx.
apply app_eq_nil in Hyx.
destruct Hyx.
rewrite H1 in Hxy.
auto.
Qed.

Theorem suffix_spec_refl : forall (A:Set), reflexive (list A) (suffix_spec A).
Proof.
unfold reflexive.
auto with suffix.
Qed.

Theorem suffix_spec_trans : forall (A:Set), transitive (list A) (suffix_spec A).
Proof.
unfold transitive.
intros A xs ys zs Hxy Hyz.
apply (suffix_app_l A) in Hxy; destruct Hxy as [ws Hxy].
apply (suffix_app_l A) in Hyz; destruct Hyz as [ws' Hyz].
rewrite Hxy in Hyz.
rewrite app_assoc in Hyz.
rewrite Hyz.
apply suffix_app_r.
Qed.

Definition suffix (A:Set) (xs:list A) (ys:list A) := suffix_spec A xs ys /\ xs <> ys.

Theorem suffix_strict_trans :  forall (A:Set), transitive (list A) (suffix A).
Proof.
unfold transitive.
intros A xs ys zs [Hxy Hxyneq] [Hyz Hyzneq].
unfold suffix in *.
split.
- exact (suffix_spec_trans A xs ys zs Hxy Hyz).
- unfold not. intros.
  rewrite <- H in Hyz.
  assert (xs = ys).
  apply suffix_spec_antisymmetric; assumption.
  contradiction.
Qed.

Lemma strict_acc_lemma: forall (A:Set) (ns xs:list A), suffix A xs ns -> Acc (suffix A) xs.
Proof.
induction ns.
    - intros. destruct H.
      apply suffix_nil_implies_nil in H.
      contradiction.
    - intros ys Hys. apply Acc_intro. intros zs Hzs.
      apply IHns.

      destruct Hys.
      destruct Hzs.
      split.
      apply suffix_spec_trans with (ys); auto.
      inversion H.
      rewrite H4 in H0. exfalso. apply H0; auto. assumption.
      unfold not. intros.
      destruct (suffix_strict_or_same A ys ns a) ; auto.
      rewrite <- H3 in H4.
      apply H2.
      apply (suffix_spec_antisymmetric A zs ys H1 H4).
Defined.

Lemma cons_neq : forall (A:Set) (x:A) xs, xs <> x::xs.
Proof.
induction xs as [|x' xs IHxs]; intro H.
- apply (nil_cons H).
- injection H; intros.
  rewrite H1 in H0.
  apply (IHxs H0).
Qed.

Theorem suffix_wf (A:Set): well_founded (suffix A).
Proof.
unfold well_founded.
intro xs. induction xs as [|x xs].
- apply Acc_intro. intros.
  destruct H.
  apply suffix_nil_implies_nil in H.
  contradiction.
- intros.  apply (strict_acc_lemma A (x::x::xs)).
  split ; auto with suffix.  intro. injection H. intros.
  apply (cons_neq A x xs). trivial.
Defined.