(* 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                                                     *)


Require Export Bool. 
Require Export fifo. 

Unset Standard Proposition Elimination Names.

Section REDUCE.

Variable E : Set.

Variable f : E -> Z.

Fixpoint reduce (q : queue E) : Z :=
  match q with
  | empty => 0%Z
  | input d q' => (reduce q' + f d)%Z
  end.

Hypothesis positive_function : forall a : E, (f a > 0)%Z.

Lemma sum_positive :
 forall a b : Z, (a >= 0)%Z -> (b > 0)%Z -> (a + b >= 0)%Z.
Proof.
(* Goal: forall (a b : Z) (_ : Z.ge a Z0) (_ : Z.gt b Z0), Z.ge (Z.add a b) Z0 *)
 intros a b H H0.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
 omega.
Qed.

Lemma reduce_nil : reduce (empty E) = 0%Z.
Proof.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
 simpl in |- *.
(* Goal: @eq Z Z0 Z0 *)
 trivial.
Qed.


Lemma reduce_null_fun :
 forall q : queue E, (forall d : E, f d = 0%Z) -> reduce q = 0%Z.
Proof.
(* Goal: forall (q : queue E) (_ : forall d : E, @eq Z (f d) Z0), @eq Z (reduce q) Z0 *)
  intro; elim q.
(* Goal: forall _ : forall d : E, @eq Z (f d) Z0, @eq Z (reduce (empty E)) Z0 *)
(* Goal: forall (d : E) (q : queue E) (_ : forall _ : forall d0 : E, @eq Z (f d0) Z0, @eq Z (reduce q) Z0) (_ : forall d0 : E, @eq Z (f d0) Z0), @eq Z (reduce (input E d q)) Z0 *)
  intro; apply reduce_nil.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: @eq Z (Z.add (reduce E f q0) (f d)) Z0 *)
  rewrite H0.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
Qed.



Lemma reduce_positive : forall q : queue E, (reduce q >= 0)%Z.
Proof.
(* Goal: forall q : queue E, Z.ge (reduce E f q) Z0 *)
  intros q.
(* Goal: Z.ge (reduce E f q) Z0 *)
  elim q.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
(* Goal: forall (d : E) (q : queue E) (_ : Z.ge (reduce E f q) Z0), Z.ge (reduce E f (input E d q)) Z0 *)
  intros d q0 H.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: Z.ge (Z.add (reduce q0) (f d)) Z0 *)
  apply sum_positive.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
(* Goal: Z.gt (f d) Z0 *)
  exact (positive_function d).
Qed.

(* We prove the following general lemma.  
   Then, we instantiate it to 
    - q1=nil: this case corresponds to adding an element in 
              a queue.
    - q2=nil: this case corresponds to removing an element 
              from a queue. *)

Lemma reduce_append :
 forall (q1 : queue E) (d : E) (q2 : queue E),
 reduce (append E q1 (input E d q2)) = (reduce (append E q1 q2) + f d)%Z.

Proof.
(* Goal: forall (q1 : queue E) (d : E) (q2 : queue E), @eq Z (reduce (append E q1 (input E d q2))) (Z.add (reduce (append E q1 q2)) (f d)) *)
  intro q1.
(* Goal: forall (d : E) (q2 : queue E), @eq Z (reduce (append E q1 (input E d q2))) (Z.add (reduce (append E q1 q2)) (f d)) *)
  elim q1.
(* Goal: forall (d : E) (q2 : queue E), @eq Z (reduce (input E d q2)) (Z.add (reduce q2) (f d)) *)
  intros d q2.
(* Goal: @eq Z (reduce (append E (empty E) (input E d q2))) (Z.add (reduce (append E (empty E) q2)) (f d)) *)
(* Goal: forall (d : E) (q : queue E) (_ : forall (d0 : E) (q2 : queue E), @eq Z (reduce (append E q (input E d0 q2))) (Z.add (reduce (append E q q2)) (f d0))) (d0 : E) (q2 : queue E), @eq Z (reduce (append E (input E d q) (input E d0 q2))) (Z.add (reduce (append E (input E d q) q2)) (f d0)) *)
  rewrite append_nil1.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
  
