coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] LEM variants vs. proof relevance, (continued)
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
Archive powered by MHonArc 2.6.18.