The Coq mailing list

[AOliveira <andandolive AT gmail.com>]

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.