(* Goal: forall (d : E) (q : queue E) (_ : forall (d0 : E) (q2 : queue E), @eq Z (reduce (append E q (input E d0 q2))) (Z.add (reduce (append E q q2)) (f d0))) (d0 : E) (q2 : queue E), @eq Z (reduce (append E (input E d q) (input E d0 q2))) (Z.add (reduce (append E (input E d q) q2)) (f d0)) *)
  intros d q H d0 q2.
(* Goal: @eq Z (reduce (append E (input E d q) (input E d0 q2))) (Z.add (reduce (append E (input E d q) q2)) (f d0)) *)
  rewrite <- input_append.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed.

(* And now two instantiations *)

Lemma reduce_append_nil1 :
 forall (d : E) (q2 : queue E), reduce (input E d q2) = (reduce q2 + f d)%Z.
Proof.
(* Goal: forall (d : E) (q2 : queue E), @eq Z (reduce (input E d q2)) (Z.add (reduce q2) (f d)) *)
  intros d q2.
(* Goal: @eq Z (reduce (input E d q2)) (Z.add (reduce q2) (f d)) *)
  rewrite <- (append_nil1 E (input E d q2)).
(* Goal: @eq Z (reduce (append E (empty E) (input E d q2))) (Z.add (reduce q2) (f d)) *)
  pattern q2 at 2 in |- *.
(* Goal: (fun q : queue E => @eq Z (reduce (append E (empty E) (input E d q2))) (Z.add (reduce q) (f d))) q2 *)
  rewrite <- (append_nil1 E q2).
(* Goal: @eq Z (reduce (append E q1 (input E d (empty E)))) (Z.add (reduce (append E q1 (empty E))) (f d)) *)
  apply reduce_append.
Qed.

Lemma reduce_append_nil2 :
 forall (q1 : queue E) (d : E),
 reduce (append E q1 (input E d (empty E))) = (reduce q1 + f d)%Z.
Proof.
(* Goal: forall (q1 : queue E) (d : E), @eq Z (reduce q1) (Z.sub (reduce (append E q1 (input E d (empty E)))) (f d)) *)
  intros q1 d.
(* Goal: @eq Z (reduce (append E q1 (input E d (empty E)))) (Z.add (reduce q1) (f d)) *)
  pattern q1 at 2 in |- *.
(* Goal: (fun q : queue E => @eq Z (reduce (append E q1 (input E d (empty E)))) (Z.add (reduce q) (f d))) q1 *)
  rewrite <- (append_nil2 E q1).
(* Goal: @eq Z (reduce (append E q1 (input E d (empty E)))) (Z.add (reduce (append E q1 (empty E))) (f d)) *)
  apply reduce_append.
Qed. 

Lemma reduce_append_nil2_symmetric :
 forall (q1 : queue E) (d : E),
 reduce q1 = (reduce (append E q1 (input E d (empty E))) - f d)%Z.
Proof.
(* Goal: forall (q1 : queue E) (d : E), @eq Z (reduce q1) (Z.sub (reduce (append E q1 (input E d (empty E)))) (f d)) *)
  intros q1 d.
(* Goal: @eq Z (reduce q1) (Z.sub (reduce (append E q1 (input E d (empty E)))) (f d)) *)
  rewrite (reduce_append_nil2 q1 d).
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed. 

End REDUCE.


Section DISJOINT.

Variable E : Set.

(* functional or *)
Definition fun_or (pred1 pred2 : E -> bool) (a : E) := pred1 a || pred2 a.


(* functional sum *)
Definition fun_sum (f1 f2 : E -> Z) (a : E) := (f1 a + f2 a)%Z.

Definition fun_minus (f1 f2 : E -> Z) (a : E) := (f1 a - f2 a)%Z.




Variable f : E -> Z.


Lemma disjoint_reduce :
 forall (f1 f2 : E -> Z) (q : queue E),
 reduce E (fun_sum f1 f2) q = (reduce E f1 q + reduce E f2 q)%Z.
