# Different theorems, identical proof script

**URL:** <https://discourse.rocq-prover.org/t/different-theorems-identical-proof-script/640>\
**Category:** Using Rocq\
**Created:** [February 25, 2020, 3:00pm UTC](https://discourse.rocq-prover.org/t/different-theorems-identical-proof-script/640 "2020-02-25T15:00:46Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [February 25, 2020, 3:00pm UTC](https://discourse.rocq-prover.org/t/different-theorems-identical-proof-script/640/1 "2020-02-25T15:00:46Z")

</div>

Consider these two results that say something about distributivity of implication.

> Lemma split\_or\_\_0ary:  
> ∀ (f g h: Prop), (f ∨ g → h) ↔ (f → h) ∧ (g → h).
> 
> Lemma split\_or\_\_1ary:  
> ∀ T (f g h: T → Prop), (∀ x: T, f x ∨ g x → h x) ↔ (∀ x: T, f x → h x) ∧ (∀ x: T, g x → h x).

Note that they apply in different situations. For example, _split\_or\_\_0ary_ cannot be used on a hypothesis such as _H : ∀ x0 : X, x = x0 ∨ x0 ∈ l1 → x0 ∈ l2_. So it seems useful to have both.

Both can be proven with the same proof script:

> Proof.
> 
> intros. split.
> 
> - intros. split.
> - intros. apply H. left. assumption.
> - intros. apply H. right. assumption.
> 
> - intros. destruct H. destruct H0.
> - apply H. assumption.
> - apply H1. assumption.
> 
> Qed.

I imagine that the same proof will apply to binary predicates and further.

Can I represent this result compactly, without repetition? What should it tell me about Coq and logic in general?

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [February 25, 2020, 4:20pm UTC](https://discourse.rocq-prover.org/t/different-theorems-identical-proof-script/640/2 "2020-02-25T16:20:41Z")

</div>

The proof terms are different, so it does not imply anything about Coq logic. With the same tactic-based reasoning you could even conclude that any two proofs of linear arithmetic are the same because they can be solved by `lia`, or that `auto` trivializes proof equivalence.

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [February 25, 2020, 8:35pm UTC](https://discourse.rocq-prover.org/t/different-theorems-identical-proof-script/640/3 "2020-02-25T20:35:19Z")

</div>

> Can I represent this result compactly, without repetition?

You could write a tactic that solves both goals. Or use the pre-defined  
tactic `intuition` (or `firstorder`), which solve both of your goals.

> What should it tell me about Coq and logic in general?

It just says that both your goals are easy to solve goals in first order  
with a somewhat similar shape.

– Maximilian