The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 7 mai 08 à 10:35, Yves Bertot a écrit :

> popescu2 AT uiuc.edu
>  wrote:
> > Hello,
> > Maybe it is just my ignorance about Coq speaking now, but working  
> > with boolean predicates P : Less n -> bool does not seem to help  
> > either, since then the functions f would be in f : {i : Less n | P  
> > i = true} -> nat and after matching P n' with true I do not seem to  
> > have access to a proof of P i = true in order to apply f to n'.
> > (In this and the previous message, I have identified elements of  
> > Less n with elements of nat, in the "Program" style, to keep the  
> > ideas clear.)
> >
> > Regards,    Andrei
> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >          http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

<snip/>

> The algorithmic intuition is quite lost in the tactics.  I think you  
> can do better with Mathieu Sozeau's
> new Program facilities, but I haven't played with it yet.

Indeed you could have:
<<
Require Import Program.

Notation Less n := {i | i < n}.

Section Sum'.
  Variables (n : nat) (P : Less n -> bool) (f : {i : Less n | P i =  
true} -> nat).

  Program Fixpoint sum' (n' : Less n) { measure proj1_sig } : nat :=
    match n' with
      | 0 => 0
      | S n'' =>
        let r := sum' n'' in
          if dec (P n') then f n' + r else r
    end.

  Next Obligation.
  Proof.
    rewrite <- H. pi.
  Qed.

End Sum'.
>>

Note that it uses the "dec" combinator which lifts a boolean to a  
sumbool (forall b : bool, { b = true } + { b = false }) so that you  
get the hypothesis [P n' = true] in the first branch. Another  
equivalent solution would be to explicitely pattern-match on the  
result of [P n']:
<<
let r := sum n'' in match P n' with true => f n' + r | false => r end.
>>
Then Program would generate the equality [P n' = true] as well. One  
could also develop a P_dec variant.

Hope this helps,
-- Matthieu