Different theorems, identical proof script

Using Coq
1

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?

2

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.

2 Likes
3

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