The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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
>   
Dear Andrei,

Since you are talking about an algorithm, you solution needs to be 
composed of
algorithms.  However, neither Less nor P are algorithms: they are 
types.  Less
is a type for algorithms, in a sense (algorithms that compute a number 
together with
a guarantee that the number satisfies smaller than n) and P is not even 
a type for
algorithms.  To progress, you need to have an algorithm corresponding to 
P, this
is why Russell proposed that you should have a boolean algorithm.

Now, if you want to define a recursive function, you have several 
approaches.
The "old-fashioned" approach is to define the function directly as a 
Fixpoint,
but for this the type Less n is not suitable, because it does not 
exhibit any
recursive structure.  It will be better to define the function as a 
recursive function
over nat.  However, as you rightly point out, if take an arbitrary 
natural number
you first have to check whether this natural number does satisfy the 
Less predicate
and the P predicate.  For the Less predicate, this can be granted by 
assumption,
because you know in advance  that you started with an element that was 
already
the first component of an element in type {i : Less n | P i = true}, but 
in the
recursive call, you will need to have that any predecessor i' of (the 
first component of)
i also satisfy  the property (i' < n).   This can be given by the following
theorem, provable using omega, or any other good manual effort.

Lemma lm : forall i', S i' < n -> i' < n.

Now to take only the elements that satisfy P i = true, you still need to 
call an algorithm,
but in this setting, P is an algorithm but it cannot be called directly 
called on natural
numbers, because P takes as input elements of Less n.  So you need to 
reconstruct
an element of Less n from an element of nat...

Require Import Arith Omega.

Section Russell_for_Andrei_according_to_Yves.

Variable n: nat.
Definition Less (n:nat) : Set := {i | i < n}.
Variable P : Less n -> bool.

Variable f : {i : Less n | P i = true}->nat.

Lemma lm: forall i', S i' < n -> i' < n.
intros; omega.
Qed.

Fixpoint sum (k:nat) : k < n -> nat :=
 match k return k < n -> nat with
   0 => fun h' : 0 < n =>
   let v0:Less n := exist (fun x => x < n) 0 h' in
   match P v0 as b return P v0 = b -> nat with
     true => fun h': P v0 = true => 
       f (exist (fun i : Less n => P i = true) v0 h')
   | false => fun _ => 0
   end (refl_equal (P v0))
 | S k' => fun h: S k' < n =>
   let vk := exist (fun x => x < n) (S k') h in
   let vpred := sum k' (lm k' h) in
     match P vk as b return P vk = b -> nat with
       true => fun h' : P vk = true =>
       f (exist (fun i => P i = true) vk h') + vpred
     | false => fun _ => vpred
     end (refl_equal (P vk))
 end.

Definition s : Less n -> nat :=  fun x => let (k, h) := x in sum k h.

The function s is what you want.

This looks complicated, but you can make simpler by using tactics:

Definition s2 : Less n -> nat.
intros [k]; induction k; intros h.
assert (v0 : Less n) by (exists 0; exact h).
case_eq (P v0); intros h'.
apply f; exists v0; exact h'.
exact 0.
assert (vk : Less n) by (exists (S k); exact h).
assert (vpred:nat) by (apply IHk; apply lm; assumption).
case_eq (P vk); intros h'.
assert (fvk:nat) by (apply f; exists vk; exact h').
exact (fvk + vpred).
exact vpred.
Defined.

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.

Another, more systematic approach, is exhibited in the ssreflect 
package: the type Less n is actually
defined as "ordinal n" and the operation of summing all elements 
satisfying a predicate is already
provided in the package (in a file called bigops).  I suggest you have a 
look.

http://www.msr-inria.inria.fr/Projects/math-components/math-components-index

Yet another solution is to keep P as a Prop predicate and to suppose the 
existence of a sumbool-typed
predicate:

Require Import Arith Omega.

Section Russell_for_Andrei_according_to_Yves.

Variable n: nat.
Definition Less (n:nat) : Set := {i | i < n}.
Variable P : Less n -> Prop.
Variable P_dec : forall x, {P x}+{~P x}.

Variable f : {i : Less n | P i}->nat.

Lemma lm: forall i', S i' < n -> i' < n.
intros; omega.
Qed.

Fixpoint sum (k:nat) : k < n -> nat :=
 match k return k < n -> nat with
   0 => fun h' : 0 < n =>
   let v0:Less n := exist (fun x => x < n) 0 h' in
   match P_dec v0 with
     left h' =>
       f (exist (fun i : Less n => P i = true) v0 h')
   | _ => 0
   end
 | S k' => fun h: S k' < n =>
   let vk := exist (fun x => x < n) (S k') h in
   let vpred := sum k' (lm k' h) in
     match P_dec vk with
       left h' =>
       f (exist (fun i => P i = true) vk h') + vpred
     |  _ => vpred
     end
 end.

Definition s : Less n -> nat :=  fun x => let (k, h) := x in sum k h.

I prefer this solution, which also has the advantage that proofs on this 
function are easier.

Yet another solution relies on the "Function package" here is the 
example (this works on
a very recent svn version of Coq).

Require Import Arith Omega Recdef.

Section Russell_for_Andrei_according_to_Yves.

Variable n: nat.
Definition Less (n:nat) : Set := {i | i < n}.
Variable P : Less n -> Prop.
Variable P_dec : forall x, {P x}+{~P x}.

Variable f : {i : Less n | P i}->nat.

Definition is_zero (k:Less n) : bool :=
 match k with (exist 0 _) => true | _ => false end.

Lemma lm: forall i', S i' < n -> i' < n.
intros; omega.
Qed.

Definition Less_pred (k:Less n) : Less n :=
 match k with (exist (S k) h) =>
   exist (fun x => x < n) k (lm k h)
 | _ => k
 end.

Definition Less_to_nat (k: Less n) : nat :=
 match k with exist k _ => k end.

Definition mk_P (k: Less n) (h: P k) :=
  exist (fun i => P i) k h.

Function s4 (k:Less n) {measure Less_to_nat} : nat :=
 if is_zero k then
   match P_dec k with
     left h => f (mk_P k h)
   | _ => 0
   end
 else
   match P_dec k with
     left h => f (mk_P k h)
   | _ => 0
   end +s4 (Less_pred k).
intros [k]; case k; simpl; intros; discriminate || omega.
Defined.


I like the fourth solution because the way you write the algorithm is close
to your initial intent.  Moreover, Function produces a collection of 
nice theorems
that will make all reasoning about the function much easier (especially 
using functional induction).
Still there are a few things that are unpleasant:
* We need to duplicate code, because Function does not like let .. = .. 
in .. constructs.
* We need to define mk_P because Function does like lambda abstractions.

Yves