The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Have you considered LEM on hProps?

  forall P, (forall x y : P, x = y) -> P \/ ~P

Together with propositional truncation / quotient types, this may give you want you want.  (I think these are similar to your irrelevant_sibling; you do:

  Module Export Trunc.

    Private Inductive PropTrunc A := tr : A -> PropTrunc A.

    Axiom PropTrunc_trunc : forall {A} (x y : PropTrunc A), x = y.

    Definition Trunc_ind {A}

      (P : PropTrunc A -> Type) {Pt : forall x y, P x = P y}

    : (forall a, P (tr a)) -> (forall aa, P aa)

    := (fun f aa => match aa with tr a => fun _ => f a end Pt).

  End Trunc.

)

Does this do what you want?

On Sat, May 28, 2016 at 5:14 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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