Определение цепочки в coq - PullRequest
Новая
       22

Определение цепочки в coq

0 голосов
/ 08 октября 2019

Я следую основам программного обеспечения книг по работе с Coq. Я в настоящее время нахожусь в главе Тактики, и я застрял на forall_exists_challenge .

Я хотел бы отрицать предикат test, используя negb, но я получаю ошибку 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.

Я ожидаю, что смогу каким-то образом опровергнуть предикат, но не могу понять, как это сделать.

1 Ответ

2 голосов
/ 08 октября 2019

Как говорится в сообщении об ошибке, negb ожидает один логический тип, а не целый предикат. Самый простой способ создать новый предикат с использованием negb - это что-то вроде fun x => negb (test x). Обратите внимание, что теперь (test x) на самом деле имеет тип bool, поэтому он может быть передан в negb.

В качестве альтернативы, вы можете сделать запись для композиции функции (я не думаю, что такая запись существует встандартная библиотека, хотя я не знаю об основах программного обеспечения). Например, Notation "f 'o' g" := (fun x => f (g x)) (at level 20). (вам может потребоваться изменить уровень, чтобы избежать конфликтов с существующими обозначениями). Тогда вы сможете сделать negb o test.

Третье решение, если вы ожидаете много отрицать предикаты и не хотите заходить так далеко, как запись композиции функций, было бы сделатьновая функция, которая отрицает логический предикат вместо отрицательного логического. Например, Definition neg_pred {X: Type} (pred: X -> bool): X -> bool := fun x => negb (pred x).. Тогда вы можете просто использовать neg_pred test.

...