Stream: Coq users

Topic: One-hot-encoding values


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Mar 02 2024 at 18:28):

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

view this post on Zulip 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
*)

view this post on Zulip 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