Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] LEM variants vs. proof relevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] LEM variants vs. proof relevance


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] LEM variants vs. proof relevance
  • Date: Mon, 30 May 2016 15:50:29 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f47.google.com
  • Ironport-phdr: 9a23:07Cc7BSfj4imZLDw1TW3/3uKENpsv+yvbD5Q0YIujvd0So/mwa64YB2N2/xhgRfzUJnB7Loc0qyN4/GmBDdLuMzR+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVPl4D3WDtKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7oW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKkkCLhsew19zOdJta+GbI9QjOk4L1sUwS5oCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==

Sorry, I got the induction principle wrong when translating from "forall aa, IsTrunc n (P aa)".  It should be

Module Export TruncP.
  Private Inductive PropTruncP (A : Prop) : Prop := tr : A -> PropTruncP A.
  Arguments tr [A] _.
  Axiom PropTruncP_trunc : forall {A : Prop} (x y : PropTruncP A), x = y.
  Definition TruncP_ind {A}
    (P : PropTruncP A -> Prop) {Pt : forall t (x y : P t), x = y}
  : (forall a, P (tr a)) -> (forall aa, P aa)
    := (fun f aa => match aa with tr a => fun _ => f a end Pt).
End TruncP.


On Mon, May 30, 2016 at 11:28 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:



On 05/28/2016 10:26 PM, Jason Gross wrote:
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?

It turns out that the Prop version of this Private trick, plus the proof relevance I'm working with, is inconsistent:

Module Export TruncP.
  Private Inductive PropTruncP (A : Prop) : Prop := tr : A -> PropTruncP A.
  Arguments tr [A] _.
  Axiom PropTruncP_trunc : forall {A : Prop} (x y : PropTruncP A), x = y.
  Definition TruncP_ind {A}
    (P : PropTruncP A -> Prop) {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 TruncP.

Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A.
Arguments erasable [A] _.
Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a=erasable b -> a=b. (*proof relevance*)

Inductive Foo : Prop := foo: bool -> Foo.

Definition foo2erasable(f : Foo) : Erasable bool :=
  match f with
    foo x => erasable x
  end.

Definition trunc_foo2erasable(f : PropTruncP Foo) : Erasable bool :=
  @TruncP_ind Foo (fun _ => Erasable bool) (fun _ _ => eq_refl) foo2erasable f.

Theorem inconsistent: False.
Proof.
  assert (tr (foo true) = tr (foo false)) as H by apply PropTruncP_trunc.
  apply f_equal with (f := trunc_foo2erasable) in H.
  cbv in H.
  apply Erasable_inj in H.
  discriminate.
Qed.


-- Jonathan





Archive powered by MHonArc 2.6.18.

Top of Page