The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/28/2016 04:56 PM, Arnaud Spiwack wrote:

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.

Oops ...  Hmm...  Looks like at one point I had "P \/ (P \/ ~P -> P)" instead - but that doesn't work.  OK - driver error. :-[

Does the irrelevant_sibling thing seem more promising?  That seems like as weak as it can be and still do the job.

-- Jonathan

​

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