The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Dear Coq' user.

Here are some explanations concerning the errors you get:

Fixpoint append [X, Y, Z: N; f: (FreeGraph X Y)] : 
    (FreeGraph Y Z) -> (FreeGraph X Z) :=
   Cases f of
        (nil X) => [g: (FreeGraph X Z)] g 
    |   (cons X X' Y a f') => [g: (FreeGraph Y Z)] (cons a (append f' g))
end.

does'nt work because the system is unable to infer a dependent type
for the branches. 

The Cases typing rule for f:(FreeGraph X Y) is the following :

    P:N->N->Type  f:(FreeGraph X Y) 
    (X:N |- f1 : (P X X)) 
    (X,X',Y:N)(a:(A X X'))(f':(FreeGraph X' Y))|-f2:(P X Y)
------------------------------------------------------------------------------
 <P>Cases f of  (nil X) => f1 |   (cons X X' Y a f') => f2 end : (P X Y)

The type annotation <P> on front of Cases is automatically inferred in
some restricted cases (P is directly a type and not a type scheme)
In your case, the scheme has to be givent explicitely, the following
definition works :

Fixpoint append [X, Y, Z: N; f: (FreeGraph X Y)] : 
    (FreeGraph Y Z) -> (FreeGraph X Z) :=
 <[X,Y:N](FreeGraph Y Z) -> (FreeGraph X Z)>Cases f of
        (nil X) => [g: (FreeGraph X Z)] g 
    |   (cons X X' Y a f') => [g: (FreeGraph Y Z)] (cons a (append f' g))
end.

In the case of the Elim rule, you have the following inference rule :

    P:(X,Y:N)(FreeGraph X Y)->Prop  f:(FreeGraph X Y) 
     |- ? :  (X:N)(P X X (nil X))
     |- ? :  (X,X',Y:N)(a:(A X Y))(f':(FreeGraph X' Y))
             (P X' Y f')->(P X Y (cons X X' Y a f'))
-------------------------------------------------------------
       |- ? : (P X Y f)

When you perform Elim f, the system has to transform your goal 
into 
     (P X Y f) with P well-typed of type (X,Y:N)(FreeGraph X Y)->Prop
In your case, the simple transformation 

   ([W,X:N][f:(Freegraph W X)](append (cons a f) g) == (cons a (append f g))
    W X f)
is not well-typed because, if we rename bound variables, we get 
 ([W0,X0:N][f:(Freegraph W0 X0)](append (cons a f) g) == (cons a (append f g))
    W X f)
while a has type (A W W) and g has type (FreeGraph W X) 
generalizing over a and g gives you first the goal :
(a:(A W W))(g: (FreeGraph X Y))(append (cons a f) g) == (cons a (append f g))
which is transforme by Elim into :
 ([W0,X0:N][f:(Freegraph W0 X0)]
  (a:(A W0 W0))(g: (FreeGraph X0 Y))
  (append (cons a f) g) == (cons a (append f g))
    W X f)
which is perfectly well-typed.

Let me give you an advice, concerning your definition of FreeGraph 
you may choose the alternative definition 
Inductive FreeGraph [X:N] : N -> Type :=
    nil : (FreeGraph X X) |
    cons : (Y, Z: N) (FreeGraph X Y) -> (A Y Z) -> (FreeGraph X Z).
This change the way the path are extended, making X a parameter of the
inductive definition (what you define inductively is not the binary
relation _ is connected to _, but a unary predicate : given X, the set
of nodes connected to X. 
Tou may compare the generated elimination principles (Check FreeGraph_ind).
The one obtained with this version is equivalent but more comfortable
to use in general.

With respect about your question on decomposing a proof of a==b when a
and b are in an inductive type, there are many different solutions. 
Let me illustrate that on integers.

First you may generate a general double induction principle, (which
already exists for integers).

Check nat_double_ind.
nat_double_ind
     : (R:(nat->nat->Prop))
        ((n:nat)(R O n))
        ->((n:nat)(R (S n) O))
        ->((n,m:nat)(R n m)->(R (S n) (S m)))
        ->(n,m:nat)(R n m)

If you need to prove n=m->P(n,m) you can use this principle :
   Pattern n m (* abstract the goal in order to make R evident *); 
   Apply nat_double_ind 

You can also generate a particular scheme for equality :

Goal nat_eq_ind
     : (R:(nat->nat->Prop))
        ((n:nat)(R O O))
        ->((n,m:nat)(R n m)->n=m->(R (S n) (S m)))
        ->(n,m:nat)n=m->(R n m)

But the simplest way would probably be to Rewrite n into m (or
vice-versa) and the performs simple induction.

However, you should be aware on the fact that you are manipulating
terms in dependent types, which sometimes introduce difficulties. 

  you an write a==b when a and b have the same type :
with a : (FreeGraph X Y) and b : (FreeGraph X' Y') then 
a==b can only be written in the case X and X' on one hand and Y and Y'
on the other hand are computationnally the same. 
If they are simply provably equal you should use a special dependent
equality  (see the file Logic/EqDep.v).

I hope these explanations on some tricky points of the Calculus of
Inductive Constructions will
help you. Please do not hesitate to send further questions to 
coq-club AT pauillac.inria.fr

Regards,
Christine Paulin.

In his message of Thu January 6, 2000, Michael Abbott writes: 
> I'd like to cancel question I sent yesterday, if I may!  The question I sent
> is actually garbled, and I've figured out the answer to the question I meant
> to ask.
> 
> I meant to try and prove:
>       Lemma append_assoc : (append (append f g) h) == (append f (append g
> h)).
> 
> and the first step, which I was missing, is:
>       Generalize Y Z g h.
> 
> I do have another question about decomposing a==b, where a and b of an
> inductive type, into the structure of the inductive type.  I'll try and
> formulate this question more clearly once people are back from holidays, and
> once I've spent more time trying to solve it.
> 
> Regards,
>       Michael Abbott
> 
> 
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84