Skip to main content
Proof Assistants Beta

Return to Question

Became Hot Network Question
edited title
Source Link
Greg Nisbet
Greg Nisbet
  • 3.1k
  • 4
  • 33

Less ridiculous way to prove that twoan Ascii characters arecharacter compares equal with itself in Coq

How do you prove that twoan Ascii characters comparecharacter 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.

Less ridiculous way to prove that two Ascii characters are equal in Coq

How do you prove that two Ascii characters compare equal 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.

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.

Source Link
Greg Nisbet
Greg Nisbet
  • 3.1k
  • 4
  • 33

Less ridiculous way to prove that two Ascii characters are equal in Coq

How do you prove that two Ascii characters compare equal 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.