Are those two proofs equivalent?

user_5688082 0
Viewed 71

I just finished the exercises in here: https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html; however I came up with 2 different proofs for following exercise https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#andb_true_elim2, and i would like to know

  • is my first attempt is completely non-sensical? While it works, it requires introducing hypothesis H : b && false = true which is obviously wrong. How come I am not stopped from introducing such statement?
Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct c.
  reflexivity.
  intro H.
  rewrite <- H.
  destruct b.
  reflexivity.
  reflexivity.
  Qed.
  • second attempt: No dubious hypothesis, and works.
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct b eqn:Eb.
  intro H.
  rewrite <- H.
  reflexivity.
  destruct c.
  reflexivity.
  discriminate.
  Qed.

Since Coq is happy with both proofs, they are equally good (I doubt this)?

coq
1 Answers

Having a False hypothesis is something common and not at all problematic in Coq. In fact, if you look at the negation of a proposition P, it is defined as P -> False. In other words, you can derive a contradiction from having P.

There is even the tactic exfalso which proves any goal as long as you provide a proof of False. This means that if you have contradictory hypotheses then you can conclude your proof.

Here is an even shorter proof:

Theorem andb_true_elim2 :
  forall b c : bool,
    andb b c = true ->
    c = true.
Proof.
  intros b c h.
  destruct b.
  - simpl in h. (* h : c = true *)
    exact h.
  - simpl in h. (* h : false = true *)
    discriminate h.
Qed.

I use the tactic discriminate which closes the goal by seeing that false = true is impossible because they are two distinct constructors of bool.

user_12759750
Related