## 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):

The type construct you ask about is `sumbool` .
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 `sumbool`in 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