The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

Michel Levy a ecrit :
 > Why (match f n1 n3 with Left -> Left | Right -> Right) is no replaced by
 > (f n1 n3) ?

The apparently stupid case analysis on the extracted code
makes sense and is a typical situation with extraction.
It comes from the fact that proving directly
usual_le_lt_dec : (n,m:nat){(le n m)}+{(lt m n)}
by fixpoint/case analysis on n and m leads to a goal:  

  usual_le_lt_dec : (n,m:nat){(le n m)}+{(lt m n)}
  n : nat
  m : nat
  ============================
   {(le (S n) (S m))}+{(lt (S m) (S n))}

But you cannot just apply usual_le_lt_dec because 
(le n m) and (le (S n) (S m)) are not convertible,
idem for (lt m n) and (lt (S m) (S n)).
Your only posible step is a case analysis on (usual_le_lt_dec n m)
which is reflected in the extracted code.

In order to overcome that you can try to work with computational
versions of le and lt (see a script below).
Actually this is possible precisely because le is decidable...
Moreover you should also prove that le and cle are equivalent,
especially if you want to use the previous result to define:

Definition comp_le_lt_dec : (n,m:nat){(le n m)}+{(lt m n)}.

A more general approach is to give the goal the following shape:

 (n,m:nat) (P:Prop)((le n m)->P) -> (Q:Prop)((lt m n)->Q) -> {P}+{Q}

To this effect you can use the following definition
which is a kind of continuation passing style:
Definition kproof : 
  (X:Prop) (S:Prop->Set) ((P:Prop)(X->P) -> (S P)) -> (S X) :=
  [X, S, HX] (HX X [H]H).

The present disadvantage of the latter solution (wrt cle_clt_dec) 
is that the additional props P and Q are translated in a vacuous 
additional argument "prop" in the extracted code. These fake "prop"s 
are new since Coq V7 and are required in order to ensure that the 
extracted code is always well behaved (under strict evaluation ?)
but I suppose that in cases like le_lt_dec, an optimization step
could remove them...

Below are the formal details.

-- 
Jean-Francois Monin 
jeanfrancois.monin AT rd.francetelecom.com
 
monin AT csl.sri.com
 
http://www.csl.sri.com/~monin/ ;


(* computational le *)

Fixpoint cle [n:nat] : nat->Prop :=
  Cases n of 
    O => [m] True
  | (S n0) => 
    [m]Cases m of
         O => False
       | (S m0) => (cle n0 m0)
       end
  end.

Definition clt [n,m:nat] : Prop := (cle (S n) m).

Definition cle_clt_dec : (n,m:nat){(cle n m)}+{(clt m n)}.
Fix 1; Intro n; Case n; Clear n.
  Left; Exact I.
  Intros n m; Case m; Clear m.
    Right; Exact I.
    Exact (cle_clt_dec n).
Defined.

Definition usual_le_lt_dec : (n,m:nat){(le n m)}+{(lt m n)}.
Fix 1; Intro n; Case n; Clear n.
  Left; Auto with arith. 
  Intros n m; Case m; Clear m.
    Right; Auto with arith.
    Intro m; Case (usual_le_lt_dec n m).
      Left; Auto with arith.
      Right; Auto with arith.
Defined.

Definition kproof : 
  (X:Prop) (S:Prop->Set) ((P:Prop)(X->P) -> (S P)) -> (S X) :=
  [X, S, HX](HX X [H]H).

Definition my_le_lt_dec : (n,m:nat){(le n m)}+{(lt m n)}.
Intros n m;
Apply (kproof (lt m n)); Apply (kproof (le n m));
Generalize n m; Clear n m.
(* (n,m:nat) (P:Prop)((le n m)->P) -> (Q:Prop)((lt m n)->Q) -> {P}+{Q} *)
Fix 1; Intro n; Case n; Clear n.
  Intros m P leP Q HQ; Left; Auto with arith.
  Intros n m; Case m; Clear m.
    Intros P Hp Q ltQ; Right; Auto with arith. 
    Intros m P leP Q ltQ;
      Refine (my_le_lt_dec n m P ? Q ?); Auto with arith.
Defined.

Extraction "min.ml" [expand kproof] cle_clt_dec my_le_lt_dec.