The Coq mailing list

[julien forest <forest AT ensiie.fr>]

Hi, 
It seems you found a little bug (I will have to investigate further to
be sure but I'm on holidays). 

For now you can change you function as bellow which solve the problem
without changing any think else. 

(* The algorithm itself *)
Function dijkstra_dist' (n' : node) (nq : list node * (list elt))
  { wf omeasure nq } : option nat :=
  match nq with
    | (visited, queue) =>
      match queue with
        | nil => None
        | (w, n) :: tlqueue =>
          if beq_node n n' then
            Some w
            else if (mem node_eq_dec n visited)
              then dijkstra_dist' n (visited, tlqueue)
                else 
                  let nqueue := q_adds (incr_succs w n) tlqueue in
                    dijkstra_dist' n' (n :: visited, nqueue)
      end
  end.
Proof.
  intros; subst.
  unfold omeasure.
  simpl.
  generalize (eq_nat_dec (max_nodes - length visited)
                         (max_nodes - length visited)); intro.
  destruct s; omega.
  simpl.
  intros n' nq visited queue e tlqueue w n teq1 teq0 teq teq2
teq3;subst. unfold omeasure.
  simpl.
  destruct (eq_nat_dec (max_nodes - S (length visited))
                       (max_nodes - length visited)).
  generalize (max_nodes_max (visited, tlqueue)); intro.
  assert (max_nodes - S (length visited) > 0) by (simpl in H; omega).
  simpl in H; omega.
  omega.
  apply wf_omeasure.
Defined.


Best regards, 
Julien Forest

On Tue, 2 Aug 2011 15:07:56 +0200
AOliveira 
<andandolive AT gmail.com>
 wrote:

> I have a Dijkstra distance algorithm (extracted from Chemouil &
> Arnold's report, www.lri.fr/~arnold/projects:coqgraphs) which uses a
> Function with a lexicographic order for termination. At the end of the
> definition, however, no induction principles are generated.
> 
> I looked at the discussion '"Function {measure}" and induction
> principles' but I'm not sure it's the same situation; if there is a
> similar trick that might work, I'd be glad to know about it.
> 
> 
> 
> (* Minimum distance between two given nodes in a graph using
> Dijkstra  *) Require Import Omega.
> Require Import Relations.
> Require Import List TheoryList.
> Require Import Wellfounded.
> Require Import Arith.
> Require Import Recdef.
> 
> (* Graph definitions *)
> Parameter node : Type.
> Parameter beq_node : node -> node -> bool.
> Parameter node_eq_dec : forall (n1 n2 : node), {n1 = n2} + {n1 <> n2}.
> Parameter max_nodes : nat.
> 
> Parameter edge : Type.
> Parameter all_edges : list edge.
> Parameter source : edge -> node.
> Parameter dest : edge -> node.
> Parameter succs : node -> list edge.
> 
> (* Priority queue element: pair (distance, node) *)
> Definition elt := (nat * node)%type.
> 
> (* q_adds new_l q : adds all elements of the list new_l
>    in the queue q, maintaining proper ordering, and
>    returns the new queue. *)
> Parameter q_adds : list elt -> list elt -> list elt.
> 
> (* Decreasing measure for the Function:
>    a lexicographically-ordered pair of naturals:
>    (increasing) length of the visited list, then
>    decreasing length of the remaining queue. *)
> Definition measure (nq: list node * list elt) : nat * nat :=
>   (max_nodes - length (fst nq), length (snd nq)).
> 
> (* Lexicographic ordering *)
> Definition lex (A B : Set) (eq_A_dec : forall a1 a2, {a1=a2}+{a1<>a2})
>   (o1 : relation A) (o2 : relation B) (s t : _ * _) :=
>   let (s1, s2) := s in
>     let (t1, t2) := t in
>       if eq_A_dec s1 t1
>         then o2 s2 t2
>         else o1 s1 t1.
> 
> Definition omeasure nq1 nq2 :=
>   lex nat nat eq_nat_dec lt lt (measure nq1) (measure nq2).
> 
> (* Some lemmas *)
> Lemma wf_lex :
>   forall (A B : Set) eq_A_dec o1 o2, well_founded o1 -> well_founded
> o2 -> well_founded (@lex A B eq_A_dec o1 o2).
> Proof.
>   intros A B eq_A_dec o1 o2 W1 W2; unfold well_founded in *; destruct
> a. generalize b; clear b; pattern a; refine (well_founded_ind W1 _ _
> a); clear a; intros a IH1 b; pattern b; refine (well_founded_ind W2 _
> _ b). clear b; intros b IH2; apply Acc_intro.
>   destruct y; simpl; elim (eq_A_dec a0 a); intro a0_eq_a.
>   subst a0; apply IH2.
>   intro; apply IH1; trivial.
> Defined.
> 
> Lemma wf_lt_lex :
>   well_founded (lex nat nat eq_nat_dec lt lt).
> Proof.
>   apply wf_lex; apply lt_wf.
> Defined.
> 
> Lemma wf_omeasure :
>   well_founded omeasure.
> Proof.
>   unfold omeasure. refine (wf_inverse_image _ _ _ _ wf_lt_lex).
> Defined.
> 
> (* We need an upper bound on the number of nodes for
>    the proof (or do we?) *)
> Axiom max_nodes_max :
>   forall (nq : list node * list elt), S (length (fst nq)) < max_nodes.
> 
> (* Auxiliary function for dijkstra_dist *)
> Definition incr_succs (w : nat) (n : node) :=
>   map (fun (e : edge) => (w + 1, dest e)) (succs n).
> 
> (* The algorithm itself *)
> Function dijkstra_dist (n' : node) (nq : list node * (list elt))
>   { wf omeasure nq } : option nat :=
>   match nq with
>     | (visited, queue) =>
>       match queue with
>         | nil => None
>         | (w, n) :: tlqueue =>
>           if beq_node n n' then
>             Some w
>             else (
>               let (new_visited, new_queue) := (
>                 if (mem node_eq_dec n visited) then (visited, tlqueue)
>                   else (
>                     let nqueue := q_adds (incr_succs w n) tlqueue in
>                       (n :: visited, nqueue)
>                   )
>               ) in
>               dijkstra_dist n' (new_visited, new_queue)
>             )
>       end
>   end.
> Proof.
>   intros; subst.
>   unfold omeasure.
>   simpl.
>   destruct (mem node_eq_dec n visited); inversion_clear teq3.
>   generalize (eq_nat_dec (max_nodes - length new_visited)
>                          (max_nodes - length new_visited)); intro.
>   destruct s; omega.
>   simpl.
>   destruct (eq_nat_dec (max_nodes - S (length visited))
>                        (max_nodes - length visited)).
>   generalize (max_nodes_max (visited, tlqueue)); intro.
>   assert (max_nodes - S (length visited) > 0) by (simpl in H; omega).
>   simpl in H; omega.
>   omega.
>   apply wf_omeasure.
> Defined.