famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[coq] some list bool stuff

This commit is contained in:
Julin S 2023-05-16 12:05:59 +05:30
parent 6a5dbec769
commit a609908ccf
2 changed files with 236 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

182
coq/nat2listbool.v Normal file
View File

@ -0,0 +1,182 @@
Require List.
Fixpoint nat2bin_aux (n pw:nat): list bool :=
match pw with
| O =>
match n with
| O => List.cons false List.nil
| _ => List.cons true List.nil
end
| S pw' =>
let pwr := Nat.pow 2 pw in
let qnt := Nat.div n pwr in
let nxt := Nat.modulo n pwr in
List.cons
(if Nat.eqb qnt 0 then false
else true)
(nat2bin_aux nxt pw')
end.
Definition nat2bin (n:nat): list bool := nat2bin_aux n (Nat.log2 n).
Fixpoint nat2bin_aux' (n pw:nat): list bool :=
match pw with
| O =>
match n with
| O => List.cons false List.nil
| _ => List.cons true List.nil
end
| S pw' =>
let pwr := Nat.pow 2 pw in
let qnt := Nat.div n pwr in
let nxt := Nat.modulo n pwr in
List.app
(nat2bin_aux' nxt pw')
(if Nat.eqb qnt 0 then List.cons false List.nil
else List.cons true List.nil)
end.
Definition nat2bin' (n:nat): list bool := nat2bin_aux' n (Nat.log2 n).
Fixpoint bin2nat_aux (l:list bool) (pw:nat): nat :=
match pw with
| O =>
match l with
| List.cons true nil => 1
| _ => 0
end
| S pw' =>
let pwr := Nat.pow 2 pw in
match l with
| List.cons true xs => pwr + (bin2nat_aux xs pw')
| List.cons false xs => bin2nat_aux xs pw'
| _ => 0
end
end.
Definition bin2nat (l:list bool): nat := bin2nat_aux l ((List.length l)-1).
Fixpoint bin2nat_aux' (l:list bool) (pw:nat): nat :=
match l with
| List.cons true xs => Nat.pow 2 pw + (bin2nat_aux' xs (S pw))
| List.cons false xs => bin2nat_aux' xs (S pw)
| _ => 0
end.
Definition bin2nat' (l:list bool): nat := bin2nat_aux' l 0.
Definition padList (n:nat) (l:list bool): list bool :=
let sz := List.length l in
if Nat.leb n sz then l
else
List.app (List.repeat false (n-sz)) l.
Definition padList' (n:nat) (l:list bool): list bool :=
let sz := List.length l in
if Nat.leb n sz then l
else
List.app l (List.repeat false (n-sz)).
Definition shiftl (n:nat) (l:list bool): list bool :=
List.app (List.skipn n l) (List.repeat false n).
(*
Definition shiftr (l:list bool): list bool :=
List.cons false ().
*)
Compute shiftl 2 (List.cons true List.nil).
Compute shiftl 0 (nat2bin 10).
Compute shiftl 1 (nat2bin 10).
Compute shiftl 2 (nat2bin 10).
Compute shiftl 3 (nat2bin 10).
(****************** Trying out... ***************)
Compute nat2bin 0.
Compute nat2bin 1.
Compute nat2bin 2.
Compute nat2bin 3.
Compute nat2bin 4.
Compute nat2bin 5.
Compute nat2bin 6.
Compute nat2bin 7.
Compute nat2bin 8.
Compute nat2bin 9.
Compute nat2bin 10.
(* = (true :: false :: true :: false :: nil)%list *)
Compute padList 4 (nat2bin 0).
Compute padList 4 (nat2bin 1).
Compute padList 4 (nat2bin 2).
Compute padList 4 (nat2bin 3).
Compute padList 4 (nat2bin 4).
Compute padList 4 (nat2bin 5).
Compute padList 4 (nat2bin 6).
Compute padList 4 (nat2bin 7).
Compute padList 4 (nat2bin 8).
Compute padList 4 (nat2bin 9).
Compute padList 4 (nat2bin 10).
(* = (true :: false :: true :: false :: nil)%list *)
Compute bin2nat (nat2bin 0).
Compute bin2nat (nat2bin 1).
Compute bin2nat (nat2bin 2).
Compute bin2nat (nat2bin 3).
Compute bin2nat (nat2bin 4).
Compute bin2nat (nat2bin 5).
Compute bin2nat (nat2bin 6).
Compute bin2nat (nat2bin 7).
Compute bin2nat (nat2bin 8).
Compute bin2nat (nat2bin 9).
Compute bin2nat (nat2bin 10).
(* = 10 : nat *)
Compute bin2nat (padList 4 (nat2bin 0)).
Compute bin2nat (padList 4 (nat2bin 1)).
Compute bin2nat (padList 4 (nat2bin 2)).
Compute bin2nat (padList 4 (nat2bin 3)).
Compute bin2nat (padList 4 (nat2bin 4)).
Compute bin2nat (padList 4 (nat2bin 5)).
Compute bin2nat (padList 4 (nat2bin 6)).
Compute bin2nat (padList 4 (nat2bin 7)).
Compute bin2nat (padList 4 (nat2bin 8)).
Compute bin2nat (padList 4 (nat2bin 9)).
Compute bin2nat (padList 4 (nat2bin 10)).
(* = 10 : nat *)
Compute nat2bin' 0.
Compute nat2bin' 1.
Compute nat2bin' 2.
Compute nat2bin' 3.
Compute nat2bin' 4.
Compute nat2bin' 5.
Compute nat2bin' 6.
Compute nat2bin' 7.
Compute nat2bin' 8.
Compute nat2bin' 9.
Compute nat2bin' 10.
(* = (false :: true :: false :: true :: nil)%list *)
Compute bin2nat' (nat2bin' 0).
Compute bin2nat' (nat2bin' 1).
Compute bin2nat' (nat2bin' 2).
Compute bin2nat' (nat2bin' 3).
Compute bin2nat' (nat2bin' 4).
Compute bin2nat' (nat2bin' 5).
Compute bin2nat' (nat2bin' 6).
Compute bin2nat' (nat2bin' 7).
Compute bin2nat' (nat2bin' 8).
Compute bin2nat' (nat2bin' 9).
Compute bin2nat' (nat2bin' 10).
(* = 10 : nat *)
Compute bin2nat' (padList' 4 (nat2bin' 0)).
Compute bin2nat' (padList' 4 (nat2bin' 1)).
Compute bin2nat' (padList' 4 (nat2bin' 2)).
Compute bin2nat' (padList' 4 (nat2bin' 3)).
Compute bin2nat' (padList' 4 (nat2bin' 4)).
Compute bin2nat' (padList' 4 (nat2bin' 5)).
Compute bin2nat' (padList' 4 (nat2bin' 6)).
Compute bin2nat' (padList' 4 (nat2bin' 7)).
Compute bin2nat' (padList' 4 (nat2bin' 8)).
Compute bin2nat' (padList' 4 (nat2bin' 9)).
Compute bin2nat' (padList' 4 (nat2bin' 10)).

57
coq/union.v
View File

@ -1,10 +1,14 @@
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 (List.existsb (fun a => Nat.eqb x a) acc) then acc
if elementOf x acc then acc
else (List.cons x acc)
) l List.nil.
@ -13,17 +17,64 @@ Definition setify (l: list nat): list nat :=
Definition union (a b: list nat): list nat :=
let aset := setify a in
List.fold_left (fun acc y =>
if (List.existsb (fun x => Nat.eqb x y) acc) then acc
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 *)