[coq] bitvectors and 'sets'
This commit is contained in:
parent
12fdca2fa9
commit
6a5dbec769
|
@ -1,5 +1,7 @@
|
||||||
#+TITLE: Coq
|
#+TITLE: Coq
|
||||||
|
|
||||||
|
- [[./union.v][union.v]]: Mimicking a set operation using lists
|
||||||
|
- [[./bv.v][bv.v]]: Demo of a few bitvector operations
|
||||||
- [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes.
|
- [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes.
|
||||||
- [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws
|
- [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws
|
||||||
- [[./eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin
|
- [[./eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin
|
||||||
|
|
42
coq/bv.v
42
coq/bv.v
|
@ -3,14 +3,16 @@ Require Vector.
|
||||||
Require List.
|
Require List.
|
||||||
|
|
||||||
(* Convert a nat list to a bitvector. Non-zero values are considered true *)
|
(* Convert a nat list to a bitvector. Non-zero values are considered true *)
|
||||||
Fixpoint list2Bvec (l:list nat) : Bvector.Bvector (List.length l) :=
|
Fixpoint list2Bvec_aux (l:list nat) : Bvector.Bvector (List.length l) :=
|
||||||
match l return Bvector.Bvector (List.length l) with
|
match l return Bvector.Bvector (List.length l) with
|
||||||
| List.cons O xs =>
|
| List.cons O xs =>
|
||||||
Bvector.Bcons false _ (list2Bvec xs)
|
Bvector.Bcons false _ (list2Bvec_aux xs)
|
||||||
| List.cons _ xs =>
|
| List.cons _ xs =>
|
||||||
Bvector.Bcons true _ (list2Bvec xs)
|
Bvector.Bcons true _ (list2Bvec_aux xs)
|
||||||
| List.nil => Bvector.Bnil
|
| List.nil => Bvector.Bnil
|
||||||
end.
|
end.
|
||||||
|
Definition list2Bvec (l:list nat) : Bvector.Bvector (List.length (List.rev l)) :=
|
||||||
|
list2Bvec_aux (List.rev l).
|
||||||
|
|
||||||
(* Convert a bitvector to nat. Little-endian representation assumed *)
|
(* Convert a bitvector to nat. Little-endian representation assumed *)
|
||||||
Fixpoint bvec2nat_aux {n:nat} (cur:nat) (bv:Bvector.Bvector n): nat :=
|
Fixpoint bvec2nat_aux {n:nat} (cur:nat) (bv:Bvector.Bvector n): nat :=
|
||||||
|
@ -23,24 +25,52 @@ Fixpoint bvec2nat_aux {n:nat} (cur:nat) (bv:Bvector.Bvector n): nat :=
|
||||||
Definition bvec2nat {n:nat} (bv:Bvector.Bvector n): nat := bvec2nat_aux 0 bv.
|
Definition bvec2nat {n:nat} (bv:Bvector.Bvector n): nat := bvec2nat_aux 0 bv.
|
||||||
|
|
||||||
(* Find nth bit of a bitvector *)
|
(* Find nth bit of a bitvector *)
|
||||||
Definition bvnth {z i:nat} (bv: Bvector.Bvector z) (pf:i<z): bool :=
|
Definition Bnth {z i:nat} (bv: Bvector.Bvector z) (pf:i<z): bool :=
|
||||||
Vector.nth_order bv pf.
|
Vector.nth_order bv pf.
|
||||||
|
|
||||||
|
(* Find list of set bits in a bitvector *)
|
||||||
|
Fixpoint find_set_bits {z:nat} (bv: Bvector.Bvector z) : list nat :=
|
||||||
|
match bv with
|
||||||
|
| Vector.cons _ x _ xs =>
|
||||||
|
if x then List.cons (z-1) (find_set_bits xs)
|
||||||
|
else (find_set_bits xs)
|
||||||
|
| Vector.nil _ => List.nil
|
||||||
|
end.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Require Import List.
|
Require Import List.
|
||||||
Import ListNotations.
|
Import ListNotations.
|
||||||
Compute list2Bvec [0;0;1;0]. (* 0100₂ ie, 4₁₀ *)
|
Compute list2Bvec [0;0;1;0]. (* 0100₂ ie, 4₁₀ *)
|
||||||
|
Check Bvector.BshiftL _ (list2Bvec [0;0;1;0]) false.
|
||||||
|
|
||||||
|
Check Vector.shiftrepeat (Vector.cons _ 0 _ (Vector.nil _)).
|
||||||
|
|
||||||
|
Require Import Vector.
|
||||||
|
|
||||||
|
|
||||||
|
Import VectorNotations.
|
||||||
|
Compute Bvector.BshiftL 1 (list2Bvec [0;0;1;0]) false.
|
||||||
(*
|
(*
|
||||||
= [false; false; true; false]
|
= [false; false; true; false]
|
||||||
: Bvector (length [0; 0; 1; 0])
|
: Bvector (length [0; 0; 1; 0])
|
||||||
*)
|
*)
|
||||||
Compute bvec2nat (list2Bvec [0;0;1;0]).
|
Compute bvec2nat (list2Bvec [0;0;1;0]).
|
||||||
|
(* = 2 : nat *)
|
||||||
|
Compute bvec2nat (list2Bvec [0;1;0;0]).
|
||||||
(* = 4 : nat *)
|
(* = 4 : nat *)
|
||||||
|
|
||||||
Compute bvnth (list2Bvec [0;0;1;0]) (_:2<_).
|
Compute Bnth (list2Bvec [0;0;1;0]) (_:2<_).
|
||||||
(* = true : bool *)
|
(* = true : bool *)
|
||||||
Compute bvnth (list2Bvec [0;0;1;0]) (_:1<_).
|
Compute Bnth (list2Bvec [0;0;1;0]) (_:1<_).
|
||||||
(* = false : bool *)
|
(* = false : bool *)
|
||||||
|
|
||||||
|
|
||||||
|
Compute find_set_bits (list2Bvec [0;0;1;0]). (* [2] : list nat *)
|
||||||
|
Compute find_set_bits (list2Bvec [1;0;1;0]). (* [2; 0] : list nat *)
|
||||||
|
|
||||||
|
Check Bvector.BshiftL .
|
||||||
|
|
||||||
Check Bcons.
|
Check Bcons.
|
||||||
|
|
||||||
Check Nat.pow.
|
Check Nat.pow.
|
||||||
|
|
|
@ -0,0 +1,31 @@
|
||||||
|
Require List.
|
||||||
|
|
||||||
|
(* 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
|
||||||
|
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 (List.existsb (fun x => Nat.eqb x y) acc) then acc
|
||||||
|
else (List.cons y acc)
|
||||||
|
) b aset.
|
||||||
|
|
||||||
|
(******************** Trying out... ********************)
|
||||||
|
|
||||||
|
Require Import List.
|
||||||
|
Import ListNotations.
|
||||||
|
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 *)
|
|
@ -0,0 +1,87 @@
|
||||||
|
stepAux :: Eq a => a -> [a] -> [a]
|
||||||
|
stepAux a (x:xs)
|
||||||
|
| a==x = a:stepAux a xs
|
||||||
|
| otherwise = []
|
||||||
|
stepAux a [] = []
|
||||||
|
|
||||||
|
|
||||||
|
-- returns: (result, remaining)
|
||||||
|
step :: Eq a => a -> [a] -> ([a], [a])
|
||||||
|
step a l =
|
||||||
|
let rv = stepAux a l in
|
||||||
|
(a:rv, drop (length rv) l)
|
||||||
|
|
||||||
|
|
||||||
|
pack :: Eq a => [a] -> [[a]]
|
||||||
|
pack [] = []
|
||||||
|
pack (x:xs) =
|
||||||
|
let (res, rem) = step x xs in
|
||||||
|
case rem of
|
||||||
|
[] -> [res]
|
||||||
|
_ -> res:pack rem
|
||||||
|
|
||||||
|
-- Test case of 9:
|
||||||
|
-- λ> pack ['a', 'a', 'a', 'a', 'b', 'c', 'c', 'a', 'a', 'd', 'e', 'e', 'e', 'e']
|
||||||
|
-- ["aaaa","b","cc","aa","d","eeee"]
|
||||||
|
|
||||||
|
encode :: Eq a => [a] -> [(Int, a)]
|
||||||
|
encode l = map (\x -> (length x, head x)) $ pack l
|
||||||
|
|
||||||
|
-- Test case of 10:
|
||||||
|
-- λ> encode "aaaabccaadeeee"
|
||||||
|
-- [(4,'a'),(1,'b'),(2,'c'),(2,'a'),(1,'d'),(4,'e')]
|
||||||
|
|
||||||
|
encodeMod :: Eq a => [a] -> [(Int, a)]
|
||||||
|
encodeMod l = foldr f [] $ pack l where
|
||||||
|
f x acc =
|
||||||
|
if length x/=1 then (length x, head x):acc
|
||||||
|
else acc
|
||||||
|
-- Test case of 11 (v1):
|
||||||
|
-- λ> encodeMod "aaaabccaadeeee"
|
||||||
|
-- [(4,'a'),(2,'c'),(2,'a'),(4,'e')]
|
||||||
|
|
||||||
|
data Multiplicity a
|
||||||
|
= Single a
|
||||||
|
| Multiple Int a
|
||||||
|
deriving Show
|
||||||
|
|
||||||
|
encodeMod' :: Eq a => [a] -> [Multiplicity a]
|
||||||
|
encodeMod' l = foldr f [] $ pack l where
|
||||||
|
f x acc =
|
||||||
|
if length x/=1 then (Multiple (length x) (head x)):acc
|
||||||
|
else (Single (head x)):acc
|
||||||
|
-- Test case of 11 (v2):
|
||||||
|
-- λ> encodeMod' "aaaabccaadeeee"
|
||||||
|
-- [Multiple 4 'a',Single 'b',Multiple 2 'c',Multiple 2 'a',Single 'd',Multiple 4 'e']
|
||||||
|
|
||||||
|
|
||||||
|
decode :: [Multiplicity a] -> [a]
|
||||||
|
decode l = foldr f [] l where
|
||||||
|
f (Single a) acc = a:acc
|
||||||
|
f (Multiple n a) acc = (replicate n a) ++ acc
|
||||||
|
|
||||||
|
-- Test case of 12:
|
||||||
|
-- λ> decode (encodeMod' "aaaabccaadeeee")
|
||||||
|
-- "aaaabccaadeeee"
|
||||||
|
--
|
||||||
|
-- λ> decode (encodeMod' "aaaabccaadeeee") == "aaaabccaadeeee"
|
||||||
|
-- True
|
||||||
|
|
||||||
|
|
||||||
|
encodeDirectAux :: Eq a => a -> [a] -> Int
|
||||||
|
encodeDirectAux a [] = 0
|
||||||
|
encodeDirectAux a (x:xs)
|
||||||
|
| x==a = 1 + (encodeDirectAux a xs)
|
||||||
|
| otherwise = 0
|
||||||
|
|
||||||
|
encodeDirect :: Eq a => [a] -> [Multiplicity a]
|
||||||
|
encodeDirect [] = []
|
||||||
|
encodeDirect (x:xs) =
|
||||||
|
let rv = encodeDirectAux x xs in
|
||||||
|
case rv of
|
||||||
|
0 -> (Single x):encodeDirect xs
|
||||||
|
_ -> Multiple (rv+1) x : encodeDirect (drop rv xs)
|
||||||
|
|
||||||
|
-- Test case of 13:
|
||||||
|
-- λ> encodeDirect "aaaabccaadeeee"
|
||||||
|
-- [Multiple 4 'a',Single 'b',Multiple 2 'c',Multiple 2 'a',Single 'd',Multiple 4 'e']
|
Loading…
Reference in New Issue