The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can throw it in Prop if you want it to be erased in extraction (and then the eliminator also has to target Prop).  I believe the private inductive semantics forbid any new pattern matches outside the module.  At worst, this will break subject reduction (vm_compute might reject a well typed term, unfolding the induction scheme on neutral terms won't work nicely), but it won't lead to inconsistency.

On Sun, May 29, 2016, 9:53 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?

So, this relies on the semantics of Private to prevent
discrimination/destruction of PropTrunc instances outside the module.
This trick scares me a bit.  Does native_compute always obey this
restriction?  It disobeys opaqueness, so that's why I'm suspicious.  How
does this mix with extraction - will PropTruncs get erased as well as Props?

As for having an induction scheme - that might be useful...

-- Jonathan