coqlogical-foundations

Mix-up of bool and Datatypes.bool after Require Import coq libraries

2

I'm going through software foundations and ran into an error. (https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html)

From Coq Require Import Arith.Arith.

From Coq Require Import Bool.Bool.

Require Export Coq.Strings.String.

From Coq Require Import Logic.FunctionalExtensionality.

From Coq Require Import Lists.List.

Import ListNotations.

The proof example:

Lemma eqb_stringP : forall x y : string,
    reflect (x = y) (eqb_string x y).

Error: In environment x : string y : string The term "eqb_string x y" has type "bool" while it is expected to have type "Datatypes.bool".

Any tips on how to proceed?

Solution

  • SF has its own definition of bool here:

    https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html

    Especially in the introductory chapters you need to be careful not to mix this up with Coq's definitions. Either import files from SF or import files from the standard library, but not both.

    In later chapters (afair) SF switches to the standard library definitions.