The Coq mailing list

[Michael Abbott <Michael AT RCP.co.uk>]

Title: Beginner's question about induction proof

(I'm not sure if this is the right place to ask this question.)

I'm trying to do a simple proof in Coq and I get a message: "Unable to do second order unification".  Am I doing this the right way?

Regards,
        Michael Abbott

Here's my Coq code:

(* This file defines operations on the free algebra of paths generated by a
 * collection of nodes and arrows. *)
Implicit Arguments On.

Section FreeGraph.
(* N is a type of nodes, A(X,Y) a type of arrows (directed paths) from X to Y. *)
Variable N : Type.
Variable A : N -> N -> Type.

(* FreeGraph(X,Y) is the type of paths from X to Y. *)
Inductive FreeGraph : N -> N -> Type :=
    nil : (X: N) (FreeGraph X X) |
    cons : (X, Y, Z: N) (A X Y) -> (FreeGraph Y Z) -> (FreeGraph X Z).

(* The append function joins together two paths to yield a new path. *)
Definition append : (X, Y, Z: N)
    (FreeGraph X Y) -> (FreeGraph Y Z) -> (FreeGraph X Z).
    Intros X Y Z f. Elim f. Intros Y' g. Apply g.
    Intros X' X'' Y' a f' app g. Apply (cons a (app g)).
Defined.

(* I tried to define append directly like this, but I can't make this type check:
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.
*)

Variable W, X, Y: N.
Variable a: (A W W).
Variable f: (FreeGraph W X).
Variable g: (FreeGraph X Y).

Lemma append_const_dist : (append (cons a f) g) == (cons a (append f g)).
Elim f.
(* At this point I get the error message about "second order unification". *)