Stream: Coq users

Topic: Distributive facts for Prop


view this post on Zulip Zhangsheng Lai (Apr 07 2021 at 08:47):

Is there any standard results for distributive results for Prop?

For example,

Theorem or_distributes_over_and_1 : ∀P Q R : Prop,
  P ∨ (Q ∧ R) → (P ∨ Q) ∧ (P ∨ R)

I can only find commutativity and associativity but no distributivity properties from here.

view this post on Zulip Kenji Maillard (Apr 07 2021 at 09:30):

I don't think the standard library makes any promise of exhaustivity; for an exhaustive "standard" library you should probably look at mathcomp, stdpp, etc.
Nonetheless, if needed the proof of this theorem is a one liner: Proof. intros ??? [p|[q r]]; [split ; left| split; right] ; assumption. Qed.

view this post on Zulip Théo Winterhalter (Apr 07 2021 at 09:33):

Or even just firstorder..

view this post on Zulip Andrej Dudenhefner (Apr 07 2021 at 09:33):

or tauto

view this post on Zulip Zhangsheng Lai (Apr 07 2021 at 11:02):

@Kenji Maillard @Théo Winterhalter @Andrej Dudenhefner thanks those suggestions will work for me. Just trying to use as much of the available library instead of rewriting them again. But it is surprising that we don't have them available considering we have others like or_comm and and_comm.

view this post on Zulip Théo Winterhalter (Apr 07 2021 at 11:04):

I think that considering that the proof can be done in a really short manner, no one really bothered providing them. But as Kenji pointed out, the library is not particularly exhaustive.
I usually start every coq project with a file for general facts like this (typically on lists).


Last updated: Jan 31 2023 at 14:03 UTC