The Coq mailing list

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

I want to understand/learn recursion and induction, using Wf.v with its Acc, well_founded, Fix. well_founded_induction.

Accessibility and well-foundedness I have understood, but not very much further.

If it's possible to do only with wf.v and without "refine" then it's the way I need. I'm beginner and want learn this one way. Anything else must wait for later. So - thanks, Rui, but it's not what I need.

On Sat, Sep 14, 2013 at 6:45 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

Here's the simplest example I can think of:

Require Import Arith.

Require Import Omega.

Definition div : forall (n1 n2 : nat) (H1 : n2 <> 0), nat.

induction 1 as [n1 div] using (induction_ltof1 _ id).

refine (fun n2 H1 =>

  match lt_dec n1 n2 with

  | left _ => 0

  | right _ => S (div (n1 - n2) _ n2 H1)

  end).

unfold ltof. unfold id. omega.

Defined.

Eval compute in div 42 3.

"induction 1" means we're doing induction on the first unnamed argument.

induction_ltof1 allows you to do well-founded induction on any datatype.

It accepts as an argument a measure function from that datatype to nat.

We just use id because we're already working with nats.

The refine tactic allows you to fill in holes interactively.

You'll probably also need induction_ltof1 to prove things about this function.

On Sat, Sep 14, 2013 at 1:29 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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.