1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
From Corelib Require Import ssreflect ssrbool ssrfun.
From Corelib Require Import ListDef.
Import Nat.
Fixpoint filter A (f : A -> bool) (l:list A) : list A :=
match l with
| nil => nil
| x :: l => if f x then x::(filter A f l) else filter A f l
end.
Arguments filter {_}.
Definition partition {X : Type}
(test : X -> bool)
(l : list X)
: list X * list X
:= (filter test l, filter (fun x => negb (test x)) l).
Section Fold_Right_Recursor.
Variables (A : Type) (B : Type).
Variable f : B -> A -> A.
Variable a0 : A.
Fixpoint fold_right (l:list B) : A :=
match l with
| nil => a0
| cons b t => f b (fold_right t)
end.
End Fold_Right_Recursor.
Arguments fold_right {_ _}.
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.
|
