Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with tactic-generated terms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with tactic-generated terms


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] problem with tactic-generated terms
  • Date: Fri, 12 Sep 2014 21:41:12 -0400

On 09/12/2014 07:59 PM, Robert Dockins wrote:

You can get this from the Hurkens paradox; see below.

Cheers,
Rob

--------------------------------------


Require Hurkens.

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


Definition er_out (X:Erasable Prop) : Prop
:= exists P, X = @erasable Prop P /\ P.

Theorem inconsistent : False.
Proof.
apply (Hurkens.paradox (Erasable Prop) (@erasable Prop) er_out).

intros.
destruct H as [P [H1 H2]].
apply Erasable_inj in H1.
subst A. trivial.

red; intros.
exists A; split; auto.
Qed.

Check inconsistent.
Print Assumptions inconsistent.


I needed to add Import Hurkens.NoRetractFromSmallPropositionToProp. and use "paradox" unqualified, for some reason - but otherwise it does work (I'm using a trunk version). Are things just as bad if I limit Erasable to be over Set instead of Type? That would be somewhat limiting, but maybe still sufficiently useful. Or, if there was a way to limit it to non-universe instances of Type?

Still - the proof (in Daniel Shepler's response) that it is incompatible with specific proof irrelevance is also upsetting - and that would remain even if limited to Set. Although I haven't yet required any variety of proof irrelevance.

Well, either I have to hope reality is sufficiently paraconsistent, or investigate an alternative erasability mechanism. Maybe the one Daniel Shepler is suggesting is suitable.

Or switch to Idris.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page