The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hum:

Variable P:Prop.

Goal (P \/ (P \/ ~P -> ~P)) <-> (P \/ ~P).
Proof.
  tauto.
Qed.

Exercise: why is it clear?

Remark: tauto is complete on propositional logic.

​

On 28 May 2016 at 22:33, Jonathan Leivent <jonikelee AT gmail.com> wrote:

After some more thought - maybe the simple and direct route is better - which works even without proof relevance:

Axiom irrelevant_sibling : forall P, {Q | (Q <-> P) /\ (forall a b : Q, a = b)}.

Definition piP (p : Prop) : Prop.
Proof.
  destruct (irrelevant_sibling p) as (q & i & e). exact q.
Defined.

Lemma piP_iff_P : forall P, piP P <-> P.
Proof.
  unfold piP. intro p.
  destruct (irrelevant_sibling p) as (q & i & e). exact i.
Qed.

Lemma piP_irrelevant : forall P (a b : piP P), a = b.
Proof.
  unfold piP. intro p.
  destruct (irrelevant_sibling p) as (q & i & e). exact e.
Qed.

It's still required that irrelevant_sibling not imply proof irrelevance...  It certainly looks weaker...

-- Jonathan