CODEWITHSUNDEEP
recursioncoqinduction
zaa
zaa

Reputation: 113

General recursion and induction in Coq

Let's suppose that I have

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.

I tried to do that with type nz: {n:nat | n<>O} (looking in the chapter 7.1 of Certified Programming with Dependent Types book) but got only this far:

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.

I couldn't understand what happens further because it was too complicated for me.

P.S. As I see it - there isn't any good enough tutorial about general recursion and induction in Coq for beginners. At least I could find. :(

Upvotes: 1

Views: 606

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

I'll try to write a more complete answer later, but Coq has a command called Function that makes it easier to write functions whose arguments decrease according to some well-ordering. Look for the command on the reference manual (http://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#hevea_command48), specifically the "wf" variant.

Upvotes: 2

Related Questions