Hugh Sipiere (Nov 07 2020 at 19:02): 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.
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.
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.
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.
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.
you can prove it
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.
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: Oct 01 2023 at 18:01 UTC