Stream: Coq users

Topic: sf help


view this post on Zulip Hugh Sipiere (Nov 07 2020 at 19:02):

Reading Software Foundations and trying to prove when c:bool, false && c = true -> c = true; is there a way to avoid getting a hypothesis after simplification of true = false? In this case b && c = c if b else false, so I can't see how to avoid it. The proof works but is odd.

view this post on Zulip Yishuai Li (Nov 07 2020 at 23:38):

Before proving this theorem in Coq, consider what its informal proof looks like:
We want to show that for all c such that false && c = true, c must be equal to true. However, there's no such c that false && c = true, thus there's no goal for us to prove. QED.

view this post on Zulip Hugh Sipiere (Nov 08 2020 at 12:22):

Ahh thanks Yishuai Li, I realise I think it is because I haven't gotten far enough in the book for a neater proof. My problem is that false = true is a False statement so any right hand side however ridiculous will always hold. I haven't defined equality or a logic on booleans though so false = true does not simplify to False, maybe I should go back to this problem when I learn more.

Inductive bool : Type :=
  | true
  | false.

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Theorem zulip : forall c : bool,
  false && c = true -> c = true.
Proof.
  intros c. simpl. intros H. destruct c.
  {reflexivity. } {rewrite -> H. reflexivity. } Qed.

view this post on Zulip Gaëtan Gilbert (Nov 08 2020 at 12:32):

not sure I understand the question but you may want to compare with the proof

Theorem zulip : forall c : bool,
  false && c = true -> c = true.
Proof.
  intros c. simpl. intros H. inversion H.
Qed.

view this post on Zulip Hugh Sipiere (Nov 08 2020 at 12:58):

Ahh thanks for the proof, sorry for bad question. Is defining an axiom for boolean equivalence a bad solution? It looks like I can't prove it.

Axiom false_equiv_False:
  false = true <-> False.

Theorem zulip : forall c : bool,
  false && c = true -> c = true.
Proof.
  intros c. simpl. rewrite -> false_equiv_False. intros [].
  Qed.

view this post on Zulip Gaëtan Gilbert (Nov 08 2020 at 13:28):

you can prove it

view this post on Zulip Andrew Miloradovsky (Nov 08 2020 at 13:40):

Yep, it's provable without additional axioms.

The general strategy is to first destruct, eliminate, perform case analysis or induction over, or inversion of the hypotheses to obtain the arguments which went into the constructor, and then construct the goal with the extracted terms.

view this post on Zulip Andrew Miloradovsky (Nov 08 2020 at 13:48):

Metaphorically speaking, proving a theorem is like building a device from other devices' parts: you first disassemble the devices to extract the parts, and the assemble the parts together to form a new device. The devices in this case are hypotheses/variables (inductive types), and the parts are their constructors.


Last updated: Jan 28 2023 at 06:30 UTC