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.

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.

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

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.

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: Jun 16 2024 at 01:42 UTC