## Stream: Coq users

### Topic: ✔ Constructing Proof Object with Iff

#### Julia Dijkstra (Dec 16 2023 at 16:37):

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?

#### Paolo Giarrusso (Dec 16 2023 at 16:46):

Best start your proof with `split` or `constructor`

#### Paolo Giarrusso (Dec 16 2023 at 16:46):

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

#### Julia Dijkstra (Dec 16 2023 at 16:47):

Yes but this is a definition not a proof.

#### Paolo Giarrusso (Dec 16 2023 at 16:47):

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

Yes.

#### Julia Dijkstra (Dec 16 2023 at 16:48):

This is from the chapter on proof objects.

#### Julia Dijkstra (Dec 16 2023 at 16:48):

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.
``````

#### Paolo Giarrusso (Dec 16 2023 at 16:49):

well, this proof starts with `conj`, not with a match

#### Paolo Giarrusso (Dec 16 2023 at 16:51):

``````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' => ...)
``````

#### Gaëtan Gilbert (Dec 16 2023 at 16:52):

`A <-> B` is defined to be `(A -> B) /\ (B -> A)` so you can use your usual way to deal with conjunctions

#### Paolo Giarrusso (Dec 16 2023 at 16:52):

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.
``````

#### Paolo Giarrusso (Dec 16 2023 at 16:53):

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.

#### Julia Dijkstra (Dec 16 2023 at 17:00):

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).
``````

#### Notification Bot (Dec 16 2023 at 17:00):

Julia Dijkstra has marked this topic as resolved.

#### Paolo Giarrusso (Dec 16 2023 at 17:07):

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' => _).
``````

#### Julia Dijkstra (Dec 16 2023 at 17:15):

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