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

[coq] update ohe.v to add of_bv

This commit is contained in:
Julin S 2024-03-05 22:54:43 +05:30
parent 89a3ab876a
commit 391e3de385
1 changed files with 25 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

104
coq/ohe.v
View File

@ -1,5 +1,8 @@
(* One hot encoding *)
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
Require Import Bvector.
(* Parameters: size and a flag indicating whether the mark has been made *)
(* Valid values have flag set to true *)
@ -19,6 +22,18 @@ Fixpoint markCount_aux {n: nat} {b: bool} (a: t n b): nat :=
Definition markCount {n: nat} (a: t n true): nat :=
markCount_aux a.
Definition to_bv {n: nat} (a: t n true): Bvector n.
move: n a => n.
elim.
- exact: [].
- move => n' b a' bv'.
exact: (false :: bv').
- move => n' a' bv'.
exact: (true :: bv').
Defined.
Lemma lmCountMark: forall (n: nat) (b: bool) (a: t n b),
markCount_aux a = if b then 1 else 0.
Proof.
@ -45,20 +60,20 @@ The 2nd term has type "t n0 b" which should be a subtype of
"t n0 true".
*)
Check Nil.
Check Pad (Mark Nil).
Check Mark (Pad Nil).
Check Pad (Mark (Pad Nil)).
Fail Check Mark (Pad (Mark (Pad Nil))).
Check Pad (Pad (Mark (Pad Nil))).
Compute (markCount (Pad (Mark Nil))).
Compute (markCount (Mark (Pad Nil))).
Compute (markCount (Pad (Mark (Pad Nil)))).
Compute (markCount (Pad (Pad (Mark (Pad Nil))))).
Example eg1: t 0 false := Nil.
Example eg2: t 2 true := Pad (Mark Nil).
Example eg3: t 2 true := Mark (Pad Nil).
Example eg4: t 3 true := Pad (Mark (Pad Nil)).
Example eg5: t 4 true := Pad (Pad (Mark (Pad Nil))).
Compute markCount eg2.
Compute markCount eg3.
Compute markCount eg4.
Compute markCount eg5.
Compute to_bv eg5.
Fixpoint genPad (z: nat): t z false :=
match z with
@ -121,72 +136,3 @@ eg =
Pad (S (S (S (S O)))) True (Pad (S (S (S O))) True (Pad (S (S O)) True (Pad
(S O) True (Mark O Nil))))
*)
(*(1* From mathcomp Require Import all_ssreflect. *1) *)
(*(1* Set Bullet Behavior "Strict Subproofs". *1) *)
(*(1* *)
(*Requirements: *)
(* - Exactly one marked bit *)
(* - Size = n *)
(**) *)
(*(1* Parameters: size and a flag indicating whether the mark has been made *1) *)
(*(1* Valid only if flag is true *1) *)
(*Inductive taux: nat -> bool -> Type := *)
(*| Nil: taux 0 false *)
(*| Pad: forall {n: nat} {b: bool}, *)
(* taux n b -> taux (S n) b *)
(*| Mark: forall {n: nat}, *)
(* taux n false -> taux (S n) true. *)
(*Check Nil. *)
(*Check Pad (Mark Nil). *)
(*Check Mark (Pad Nil). *)
(*Check Pad (Mark (Pad Nil)). *)
(*Fail Check Mark (Pad (Mark (Pad Nil))). *)
(*Check Pad (Pad (Mark (Pad Nil))). *)
(*Definition t (n: nat): Type := taux (S n) true. *)
(*Fixpoint markCount_aux {n: nat} {b: bool} (a: taux n b): nat := *)
(* match a with *)
(* | Nil => 0 *)
(* | Pad a' => markCount_aux a' *)
(* | Mark a' => S (markCount_aux a') *)
(* end. *)
(*Definition markCount {n: nat} (a: t n): nat := *)
(* markCount_aux a. *)