The Coq mailing list

[Mwyann <mwyann AT gmail.com>]

Hello,

I’m trying to make this example work (found at  http://disi.unitn.it/~zunino/teaching/formalTechniques/dependentMatch.html):

Inductive color : Set := white | black .

Definition match_as_0 (P : color -> Prop) (Hw : P white) (Hb : P black)

                  (f : color -> color) : P (f white) :=

 match f white with

 | white => Hw  (* : P white *)

 | black => Hb  (* : P black *)

 end

.

I can’t find a way to make this definition work, there’s no example and I don’t see how to make it output something. Can someone help me out? Here is what I tried:

(* color -> Prop *)

Definition f0 (c: color) : Prop :=

match c with

| white => True

| black => False

end.

(* color -> color *)

Definition f1 (c: color) : color :=

match c with

| white => black

| black => white

end.

Check match_as_0 f0 (f0 white) (f0 black) f1.

Last Check raises an error, saying “The term "f0 white" has type "Prop" while it is expected to have type "f0 white".”

Thanks in advance.

Yann