The Coq mailing list

[Florent Becker <florent.becker AT ens-lyon.fr>]

Hi all,

I am currently toying with a formalization of graph theory, and I can't 
help tripping as I catch my own feet into the exposed guts of inversion, 
which is a little gore.

Here is a less horror-movie-graphic and more formal definition of the 
problem. I define graphs inductively independently of any "set of nodes" 
(contrarily to what J Duprat did in his library). The definition is as 
follows:

Inductive graph : nat -> Set :=
 | gnil : graph 0
 | gcons :  forall (n : nat) (l : Bvector n),  graph n -> graph (S n).

The Bvector is the adjacency list of the vertex being added, restricted 
to the previous vertices; thus, a graph is represented by the superior 
half of its adjacency matrix

Then I define a proposition edge stating that there is an edge between 
two vertices of the graph (Vnth is, as the name states, nth adapted for 
BVectors; I include it in graphs-coq-club.v):

Inductive edge : forall n, (graph n) -> nat -> nat -> Prop :=
 | edge_last_r : forall n (g : graph n) (v : Bvector n) m (Hm : m < n),
                                     Is_true (Vnth n m v Hm) -> edge (S 
n) (gcons n v g) n m
 | edge_last_l : forall n (g : graph n) (v : Bvector n) m (Hm : m < n),
                                     Is_true (Vnth n m v Hm) -> edge (S 
n) (gcons n v g) m n
 | edge_inside : forall n x y (g:graph n) (v : Bvector n),
                                      edge n g x y -> edge (S n) (gcons 
n v g) x y.


