The Coq mailing list

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

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