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.

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

Or even just `firstorder.`

.

or `tauto`

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

.

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: Jun 18 2024 at 10:02 UTC