Until here, everything is in order and I get on to proving basic facts 
about edges: there are no loops, edges are symmetric ... This proofs 
carry on well except that I sometimes have to use simple inversion 
instead of inversion, which seems to forget that the graph used in gcons 
is given unambiguously by gcons even when applying edge_last_{r,l}. Is 
there a not-inria-employee accessible reason for this ? This problem 
seems to be version-dependent: it seems to only show up in 8.1, as 
opposed to 8.0. Is there any change to inversion in 8.1 that can explain 
this ? (I'm using 8.1)

Then I want to define a function for deciding whether an edge is in a 
graph or not. I'm defining:

Definition edge_dec : forall n (g:graph n) x y, {edge n g x y}+{~edge n 
g x y}

I get to the case where I have y=n, g=(gcons n l g) and (Vnth n x l _ = 
false), and I want to prove that there is no edge.

The goal is:

x : nat
n : nat
l : Bvector n
g : graph n
Hxn : x < n
n0 : ~ edge n g x n
e : Vnth n x l Hxn = false
He : edge (S n) (gcons n l g) x n
______________________________________(1/4)
False


When I (simple) invert He, I get rid of the case edge_last_r with omega, 
but for the next case I have the following goal:

x : nat
n : nat
l : Bvector n
g : graph n
Hxn : x < n
n0 : ~ edge n g x n
He : edge (S n) (gcons n l g) x n
g0 : graph n
v : Bvector n
H1 : existT (fun n : nat => graph n) (S n) (gcons n v g0) =
    existT (fun n : nat => graph n) (S n) (gcons n l g)
Hm : x < n
Hg_g0 : existT (fun n : nat => graph n) n g0 =
       existT (fun n : nat => graph n) n g
Htrue : Is_true (Vnth n x v Hm)
>>>>> Hvl : existT (fun n : nat => Bvector n) n v =
>>>>>       existT (fun n : nat => Bvector n) n l
>>>>> e : Vnth n x l Hxn = false
>>>>> e0 : Vnth n x v Hxn = true
______________________________________(1/6)
False

given Hvl, e0 and e seem clearly in contradiction.

Yet, dependent rewrite Hvl doesn't work on any of them : it "Cannot find 
a well-typed generalization of the goal that makes the proof progress". 
How comes ? Why can't it rewrite e0 as Vnth n x l Hxn = true ? Moreover, 
this error message doesn't seem to show up in 
http://coq.inria.fr/V8.1/refman/index.html. Am I stuck for a deep 
reason, or is there a way around that problem? I attach a file with more 
context for those wanting to see the actual proofs (or non proofs, given 
this problem).

Friendly

Florent

Require Import List.
Require Import Bool.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Even.
Require Import Bvector.
Require Import Arith.
Require Import Omega.


Inductive graph : nat -> Set :=
  | gnil : graph 0
  | gcons :  forall (n : nat) (l : Bvector n),  graph n -> graph (S n).


Definition Vnth : forall (n m : nat) (v : Bvector n), m < n -> bool.
Proof.
intros n m v.
generalize m.
clear m.
induction v.
         intros.
         elim (lt_n_O m H).

         destruct m.
              intros _.
              exact a.
                
              intro Hmn. apply lt_S_n in Hmn.
          exact (IHv m Hmn).
Defined.

(* Vnth doesn't depend on its proof argument *)

Lemma Vnth_ind_proof_lt : forall (n m : nat) (v : Bvector n) (H1 H2 : m<n),
        Vnth n m v H1 = Vnth n m v H2.
Proof.
intros n m v; generalize m; clear m.
induction v; intros.
         inversion H1.
         
         destruct m.
         simpl; reflexivity.
         simpl. apply IHv.
Qed.


(* Definition of an edge; vertices are numbered from 0 to n-1 *)
Inductive edge : forall n, (graph n) -> nat -> nat -> Prop :=
  | edge_last_r : forall n (g : graph n) (v : Bvector n) m (Hm : m < n),
                                      Is_true (Vnth n m v Hm) -> edge (S n) 
(gcons n v g) n m
  | edge_last_l : forall n (g : graph n) (v : Bvector n) m (Hm : m < n),
                                      Is_true (Vnth n m v Hm) -> edge (S n) 
(gcons n v g) m n
  | edge_inside : forall n x y (g:graph n) (v : Bvector n),
                                       edge n g x y -> edge (S n) (gcons n v 
g) x y.

(* there are no loops*)

Hypothesis edge_irrefl : forall n (g: graph n) x, ~edge n g x x.

(* there are only edges between vertices that are in the graph *)

Hypothesis edge_bounded : forall n (g:graph n) x y, edge n g x y -> x < n /\ 
y < n.


(* edge is symmetrical *)

Lemma edge_sym_last_l : forall n  (g: graph (S n)) y, edge (S n) g n y -> 
edge (S n) g y n.
Proof.

intros n g y H; simple inversion H; simpl in *.
(* the «simple» seems indispensable to get g "=" g0 *)
         subst n0. subst y. intro Hv. dependent rewrite <- H2.
         exact (edge_last_l n g0 v m Hm Hv).
                 
         apply False_ind; omega.
                 
         intro Hedge; apply False_ind; injection H1; intro Hn0; subst n0 y0 x;
         generalize (edge_bounded n g0 n y Hedge); omega.
Qed.

Hypothesis edge_sym_last_r : forall n  (g: graph (S n)) y, edge (S n) g y n 
-> edge (S n) g n y.

Hypothesis edge_sym : forall n (g: graph n) x y, edge n g x y -> edge n g y x.

(* deciding edge... or rather, getting stuck with (simple) inversion *)
Definition edge_dec : forall (n x y:nat) (g:graph n), {edge n g x y}+{~edge n 
g x y}.
Proof.
induction g.
 (* empty graph *)
 right; intro H; inversion H.
 destruct IHg as [e | Hnegxy].
  (* recursive case *)
  left; apply edge_inside; trivial.
  
  (* negative case, now we have to see why ... *)
  destruct (lt_eq_lt_dec x n) as [[Hxn|Hxn]|Hxn].
    destruct (lt_eq_lt_dec y n) as [[Hyn|Hyn]|Hyn].
      
      (* the edge would be inside but is not *)
      right; intro He.  inversion He.
       omega.
       omega.
       elim Hnegxy; dependent rewrite <- H2; trivial.
       
       (*  y=n, troubles start *)
       subst. clear Hnegxy.
      destruct (sumbool_of_bool (Vnth n x l Hxn)).
       (* the edge is here, easy *)
       left; apply edge_last_l with (Hm := Hxn).
         rewrite e; simpl; tauto.
       (* the edge doesn't exist, we have to invert... *)
       right. intro He. simple inversion He.
        intros; omega.
        subst. clear H0.
        injection H1.
        intros Hg_g0 Hvl.
        intros Htrue.
        destruct (sumbool_of_bool (Vnth n x v Hm)) .
        rewrite (Vnth_ind_proof_lt n x v Hm Hxn) in e0.
        Admitted. (* dependent rewrite Hvl in e0. échoue, et moi avec*)(** 
Pour edge, dans un graphe de taille n, les sommets sont numérotés de
   * 0 à n-1 *)

(* Proofs for the lemmas which were admitted : *)


Lemma edge_irrefl_l : forall n (g: graph n) x, ~edge n g x x.
Proof.
        induction g.
         intros x H; inversion H.
         intros x H; inversion H.
          omega.
          omega.
          elim (IHg x); dependent rewrite <- H3; trivial.
Qed.


(* il n'y a d'arete qu'entre des sommets du graphe*)

Lemma edge_bounded_l : forall n (g:graph n) x y, edge n g x y -> x < n /\ y < 
n.
Proof.
        induction g.
         intros x y He; inversion He.
         intros x y He; inversion He.
          omega.
          omega.
          generalize H4; dependent rewrite H2; simpl in |- *; intros H5.
            generalize (IHg x y H5); omega.
Qed.

(* la relation edge est symetrique*)

Lemma edge_sym_last_l_l : forall n  (g: graph (S n)) y, edge (S n) g n y -> 
edge (S n) g y n.
Proof.

intros n g y H; simple inversion H; simpl in *.
         subst n0. subst y. intro Hv. dependent rewrite <- H2.
         exact (edge_last_l n g0 v m Hm Hv).
                 
         apply False_ind; omega.
                 
         intro Hedge; apply False_ind; injection H1; intro Hn0; subst n0 y0 x;
         generalize (edge_bounded n g0 n y Hedge); omega.
Qed.

Lemma edge_sym_last_r_l : forall n  (g: graph (S n)) y, edge (S n) g y n -> 
edge (S n) g n y.
Proof.

intros n g y H; simple inversion H; simpl in *.          
         apply False_ind; omega.
                 
         subst n0. subst y. intro Hv. dependent rewrite <- H2.
         simpl. exact (edge_last_r n g0 v m Hm Hv).

         intro Hedge; apply False_ind; injection H1; intro Hn0; subst n0 y0 x.
         generalize (edge_bounded n g0 y n Hedge); omega.
Qed.

Lemma edge_sym_l : forall n (g: graph n) x y, edge n g x y -> edge n g y x.
Proof.
        induction g.
         intros x y H; inversion H.
         intros x y H; inversion H.
          subst; apply edge_sym_last_l_l; trivial.
          subst; apply edge_sym_last_r_l; trivial.
          apply edge_inside.
            apply IHg; dependent rewrite <- H3; trivial.
Qed.