83 lines
1.8 KiB
Coq
83 lines
1.8 KiB
Coq
Require List.
|
|
|
|
(* x ∈ l *)
|
|
Definition elementOf (x: nat) (l: list nat): bool :=
|
|
List.existsb (fun a => Nat.eqb x a) l.
|
|
|
|
(* By the way, this function is a good example to illustrate
|
|
the difference between foldl and foldr... *)
|
|
Definition setify (l: list nat): list nat :=
|
|
List.fold_left (fun acc x =>
|
|
if elementOf x acc then acc
|
|
else (List.cons x acc)
|
|
) l List.nil.
|
|
|
|
|
|
(* Not caring about efficiency here... *)
|
|
Definition union (a b: list nat): list nat :=
|
|
let aset := setify a in
|
|
List.fold_left (fun acc y =>
|
|
if elementOf y acc then acc
|
|
else (List.cons y acc)
|
|
) b aset.
|
|
|
|
|
|
(******************** Random stuff ********************)
|
|
|
|
(* Count number of times an element appears in a list *)
|
|
Definition countx (x:nat) (l:list nat): nat :=
|
|
List.fold_left (fun count a =>
|
|
if Nat.eqb x a then (S count)
|
|
else count) l 0.
|
|
(*
|
|
Fixpoint countx' (a:nat) (l:list nat): nat :=
|
|
match l with
|
|
| List.cons x xs =>
|
|
if Nat.eqb x a then S (countx' a xs)
|
|
else (countx' a xs)
|
|
| _ => 0
|
|
end.
|
|
*)
|
|
|
|
Require Import Lia.
|
|
Lemma inlstCount: forall (l:list nat) (x:nat),
|
|
List.In x (setify l) -> countx x (setify l) = 0.
|
|
Proof.
|
|
intros l x H.
|
|
induction l.
|
|
- contradiction.
|
|
- unfold setify.
|
|
Admitted.
|
|
*)
|
|
|
|
Theorem foo (l:list nat): forall (x:nat),
|
|
let ll := setify l in
|
|
List.In x ll -> countx x ll = 1.
|
|
Proof.
|
|
simpl.
|
|
intros x H.
|
|
induction l.
|
|
- contradiction.
|
|
-
|
|
|
|
|
|
(******************** Trying out... ********************)
|
|
|
|
Require Import List.
|
|
Import ListNotations.
|
|
|
|
Compute elementOf 1 [0;0;0].
|
|
|
|
Compute countx 0 [0;0;0].
|
|
(* = 3 : nat *)
|
|
Compute countx 1 [0;0;0].
|
|
(* = 0 : nat *)
|
|
|
|
Compute setify [0;0;0].
|
|
(* = [0] : list nat *)
|
|
Compute setify [0;1;1;2;2;2;3;3;3;3].
|
|
(* = [3; 2; 1; 0] : list nat *)
|
|
|
|
Compute union [0;1;1;2;2;2;3;3;3;3] [1;1;4;4].
|
|
(* = [4; 3; 2; 1; 0] : list nat *)
|