(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* FIFO *)

(*relatif aux files d'attente*)

Require Export bibli.

Unset Standard Proposition Elimination Names.

Section DEF_FIFO.

(* definition d'une file d'attente comme d'une liste avec un acces a
chaque extremite *)

Variable data : Set.

Inductive queue : Set :=
  | empty : queue
  | input : data -> queue -> queue.
	
Inductive exc : Set :=
  | value : data -> exc
  | error : exc.
	
Definition last (q : queue) :=
  match q with
  | empty => error
  | input d _ => value d
  end.

Fixpoint first (q : queue) : exc :=
  match q with
  | empty => error
  | input d q' =>
      match q' with
      | empty => value d
      | input _ _ => first q'
      end
  end.
	
Fixpoint first_out (q : queue) : queue :=
  match q with
  | empty => empty
  | input d q' =>
      match q' with
      | empty => empty
      | input _ _ => input d (first_out q')
      end
  end.
	
Fixpoint In_queue (d : data) (q : queue) {struct q} : Prop :=
  match q with
  | empty => False
  | input d' q' => d = d' \/ In_queue d q'
  end.
	
Lemma not_in_empty : forall d : data, ~ In_queue d empty.
Proof.
(* Goal: forall d : data, not (In_queue d empty) *)
 intros; red in |- *; simpl in |- *; trivial.
Qed.

(* lorsque l'egalite est decidable, on peut compter le nombre
d'occurence d'un element dans la liste *)

Hypothesis eq_data_dec : eq_dec data.

Fixpoint card (d : data) (q : queue) {struct q} : Z :=
  match q with
  | empty => 0%Z
  | input d' q' =>
      if eq_data_dec d d'
      then (card d q' + 1)%Z
      else card d q'
  end.

Lemma card_pos : forall (d : data) (q : queue), (card d q >= 0)%Z.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : @eq (exc data) (first data q) (value data d)), In_queue data d q *)
 simple induction q; simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq (exc data) (first data (input data d1 q1)) (value data d) *)
(* Goal: @eq data d d *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 omega.

(* Goal: @eq Z (Z.add (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq (exc data) (first data (input data d1 q1)) (value data d) *)
(* Goal: @eq data d d *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 intros; case (eq_data_dec d d0); intros; omega.
Qed.

Lemma card_strct_pos :
 forall (d : data) (q : queue), In_queue d q -> (card d q > 0)%Z.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : @eq (exc data) (first data q) (value data d)), In_queue data d q *)
 simple induction q; simpl in |- *.
(* Goal: In_queue data m q2 *)
(* Goal: In_queue data m q2 *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : or (In_queue data m q) (In_queue data m q2)), In_queue data m (append data q q2)) (q2 : queue data) (_ : or (In_queue data m (input data d q)) (In_queue data m q2)), In_queue data m (append data (input data d q) q2) *)
 contradiction.

(* Goal: forall (d0 : data) (q : queue) (_ : forall _ : In_queue d q, Z.gt (card d q) Z0) (_ : or (@eq data d d0) (In_queue d q)), Z.gt (if eq_data_dec d d0 then Z.add (card d q) (Zpos xH) else card d q) Z0 *)
 intros; case (eq_data_dec d d0); intro.
(* Goal: @eq Z (Z.add (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq (exc data) (first data (input data d1 q1)) (value data d) *)
(* Goal: @eq data d d *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 generalize (card_pos d q0); omega.

(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
 elim H0; intro.
(* Goal: Z.gt (card d q0) Z0 *)
(* Goal: Z.gt (card d q0) Z0 *)
 absurd (d = d0); trivial.

(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 auto.
Qed.

Lemma card_null :
 forall (d : data) (q : queue), ~ In_queue d q -> card d q = 0%Z.
Proof.
(* Goal: forall (d : data) (q : queue) (_ : not (In_queue d q)), @eq Z (card d q) Z0 *)
 simple induction q; simpl in |- *; intros.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.

(* Goal: @eq Z (if eq_data_dec d d0 then Z.add (card d q0) (Zpos xH) else card d q0) Z0 *)
 case (eq_data_dec d d0); intro.
(* Goal: @eq Z (Z.add (card d q0) (Zpos xH)) Z0 *)
(* Goal: @eq Z (card d q0) Z0 *)
 absurd (d = d0).
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 red in |- *; intro; elim H0; auto.

(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.

(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 apply H; red in |- *; intro; elim H0; auto.
Qed.



End DEF_FIFO.

Section BELONG.

(* quelques lemmes sur des considerations plus dynamiques, l'existence
d'un element dans la liste apres ajout ou retrait d'un element *)

Variable data : Set.

Lemma first_in :
 forall (d : data) (q : queue data),
 first data q = value data d -> In_queue data d q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : @eq (exc data) (first data q) (value data d)), In_queue data d q *)
 simple induction q; simpl in |- *.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), False *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), In_queue data d q) (_ : @eq (exc data) match q with | @empty _ => value data d0 | @input _ d q0 => first data q end (value data d)), or (@eq data d d0) (In_queue data d q) *)
 intros H; discriminate H.

(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), In_queue data d q) (_ : @eq (exc data) match q with | @empty _ => value data d0 | @input _ d q0 => first data q end (value data d)), or (@eq data d d0) (In_queue data d q) *)
 intros d0 q0; case q0; intros.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 inversion H0; auto.

