Stream: Coq users

Topic: ✔ Show that (false -> Q) holds?

Jiahong Lee (Jun 07 2022 at 06:25):

Thanks, discriminate does the job for me. My updated solution:

Theorem andb_true_elim2'' : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros [].
  - simpl andb.
    intros c H.
    apply H.
  - discriminate.
Qed.

As for easy and now, they are too much magic for me right now. So, I'll leave them for future usage.

Notification Bot (Jun 07 2022 at 06:28):

Jiahong Lee has marked this topic as resolved.

Last updated: Feb 08 2023 at 23:03 UTC