(* == Programme Spécification Vérification *)
Require Import Arith.
Require Import List.

(* -- Un exemple: la fonction get_prefix *)
Fixpoint get_prefix {A:Set} (n:nat) (xs:list A) :=
  match n, xs with
      0, _ => nil
    | (S n), nil => nil
    | (S n), (cons x xs) => (cons x (get_prefix n xs))
  end.

(* -- La relation «est préfixe de»: trois variantes *)
(* .. Listes comme suites indicées *)
(* Rappel: *)
Fixpoint the_nth {A:Set} (i:nat) (xs:(list A)) : (option A) :=
  match i, xs with
    i, nil => None
  | 0, (cons x xs) => (Some x)
  | (S i), (cons x xs) => (the_nth i xs)
  end.

(* zs est préfixe de xs ssi pour tout i < length zs,
   zs[i] = xs[i] et (length zs) <= (length xs)
*)
Definition Is_prefix1 {A:Set} (zs xs:list A) : Prop :=
  (length zs <= length xs) /\
  forall (i:nat), (i < length zs) 
                  -> (the_nth i zs) = (the_nth i xs).

(* .. Le monoïde 
   zs est préfixe de xs ssi il exsist ys tq. xs = zs@ys
*)
Definition Is_prefix2 {A:Set} (zs xs : list A) : Prop :=
  exists (ys:list A), (app zs ys) = xs.

(* .. Prédicat inductif *)
Inductive Is_prefix {A:Set} : (list A) -> (list A) -> Prop :=
  is_prefix_nil : forall (xs:list A), (Is_prefix nil xs)
| is_prefix_cons : forall (a:A) (zs xs:list A),
                    (Is_prefix zs xs) -> (Is_prefix (cons a zs) (cons a xs)).

(* -- Equivalence des 3 définitions *)

(* .. Lemme auxilaire: si a1::zs est préfixe de a2::xs alors a1=a2 *)
Lemma Is_prefix1_hd :
  forall (A:Set) (a1 a2:A) (zs xs:list A),
    (Is_prefix1 (cons a1 zs) (cons a2 xs)) -> (a1 = a2).
Proof.
  intros.  
  unfold Is_prefix1  in H.
  elim H.
  intros.
  specialize H1 with (i:=0).
  simpl the_nth in H1. injection H1.
  - trivial.
  - simpl.
    auto with arith.
Qed.

(* .. Lemme auxiliaire: si a1::zs est préfixe de a2::xs 
      alors zs est préfixe de xs *)
Lemma Is_prefix1_tl :
  forall (A:Set) (a1 a2:A) (zs xs:list A),
    (Is_prefix1 (cons a1 zs) (cons a2 xs)) -> (Is_prefix1 zs xs).
Proof.
  unfold Is_prefix1.
  intros.
  elim H.
  intros.
  split.
  - simpl in H0.
    auto with arith.
  - intros.
    specialize (H1 (S i)).
    simpl in H1.    
    apply H1.
    auto with arith.
Qed.

(* .. Is_prefix1 -> Is_prefix2 *)
Lemma Is_prefix1_Is_prefix2 :
  forall (A:Set) (zs xs:list A), (Is_prefix1 zs xs) -> (Is_prefix2 zs xs).
Proof.
  induction zs.
  - intros.
    unfold Is_prefix2.
    exists xs.
    trivial.
  - destruct xs.
    + unfold Is_prefix1.
      intro.
      elim H. intros.
      inversion H0.
    + intros.
      rewrite Is_prefix1_hd with (a1:=a)(a2:=a0)(zs:=zs)(xs:=xs).
      * unfold Is_prefix2.
        elim IHzs with (xs:=xs).

          intros.
          exists x.
          simpl.
          rewrite H0.
          reflexivity.

          apply Is_prefix1_tl with (a1:=a)(a2:=a0).
          assumption.

      * assumption.
Qed.