(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 right; apply H; auto.
Qed.

Lemma in_q_input :
 forall (d' d : data) (q : queue data),
 d <> d' -> In_queue data d (input data d' q) -> In_queue data d q.
Proof.
(* Goal: forall (d' d : data) (q : queue data) (_ : not (@eq data d d')) (_ : In_queue data d (input data d' q)), In_queue data d q *)
 intros; elim H0.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 intro; absurd (d = d'); auto.

(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.
Qed.

Lemma not_in_q_input :
 forall (data : Set) (d' d : data) (q : queue data),
 d <> d' -> ~ In_queue data d (input data d' q) -> ~ In_queue data d q.
Proof.
(* Goal: forall (data : Set) (d' d : data) (q : queue data) (_ : not (@eq data d d')) (_ : not (In_queue data d (input data d' q))), not (In_queue data d q) *)
  intros data0 d' d q H H0.
(* Goal: not (In_queue data0 d q) *)
  generalize H0.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
Qed.
		

Lemma in_q_output :
 forall (d : data) (q : queue data),
 In_queue data d (first_out data q) -> In_queue data d q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : not (@eq (exc data) (first data q) (value data d))), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q) *)
 simple induction q.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 simpl in |- *; trivial.

(* Goal: forall (d0 : data0) (q : queue data0) (_ : forall _ : not (In_queue data0 d q), not (In_queue data0 d (first_out data0 q))) (_ : not (In_queue data0 d (input data0 d0 q))), not (In_queue data0 d (first_out data0 (input data0 d0 q))) *)
 intros d0 q0; case q0; simpl in |- *; intros.
(* Goal: In_queue data m q2 *)
(* Goal: In_queue data m q2 *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : or (In_queue data m q) (In_queue data m q2)), In_queue data m (append data q q2)) (q2 : queue data) (_ : or (In_queue data m (input data d q)) (In_queue data m q2)), In_queue data m (append data (input data d q) q2) *)
 contradiction.

(* Goal: or (@eq data d d0) (or (@eq data d d1) (In_queue data d q1)) *)
 elim H0; clear H0; intros.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 auto.

(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 right; apply H; auto.
Qed.

Lemma not_in_q_output :
 forall (data : Set) (d : data) (q : queue data),
 ~ In_queue data d q -> ~ In_queue data d (first_out data q).
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : not (@eq (exc data) (first data q) (value data d))), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q) *)
  simple induction q.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  simpl in |- *; trivial.
(* Goal: forall (d0 : data0) (q : queue data0) (_ : forall _ : not (In_queue data0 d q), not (In_queue data0 d (first_out data0 q))) (_ : not (In_queue data0 d (input data0 d0 q))), not (In_queue data0 d (first_out data0 (input data0 d0 q))) *)
  intros d0 q0; case q0; simpl in |- *; intros.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
Qed.

Hypothesis eq_data_dec : eq_dec data.

Lemma equality_from_queue_membership :
 forall (x y : data) (q : queue data),
 In_queue data y q -> ~ In_queue data x q -> x <> y.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : not (@eq (exc data) (first data q) (value data d))), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q) *)
  simple induction q.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
(* Goal: forall (d : data) (q : queue data) (_ : forall (_ : In_queue data y q) (_ : not (In_queue data x q)), not (@eq data x y)) (_ : In_queue data y (input data d q)) (_ : not (In_queue data x (input data d q))), not (@eq data x y) *)
  intros d q' H.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
  case (eq_data_dec y d).
