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

```
Inductive base : Type :=
| C (* cytosine *)
| G (* guanine *)
| A (* adenine *)
| 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:

- Is there an easier way to prove it?
- 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!

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.
```

About your subgoal.

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

too.

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!

About your subgoal.

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

too.

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

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.

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

Jiahong Lee has marked this topic as resolved.

Last updated: Jun 24 2024 at 00:02 UTC