The Coq mailing list

[Fr�d�ric Peschanski <Frederic.Peschanski AT lip6.fr>]

Dear provers,

I am an occasional Coq user and I have a beginner-level question
(sorry if this is too naive, but please note I *do* own coq'Art ;-).

In general, I follow the principle of proving my lemmas about
recursive functions using structural induction on their principal
argument. But there are (many) cases when better induction
principles can be followed.

I take the simplest example I had in stock.
It is about a model of computation as observation sequences,
a kind of list. The main types are the following ones:

Variable Act : Set.

Inductive obs : Set :=
| err : obs
| term : obs
| act : Act -> obs.

Inductive seq : Set :=
 | nil: seq
 | cons: Act -> seq -> seq.

Many functions are defined on seq and most lemmas use seq_ind or seq_rec.
Consider, however, the following function to fetch the n-th element of a 
sequence:

Fixpoint nth (s : seq) (n : nat) {struct n}: obs :=
match (n) with
| O => err
| S O => hd s
| S m => match (s) with
              | nil => term
              | _::t => nth t m
             end
end.

Here the principal argument is n ... but it could be s instead of course,
and what I really need is a principle on both s and n.
In fact, most lemmas are more easily demonstrated using the principle
suggested by the following inductive type:

Inductive isNth : seq -> nat -> obs -> Prop :=
| isnth0 : forall s:seq, isNth s O err
| isnth1 : forall n:nat, isNth nil (S n) term
| isnth2 : forall (a:Act) (t :seq), isNth (cons a t) (S O) (act a)
| isnth3 : forall (b:Act) (o:obs) (m:nat) (t:seq), isNth t (S m) o -> 
isNth (cons b t) (S (S m)) o.

And the following are easily provable:

Lemma isNth_nth : forall (s:seq) (n:nat) (o:obs), isNth s n o -> (nth s 
n) = o.
Lemma nth_isNth : forall (n:nat) (s: seq)(o:obs), (nth s n) = o -> isNth 
s n o.

For the moment, I switch from the function to the predicate form 
depending on the situation.
The function form benefits from reduction and convertibility, whereas 
the predicate form
suggest the general induction principle.

An example of a lemma I had to prove was:

Lemma Nth_last : forall (s : seq), (nth s (length s)) = (last s).

The simplest proof I was able to do was to prove instead:

Lemma Nth_last_aux : forall (s: seq), isNth s (length s) (last s).

I wonder, though, if there is an easy way to derive from isNth an 
induction principle that
could be applied directly on the functional form, e.g. with  elim XXX 
using YYY.
Maybe there is even a construction assisting all this work at once 
(taking a function, its predicate form and the two lemmas, and then 
generate the induction principle) ?

Thanks in advance,
Frederic.