Stream: Coq users

Topic: Distributive facts for Prop

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.

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.

Théo Winterhalter (Apr 07 2021 at 09:33):

Or even just firstorder..

Andrej Dudenhefner (Apr 07 2021 at 09:33):

or tauto

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.

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: Oct 13 2024 at 01:02 UTC