The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Sorry, I previously sent it only to Adam Chlipala.

---------- Forwarded message ----------
From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
Date: Sat, Sep 14, 2013 at 12:32 PM
Subject: Re: [Coq-Club] Question about recursion and induction
To: Adam Chlipala <adamc AT csail.mit.edu>

Yes, it seems like a direct match but it didn't help me enough.

This is how far I got:

Require Import Omega.

Definition nz: Set := {n:nat | n<>O}.

Theorem nz_t1 (n:nat): S n<>O. Proof. auto. Qed.

Definition nz_eq (n m:nz) := eq (projT1 n) (projT1 m).

Definition nz_one: nz := exist _ 1 (nz_t1 O).

Definition nz_lt (n m:nz) := lt (projT1 n) (projT1 m).

Definition nz_pred (n:nz): nz := exist _ (S (pred (pred (projT1 n)))) (nz_t1 _).

Theorem nz_Acc: forall (n:nz), Acc nz_lt n.

Proof.

 intro. destruct n as [n pn], n as [|n]. omega.

 induction n; split; intros; destruct y as [y py]; unfold nz_lt in *; simpl in *.

   omega.

   assert (y<S n\/y=S n). omega. destruct H0.

    assert (S n<>O); auto.

    assert (nz_lt (exist _ y py) (exist _ (S n) H1)). unfold nz_lt; simpl; assumption.

    fold nz_lt in *. apply Acc_inv with (exist (fun n0:nat=>n0<>O) (S n) H1). apply IHn.

    unfold nz_lt; simpl; assumption.

    rewrite <- H0 in IHn. apply IHn.

Defined.

Theorem nz_lt_wf: well_founded nz_lt. Proof. exact nz_Acc. Qed.

Lemma pred_wf: forall (n m:nz), nz_lt nz_one n -> m = nz_pred n -> nz_lt m n.

Proof.

 intros. unfold nz_lt, nz_pred in *. destruct n as [n pn], m as [m pm]. simpl in *.

 destruct n, m; try omega. simpl in *. inversion H0. omega. 

Defined.

And then I have no idea what to do because mergeSort example seems too complicated.

On Sat, Sep 14, 2013 at 1:13 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.