Proof.
(* Goal: forall (f1 f2 : forall _ : E, Z) (q : queue E) (_ : forall d : E, @eq Z (f1 d) (f2 d)), @eq Z (reduce E f1 q) (reduce E f2 q) *)
  simple induction q.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
  
(* Goal: forall (d : E) (q : queue E) (_ : Z.ge (reduce E f q) Z0), Z.ge (reduce E f (input E d q)) Z0 *)
  intros d q0 H.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: @eq Z (Z.add (Z.add (reduce E f1 q0) (reduce E f2 q0)) (fun_sum f1 f2 d)) (Z.add (Z.add (reduce E f1 q0) (f1 d)) (Z.add (reduce E f2 q0) (f2 d))) *)
  unfold fun_sum in |- *.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed.

Lemma disjoint_reduce3 :
 forall (f1 f2 : E -> Z) (q : queue E),
 reduce E (fun_minus f1 f2) q = (reduce E f1 q - reduce E f2 q)%Z.
Proof.
(* Goal: forall (f1 f2 : forall _ : E, Z) (q : queue E) (_ : forall d : E, @eq Z (f1 d) (f2 d)), @eq Z (reduce E f1 q) (reduce E f2 q) *)
  simple induction q.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  simpl in |- *; auto.
(* Goal: forall (d : E) (q : queue E) (_ : Z.ge (reduce E f q) Z0), Z.ge (reduce E f (input E d q)) Z0 *)
  intros d q0 H.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: @eq Z (Z.add (Z.sub (reduce E f1 q0) (reduce E f2 q0)) (fun_minus f1 f2 d)) (Z.sub (Z.add (reduce E f1 q0) (f1 d)) (Z.add (reduce E f2 q0) (f2 d))) *)
  unfold fun_minus in |- *.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed.

Lemma reduce_simpl :
 forall (f1 f2 : E -> Z) (q : queue E),
 (forall d : E, f1 d = f2 d) -> reduce E f1 q = reduce E f2 q.
Proof.
(* Goal: forall (f1 f2 : forall _ : E, Z) (q : queue E) (_ : forall d : E, @eq Z (f1 d) (f2 d)), @eq Z (reduce E f1 q) (reduce E f2 q) *)
  simple induction q.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  simpl in |- *; auto.
(* Goal: forall (d : E) (q : queue E) (_ : forall _ : forall (x : E) (_ : In_queue E x q), @eq Z (f x) Z0, @eq Z (reduce E f q) Z0) (_ : forall (x : E) (_ : or (@eq E x d) (In_queue E x q)), @eq Z (f x) Z0), @eq Z (Z.add (reduce E f q) (f d)) Z0 *)
  intros d q0 H H0.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: @eq Z (Z.add (reduce E f q0) (f d)) Z0 *)
  rewrite H0.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
Qed.

End DISJOINT.

Section REDUCE_MORE.


Variable data : Set.
Hypothesis eq_data_dec : eq_dec data.


Variable f : data -> Z.



Lemma reduce_first_out :
 forall (q : queue data) (m : data),
 first data q = value data m ->
 reduce data f (first_out data q) = (reduce data f q - f m)%Z.

Proof.
(* Goal: forall (q : queue data) (m : data) (_ : @eq (exc data) (first data q) (value data m)), @eq Z (reduce data f (first_out data q)) (Z.sub (reduce data f q) (f m)) *)
  intros q m H.
(* Goal: @eq Z (reduce data f (first_out data q)) (Z.sub (reduce data f q) (f m)) *)
  rewrite (reduce_append_nil2_symmetric data f (first_out data q) m).
(* Goal: @eq Z (Z.sub (reduce data f (append data (first_out data q) (input data m (empty data)))) (f m)) (Z.sub (reduce data f q) (f m)) *)
  rewrite (append_first_out2 data m q).
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
Qed.


End REDUCE_MORE.

Section reduce_pos.


Variable E : Set.

Variable f : E -> Z.
Hypothesis positive_function : forall a : E, (f a >= 0)%Z.

