## Stream: Coq users

### Topic: ✔ Destruct an enumerated datatype into FOO and not FOO?

#### Jiahong Lee (Jun 20 2022 at 03:36):

Hi, I'm self-learning Coq with this. Given these

Inductive base : Type :=
| C  (* cytosine *)
| G  (* guanine *)
| T. (* thymine *)

Definition eq_base (b1 b2 : base) : bool :=
match (b1, b2) with
| (C, C) => true
| (G, G) => true
| (A, A) => true
| (T, T) => true
| (_, _) => false
end.

I want to prove this:

Lemma eq_base_true : forall (b1 b2 : base),
eq_base b1 b2 = true -> b1 = b2.

Note that I have proven it by going through all the 16 combinations of b1 and b2. But I found it to be tedious.

So my questions are:

1. Is there an easier way to prove it?
2. Here is my own attempt. If I were to proceed as such:
Lemma eq_base_true : forall (b1 b2 : base),
eq_base b1 b2 = true -> b1 = b2.
Proof.
intros [] b2 H.
- (* b1 = C *)
unfold eq_base in H.

I obtain the goal:

-  b2 : base
-  H : match b2 with
| C => true
| _ => false
end = true
============================
C = b2

I would like to destruct b2 into C and not C to simplify my proof. How can I do that?

Thanks!

#### Pierre Castéran (Jun 20 2022 at 06:07):

Here is a shorter proof script.

Lemma eq_base_true : forall (b1 b2 : base),
eq_base b1 b2 = true -> b1 = b2.
Proof. destruct b1,b2; (reflexivity ||discriminate). Qed.

If you look at the proof term (by Print eq_base_true), you will notice that the 16 cases are all present.
It may be interesting to look also at the term generated by decide equality.

Definition base_eqdec : forall b b': base, {b=b'}+{b <> b'}.
decide equality.
Qed.

Print base_eqdec.

Note that you can also prove useful lemmas.

Lemma eq_base_xx (x:base) : eq_base x x = true.
Proof. case x; reflexivity. Qed.

Lemma eq_base_false:  forall x y:base, eq_base x y = false -> x <> y.
Proof. intros x y Heqf Heq. subst; now rewrite eq_base_xx in Heqf.
Qed.

You can solve it with destruct b2; (reflexivity || discriminate)too.

#### Jiahong Lee (Jun 20 2022 at 07:33):

Pierre Castéran said:

Here is a shorter proof script.

Lemma eq_base_true : forall (b1 b2 : base),
eq_base b1 b2 = true -> b1 = b2.
Proof. destruct b1,b2; (reflexivity ||discriminate). Qed.

If you look at the proof term (by Print eq_base_true), you will notice that the 16 cases are all present.

Wow, thanks! Just knew that I can apply a tactic to every destructed case with ; <tactic>. That's very handy!

It may be interesting to look also at the term generated by decide equality.

Definition base_eqdec : forall b b': base, {b=b'}+{b <> b'}.
decide equality.
Qed.

Print base_eqdec.

Hi, I'm just a beginner. May I know what is {} (its terminology) in Coq? What does it do? And why do you want to do this?

From the result of Print base_eqdec, it seems that it produces similar theorem as my eq_base_true. So, maybe one can use base_eqdec in place of eq_base_true?

Note that you can also prove useful lemmas.

Lemma eq_base_xx (x:base) : eq_base x x = true.
Proof. case x; reflexivity. Qed.

Lemma eq_base_false:  forall x y:base, eq_base x y = false -> x <> y.
Proof. intros x y Heqf Heq. subst; now rewrite eq_base_xx in Heqf.
Qed.

I see. Thanks!

You can solve it with destruct b2; (reflexivity || discriminate)too.

Thanks, now I prefer your solution as given above =D

#### Pierre Castéran (Jun 20 2022 at 14:20):

Among a lot of tutorials and books, I found this blog
https://smondet.github.io/blog/post/coqtests-02-sumbools.html which explains nicely the difference between sumbool and the plain boolean type.
But I think you will also find sumboolin any index of any book or tutorial on Coq.

#### Jiahong Lee (Jun 21 2022 at 00:56):

I see, thank you for pointing me to the blog post! It's way above my head right now, but I'll check it out again in the future

#### Notification Bot (Jun 21 2022 at 00:56):

Jiahong Lee has marked this topic as resolved.

Last updated: Sep 23 2023 at 07:01 UTC