The Coq mailing list

[Julien Forest <forest AT ensiie.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:
*)

Dear Frederic, 
you can use Function (to create principles) and functionnal induction (to use 
them).
I've done the proofs using this technique (I needed to define hd, last and 
length and 
I hope I didn't do any mistake) 


Variable Act : Set.

Inductive obs : Set :=
| err : obs
| term : obs
| act : Act -> obs.
 
Inductive seq : Set :=
  | nil: seq
  | cons: Act -> seq -> seq.
Notation "x :: y" := (cons x y) (at level 80).
(*
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:
*)

Definition hd (s:seq) : obs := 
  match s with 
    | nil => term
    | x::_ => act x
  end.

(* You could use Function instead of Fixpoint *)

Function 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.
(* This will AUTOMATICALLY construct an inductive R_nth which is more or less 
equivalent 
to isNth, induction principles associated to nth (named nth_rect, nth_rec and 
nth_ind 
depending on the sort considered) and two lemmas stating that nth and R_nth 
are equivalent
*)

(*
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 -> Type :=
| 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.
(* Proof of equivalence between isNth and R_nth (just here to demonstrate that
the inductive generated by Function is equivalent to isNth *)
Lemma isNth_is_R_nth  : forall s n o, 
  isNth s n o -> (R_nth s n o).
Proof.
intros s n o H.
induction H as [s| n | a t | b o m t H IH].
apply R_nth_0 with (n:=0). reflexivity.
case n.
replace term with (hd nil) by reflexivity;
eapply R_nth_1 with (n:=1);reflexivity.
intros n0;
eapply R_nth_2 with (n := S (S n0)) (m:= (S n0)) (s := nil).
reflexivity.
exact I.
reflexivity.

replace (act a) with (hd (a::t)) by reflexivity.
eapply R_nth_1 with (n:=1);reflexivity.
eapply R_nth_3 with (n:= S(S m)) (s:=b::t).
reflexivity.
exact I.
reflexivity.
exact IH.
Qed.

Lemma R_nth_is_isNth : forall s n o, 
  R_nth s n o -> isNth s n o .
Proof.
  intros s n o H.
  induction H. 

  apply isnth0.
  case s.
  apply isnth1.
  intros a s0;  apply isnth2.
  destruct m.  tauto.
  apply isnth1.
  destruct m. tauto.
  apply isnth3. exact IHR_nth.
Qed.

(*Then you trivial lemmas are also trivial 
   They are just application of previous lemmas and automatic equivalence 
lemmas 
*)
Lemma isNth_nth : forall (s:seq) (n:nat) (o:obs), isNth s n o -> (nth s n)= o.
Proof.
  intros s n o H.
  symmetry.
  apply R_nth_complete.
  apply isNth_is_R_nth;assumption.
Qed.



Lemma nth_isNth : forall (n:nat) (s: seq)(o:obs), (nth s n) = o -> isNth 
s n o.
Proof.
  intros n s o H.
  apply R_nth_is_isNth.
  apply R_nth_correct.
  symmetry;assumption.
Qed.

(*
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:

But the previous lemmas are no more needed. 
*)
Fixpoint length (s:seq) {struct s} : nat := 
  match s with 
    | nil => 0
    | _::t => S (length t)
  end.

Function last (s:seq) {struct s} : obs := 
  match s with 
    | nil => err
    | x::nil => act x
    | _:: t => last t
  end.

Lemma Nth_last : forall (s : seq), (nth s (length s)) = (last s).
Proof.
  intros s.
  (* Induction works well only on variables and so does functional induction.
     I do need to replace length s by a variable 
     *)
  set (n := length s).
  generalize (refl_equal n);unfold n at 2;clearbody n.
  (* And now, I can prove the lemma using the tactic functional induction *)
  functional induction nth s n.
  (* a seq with length 0 is obviously nil *)
  case s;clear s;simpl.
  auto.
  intros a s abs. discriminate abs.
  (* a seq with length 0 is obviously x::nil for some x *)
  case s;clear s;simpl.
  intros abs. discriminate abs.
  intros a s;case s.  
  auto.
  intros;discriminate.
  
  intro abs;discriminate abs.

  intros Hlenght;injection Hlenght;clear Hlenght. intros Hlenght.
  destruct m.
  tauto.
  rewrite (IHo Hlenght). 
  destruct t.
  discriminate.
  reflexivity.
Qed.

(* I hope that this might help you. 
   Best regards 
   Julien Forest.
*)