The Coq mailing list

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

Hi Jason (cc Fabian),

May be this could help you. I am not sure and moreover it is

not a straightforward trick.

Your problem with size reminds me of the proof of the Prop-bounded

version of Kruskal's tree theorem I did 4 years ago, following some of

the ideas developed in Wim Veldman's paper. For the Type-bounded

version, size was measured with well-founded trees

Variables X : Type.

Inductive wft : Type :=
    | in_wft_zt : wft
    | in_wft_sup : (X -> wft) -> wft.

to account for W. Veldman's "stumps". Then these measures are

combined using lexicographic products. They measure the

termination complexity of an inductive well-quasi order.

The problem was that with the Prop-bounded version of the theorem,

one could not compute a size from the hypotheses; and because of

the closure, not even show that one existed (when eg X is infinite).

Of course unless admitting something like

AC_trunc P : forall x, inhabited (P x) -> inhabited (forall x, P x).

No such problems occurred with the Type-bounded version of the

theorem though; because choice is provable in Type:

choice R : forall x, { y | R x y } -> { f | forall x, R x (f x) }

The solution I did find at that time took me a while. It was to convert

reasoning over a size into reasoning over an inductive predicate

(similar to Acc/well_founded) in Prop. But one should be able

to combine those predicates into *finitary* lexicographic products

and that was the big problem (binary would have been easy by

nested induction).

I called the corresponding notion

         "well-foundness upto a projection".

The idea was that while you could only prove properties

of projected values by "induction", inductive hypotheses could

use hidden information (i.e. information that is being projected

away) to fulfill the goals.

Well-foundness upto is stable under lexicographic

products. It solved the problem nicely while keeping most of

the structure of the Type-bounded version of the proof. But

it is not easy to explain outside of the context of that

particular development. I'd be happy to find another

use of the notion in a simpler context.

Here is the comment that I let in the file wf_upto.v of that

project:

(*

   Recall the well_founded predicate definition (with implicit
   arguments):

   Definition well_founded R :=
          forall Q, (forall a, (forall b, R b a -> Q b) -> Q a)
                  -> forall a, Q a.

   Hence, while proving Q a, you can assume Q b for any b such
   that R b a.

   Let f be a map (that potentially "forgets" some information).
   Basically, with a "well-founded upto f" relation R you can prove
   a predicate Q by induction using R provided that Q expresses no
   property about the information that is forgotten.

   Definition well_founded_upto f R :=
          forall Q, (forall a, (forall b, R b a -> Q (f b)) -> Q (f a))
                  -> forall a, Q (f a).

   But in that case, R is not necessarily well-founded (it can even
   contain x such that R x x !!)

   With a "well-founded upto" relation, you can use "hidden" information
   in the inductive steps of the proofs. But you cannot prove any arbitrary

   predicate Q that way:

      1/ Q must be extensional (not really a constraint)
      2/ Q cannot expresses properties about the "hidden" information

   Most importantly, the well-founded upto predicate is stable under
   lexicographic products.

   That concept solved very nicely the problem of finding an outermost
   induction principle suitable for the logical/prop-bounded version of
   both Higman's theorem and Kruskal's theorem.

*)

Dominique

---

De: "Jason" <fdhzs2010 AT hotmail.com>
À: "Fabian Kunze" <kunze AT ps.uni-saarland.de>, "coq-club" <coq-club AT inria.fr>
Envoyé: Vendredi 22 Mars 2019 23:50:45
Objet: Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop

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> 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