1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
From Coq Require Import ssreflect ssrbool ssrfun.
From Coq Require Import List.
Import Nat.
Definition partition {X : Type}
(test : X -> bool)
(l : list X)
: list X * list X
:= (filter test l, filter (fun x => negb (test x)) l).
Definition fold (A B: Type) f l b:= @fold_right B A f b l.
Theorem partition_fst: forall (X : Type) (test : X -> bool) (l : list X),
fold_right andb true (map test (fst (partition test l))) = true.
Proof.
move => ? test.
elim => [|x xs IHxs] //.
case H: eqb (test x) true. (* <-- anomaly here! *)
Abort.
|
