The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

----- Jason -Zhong Sheng- Hu 
<fdhzs2010 AT hotmail.com>
 a écrit :
> 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?

Hi Jason,

  I think you basically have two options: putting your derivations in 
Type/Set and defining a measure on them or indexing your propositional 
derivation trees with their size/depth (i.e nat -> Prop), building in the 
measure you want and then showing that some functions are size preserving or 
decreasing on derivations. I think the later is a bit more delicate in 
general as this forces you to carry around the size information even in 
lemmas that have nothing to do with it e.g. by existentially quantifying on 
sizes. Also you can always go back to seeing a derivation tree in Set as a 
Prop using an explicit squashing operation, if needed. You might have to make 
some of your lemmas transparent to show size preservation in the Set case, 
but that’s to be expected when you’re really doing proof-relevant reasoning.

My 2 cents,
— Matthieu