(* Goal: forall (_ : @eq data y d) (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
(* Goal: forall (_ : not (@eq data y d)) (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
  intro e.
(* Goal: forall (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
(* Goal: forall (_ : not (@eq data y d)) (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
  rewrite e.
(* Goal: forall (_ : or (@eq data d d) (In_queue data d q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x d) *)
(* Goal: forall (_ : not (@eq data y d)) (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
  intro H0.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
  
(* Goal: forall (_ : not (@eq data y d)) (_ : or (@eq data y d) (In_queue data y q')) (_ : not (or (@eq data x d) (In_queue data x q'))), not (@eq data x y) *)
  intros n H0 H1.
(* Goal: In_queue data m (append data q q2) *)
  apply H.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
  
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
Qed.


End BELONG.


Section MORE_NOT_INQ.

Variable data : Set.

Hypothesis eq_data_dec : eq_dec data.


Lemma not_in_q_input2 :
 forall (d' d : data) (q : queue data),
 ~ In_queue data d (input data d' q) -> ~ In_queue data d q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
  simpl in |- *; intros.
(* Goal: not (In_queue data d q) *)
  case (eq_data_dec d d'); intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  elim H; auto.
  
(* Goal: not (In_queue data d q) *)
  unfold not in |- *; intro; elim H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.
		

End MORE_NOT_INQ.



Section OCCUR.

(* considerations dynamiques sur l'evolution du nombre d'occurence
d'un element dans la liste apres ajout ou retrait *)

Variable data : Set.

Hypothesis eq_data_dec : eq_dec data.

Lemma input_S_card :
 forall (d d' : data) (q : queue data),
 d = d' ->
 card data eq_data_dec d (input data d' q) =
 (card data eq_data_dec d q + 1)%Z.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
 intros; simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 rewrite H; rewrite case_eq; trivial.
Qed.

Lemma input_diff_card :
 forall (d d' : data) (q : queue data),
 d <> d' ->
 card data eq_data_dec d (input data d' q) = card data eq_data_dec d q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
 intros; simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 rewrite case_ineq; trivial.
Qed.

Lemma firstout_pred_card :
 forall (d : data) (q : queue data),
 first data q = value data d ->
 card data eq_data_dec d (first_out data q) =
 (card data eq_data_dec d q - 1)%Z.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : not (@eq (exc data) (first data q) (value data d))), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q) *)
 simple induction q.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), False *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), In_queue data d q) (_ : @eq (exc data) match q with | @empty _ => value data d0 | @input _ d q0 => first data q end (value data d)), or (@eq data d d0) (In_queue data d q) *)
 simpl in |- *; intros H; discriminate H.

(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq Z (card data eq_data_dec d (first_out data q)) (Z.sub (card data eq_data_dec d q) (Zpos xH))) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq Z (card data eq_data_dec d (first_out data (input data d0 q))) (Z.sub (card data eq_data_dec d (input data d0 q)) (Zpos xH)) *)
 simpl in |- *; intros d0 q0; case q0.
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq Z (card data eq_data_dec d (first_out data (input data d1 q))) (Z.sub (card data eq_data_dec d (input data d1 q)) (Zpos xH))) (_ : @eq (exc data) (first data (input data d1 q)) (value data d)), @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q)))) (Z.sub (if eq_data_dec d d0 then Z.add (card data eq_data_dec d (input data d1 q)) (Zpos xH) else card data eq_data_dec d (input data d1 q)) (Zpos xH)) *)
 case (eq_data_dec d d0); intros.
(* Goal: @eq Z (Z.add (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq (exc data) (first data (input data d1 q1)) (value data d) *)
(* Goal: @eq data d d *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 simpl in |- *; omega.

(* Goal: @eq Z (card data eq_data_dec d (empty data)) (Z.sub (card data eq_data_dec d (empty data)) (Zpos xH)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq Z (card data eq_data_dec d (first_out data (input data d1 q))) (Z.sub (card data eq_data_dec d (input data d1 q)) (Zpos xH))) (_ : @eq (exc data) (first data (input data d1 q)) (value data d)), @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q)))) (Z.sub (if eq_data_dec d d0 then Z.add (card data eq_data_dec d (input data d1 q)) (Zpos xH) else card data eq_data_dec d (input data d1 q)) (Zpos xH)) *)
 injection H0; intros.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 absurd (d0 = d); auto.

(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq Z (card data eq_data_dec d (first_out data (input data d1 q))) (Z.sub (card data eq_data_dec d (input data d1 q)) (Zpos xH))) (_ : @eq (exc data) (first data (input data d1 q)) (value data d)), @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q)))) (Z.sub (if eq_data_dec d d0 then Z.add (card data eq_data_dec d (input data d1 q)) (Zpos xH) else card data eq_data_dec d (input data d1 q)) (Zpos xH)) *)
 case (eq_data_dec d d0); intros.
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 rewrite <- e; rewrite input_S_card.
(* Goal: @eq (queue data) (input data d0 (append (first_out data (input data d1 q)) (input data d (empty data)))) (input data d0 (input data d1 q)) *)
 rewrite H.
(* Goal: @eq Z (Z.add (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) (Z.sub (Z.add (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) (Zpos xH)) *)
(* Goal: @eq (exc data) (first data (input data d1 q1)) (value data d) *)
(* Goal: @eq data d d *)
(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 omega.
 
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.

(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.

(* Goal: @eq Z (card data eq_data_dec d (input data d0 (first_out data (input data d1 q1)))) (Z.sub (card data eq_data_dec d (input data d1 q1)) (Zpos xH)) *)
 rewrite input_diff_card.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 apply H; trivial.

(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.
Qed.

Lemma firstout_diff_card :
 forall (d : data) (q : queue data),
 first data q <> value data d ->
 card data eq_data_dec d (first_out data q) = card data eq_data_dec d q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : not (@eq (exc data) (first data q) (value data d))), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q) *)
 simple induction q.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 auto.

(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : not (@eq (exc data) (first data q) (value data d)), @eq Z (card data eq_data_dec d (first_out data q)) (card data eq_data_dec d q)) (_ : not (@eq (exc data) (first data (input data d0 q)) (value data d))), @eq Z (card data eq_data_dec d (first_out data (input data d0 q))) (card data eq_data_dec d (input data d0 q)) *)
 intros d0 q0; case q0.
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
 simpl in |- *; intros.
(* Goal: @eq Z Z0 (if eq_data_dec d d0 then Zpos xH else Z0) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : not (@eq (exc data) (first data (input data d1 q)) (value data d)), @eq Z (card data eq_data_dec d (first_out data (input data d1 q))) (card data eq_data_dec d (input data d1 q))) (_ : not (@eq (exc data) (first data (input data d0 (input data d1 q))) (value data d))), @eq Z (card data eq_data_dec d (first_out data (input data d0 (input data d1 q)))) (card data eq_data_dec d (input data d0 (input data d1 q))) *)
 rewrite case_ineq.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 trivial.

