# Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

How do you prove that an Ascii character compares equal with itself in Coq idiomatically?

In the course of trying to prove a random exercise in Logical Foundations, I wanted to prove the following very simple lemma. This lemma is removed enough from the way a student is intended to prove the theorems in LF that I'm comfortable posting it in a public forum.

Lemma ascii_equals_self : forall x, Ascii.eqb x x = true.


I can prove this exhaustively by examining 256 goals in parallel, one for each boolean within Ascii.ascii.

Require Export Coq.Strings.String.

Lemma ascii_equals_self : forall x, Ascii.eqb x x = true.
Proof.
intros.
destruct x.
all:destruct b.
all:destruct b0.
all:destruct b1.
all:destruct b2.
all:destruct b3.
all:destruct b4.
all:destruct b5.
all:destruct b6.
all:auto.
Qed.


However, this is a little unsatisfying and it feels like there's a higher-level tactic or language feature that I could use to prove this quickly.

Looking at the definition of Ascii.eqb (shown below), it is defined using Bool.eqb. So we should prove facts about Ascii.eqb by using facts about Bool.eqb.

(* Output of "Print Ascii.eqb." *)
Ascii.eqb =
fun a b : Ascii.ascii =>
match a with
| Ascii.Ascii a0 a1 a2 a3 a4 a5 a6 a7 =>
match b with
| Ascii.Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
if
if
if
if
if
if if Bool.eqb a0 b0 then Bool.eqb a1 b1 else false
then Bool.eqb a2 b2
else false
then Bool.eqb a3 b3
else false
then Bool.eqb a4 b4
else false
then Bool.eqb a5 b5
else false
then Bool.eqb a6 b6
else false
then Bool.eqb a7 b7
else false
end
end
: Ascii.ascii -> Ascii.ascii -> bool


In Ascii.eqb x x, after destructing x, we will have 8 occurrences of Bool.eqb b b (for different b), which can be simplified by rewrite using a similar reflexivity lemma for Bool.eqb (Bool.eqb_reflx).

Require Export Coq.Strings.String.

Lemma ascii_equals_self : forall x, Ascii.eqb x x = true.
Proof.
unfold Ascii.eqb.
intros [].
(* Search Bool.eqb. *)
rewrite 8 Bool.eqb_reflx.
reflexivity.
Qed.

• This is the best answer, both technically and perspectivally. One should prove facts about definitions using API-like lemmas about its direct subcomponents, i.e. at as high a level as possible. Theories built on intrinsic rather than extrinsic definitions. This makes it more readable and resilient to change. Commented Jun 29 at 6:57

I mean, it's still exhaustive case analysis, but

intros [[] [] [] [] [] [] [] []]; reflexivity.


at least is shorter.

If you use ssreflect (probably not in the cards for LF), you can shorten it to repeat elim; reflexivity. or even just by repeat elim.

• To do something similar to ssreflect in vanilla Ltac you can for instance go for: intros []; repeat match goal with | b : bool |- _ => destruct b end; reflexivity. Commented Jun 27 at 4:37

Here is yet another way to write it (this is half way between your code and that in @djao's answer):

Require Export Coq.Strings.String.

Import Ascii.

Lemma ascii_equals_self : forall x,
eqb x x = true.
Proof.
intros [b0 b1 b2 b3 b4 b5 b6 b7].
destruct b0, b1, b2, b3, b4, b5, b6, b7.
all: reflexivity.
Qed.


But Search is your friend: when you require a library, the immediate way to find available definitions and theorems is with Search. Here, (assuming you have imported Ascii) if you just do a Search eqb, you discover you need proving nothing at all: that statement is already proven under the name eqb_refl.

Whence, proving it again (proving it under another name) is at most one line of code, as in a single apply. Or, even more directly:

Require Export Coq.Strings.String.

Import Ascii.

Definition ascii_equals_self : forall x,
eqb x x = true := eqb_refl.

• Inspecting the proof of that library lemma eq_bool at github.com/coq/coq/blob/master/theories/Strings/Ascii.v#L74 , one can see that it’s proven there using an ad hoc local tactic t_eqb, designed for several “easy” equality lemmas like this that are given there, which simply automatically repeatedly tries applying basic lemmas on equality of Booleans and destructing the goal. Commented Jun 28 at 9:58
• @PeterLeFanuLumsdaine Generally speaking, if I have to dig into a library's implementation details in order to use it, then the library is not good enough... Encapsulation is a name for this. Commented Jul 1 at 11:37

The low-tech way is to make the computer to the repetition for you. Use the repeat tactic to keep doing the same thing again and again until it stops having any effect. Use try … to try resolving the goals automatically. In this simple case, there are no goals left unsolved.

Require Export Coq.Strings.String.

Lemma ascii_equals_self : forall x, Ascii.eqb x x = true.
Proof.
intros.
repeat (destruct 0; try reflexivity).
Qed.


With data structures that are nontrivially inductive, you'll need induction 0 instead of destruct 0. With data structure that have many parts, replace 0 by the index of the part(s) that you want to descend into.

The downside of this kind of brute-force approach is that you don't have any control of which goals get left over. When your data structure is changing, or when the parts that can be solved automatically change, this can invalidate your proof code often.