Missing lemmas about Prop: absorbing or neutral elements for various operations

[SnarkBoojum]

I asked the question on zulip, but didn't get much feedback. At first I didn't find anything to rewrite True /\ P to P, but then I realized there might be other similar situations ; here is some code:

Require Import Setoid. (* FIXME: why!? *)
 
Section Missing.

Variable P: Prop.

Lemma and_true_l: True /\ P <-> P.
Proof.
split.
  intros [_ ?].
  assumption.
intros ?.
split.
  exact I.
assumption.
Qed.

Lemma and_true_r: P /\ True <-> P.
Proof.
rewrite and_comm.
exact and_true_l.
Qed.

Lemma and_false_l: False /\ P <-> False.
Proof.
split.
  intros [? _].
  assumption.
intros ?.
exfalso.
assumption.
Qed.

Lemma and_false_r: P /\ False <-> False.
Proof.
rewrite and_comm.
exact and_false_l.
Qed.

Lemma or_true_l: True \/ P <-> True.
Proof.
split.
  intros _.
  exact I.
intros ?.
left.
assumption.
Qed.

Lemma or_true_r: P \/ True <-> True.
Proof.
rewrite or_comm.
exact or_true_l.
Qed.

Lemma or_false_l: False \/ P <-> P.
Proof.
split.
  intro H.
  case H.
    intros ?.
    exfalso ; assumption.
  intros ?.
  assumption.
intros ?.
right.
assumption.
Qed.

Lemma or_false_r: P \/ False <-> P.
Proof.
rewrite or_comm.
exact or_false_l.
Qed.

Lemma impl_false_l: (False -> P) <-> True.
Proof.
split.
  intros _.
  exact I.
intros _ ?.
exfalso ; assumption.
Qed.

Lemma impl_true_l: (True -> P) <-> P.
Proof.
split.
  intro H.
  exact (H I).
intros ? _.
assumption.
Qed.

Lemma impl_true_r: (P -> True) <-> True.
Proof.
split.
  intros _.
  exact I.
intros _ _.
exact I.
Qed.

End Missing.

(Notice: I'm more used to writing proof in MC-style, so my proofs in pure Coq might be a bit awkward...)

They are supposed to be used for rewriting complex goals (which is why the existing False_ind and my impl_false_l might both make sense).

[mrhaandi]

Possibly, all of the above lemmas are solved by tauto.
In general, more complicated lemmas are addressed by the tactics tauto, intuition, and firstorder, which is the proper infrastructure for dealing with such statements.

[silene]

You found nothing to rewrite True /\ P to P because it is not possible to do so in the general case. Indeed, you can only rewrite between things that are equal. But short of some axioms, you do not have the equality (True /\ P) = P. So, Coq provides a fundamentally different mechanism for relations that are not pure equality, called "setoid rewriting". That is why you ended up loading the Setoid library. By doing so, you get a fundamentally different implementation of the rewrite tactic, which then lets you do things like rewrite and_comm. Documentation is here: https://coq.inria.fr/distrib/current/refman/addendum/generalized-rewriting.html

[SnarkBoojum]

@mrhaandi I thought using too-automatic tactics on lemmas was discouraged in Coq, in favor of more direct proofs ; but indeed tauto does them all.

@silene that explains the FIXME at the start.

As I explained, I had a complex goal and needed the first of the above lemmas to simplify things inside before proceeding further. Since it was inside, no simple tactic could help -- a rewriting was necessary.