[coq] add one hot encoding

coq/ohe.v

@@ -0,0 +1,192 @@
+(* One hot encoding *)
+From mathcomp Require Import all_ssreflect.
+
+(* Parameters: size and a flag indicating whether the mark has been made *)
+(* Valid values have flag set to true *)
+Inductive t: nat -> bool -> Type :=
+| Nil: t 0 false
+| Pad: forall {n: nat} {b: bool},
+    t n b -> t (S n) b
+| Mark: forall {n: nat},
+    t n false -> t (S n) true.
+
+Fixpoint markCount_aux {n: nat} {b: bool} (a: t 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 true): nat := 
+  markCount_aux a.
+
+Lemma lmCountMark: forall (n: nat) (b: bool) (a: t n b),
+ markCount_aux a = if b then 1 else 0.
+Proof.
+  move => n b a.
+  elim: a => //=.
+  by move => n' a' ->.
+Qed.
+  
+Lemma lmCountMarkTrue: forall (n: nat) (a: t n true),
+  markCount a = 1.
+Proof.
+  move => n a.
+  exact: (lmCountMark n true a).
+Qed.
+
+(*
+The command has indeed failed with message:
+Illegal application: 
+The term "@markCount" of type "forall n : nat, t n true -> nat"
+cannot be applied to the terms
+ "n0" : "nat"
+ "t" : "t n0 b"
+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))))).
+
+
+
+Fixpoint genPad (z: nat): t z false :=
+  match z with
+  | O => Nil
+  | S z' => Pad (genPad z')
+  end.
+
+Fixpoint padL {n: nat} (a: t n true) (z: nat): t (z+n) true.
+refine (
+  match z with
+  | O => _
+  | S z' => Pad (padL n a z')
+  end).
+by [].
+Defined.
+
+
+Fixpoint padR {n: nat} {b: bool} (a: t n b) (z: nat): t (z+n) b.
+refine (
+  match a with
+  | Nil => _
+  | Pad _ _ a' =>
+      match z with
+      | O => _
+      | S z' => _
+      end
+  | Mark _ a' =>
+      match z with
+      | O => _
+      | S z' => _
+      end
+  end).
+- rewrite addn0.
+  exact: genPad z.
+- rewrite add0n.
+  exact: (Pad a').
+- rewrite addSnnS.
+  exact: padR _ _ (Pad (Pad a')) z'. 
+- rewrite add0n.
+  exact: Mark a'.
+- rewrite addSnnS.
+  exact: padR _ _ (Pad (Mark a')) z'.
+Defined.
+
+Compute padL (Pad (Mark Nil)) 3.
+Compute padR (Pad (Mark Nil)) 3.
+
+Example eg := Eval compute in padR (Pad (Mark Nil)) 3.
+Require Import Extraction.
+Extraction Language Haskell.
+Recursive Extraction eg.
+(*
+data T =
+   Nil
+ | Pad Nat Bool T
+ | Mark Nat T
+
+eg :: T
+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. *)
+