CODEWITHSUNDEEP
coq
Arne Goeteyn
Arne Goeteyn

Reputation: 166

Chaining definitions in coq

I'm following trough the software foundations books for working with Coq. I'm currently at the Tactics chapter and I'm stuck on the forall_exists_challenge.

I would like to negate the test predicate using negb but I receive the error The term "test" has type "X -> bool" while it is expected to have type "bool".

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
  | [] => true
  | h :: t => test h && forallb test t
  end.

Example test_forallb_1 : forallb oddb [1;3;5;7;9] = true.
Proof. simpl. reflexivity. Qed.

Example test_forallb_2 : forallb negb [false;false] = true.
Proof. simpl. reflexivity. Qed.

Example test_forallb_3 : forallb evenb [0;2;4;5] = false.
Proof. simpl. reflexivity. Qed.

Example test_forallb_4 : forallb (eqb 5) [] = true.
Proof. simpl. reflexivity. Qed.

Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
  | [] => false
  | h :: t => test h || forallb test t
  end.


Example test_existsb_1 : existsb (eqb 5) [0;2;3;6] = false.
Proof. simpl. reflexivity. Qed.

Example test_existsb_2 : existsb (andb true) [true;true;false] = true.
Proof. simpl. reflexivity. Qed.

Example test_existsb_3 : existsb oddb [1;0;0;0;0;3] = true.
Proof. simpl. reflexivity. Qed.

Example test_existsb_4 : existsb evenb [] = false.
Proof. simpl. reflexivity. Qed.

Definition existsb' {X : Type} (test : X -> bool) (l : list X) : bool :=
  negb (forallb (negb test) l).

Example test_existsb_1' : existsb' (eqb 5) [0;2;3;6] = false.
Proof. simpl. reflexivity. Qed.

Theorem existsb_existsb' : forall (X : Type) (test : X -> bool) (l : list X),
  existsb test l = existsb' test l.
Proof. (* FILL IN HERE *) Admitted.

I expect I could be able to negate a predicate in some way but I can't seem to quite figure out how.

Upvotes: 0

Views: 256

Answers (1)

SCappella
SCappella

Reputation: 10474

As the error message says, negb expects a single boolean, rather than a whole predicate. The simplest way to make a new predicate using negb would be something like fun x => negb (test x). Note that now (test x) actually does have type bool so it can be fed to negb.

Alternatively, you could make a notation for function composition (I don't think such a notation exists in the standard library, though I don't know about Software Foundations). For example, Notation "f 'o' g" := (fun x => f (g x)) (at level 20). (you might need to change the level to avoid conflicts with existing notations). Then you'd be able to do negb o test.

A third solution, if you expect to be negating predicates a lot and don't want to go as far as a function composition notation, would be to make a new function that negates a boolean predicate instead of negating a boolean. For example, Definition neg_pred {X: Type} (pred: X -> bool): X -> bool := fun x => negb (pred x).. Then you can simply use neg_pred test.

Upvotes: 2

Related Questions