coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mysterious type of sig for predicates on identity types

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Mysterious type of sig for predicates on identity types
Date: Wed, 16 Nov 2016 18:13:30 +0000
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-qk0-f179.google.com
Ironport-phdr: 9a23:smCEBhY2mdU6dPdqvu25Sqn/LSx+4OfEezUN459isYplN5qZoM25bnLW6fgltlLVR4KTs6sC0LuN9fm8EjVZud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ihi6txjdu8YZjYd/N6o91gbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2uqRxwwY7abo+WOvRjYK3SYcgXSnBdUstLTSFNHp+wYokJAuEcPehYtY79p14WoBW6HwasH+TvyjlVjXH3x6061P8hERrb1wEnHdIBqm/UrNLzNKcdS+C1y7LIzS7HYv5N1jf97ZLHchElof2WQb1wds/RxFApGgjYjVuQsZToMy2J2ukJqWSW7OptWfixh2I5tw19uCWjy8Uoh4TPm4kb0ErL9T9jz4YwPdC4SFB0YdqjEJZIsiGVLYp2Qsc7T2FxuyY21qQKuZCmcCUIzJkr3RHfa/uAc4iH5hLsSvydLit/hHJgYL6/hhCy/la8yuDkSMW4zFJHojBGn9TMrHwByQLf5tSdRvdg/Eqs3S6D1wXJ5eFFJUA0m7DbK5kkwrMolJocq1/DHijwmEX5lq+WcV4k+vOs5un8bbXmo4WTN45wig3kLqsuncm/DfwiMgcSR2ib5fi81Lr78ELlR7VKl+Q6nbXdsJDHPssWvbW5Ag9Q0oY78RmzFTam0NICnXkGNl1JYhyHj5K6c23Jdfv/FLK0h0mmuDZt3fHPeLP7UbvXKX2Wsr76erA1xFRb0xF7mdJW/JVSBasGO+mickD0vd3cSBQ+NlrnkK7cFNxh29ZGCiq0CaiDPfaKvA==

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
>

[Coq-Club] Reduction rule for fixpoints, Randy Pollack, 11/14/2016
- Re: [Coq-Club] Reduction rule for fixpoints, Maxime Dénès, 11/14/2016
  - Re: [Coq-Club] Reduction rule for fixpoints, Maxime Dénès, 11/14/2016
  - Re: [Coq-Club] Reduction rule for fixpoints, Pierre Courtieu, 11/14/2016
    - Re: [Coq-Club] Reduction rule for fixpoints, Randy Pollack, 11/14/2016
- [Coq-Club] Mysterious type of sig for predicates on identity types, Dominique Larchey-Wendling, 11/16/2016
  - Re: [Coq-Club] Mysterious type of sig for predicates on identity types, Jason Gross, 11/16/2016
    - Re: [Coq-Club] Mysterious type of sig for predicates on identity types, Dominique Larchey-Wendling, 11/16/2016