The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Well I did not think (sig P) could be of type Prop .... but it appears that (sig P : Prop) holds in the context A : Prop, P : A -> Prop.

I was very surprised by that ... I think I have not understood all the subtleties of Coq typing rules for inductive predicates.

So it is possible to destruct a proposition like exists x, P x in a Type context in that specific case with

the following induction principle:

Definition ex_rect (A : Prop) (P : A -> Prop) (Q : Type) : (forall x : A, P x -> Q) -> (exists x, P x) -> Q.
Proof.
  intros HA H.
  assert ({ x | P x}) as H1.
    destruct H as (x & ?); exists x; assumption.
  destruct H1 as (? & H1); revert H1; apply HA.
Qed.

Dominique

---

De: "Jason Gross" <jasongross9 AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Mercredi 16 Novembre 2016 19:13:30
Objet: Re: [Coq-Club] Mysterious type of sig for predicates on identity types

This does not break extraction.  Extraction erases Props.  This includes proofs of equality, and your sigma type where both components are Props.

On Wed, Nov 16, 2016, 6:41 AM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Hi all,

I did find out that { H : a = B | ... } has type Prop
under 8.5pl2 ? Why is this so ? This implies that
such a result allows to prove something like

Theorem strange X (P : forall x y, x = y -> Prop) (x y : X) :
   (exists H : x = y, P x y H) -> { H : x = y | P _ _ H }.
Proof.
  intros (H & ?); exists H; auto.
Qed.

Does this not break extraction ?

Best regards,

Dominique

-----

Le 14/11/2016 à 13:35, Randy Pollack a écrit :
> Page 134 of the reference manual (8.5pl2) describes the reduction rule
> for a fixpoint application:
>
> ================================
> The reduction for fixpoints is:
>    [...]
> when aki starts with a constructor. This last restriction is needed in
> order to keep strong normalization.
> ==================================
>
> Is is known if this last restriction is needed when the context in
> which the fixpoint application is well typed doesn't contain any
> axioms?  (References or examples?)
>
> What about for specific axioms, such as functional extensionality, axiom K, ...?
>
> Thanks,
> --Randy
>