The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

Hello,
        I'm building a "toy" example using the Refine tactic.
This tactic is a very interesting and powerful tactic for the
development of
recursive functions, but as far as I know, it lacks of documentation.
The only  examples I found were the examples of the Reference
manual (p.137,138), and the more realistic one of the Eduardo's
Tutorial on Recursive Types.

I think that the following could became another example, so I explain it
in
some detail.

My goal is to define  Quicksort, the following definition is not
accepted by Coq because it don't verify the syntactical condition of
termination (see the definitions of Filter, etc; below):

Fixpoint Quick [l:(list nat)] : (list nat) :=
   Cases l of
       nil        => (nil nat)
   |  (cons a l') => (Quick (Filter (before a) l')) ^ 
                     (cons a (Quick (Filter (after a) l' )))
end.

(NB: `^'is function `app' [PolyList] infixed)

As in Eduardo's example of function div, I'll define Quick 
proving termination explicitly using the predicate of accessibility Acc.

You can see the lemmas proving accessibility of the list by respect
of the relation LgthOrder:

Definition LgthOrder  [A:Set] : (list  A) -> (list  A) -> Prop :=
[l1,l2:(list A)](lt (length l1) (length l2)).

So, here my question.
The theorem I have to prove is :

Theorem Quick : (l:(list nat))(Acc (list nat) (LgthOrder nat) l)->(list
nat).
Proof
Fix 2; Intros l H.
Refine
  <(list nat)>Cases l of
       nil        => (nil nat)
   |  (cons a l') => (Quick (Filter (before a) l') ?) ^ 
                     (cons a (Quick (Filter (after a) l') ?))
  end.

I obtain the 2 awaited goals:

subgoal 1 is:
  
  Quick : (l:(list nat))(Acc (list nat) (LgthOrder nat) l)->(list nat)
  l : (list nat)
  H : (Acc (list nat) (LgthOrder nat) l)
  a : nat
  l' : (list nat)
  ============================
   (Acc (list nat) (LgthOrder nat) (Filter (before a) l'))

subgoal 2 is:
  
  Quick : (l:(list nat))(Acc (list nat) (LgthOrder nat) l)->(list nat)
  l : (list nat)
  H : (Acc (list nat) (LgthOrder nat) l)
  a : nat
  l' : (list nat)
  ============================
   (Acc (list nat) (LgthOrder nat) (Filter (after a) l'))

It should be easy to go through in both cases, using the theorem:

Theorem decrease :
 (l:(list nat))(a:nat)(Acc (list nat) (LgthOrder nat) (cons a l))->
         (f:nat->bool)(Acc (list nat) (LgthOrder nat) (Filter f l)).

But  "I loose" the equality l=(cons a l') deriving from the
case analysis.
I don't see any "simple" way (without modifying the function
given in the Refine) to reintroduce this equality in the hypothesis.

Thank you in advance for comments and/or solutions, 
        Pablo Argon

Here is my script:
--------------------------------------------------------------
Require PolyList.
(* infix append function *)
Infix RIGHTA 7 "^" app. 


Fixpoint Filter [pff : nat ->bool; l : (list nat)] : (list nat) :=
  Cases l of
     nil         => (nil nat)
   | (cons a l') => 
           if (pff a) 
           then (cons a (Filter pff l'))
           else (Filter pff l')
  end.

Lemma FilterDescend : (l:(list nat))(pff : nat ->bool)
  (le (length (Filter pff l)) (length l)).
Proof.
Induction l.
Intros.
Simpl.
Apply le_n.

Intros.
Simpl.
Elim (pff a).
Simpl.
Apply le_n_S.
Apply H.

Apply le_S.
Apply H.
Qed.

Fixpoint inf_dec [n:nat] : nat->bool :=
      [m:nat] Cases n m of
                  O     _     => true
              | (S n')  O     => false
              | (S n') (S m') => (inf_dec n' m')
             end.

Definition negb [b:bool] : bool :=
Cases b of
  true  => false
| false => true
end.


Definition after [a:nat] : nat -> bool :=
 [b:nat](negb (inf_dec a b)).

Definition before [a:nat] : nat -> bool :=
 [b:nat] (inf_dec a b).

(* On ne peut definir ceci directement :

Fixpoint Quick [l:(list nat)] : (list nat) :=
   Cases l of
       nil        => (nil nat)
   |  (cons a l') => (Quick (Filter (before a) l')) ^ 
                     (cons a (Quick (Filter (after a) l' )))
end.
*)

(* -----------------------------------*)
(* Accessibilite par length d'une liste *)

Definition LgthOrder  [A:Set] : (list  A) -> (list  A) -> Prop :=
[l1,l2:(list A)](lt (length l1) (length l2)).


(*---------------- Preliminary Lemmas about the ordering
--------------------*)
Lemma Acc_nil : (A : Set)(Acc (list A) (LgthOrder A) (nil A)).
Proof.
Intro.
Apply Acc_intro.
Unfold LgthOrder lt.
Simpl.
Intros.
Inversion H.
Qed.


Lemma AccList_ind : (A:Set)(l:(list A))(Acc (list A) (LgthOrder A) l)
                         -> (y:(list A))((length y)= (length l))
                                  ->(Acc (list A) (LgthOrder A) y).
Proof.
Intros.
Apply Acc_intro.
Intros.
Elim H0.
Unfold LgthOrder lt in H1.
Inversion H.
Apply H2.
Unfold LgthOrder lt.
Rewrite <- H0.
Assumption.
Qed.


Lemma List_Accessibility : (A:Set)(l:(list A))(Acc (list A) (LgthOrder
A) l).
Proof.
Induction l.
Apply Acc_nil.

Intros.
Apply Acc_intro.
Intros.
Unfold LgthOrder lt in H0.
Simpl in H0.
Inversion H0.
Apply AccList_ind with l:=l0; Assumption.

Inversion H.
Apply H3.
Unfold LgthOrder lt.
Assumption.
Qed.

(*----------------------------------------------------------*)


Theorem decrease :
 (l:(list nat))(a:nat)(Acc (list nat) (LgthOrder nat) (cons a l))->
         (f:nat->bool)(Acc (list nat) (LgthOrder nat) (Filter f l)).
Proof.
Intros.
Apply Acc_intro.
Intros.
Inversion H.
Apply H1.
Cut (le (length (Filter f l)) (length l)).
(*---*)
Intros.
Unfold LgthOrder lt.
Simpl.
Unfold LgthOrder lt in H0.
Inversion H3.
Apply le_S.
Assumption.

Apply le_S.
Apply le_S.
Apply le_trans with m:=(length (Filter f l)).
Assumption.

Assumption.

Apply FilterDescend.
Qed.

(*=== Quicksort retrouvé  ========================================*)
Require Refine.

Theorem Quick : (l:(list nat))(Acc (list nat) (LgthOrder nat) l)->(list
nat).
Proof
Fix 2; Intros l H.
Refine
  <(list nat)>Cases l of
       nil        => (nil nat)
   |  (cons a l') => (Quick (Filter (before a) l') ?) ^ 
                     (cons a (Quick (Filter (after a) l' ) ?))
  end.