The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/28/2016 12:48 PM, Gérard Huet wrote:
> What you are toying with in the free Heyting algebra generated by one element 
> (P).
> It is not finite, this is Nishimura’s lattice. Your infinite regress is going 
> up this lattice, but True is unreacheable by unions of P’s and ~P’s (in 
> intuitionistic propositional calculus).
> P \/ (P \/ ~P -> ~P) is not just stating the obvious, anymore than his sister at 
> the first level ~P->P.
>
> GH

I confess that that's over my head, so I'm not sure if it helps me 
towards the goal.

Attached is what I'm working towards.  I just need to be sure the 
lemlike hypothesis does not imply proof irrelevance...

-- Jonathan

> > Le 28 mai 2016 à 17:47, Jonathan Leivent 
> > <jonikelee AT gmail.com>
> >  a écrit :
> >
> > Coq.Logic.ClassicalFacts shows that excluded middle (LEM) implies proof irrelevance.  I'm working with a form of 
> > proof relevance, but would still like some alternative to LEM - which would allow       me to have "forall 
> > P, P \/ something else about P" that would still form an excluded middle in that both sides of the 
> > "\/" could not be true at the same time.  Because, it looks like if I can have such a thing, then I can 
> > get the benefits of proof irrelevance without full proof irrelevance:  It would allow me to easily find for any 
> > arbitrary Prop P, a P' such that P <-> P' and P' is irrelevant (forall p q : P', p = q).  As pointed out in 
> > the "Proof irrelevant Specif?" thread, coincidentally, this is already possible in Coq without any 
> > axioms for all P that are type-decidable ({P}+{~P}) - because that allows a version of P that is a boolean 
> > predicate.  The form of proof relevance I'm working with makes it the case for any P that is prop-decidable (P \/ 
> > ~P : locally LEM).  This last bit I'm looking for would make it the case for all P period.
> > The first thing I though of was "forall P, P \/ (P \/ ~P -> ~P)".  Interestingly, this is 
> > not a tautology in Coq (at least tauto doesn't think so), but it seems like it's just stating the 
> > obvious.  Could it be possible that "forall P, P \/ (P \/ ~P -> ~P)" does not imply proof 
> > irrelevance?  If so, then it's just what I need.
> > Otherwise, there is an infinite regress of these:
> >
> > Fixpoint nlem(n : nat)(P : Prop) :=
> > P \/ (match n with
> >        | 0 => True
> >        | S m => nlem m P
> >        end -> ~P).
> >
> > Arguments nlem : simpl nomatch.
> >
> > Lemma nlem0_is_lem : (forall P, nlem 0 P) <-> (forall P, P \/ ~P).
> > Proof.
> >    cbn. split; intros H P.
> >    all: specialize (H P); tauto.
> > Qed.
> >
> > Lemma nlem1_is_ : (forall P, nlem 1 P) <-> (forall P, P \/ (P \/ ~P -> ~P)).
> > Proof.
> >    cbn. split; intros H P.
> >    all: specialize (H P); tauto.
> > Qed.
> >
> > Lemma nlem_inc : forall n P, nlem n P -> nlem (S n) P.
> > Proof.
> >    cbn. destruct n.
> >    - cbn in *. tauto.
> >    - destruct n. all: cbn in *; tauto.
> > Qed.
> >
> > If not "nlem 1 P", what about "nlem n P" for some high enough n?
> >
> > As it turns out, I really only need to claim the existence of some arbitrary 
> > "something else about P":
> >
> > Axiom lemlike : forall (P:Prop), exists (Q:Prop), (P \/ Q) /\ (P /\ Q -> 
> > False).
> > Might that be safe enough (not imply proof irrelevance)?
> > -- Jonathan

Require Eqdep_dec.
Section PIP.
  Variable pbool : Prop.
  Variables ptrue pfalse : pbool.
  Hypotheses pbool_binary : forall b, b = ptrue \/ b = pfalse.
  (*Proof relevance of pbool means it can be discriminable:*)
  Hypothesis pbool_discriminable : pfalse <> ptrue.
  
  Let pbool_discriminable_sym := not_eq_sym pbool_discriminable.

  Lemma pbool_dec : forall (a b : pbool), a=b \/ a<>b.
  Proof.
    intros. destruct (pbool_binary a), (pbool_binary b); subst. all:intuition contradiction.
  Qed.

  (*An alternative to LEM that hopefully does not imply proof irrelevance:*)
  Hypothesis lemlike : forall (P:Prop), exists (Q:Prop), (P \/ Q) /\ (P /\ Q -> False).

  Definition P2pbool P : pbool :=
    match lemlike P with
    | ex_intro _ _ (conj (or_introl _) _) => ptrue
    | ex_intro _ _ (conj (or_intror _) _) => pfalse
    end.

  (*for any P, piP P is an irrelevant equivalent to P:*)
  Definition piP(P : Prop) := P2pbool P = ptrue.

  Lemma piP_iff_P : forall P, piP P <-> P.
    intro p. cbv. destruct (lemlike p) as (?&()&?). all:intuition contradiction.
  Qed.

  Lemma piP_is_irrelevant{P}(a b : piP P) : a = b.
  Proof.
    apply Eqdep_dec.eq_proofs_unicity. apply pbool_dec.
  Qed.
  
End PIP.