coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Pichardie <david.pichardie AT irisa.fr>
- To: "Adam Koprowski" <adam.koprowski AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club]Decreasing arguments for fixpoint definitions
- Date: Wed, 26 Jul 2006 17:05:05 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear Adam,
You have effectively a syntax problem:
Fixpoint Computable (M: Term) {measure M term_type_measure} : Prop :=
match (type M) with
| #T => AccR M
| TL --> TR =>
forall P (Papp: isApp P) (PL: appBodyL Papp = M) (typeL: type P = TR),
Computable (appBodyR Papp) ->
Computable P
end.
should be
Function Computable (M: Term) {measure term_type_measure M} : Prop :=
match (type M) with
| #T => AccR M
| TL --> TR =>
forall P (Papp: isApp P) (PL: appBodyL Papp = M) (typeL: type P = TR),
Computable (appBodyR Papp) ->
Computable P
end.
Unfortunately, you will now obtain a Coq error like "User error: find_call_occs : Prod".
I am not expert in the current implementation of Function but I think you are too greedy for us.
Your quantification "forall P Papp" before the recursive call is too difficult for the current capabilities of Function.
Sorry, I think you will have to present you problem in a different way if you want to use Function here.
Best,
David.
- [Coq-Club]Decreasing arguments for fixpoint definitions, Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, Sébastien Hinderer
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, jean-francois . monin
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions,
David Pichardie
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions,
Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, David Pichardie
Archive powered by MhonArc 2.6.16.