(* Goal: not (@eq data d d0) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : not (@eq (exc data) (first data (input data d1 q)) (value data d)), @eq Z (card data eq_data_dec d (first_out data (input data d1 q))) (card data eq_data_dec d (input data d1 q))) (_ : not (@eq (exc data) (first data (input data d0 (input data d1 q))) (value data d))), @eq Z (card data eq_data_dec d (first_out data (input data d0 (input data d1 q)))) (card data eq_data_dec d (input data d0 (input data d1 q))) *)
 red in |- *; intro; elim H0.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
 rewrite H1; trivial.

(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
 simpl in |- *; intros.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 rewrite H; auto.
Qed.

End OCCUR.

Section APPEND.

Variable data : Set.

Fixpoint append (q : queue data) : queue data -> queue data :=
  fun q2 : queue data =>
  match q with
  | empty => q2
  | input d q' => input data d (append q' q2)
  end.

Lemma append_nil1 : forall q : queue data, append (empty data) q = q.
Proof.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
Qed.

Lemma append_nil2 : forall q : queue data, append q (empty data) = q.
Proof.
(* Goal: forall q : queue data, @eq (queue data) (append q (empty data)) q *)
  intro q.
(* Goal: forall _ : @eq (exc data) (first data q) (value data d), @eq E match q with | @empty _ => x | @input _ d q => y end y *)
  elim q.
(* Goal: @eq (queue data) (append (empty data) (empty data)) (empty data) *)
(* Goal: forall (d : data) (q : queue data) (_ : @eq (queue data) (append q (empty data)) q), @eq (queue data) (append (input data d q) (empty data)) (input data d q) *)
  apply append_nil1.
(* Goal: forall (d : data) (q : queue data) (_ : @eq (queue data) (append q (empty data)) q), @eq (queue data) (append (input data d q) (empty data)) (input data d q) *)
  intros d q0 H.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d0 (append (first_out data (input data d1 q)) (input data d (empty data)))) (input data d0 (input data d1 q)) *)
  rewrite H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.

Lemma input_append :
 forall (d : data) (q1 q2 : queue data),
 input data d (append q1 q2) = append (input data d q1) q2.
Proof.
(* Goal: forall (d : data) (q1 q2 : queue data), @eq (queue data) (input data d (append q1 q2)) (append (input data d q1) q2) *)
 intros d q1 q2.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
 simpl in |- *.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
 auto.
Qed.

Lemma append_assoc :
 forall q1 q2 q3 : queue data,
 append q1 (append q2 q3) = append (append q1 q2) q3.
Proof.
(* Goal: forall q1 q2 q3 : queue data, @eq (queue data) (append q1 (append q2 q3)) (append (append q1 q2) q3) *)
  intro q1.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall q2 q3 : queue data, @eq (queue data) (append (empty data) (append q2 q3)) (append (append (empty data) q2) q3) *)
(* Goal: forall (d : data) (q : queue data) (_ : forall q2 q3 : queue data, @eq (queue data) (append q (append q2 q3)) (append (append q q2) q3)) (q2 q3 : queue data), @eq (queue data) (append (input data d q) (append q2 q3)) (append (append (input data d q) q2) q3) *)
  intros q2 q3.
(* Goal: @eq (queue data) (first_out data (append (empty data) (input data d (empty data)))) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (queue data) (first_out data (append q (input data d (empty data)))) q), @eq (queue data) (first_out data (append (input data d0 q) (input data d (empty data)))) (input data d0 q) *)
  rewrite append_nil1.
(* Goal: @eq (queue data) (first_out data (append (empty data) (input data d (empty data)))) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (queue data) (first_out data (append q (input data d (empty data)))) q), @eq (queue data) (first_out data (append (input data d0 q) (input data d (empty data)))) (input data d0 q) *)
  rewrite append_nil1.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
(* Goal: forall (d : data) (q : queue data) (_ : forall q2 q3 : queue data, @eq (queue data) (append q (append q2 q3)) (append (append q q2) q3)) (q2 q3 : queue data), @eq (queue data) (append (input data d q) (append q2 q3)) (append (append (input data d q) q2) q3) *)
  intros d q H q2 q3.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d0 (append (first_out data (input data d1 q)) (input data d (empty data)))) (input data d0 (input data d1 q)) *)
  rewrite H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.


Lemma append_right_non_empty :
 forall (q1 q2 : queue data) (d : data),
 append q1 (input data d q2) <> empty data.