(* .. Lemma auxiliaire: nil est toujours préfixe *)
Lemma Is_prefix1_nil :
  forall (A:Set)(xs:list A), (Is_prefix1 nil xs).
Proof.
  intros.
  unfold Is_prefix1.
  split.
  - simpl.
    auto with arith.
  - intros. simpl in H.
    inversion H.
Qed.

(* .. Is_prefix2 -> Is_prefix *)
Lemma Is_prefix2_Is_prefix :
  forall (A:Set) (zs xs:list A),
    (Is_prefix2 zs xs) -> (Is_prefix zs xs).
Proof.
  induction zs.
  - intros. apply is_prefix_nil.
  - intros.
    unfold Is_prefix2 in H.
    elim H. intros.
    destruct xs.
    + discriminate H0.
    + injection H0. intros. rewrite H2.
      apply is_prefix_cons.
      apply IHzs.
      unfold Is_prefix2.
      exists x.
      assumption.
Qed.
 
(* .. Is_prefix -> Is_prefix1 (zs[i]=xs[i]) *)
Lemma Is_prefix_Is_prefix1 :
  forall (A:Set)(zs xs:list A),
    (Is_prefix zs xs) -> (Is_prefix1 zs xs).
Proof.
  intros.
  unfold Is_prefix1.
  induction H. 
  - split.
    + auto with arith.
    + intros.
      inversion H.
  - elim IHIs_prefix. clear IHIs_prefix.
    intros.
    split.
    + simpl.
      auto with arith.
    + destruct i.
      * intro. simpl. trivial.
      * intro.
        simpl.
        apply H1.
        simpl in H2.
        auto with arith.
Qed.

(* -- Correction de get_prefix *)
(* .. Ppte1: get_prefix calcule un préfixe *)
Lemma Is_prefix_get_prefix :
  forall (A:Set) (n:nat) (xs:list A), (Is_prefix (get_prefix n xs) xs).
Proof.
  induction n.
  - intro. simpl. apply is_prefix_nil.
  - destruct xs.
    + simpl. apply is_prefix_nil.
    + simpl. apply is_prefix_cons.
      apply IHn.
Qed.

(* .. Ppte2: get_prefix calcule une liste de longueur n,
             si n est inférieure ou égale à la longueur de la liste *)
Lemma length_get_prefix :
  forall (A:Set) (n:nat) (xs:list A),
    (le n (length xs)) -> (length (get_prefix n xs)) = n.
Proof.
  induction n.
  - intros. simpl get_prefix. simpl length. trivial.
  - destruct xs.
    + simpl length.
      intro.
      inversion H.
    + simpl. intro.
      rewrite IHn.
      * reflexivity.
      * auto with arith.
Qed.

(* .. Correction de get_prefix *)
Theorem get_prefix_correct :
  forall (A:Set) (n:nat) (xs:list A),
    (n <= (length xs))
    -> (Is_prefix (get_prefix n xs) xs) /\ (length (get_prefix n xs)) = n.
  intros. split.
  - apply Is_prefix_get_prefix.
  - apply length_get_prefix. assumption.
Qed.

(* -- Complétude: get_prefix peut calculer tous les préfixes d'une liste
      si zs est préfixe de xs alors il existe n tel que zs=(get_préfix n xs) *)
Theorem get_prefix_complete :
  forall (A:Set) (zs xs:list A),
    (Is_prefix zs xs) -> exists (n:nat), zs = (get_prefix n xs).
Proof.
  intros. induction H.
  - exists 0.
    trivial.
  - elim IHIs_prefix. intros.
    exists (S x).
    simpl.
    rewrite H0.
    reflexivity.
Qed.

Lemma get_prefix_all : forall (A:Set) (n:nat) (xs:list A),
    (n > (length xs)) -> (get_prefix n xs) = xs.
Proof.
  induction n.
  - intros. inversion H.
  - destruct xs.
    + trivial.
    + intro. simpl.
      rewrite IHn.
      * trivial.
      * auto with arith.
Qed.