Lemma reduce_positive_or_null : forall q : queue E, (reduce E f q >= 0)%Z.
Proof.
(* Goal: forall q : queue E, Z.ge (reduce E f q) Z0 *)
  intros q.
(* Goal: Z.ge (reduce E f q) Z0 *)
  elim q.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
  
(* Goal: forall (d : E) (q : queue E) (_ : Z.ge (reduce E f q) Z0), Z.ge (reduce E f (input E d q)) Z0 *)
  intros d q0 H.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simpl in |- *.
(* Goal: Z.ge (Z.add (reduce E f q0) (f d)) Z0 *)
  generalize (positive_function d).
(* Goal: forall _ : Z.ge (f d) Z0, Z.ge (Z.add (reduce E f q0) (f d)) Z0 *)
  intro H0.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed.

End reduce_pos.

Section reduce_strictly_pos.


Variable E : Set.

Variable f : E -> Z.
Hypothesis positive_function : forall a : E, (f a >= 0)%Z.

Hypothesis eq_E_dec : eq_dec E.

Lemma reduce_in_queue_strictly_positive :
 forall (x : E) (q : queue E),
 (f x > 0)%Z -> In_queue E x q -> (reduce E f q > 0)%Z.
Proof.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simple induction q; simpl in |- *.
(* Goal: forall (_ : Z.gt (f x) Z0) (_ : False), Z.gt Z0 Z0 *)
(* Goal: forall (d : E) (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  intuition.
  
(* Goal: forall (d : E) (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  intro d.
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  case (eq_E_dec d x); intro.
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  rewrite e; intros.
(* Goal: Z.gt (Z.add (reduce E f q0) (f x)) Z0 *)
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  generalize (reduce_positive_or_null E f positive_function q0); intro.
(* Goal: Z.gt (Z.add (reduce E f q0) (f x)) Z0 *)
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  clear H.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
  
(* Goal: forall (q : queue E) (_ : forall (_ : Z.gt (f x) Z0) (_ : In_queue E x q), Z.gt (reduce E f q) Z0) (_ : Z.gt (f x) Z0) (_ : or (@eq E x d) (In_queue E x q)), Z.gt (Z.add (reduce E f q) (f d)) Z0 *)
  intros q0 H H0 H1.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  elim H1; intro.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  elim n; auto.
  
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  generalize (positive_function d); intro.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  generalize (H H0 H2); intro.
(* Goal: Z.gt (Z.add (reduce E f q0) (f d)) Z0 *)
  omega.
Qed.
End reduce_strictly_pos.

Section reduce_in_q_null.
Variable E : Set.

Variable f : E -> Z.

Hypothesis eq_E_dec : eq_dec E.


Lemma reduce_in_queue_null :
 forall q : queue E,
 (forall x : E, In_queue E x q -> f x = 0%Z) -> reduce E f q = 0%Z.
Proof.
(* Goal: Z.ge (reduce E f (input E d q0)) Z0 *)
  simple induction q; simpl in |- *.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
  
(* Goal: forall (d : E) (q : queue E) (_ : forall _ : forall (x : E) (_ : In_queue E x q), @eq Z (f x) Z0, @eq Z (reduce E f q) Z0) (_ : forall (x : E) (_ : or (@eq E x d) (In_queue E x q)), @eq Z (f x) Z0), @eq Z (Z.add (reduce E f q) (f d)) Z0 *)
  intros d q0 H H0.
(* Goal: @eq Z (Z.add (reduce E f q0) (f d)) Z0 *)
  rewrite H0.
(* Goal: @eq Z (Z.add (reduce E f q0) Z0) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  rewrite H.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  auto.
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  intros x H1.
(* Goal: @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  apply H0.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  right; auto.
(* Goal: @eq Z (Z.add Z0 Z0) Z0 *)
(* Goal: forall (x : E) (_ : In_queue E x q0), @eq Z (f x) Z0 *)
(* Goal: or (@eq E d d) (In_queue E d q0) *)
  left; auto.
Qed.

End reduce_in_q_null.
