# Library PAutomata.PGM.Queue

Set Implicit Arguments.
Unset Strict Implicit.
Require Import Arith.
Require Import Comp.

Section QUEUE_DEF.

Variable Domain : Set.

Variable err : Domain.

Variable weight : Domainnat.

Let max (d1 d2 : Domain) : Domain :=
if less (weight d2) (weight d1) then d1 else d2.

Inductive Queue : Set :=
| empty : Queue
| push : DomainQueueQueue.

Fixpoint queue_length (q : Queue) : nat :=
match q with
| empty ⇒ 0
| push d q'S (queue_length q')
end.

Fixpoint pop_ele (q : Queue) : Domain :=
match q with
| emptyerr
| push d q'
match q' with
| emptyd
| push d' p''max d (pop_ele q')
end
end.

Fixpoint pop_que (q : Queue) : Queue :=
match q with
| emptyempty
| push d q'
match q' with
| emptyempty
| push _ _
if less (weight d) (weight (pop_ele q'))
then q'
else push d (pop_que q')
end
end.

Fixpoint del_que (q1 : Queue) : Queue → (DomainProp) → Prop :=
match q1 with
| empty
fun q2 : Queue
match q2 with
| emptyfun P : DomainPropTrue
| push d2 q2'fun P : DomainPropFalse
end
| push d1 q1'
fun (q2 : Queue) (P : DomainProp) ⇒
(P d1del_que q1' q2 P)
(¬ P d1
match q2 with
| emptyFalse
| push d2 q2'd1 = d2 del_que q1' q2' P
end)
end.

Fixpoint push_ram (q1 q2 : Queue) {struct q2} : DomainProp :=
match q1, q2 with
| empty, emptyfun d : DomainFalse
| empty, push d2 q2'fun d : Domaind2 = d q2' = empty
| push d1 q1', emptyfun d : DomainFalse
| push d1 q1', push d2 q2'
fun d : Domain
(d2 = dq2' = q1) (d2 dd1 = d2 push_ram q1' q2' d)
end.

End QUEUE_DEF.