5
$\begingroup$

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.

Improve this question
$\endgroup$
1

4 Answers 4

Reset to default
8
$\begingroup$

Follow the structure of the function you are proving things about.

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.
Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Feryll
    Commented 2 days ago
7
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 3
    $\begingroup$ 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. $\endgroup$
    – Yannick Zakowski
    Commented Jun 27 at 4:37
4
$\begingroup$

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.
Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Jun 28 at 9:58
3
$\begingroup$

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.

Improve this answer
New contributor
Gilles 'SO- stop being evil' is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.