Proof.
(* Goal: forall (q1 q2 : queue data) (d : data), not (@eq (queue data) (append q1 (input data d q2)) (empty data)) *)
  intros q1 q2 d.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  discriminate.
  
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (exc data) (first data (append q (input data d (empty data)))) (value data d)), @eq (exc data) (first data (append (input data d0 q) (input data d (empty data)))) (value data d) *)
  intros d0 q H.
(* Goal: @eq (queue data) (append (input data d0 (first_out data (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  rewrite <- input_append.
(* Goal: @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  discriminate.
Qed.

Lemma case_append_right :
 forall (E : Set) (x y : E) (q1 q2 : queue data) (d : data),
 match append q1 (input data d q2) with
 | empty => x
 | input _ _ => y
 end = y. 
Proof.
(* Goal: forall (E : Set) (x y : E) (q1 q2 : queue data) (d : data), @eq E match append q1 (input data d q2) with | @empty _ => x | @input _ d0 q => y end y *)
  intros E x y q1 q2 d.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (exc data) (first data (append q (input data d (empty data)))) (value data d)), @eq (exc data) (first data (append (input data d0 q) (input data d (empty data)))) (value data d) *)
  intros d0 q H.
(* Goal: @eq E match append (input data d0 q) (input data d q2) with | @empty _ => x | @input _ d q => y end y *)
  rewrite <- (input_append d0 q (input data d q2)).
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
Qed.


Lemma case_first_value :
 forall (E : Set) (x y : E) (d : data) (q : queue data),
 first data q = value data d ->
 match q with
 | empty => x
 | input _ _ => y
 end = y. 
Proof.
(* Goal: forall (E : Set) (x y : E) (d : data) (q : queue data) (_ : @eq (exc data) (first data q) (value data d)), @eq E match q with | @empty _ => x | @input _ d0 q0 => y end y *)
  intro; intro; intro; intro; intro.
(* Goal: forall _ : @eq (exc data) (first data q) (value data d), @eq E match q with | @empty _ => x | @input _ d q => y end y *)
  elim q.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
(* Goal: @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  discriminate.
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq E match q with | @empty _ => x | @input _ d q0 => y end y) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq E y y *)
  intros d0 q0 H H0.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
Qed.


Lemma append_first_out :
 forall (q1 : queue data) (d : data),
 first_out data (append q1 (input data d (empty data))) = q1.
Proof.
(* Goal: forall (q1 : queue data) (d : data), @eq (exc data) (first data (append q1 (input data d (empty data)))) (value data d) *)
  intros q1 d.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: @eq (queue data) (first_out data (append (empty data) (input data d (empty data)))) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (queue data) (first_out data (append q (input data d (empty data)))) q), @eq (queue data) (first_out data (append (input data d0 q) (input data d (empty data)))) (input data d0 q) *)
  rewrite append_nil1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (exc data) (first data (append q (input data d (empty data)))) (value data d)), @eq (exc data) (first data (append (input data d0 q) (input data d (empty data)))) (value data d) *)
  intros d0 q H.
