Chapter 2.3.7 of Logical Foundations introduces definitions for "bit" and "nybble", followed by a boolean function "all_zero" that returns true if the nybble is "0000":
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Definition all_zero (nb : nybble) : bool :=
match nb with
| (bits B0 B0 B0 B0) => true
| (bits _ _ _ _) => false
end.
From that, I wanted to create a function that returns true if all the bits are equal, and the following looked like a natural solution to me:
Definition all_same (nb: nybble) : bool :=
match nb with
| (bits a a a a) => true
| (bits _ _ _ _) => false
end.
Alas, I the above yielded "The variable a is bound several times in pattern.". Of course, it's easy to find a working solution for this case:
Definition all_same (nb: nybble) : bool :=
match nb with
| (bits B0 B0 B0 B0) => true
| (bits B1 B1 B1 B1) => true
| (bits _ _ _ _) => false
end.
However, mentioning all cases seems rather inelegant, as changing "bit" for a type with 10 possible values would require 10 cases, and changing for an inductively defined type would require infinite cases, so the solution above doesn't suffice in the general case.
Knowing that, is it possible to use the same variable in different places in a definition to represent "if these are the same"? If not, how may one define "all_same" in a way that doesn't require mentioning every case?
As the error message suggests, you cannot have the same variable several times in a pattern. When you are using pattern-matching (thus the match construct), you are building a function that will compute. If some branches were to be taken only when several parameters are equal then it would have to decide equality for them.
You can use this approach more logically by using inductive types:
Inductive all_same : nybble -> Prop :=
| all_same_bits : forall b, all_same (bits b b b b).
There is only one constructor to this predicate, which states that all_same (bits a b c d) holds if and only if a = b = c = d.
If you still want to write a function, then you have to decide the equality of your bits. For instance you could write a simple function:
Definition eqb (b1 b2 : bool) : bool :=
match b1, b2 with
| true, true => true
| false, false => true
| _, _ => false
end.
And then write your function by checking all four bits are equal.
Of course this equality of booleans is already defined, and properties are proven about it. And you will have decidable equality for a lot of types, including natural numbers that are indeed infinite. That doesn't mean that deciding equality requires an infinite number of cases, we have fixed-points for that:
Fixpoint eqb_nat (n m : nat) : bool :=
match n, m with
| S n, S m => eqb_nat n m
| 0, 0 => true
| _, _ => false
end.