CODEWITHSUNDEEP
booleancomparecoq
adfexxr
adfexxr

Reputation: 21

How to write boolean comparsion function in Coq

I'm trying to remove all integers that are greater than 7 from a list as follows

filter (fun n => n > 7).

However I get the following error

The term "n > 7" has type "Prop" while it is expected to have type "bool".

I am new to Coq, how can I fix it?

Upvotes: 2

Views: 692

Answers (1)

emi
emi

Reputation: 5410

The problem is that @List.filter nat expects a function of type nat -> bool but you supplied a function of type nat -> Prop. Here, @List.filter nat is List.filter applied to the type argument nat. One difference between bool and Prop is that bool is decidable while Prop is not: there are propositions P such that neither P nor ~P are known; one can always determine whether something is true or false.

In order to resolve this situation, you need to write a function of type nat -> bool that returns true when applied to an argument greater than 7 and false otherwise. You can take advantage of the fact that the standard library defines boolean comparison functions over the natural numbers. I would also suggest reading the first volume of Software Foundations to familiarize yourself with Coq. It is more accessible and easy-going than some other prominent introductions (it was used in a program verification course at my university that presupposed little functional programming experience).

Here is a minimal example using only the builtin list type and notations:

Require Import Coq.Lists.List.
Import ListNotations. 

Fixpoint filterb {A : Type} (f : A -> bool) (xs : list A) : list A :=
  match xs with
  | []      => []
  | x :: xs => if f x then x :: filterb f xs else filterb f xs
  end. 

Fixpoint ltb (n m : nat) : bool :=
  match n, m with
  | n  , 0   => false
  | 0  , S m => true
  | S n, S m => ltb n m
  end.

Eval compute in (filterb (fun n => ltb 7 n) [5;6;7;8;9]).
(* = [8;9] *)

Upvotes: 4

Related Questions