Stream: Coq users

Topic: ✔ Constructing Proof Object with Iff


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 16:46):

Best start your proof with split or constructor

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 16:46):

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

view this post on Zulip Julia Dijkstra (Dec 16 2023 at 16:47):

Yes but this is a definition not a proof.

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 16:47):

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

view this post on Zulip Julia Dijkstra (Dec 16 2023 at 16:47):

Yes.

view this post on Zulip Julia Dijkstra (Dec 16 2023 at 16:48):

This is from the chapter on proof objects.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 16:49):

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

view this post on Zulip 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' => ...)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Notification Bot (Dec 16 2023 at 17:00):

Julia Dijkstra has marked this topic as resolved.

view this post on Zulip 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' => _).

view this post on Zulip 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