Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]Decreasing arguments for fixpoint definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Decreasing arguments for fixpoint definitions


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page