CODEWITHSUNDEEP
coq
Denis
Denis

Reputation: 1555

Are those two proofs equivalent?

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

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.

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)?

Upvotes: 2

Views: 85

Answers (1)

Th&#233;o Winterhalter
Th&#233;o Winterhalter

Reputation: 5108

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.

Upvotes: 2

Related Questions