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

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.

About your subgoal.
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!

About your subgoal.
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 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: Apr 18 2024 at 22:02 UTC