## Stream: Coq users

### Topic: One-hot-encoding values

#### Julin Shaji (Mar 02 2024 at 18:03):

I was trying to make a type capable of representing one-hot-encoding.
As in a bit vector where exactly one bit is set.

So, I made this:

``````Require Import ssreflect.

(* Indices: size and a flag indicating whether the mark has been made *)
Inductive t: nat -> bool -> Type :=
| Mark: forall {n: nat},
t n false -> t (S n) true
| Pad: forall {n:nat} {b: bool},
t n b -> t (S n) b
| Zero: t 1 false
| One: t 1 true.
``````

Then I tried to prove that zero length values are impossible:

``````Goal forall (b: bool),
t 0 b -> False.
Proof.
move => b a.
case a eqn:Hcase.
Restart.
move => b.
elim.
- by [].
- by [].
-
(*
b : bool

========================= (1 / 1)

False
*)
``````

where I sort of paint myself into a corner with a goal to prove False
with just a bool as assumption.

Is there something wrong with encoding or is it that it isn't 'strong' enough?

Any idea?

I tried to find pre-existing one-hot-encoding representation in coq,
but couldn't spot any.

#### Julin Shaji (Mar 02 2024 at 18:28):

I guess this type would be okay as well?

``````Inductive t: nat -> bool -> Type :=
| Mark: forall {n: nat},
t n false -> t (S n) true
| Pad: forall {n:nat} {b: bool},
t n b -> t (S n) b
| Nil: forall (n:nat) (b:bool), t (S n) b.
``````

#### Julin Shaji (Mar 02 2024 at 18:28):

(Had a look at how `Fin.t` is defined)

#### Julin Shaji (Mar 02 2024 at 18:32):

Oh, I got the same problem with `Fin.t` as well:

``````Require Import Fin ssreflect.

Goal
Fin.t 0 -> False.
Proof.
elim.
- move => n.
(*
n : nat

========================= (1 / 1)

False
*)
``````

#### Gaëtan Gilbert (Mar 02 2024 at 19:27):

you can use `inversion` or prove a more general lemma (which is what inversion does)

``````Require Import Fin.

Goal Fin.t 0 -> False.
Proof.
intros x.
inversion x.
Qed.

Lemma lem : forall n, Fin.t n -> match n with 0 => False | S _ => True end.
Proof.
intros n x.
destruct x.
all:trivial.
Qed.

Goal Fin.t 0 -> False.
Proof.
exact (lem 0).
Qed.
``````

Last updated: Jun 23 2024 at 05:02 UTC