(* Goal: @eq (queue data) (append (input data d0 (first_out data (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  rewrite <- input_append.
(* Goal: @eq (queue data) (first_out data (input data d0 (input data d1 q))) (input data d0 (first_out data (input data d1 q))) *)
  unfold first_out in |- *.
(* Goal: @eq (exc data) match append q (input data d (empty data)) with | @empty _ => value data d0 | @input _ d0 q0 => (fix first (q : queue data) : exc data := match q with | @empty _ => error data | @input _ d (@empty _ as q') => value data d | @input _ d (@input _ d1 q1 as q') => first q' end) (append q (input data d (empty data))) end (value data d) *)
  rewrite case_append_right.
(* Goal: @eq (queue data) (input data d0 ((fix first_out (q : queue data) : queue data := match q with | @empty _ => empty data | @input _ d (@empty _ as q') => empty data | @input _ d (@input _ d0 q0 as q') => input data d (first_out q') end) (append q (input data d (empty data))))) (input data d0 q) *)
  unfold first_out in H.
(* Goal: @eq (queue data) (input data d0 (append (first_out data (input data d1 q)) (input data d (empty data)))) (input data d0 (input data d1 q)) *)
  rewrite H.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
Qed.


Lemma append_first :
 forall (q1 : queue data) (d : data),
 first data (append q1 (input data d (empty data))) = value data d.
Proof.
(* Goal: forall (q1 : queue data) (d : data), @eq (exc data) (first data (append q1 (input data d (empty data)))) (value data d) *)
  intros q1 d.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
(* Goal: forall (d0 : data) (q : queue data) (_ : @eq (exc data) (first data (append q (input data d (empty data)))) (value data d)), @eq (exc data) (first data (append (input data d0 q) (input data d (empty data)))) (value data d) *)
  intros d0 q H.
(* Goal: @eq (queue data) (append (input data d0 (first_out data (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  rewrite <- input_append.
(* Goal: @eq (exc data) (first data (input data d0 (input data d1 q))) (first data (input data d1 q)) *)
  unfold first in |- *.
(* Goal: @eq (exc data) match append q (input data d (empty data)) with | @empty _ => value data d0 | @input _ d0 q0 => (fix first (q : queue data) : exc data := match q with | @empty _ => error data | @input _ d (@empty _ as q') => value data d | @input _ d (@input _ d1 q1 as q') => first q' end) (append q (input data d (empty data))) end (value data d) *)
  rewrite case_append_right.
(* Goal: @eq (exc data) ((fix first (q : queue data) : exc data := match q with | @empty _ => error data | @input _ d (@empty _ as q') => value data d | @input _ d (@input _ d0 q0 as q') => first q' end) (append q (input data d (empty data)))) (value data d) *)
  unfold first in H.
(* Goal: In_queue data m (append data q q2) *)
  apply H.
Qed.

Lemma first_out_input :
 forall (d0 d1 : data) (q : queue data),
 first_out data (input data d0 (input data d1 q)) =
 input data d0 (first_out data (input data d1 q)).
Proof.
(* Goal: forall (d0 d1 : data) (q : queue data), @eq (exc data) (first data (input data d0 (input data d1 q))) (first data (input data d1 q)) *)
  intros d0 d1 q.
(* Goal: @eq (queue data) (first_out data (input data d0 (input data d1 q))) (input data d0 (first_out data (input data d1 q))) *)
  unfold first_out in |- *.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.

Lemma first_input :
 forall (d0 d1 : data) (q : queue data),
 first data (input data d0 (input data d1 q)) = first data (input data d1 q).
Proof.
(* Goal: forall (d0 d1 : data) (q : queue data), @eq (exc data) (first data (input data d0 (input data d1 q))) (first data (input data d1 q)) *)
  intros d0 d1 q.
(* Goal: @eq (exc data) (first data (input data d0 (input data d1 q))) (first data (input data d1 q)) *)
  unfold first in |- *.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.

(* This one was a nightmare!! *)

Lemma append_first_out2 :
 forall (d : data) (q1 : queue data),
 first data q1 = value data d ->
 append (first_out data q1) (input data d (empty data)) = q1.
Proof.
(* Goal: forall (d : data) (q1 : queue data) (_ : @eq (exc data) (first data q1) (value data d)), @eq (queue data) (append (first_out data q1) (input data d (empty data))) q1 *)
  intro; intro.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall _ : @eq (exc data) (error data) (value data d), @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intuition.
(* Goal: @eq (queue data) (input data d (empty data)) (empty data) *)
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  discriminate.
  
(* Goal: forall (d0 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data q) (value data d), @eq (queue data) (append (first_out data q) (input data d (empty data))) q) (_ : @eq (exc data) (first data (input data d0 q)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q)) (input data d (empty data))) (input data d0 q) *)
  intros d0 q0.
(* Goal: forall (_ : forall _ : @eq (exc data) (first data q0) (value data d), @eq (queue data) (append (first_out data q0) (input data d (empty data))) q0) (_ : @eq (exc data) (first data (input data d0 q0)) (value data d)), @eq (queue data) (append (first_out data (input data d0 q0)) (input data d (empty data))) (input data d0 q0) *)
  case q0.
(* Goal: forall (_ : forall _ : @eq (exc data) (first data (empty data)) (value data d), @eq (queue data) (append (first_out data (empty data)) (input data d (empty data))) (empty data)) (_ : @eq (exc data) (first data (input data d0 (empty data))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (empty data))) (input data d (empty data))) (input data d0 (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  intros H H0.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d0 (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  unfold first in H0.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d0 (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  inversion H0.
(* Goal: @eq (queue data) (input data d (empty data)) (input data d (empty data)) *)
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  trivial.
  
(* Goal: forall (d1 : data) (q : queue data) (_ : forall _ : @eq (exc data) (first data (input data d1 q)) (value data d), @eq (queue data) (append (first_out data (input data d1 q)) (input data d (empty data))) (input data d1 q)) (_ : @eq (exc data) (first data (input data d0 (input data d1 q))) (value data d)), @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  intros d1 q H H0.
(* Goal: @eq (queue data) (append (first_out data (input data d0 (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  rewrite first_out_input.
(* Goal: @eq (queue data) (append (input data d0 (first_out data (input data d1 q))) (input data d (empty data))) (input data d0 (input data d1 q)) *)
  rewrite <- input_append.
(* Goal: @eq (queue data) (input data d0 (append (first_out data (input data d1 q)) (input data d (empty data)))) (input data d0 (input data d1 q)) *)
  rewrite H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: @eq (exc data) (first data (input data d1 q)) (value data d) *)
  rewrite <- (first_input d0 d1 q).
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.


End APPEND.

Section INQUEUE_APPEND.

Variable data : Set.


Lemma inqueue_append :
 forall (m : data) (q1 q2 : queue data),
 In_queue data m q1 \/ In_queue data m q2 ->
 In_queue data m (append data q1 q2).
Proof.
(* Goal: forall (m : data) (q1 q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  intros m q1.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (q2 : queue data) (_ : and (not False) (not (In_queue data m q2))), not (In_queue data m q2) *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
  intros q2 H.
(* Goal: In_queue data m q2 *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : or (In_queue data m q) (In_queue data m q2)), In_queue data m (append data q q2)) (q2 : queue data) (_ : or (In_queue data m (input data d q)) (In_queue data m q2)), In_queue data m (append data (input data d q) q2) *)
  elim H; intro.
(* Goal: In_queue data m q2 *)
(* Goal: In_queue data m q2 *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : or (In_queue data m q) (In_queue data m q2)), In_queue data m (append data q q2)) (q2 : queue data) (_ : or (In_queue data m (input data d q)) (In_queue data m q2)), In_queue data m (append data (input data d q) q2) *)
  contradiction.
  
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : or (In_queue data m q) (In_queue data m q2)), In_queue data m (append data q q2)) (q2 : queue data) (_ : or (or (@eq data m d) (In_queue data m q)) (In_queue data m q2)), or (@eq data m d) (In_queue data m (append data q q2)) *)
  intros d q H q2 H0.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  elim H0; intro.
(* Goal: or (@eq data m d) (In_queue data m (append data q q2)) *)
(* Goal: or (@eq data m d) (In_queue data m (append data q q2)) *)
  elim H1; intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  right.
(* Goal: In_queue data m (append data q q2) *)
  apply H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  right.
(* Goal: In_queue data m (append data q q2) *)
  apply H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.

Lemma not_inqueue_append :
 forall (m : data) (q1 q2 : queue data),
 ~ In_queue data m q1 /\ ~ In_queue data m q2 ->
 ~ In_queue data m (append data q1 q2).
Proof.
(* Goal: forall (m : data) (q1 q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  intros m q1.
(* Goal: forall (q2 : queue data) (_ : and (not (In_queue data m q1)) (not (In_queue data m q2))), not (In_queue data m (append data q1 q2)) *)
  elim q1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (q2 : queue data) (_ : and (not False) (not (In_queue data m q2))), not (In_queue data m q2) *)
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
  intros q2 H.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  decompose [and] H; auto.
  
(* Goal: forall (d : data) (q : queue data) (_ : forall (q2 : queue data) (_ : and (not (In_queue data m q)) (not (In_queue data m q2))), not (In_queue data m (append data q q2))) (q2 : queue data) (_ : and (not (In_queue data m (input data d q))) (not (In_queue data m q2))), not (In_queue data m (append data (input data d q) q2)) *)
  simpl in |- *; intros.
(* Goal: not (or (@eq data m d) (In_queue data m (append data q q2))) *)
  decompose [and] H0.
(* Goal: not (or (@eq data m d) (In_queue data m (append data q q2))) *)
  unfold not in |- *.
(* Goal: forall _ : or (@eq data m d) (In_queue data m (append data q q2)), False *)
  intro H1'.
(* Goal: False *)
  elim H1'; intro.
(* Goal: False *)
(* Goal: forall _ : In_queue data m q2, False *)
(* Goal: In_queue data m (append data q q2) *)
  elim H1.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: False *)
  unfold not in H.
(* Goal: False *)
  apply (H q2).
(* Goal: and (not (In_queue data m2 q3)) (not (or (@eq data m2 m1) (In_queue data m2 q4))) *)
  split.
(* Goal: forall _ : In_queue data m q, False *)
(* Goal: forall _ : In_queue data m q2, False *)
(* Goal: In_queue data m (append data q q2) *)
  intro H5.
(* Goal: False *)
(* Goal: forall _ : In_queue data m q2, False *)
(* Goal: In_queue data m (append data q q2) *)
  elim H1.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  intro; elim H2; auto.
  
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.

Lemma in_q_shuffle1 :
 forall (m1 m2 : data) (q3 q4 : queue data),
 In_queue data m2 (input data m1 (append data q3 q4)) ->
 In_queue data m2 (append data q3 (input data m1 q4)).
Proof.
(* Goal: forall (m1 m2 : data) (q3 q4 : queue data) (_ : not (In_queue data m2 (input data m1 (append data q3 q4)))), not (In_queue data m2 (append data q3 (input data m1 q4))) *)
  intros m1 m2 q3 q4 H.
(* Goal: In_queue data m2 (append data q3 q4) *)
  apply inqueue_append.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (In_queue data m2 q3) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  generalize H; simpl in |- *; intro.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  elim H0; intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (In_queue data m2 q3) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  generalize H1.
(* Goal: forall _ : In_queue data m2 (append data q3 (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  elim q3.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall _ : In_queue data m2 q4, or False (or (@eq data m2 m1) (In_queue data m2 q4)) *)
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q q4), or (In_queue data m2 q) (or (@eq data m2 m1) (In_queue data m2 q4))) (_ : In_queue data m2 (append data (input data d q) q4)), or (In_queue data m2 (input data d q)) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  intro H2.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q q4), or (In_queue data m2 q) (or (@eq data m2 m1) (In_queue data m2 q4))) (_ : or (@eq data m2 d) (In_queue data m2 (append data q q4))), or (or (@eq data m2 d) (In_queue data m2 q)) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  intros d q H2 H3.
(* Goal: or (or (@eq data m2 d) (In_queue data m2 q)) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  elim H3; intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (or (@eq data m2 d) (In_queue data m2 q)) (or (@eq data m2 m1) (In_queue data m2 q4)) *)
  generalize (H2 H4); intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  elim H5; intro; auto.
Qed.



Lemma not_in_q_shuffle1 :
 forall (m1 m2 : data) (q3 q4 : queue data),
 ~ In_queue data m2 (input data m1 (append data q3 q4)) ->
 ~ In_queue data m2 (append data q3 (input data m1 q4)).
Proof.
(* Goal: forall (m1 m2 : data) (q3 q4 : queue data) (_ : not (In_queue data m2 (input data m1 (append data q3 q4)))), not (In_queue data m2 (append data q3 (input data m1 q4))) *)
  intros m1 m2 q3 q4 H.
(* Goal: not (In_queue data m2 (append data q3 (input data m1 q4))) *)
  apply not_inqueue_append.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: and (not (In_queue data m2 q3)) (not (or (@eq data m2 m1) (In_queue data m2 q4))) *)
  split.
(* Goal: not (or (@eq data m2 m1) (In_queue data m2 (append data q1 q2))) *)
  unfold not in |- *; intro.
(* Goal: False *)
  elim H.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  right.
(* Goal: In_queue data m2 (append data q3 q4) *)
  apply inqueue_append.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: not (or (@eq data m2 m1) (In_queue data m2 (append data q1 q2))) *)
  unfold not in |- *; intro.
(* Goal: False *)
  elim H.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  elim H0; intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  right.
(* Goal: In_queue data m2 (append data q3 q4) *)
  apply inqueue_append.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.


Lemma not_in_q_shuffle :
 forall (m1 m2 : data) (q1 q2 q3 q4 : queue data),
 ~ In_queue data m2 (append data q1 (input data m1 q2)) ->
 append data q1 q2 = append data q3 q4 ->
 ~ In_queue data m2 (append data q3 (input data m1 q4)).
Proof.
(* Goal: forall (m1 m2 : data) (q1 q2 q3 q4 : queue data) (_ : In_queue data m2 (append data q3 (input data m1 q4))) (_ : @eq (queue data) (append data q1 q2) (append data q3 q4)), In_queue data m2 (append data q1 (input data m1 q2)) *)
  intros m1 m2 q1 q2 q3 q4 H H0.
(* Goal: not (In_queue data m2 (append data q3 (input data m1 q4))) *)
  apply not_in_q_shuffle1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: not (or (@eq data m2 m1) (In_queue data m2 (append data q3 q4))) *)
  rewrite <- H0.
(* Goal: not (or (@eq data m2 m1) (In_queue data m2 (append data q1 q2))) *)
  unfold not in |- *; intro.
(* Goal: False *)
  elim H.
(* Goal: In_queue data m2 (append data q1 (input data m1 q2)) *)
  apply in_q_shuffle1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
Qed.


Lemma in_q_shuffle :
 forall (m1 m2 : data) (q1 q2 q3 q4 : queue data),
 In_queue data m2 (append data q3 (input data m1 q4)) ->
 append data q1 q2 = append data q3 q4 ->
 In_queue data m2 (append data q1 (input data m1 q2)).
Proof.
(* Goal: forall (m1 m2 : data) (q1 q2 q3 q4 : queue data) (_ : In_queue data m2 (append data q3 (input data m1 q4))) (_ : @eq (queue data) (append data q1 q2) (append data q3 q4)), In_queue data m2 (append data q1 (input data m1 q2)) *)
  intros m1 m2 q1 q2 q3 q4 H H0.
(* Goal: In_queue data m2 (append data q1 (input data m1 q2)) *)
  apply in_q_shuffle1.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q1 q2)) *)
  rewrite H0.
(* Goal: or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  generalize H.
(* Goal: forall _ : In_queue data m2 (append data q3 (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q3 q4)) *)
  elim q3.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : In_queue data m2 (append data (input data d q) (input data m1 q4))), or (@eq data m2 m1) (In_queue data m2 (append data (input data d q) q4)) *)
  simpl in |- *.
(* Goal: forall (d : data) (q : queue data) (_ : forall _ : In_queue data m2 (append data q (input data m1 q4)), or (@eq data m2 m1) (In_queue data m2 (append data q q4))) (_ : or (@eq data m2 d) (In_queue data m2 (append data q (input data m1 q4)))), or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  intros d q H1 H2.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  elim H2; intro.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  auto.
  
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  generalize (H1 H3).
(* Goal: forall _ : or (@eq data m2 m1) (In_queue data m2 (append data q q4)), or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  intro H4.
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
(* Goal: or (@eq data m2 m1) (or (@eq data m2 d) (In_queue data m2 (append data q q4))) *)
  elim H4; intro; auto.
Qed.

End INQUEUE_APPEND.
