The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Yann,

 

you are mixing up types and values here. The easiest way to get something of type "f0 white" is to ask Coq to help you with it:

 

Definition f0w : f0 white.

unfold f0. trivial. Defined.

 

The above means I want to define a term named f0w, which shall have type f0 white. Then you can use tactics to construct such a term.

 

If you print it:

 

Print f0w.

 

you get

 

f0w = I

     : f0 white

 

“I” is the one constructor of the Prop True. Unfortunately the same won’t work for f0 black:

 

Definition f0b : f0 black.

unfold f0. (* Stuck *)

 

because you would have to construct a term of type False. I guess here the difference between the Prop False and a term which has this type becomes more clear than in the True case. You can write down the Prop False, but you cannot give a term which has type False (unless Coq has some bug). If you change your definition of f0 to return True in both cases (or to something more interesting, that is some provable proposition which involves the argument of f0) it works:

 

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.

 

(* color -> Prop *)

Definition f0 (c: color) : Prop :=

match c with

| white => True

| black => True

end.

 

(* color -> color *)

Definition f1 (c: color) : color :=

match c with

| white => black

| black => white

end.

 

Definition f0w : f0 white. unfold f0. trivial. Defined.

Definition f0b : f0 black. unfold f0. trivial. Defined.

 

Print f0w.

Print f0b.

 

Check match_as_0 f0 (f0w) (f0b) f1.

Check match_as_0 f0 I I f1.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928