I was trying to make a type capable of representing onehotencoding.
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 preexisting onehotencoding representation in coq,
but couldn't spot any.
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.
(Had a look at how Fin.t
is defined)
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
*)
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