Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop
  • Date: Sat, 23 Mar 2019 00:09:24 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay2-d.mail.gandi.net
  • Ironport-phdr: 9a23:QiM+JReoPZ8eIJFnXOZvcjjklGMj4u6mDksu8pMizoh2WeGdxcSzZh7h7PlgxGXEQZ/co6odzbaP6+a/AydYut6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMBm6twfcutcZjYd+JKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoAODAk7WHXkdRwg7xHrxK9qRJ/xIvUb5uUNPp4Y6jRedwXSG5EUstXSidPAJ6zb5EXAuQcI+hYoYnzqVgAoxSwCgajBv/gxDBTi3/q3qA3yfgtHR3I0QEgGd8FrXTarM/yNKcXSe27zbPHyinfb/xM3zfy8InGchElof6XQ71wa9bRwlQoGgPKlFqft5DlMCmT1ugXvGib7u5gWvmxhG49twF8uSOvxsQsi4nShYIVy1XE9SBnz4YvP9G4TlB0YcK9HZZWqiqUOYx2QsY4TGFpviY30qYGuYahfCgLzpQnyADQa+adf4eU5RLjUf6dITh5hHJ5eLK/mg29/VKhyu37UMS/zVVErjJdn9XSq3wA1Qbf58qbRvdn40us2jiC2xrO5uxALk04jbTXJ4Mvz7Iqi5YesVrPEjXrlEj3kqOabEEp9+eu5u/6eLvpvIWcOJVxigzmMqQhhMi/AeMgPwgUQWeb/f6z1b398UHgXbpGlPg2nbPYsJDeP8gbqbS2AwlI3YYi8Rq/CSmp0MgAkXkGKlJKZg6HgpD3N13TIv30F/Wyj0i2nDt2xP3LMKftDojJI3XMiLvheKxy609YyAo919Bf4JdUB6kOIP3pREDxqMbXDhkjPwy7wubnDM5y2Z0EWWKTGaKZK6DSsF+T5uIsIumMYYoVtyjnK/Q/4f7hk2M5lUcHfaa1xZsXdGy4HvN+LkqFZnrsm84NHnsOvgojV+Pnk0aCUD5WZ3aqRa0w/DA7CIS8DYfCXI+hmrKB3D3oVqFRM2tBExWHFWriX4SCQfYFLiyIceF7lTlRerEiV4Yn4j6vsAX30aYveuXd9zERs9Ts1dx/6vfPvQox5Cd3DsGY3nvLSWxoyDBbDwQq1bxy9BQugmyI1rJ11qAJTI0B17ZySg4/cKXk4al/AtH2VBjGe47XGk2lU86lADQ0Q8h3xdISMR8kR4eSyyvb1i/vOIc70qSRDcVqoLnfzmPyJsN4xmyA0qQ93QF/H5l/cFa+j6s6zDD9Qo7El0LDyvSweKAVzXSI+CGGxGuK+k5RVgJxF6PIQSJHaw==

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*




Archive powered by MHonArc 2.6.18.

Top of Page