The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Have you read Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/>?  Especially Section 7.1 seems like a fairly direct match with your question.

On 09/13/2013 05:34 PM, Ilmārs Cīrulis wrote:

Let's suppose that I have

- type T

- wellfounded relation R: T->T->Prop

- function F1: T->T that makes argument "smaller"

- condition C: T->Prop that describes "start values" of R

- function F2: T->T that makes argument "bigger"

How can I make Fixpoint that looks similar to this:

Fixpoint Example (n:T):X :=

  match {C n} + {~C n} with

    left _ => ... |

  right _ => Example (F1 n)

  end.

  

And how I can make possible the following usage of tactic 'induction' (or similar):

Theorem ...

Proof.

 ...

 induction n F.

(* And now I have two goals:

   the first with assumption C n and goal P n,

   the second with assumption P n and goal P (F2 n) *)

 ...

Qed.