The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

To be retrospective, I indeed want to put all definitions into Type. However, there are external dependencies / historical development.

For example, I depend on a library which puts things into Prop, so if I don't operate in Prop, I will not be able to eliminate from definitions from this library. This library, in turn, depends on some definitions from stdlib, which are also defined in Prop.

I am not sure if stdlib2 plans to make things primarily in Type and make use of sProp whenever necessary. If that's the case, it would make the future much brighter.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Sent: March 22, 2019 7:09 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop

 

Why do you want your inductive to be in Prop? Is there a problem with
putting it in Set or Type?

Gaëtan Gilbert

On 22/03/2019 23:50, Jason -Zhong Sheng- Hu wrote:
> Hi,
>
> thanks again for all your help. I want to follow up on this question.
>
> Experimenting around, I found that most of the methods work only for
> those inductive types in which no recursive case live in closure (what's
> the terminology for this? it's free algebras generated by poly functors
> with at most 1st order). for example, following kind of definitions
> wouldn't work well:
>
> Inductive T : Prop := ... | ctor : (forall x, P x -> T) -> T | ...
>
> This kind of definitions appears, for example, in locally nameless
> representation [*]. Consider the case for subtyping between universal
> types in F<: (imagine the constructor to be `tabs` and a type opening
> operation `open`),
>
> case_tabs : forall L G S1 S2 U1 U2,
>                     G |- S2 <: S1 ->
>                     (forall x, x \notin L -> (x , S2) :: G |- open x U1
> <: open x U2) ->
>                     G |- tabs S1 U1 <: tabs S2 U2
>
> Notice that the body case lives in a closure. Therefore, the size of the
> derivation tree cannot be measured by natural numbers.
>
> I was exploring a more general counter. Consider following definition.
>
>    Inductive card : Type :=
>    | base : card
>    | rec1 : card -> card
>    | rec2 : card -> card -> card
>    | clsr : forall L, card -> (forall x, x `notin` L -> card) -> card.
>
> The intention of this definition is to form a simulation of Prop's
> containing recursive cases in closures. However, it turns out that I
> cannot prove this simulation exists, even with Fabian's trick. To
> understand the blocker, consider a modified version of case_tabs:
>
> case_tabs' : forall L G S1 S2 U1 U2 c1 c2,
>                     [ c1 ] G |- S2 <: S1 ->
>                     (forall x (ni : x \notin L), [ c2 x ni ] (x , S2) ::
> G |- open x U1 <: open x U2) ->
>                     [ clsr c1 c2 ] G |- tabs S1 U1 <: tabs S2 U2
> where card is contained in the square brackets preceding the judgment.
>
> when mapping from case_tabs to case_tabs', the inductive hypothesis becomes
>
> forall x, x \notin L -> exists c, [ c ] (x , S2) :: G |- open x U1 <:
> open x U2
>
> and I need to constructor a c2, which lives in Type. this cannot be
> proved because ex cannot be eliminated into Type. On the other hand,
> card needs to be defined in Type because it serves as size.
>
> I hope this problem makes sense. I once a while find Prop in Coq is so
> hard to work with and cumbersome to have. I am wondering if there is a
> way out?
>
> *Thanks,*
> *Jason Hu*
> *https://hustmphrrr.github.io/*
>
> [*] https://link.springer.com/article/10.1007/s10817-011-9225-2
>
> ****
> ------------------------------------------------------------------------
> *From:* Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
> *Sent:* February 4, 2019 9:36 AM
> *To:* Fabian Kunze; coq-club AT inria.fr
> *Subject:* Re: [Coq-Club] well-founded induction on the size of the
> derivation tree of Prop
> great, thx you all. I will try out these approaches.
>
> *Sincerely Yours,
> *
> *
> Jason Hu*
> ------------------------------------------------------------------------
> *From:* coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf
> of Fabian Kunze <kunze AT ps.uni-saarland.de>
> *Sent:* February 2, 2019 5:14 PM
> *To:* coq-club AT inria.fr
> *Subject:* Re: [Coq-Club] well-founded induction on the size of the
> derivation tree of Prop
> Hello Jason,
>
> One way to do this would be to add another parameter to your inductive
> predicate to track the 'size' of the tree. Then induction on this
> parameter works. (An example is the derivation of vectors of length n
> from list that adds the length as an explicit parameter.)
>
> If you don't want to change your definition, you can copy it with this
> parameter and show equivalence of the two inductive types ( P x <->
> exists n, P' n x).
>
> Best,
> Fabian
>
> On Sat, 2 Feb 2019, 22:54 Jason -Zhong Sheng- Hu, <fdhzs2010 AT hotmail.com
> <mailto:fdhzs2010 AT hotmail.com>> wrote:
>
>     Hi,
>
>     Conceptually, when proving one inductively defined Prop from another
>     can be considered as a translation between derivation trees.
>     However, I am recently running into a problem that, when taking this
>     view, such translation does not have to be structural. In
>     particular, sometimes generated inductive hypothesis  by `induction`
>     doesn't make immediately sense, but can be applied to some other
>     derivation trees after certain processing, so that some measure can
>     also be applied to argue termination.
>
>     The tricky part here is Prop -> nat is not meaningfully definable
>     type, because Prop cannot be eliminated in Type/Set, so even if I
>     know how to define measures on paper, I am not able to define one in
>     Coq.
>
>     Is there any way out so that well-founded induction can be done
>     intuitively?
>
>     *Sincerely Yours,
>     *
>     *
>     Jason Hu*
>