I am doing the exercises in Logic Foundations and got stuck on exercises requiring me to make proof objects that include iff-statements. For example

```
Definition or_distributes_over_and : forall P Q R : Prop,
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) :=
(* not sure how to destructure this *)
```

I expect there is a way to destruct the hypotheses for such a statement and then create a conjunction for directions of the iff-statement, but the book does not seem to mention how (or if that is possible). Does anybody know how to do this?

Best start your proof with `split`

or `constructor`

then you have to prove the two directions of the bi-implication

Yes but this is a definition not a proof.

is it required by the exercise to write it as a definition instead of a lemma?

Yes.

This is from the chapter on proof objects.

one of the proof objects I made for another exercise for instance:

```
Definition and_assoc : forall P Q R : Prop,
P /\ (Q /\ R) -> (P /\ Q) /\ R :=
fun P Q R HPQR => match HPQR with
| conj HP (conj HQ HR) => conj (conj HP HQ) HR
end.
```

well, this proof starts with `conj`

, not with a match

```
Definition or_distributes_over_and : forall P Q R : Prop,
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) := fun P Q R =>
conj (fun HPQR => ...) (fun HPQR' => ...)
```

`A <-> B`

is defined to be `(A -> B) /\ (B -> A)`

so you can use your usual way to deal with conjunctions

since the book mentions `Show Proof.`

, you could discover this by

```
Lemma or_distributes_over_and : forall P Q R : Prop,
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
split.
Show Proof.
```

the problem might be that the plan you describe is backwards.

I expect there is a way to destruct the hypotheses for such a statement and then create a conjunction for directions of the iff-statement

that doesn't work, because `A <-> B`

has no hypotheses. Instead, you create a conjunction of the two directions, and then _for each direction_ you have hypotheses you can manipulate.

Okay I guess I didn't see it like that. I find normal proofs easier than this tbh :sweat_smile:

Here is my solution:

```
Definition or_distributes_over_and : forall P Q R : Prop,
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) :=
fun P Q R => conj
(fun impl_l => match impl_l with
| or_introl HP => conj (or_introl HP) (or_introl HP)
| or_intror HQR => match HQR with
| conj HQ HR => conj (or_intror HQ) (or_intror HR)
end
end)
(fun impl_r => match impl_r with
| conj HPQ HPR => match HPQ with
| or_introl HP => or_introl HP
| or_intror HQ => match HPR with
| or_introl HP => or_introl HP
| or_intror HR => or_intror (conj HQ HR)
end
end
end).
```

Julia Dijkstra has marked this topic as resolved.

the `refine`

tactic might help do this incrementally — it lets you give proof objects with holes.

For instance after

```
Lemma or_distributes_over_and : forall P Q R : Prop,
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
```

you can write

```
refine (fun P Q R =>
conj (fun HPQR => _) (fun HPQR' => _)).
```

but also

```
refine (fun P Q R => _).
refine (conj _ _).
1: refine (fun HPQR => _).
2: refine (fun HPQR' => _).
```

I was not aware of the existence of refine, that actually makes writing these proof objects significantly easier!

Last updated: Jun 22 2024 at 15:01 UTC