The Coq mailing list

[Nicolas Magaud <magaud AT dpt-info.u-strasbg.fr>]

> 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 
Here is a script which solves your current goal. To perform dependent 
rewrite, I had to
generalize Hm and e0. As far as I understand, the error message you got 
usually means
there are too many hypotheses in the context and they need to be 
transferred back into the
goal. This happens quite often when dealing with dependent types.

Hopefully, you'll figure out how to prove the remaining goals in the 
same way.

Have fun !

Nicolas Magaud

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 -b«simple» seems indispensable to get g "=" g0 *)-A
         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.
clear H1.*)
generalize Hm e0; clear e0.
dependent rewrite Hvl.
simpl.
intros Hn newH.
 rewrite (Vnth_ind_proof_lt n x l Hn Hxn) in newH.
rewrite e in newH.
inversion newH.
generalize Htrue e0 ; case (Vnth n x v Hm).
intros H1' H2'.
inversion H2'.
simpl;auto.
        Admitted. (* dependent rewrite Hvl in e0. -béchoue, et moi 
avec*)(** Pour edge, dans un graphe de taille n, les sommets sont numérotés 
de-A
   * 0 -bà n-1 *)-A

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