The Coq mailing list

[David Monniaux <monniaux AT clipper.ens.fr>]

J'ai des problemes avec le realizer.

Require Bool.
Require Lt.
Require Le.

Section initial_ranges.
Variable n: nat.

Definition initial_range := { x: nat | (lt x n) }.

Definition is_not_empty: (initial_range->bool)->bool.
Realizer
  [xs: initial_range->bool] ((
  Fix test_upto {test_upto [i: nat]: bool :=
    [{Hi: (le i n)}] Cases i of
      O => true
    | (S j) => (andb (xs j) (test_upto j))
    end}) n).

is_not_empty< Show Program.
[Realizer [xs:initial_range->bool]
           (Fix test_upto{test_upto [i:nat] : bool := 
                            [_:([Error printing #GENTERM (MUTIND
                                                            #Peano#le.cci
                                                            0)] i n)]
                             Cases i of
                               O => true
                             | (S j) => (andb (xs j) (test_upto j))
                             end} n)]

Pourquoi cette erreur?

is_not_empty < Program_all.
Program_all.
Subtree proved!

is_not_empty < Show Proof.
Show Proof.
LOC: 
Subgoals
Proof: [_:initial_range->bool]
        ([H:nat->bool](H n)
          Fix test_upto{test_upto [i:nat] : bool := (test_upto i)})

Aie! Mais ce n'est absolument pas ce que je voulais!

N'ai-je rien compris aux annotations?

-- D. Monniaux

PS: Ce que je veux c'est du genre:
is_not_empty = 
[xs:initial_range->bool]
 (nat_rec [n0:nat](le n0 n)->bool [_:(le O n)]true
   [x:nat]
    [f:(le x n)->bool]
     [H:(le (S x) n)]
      (andb (xs (exist nat [x0:nat](lt x0 n) x H))
        (f (lt_le_weak x n H))) n (le_n n))
     : (initial_range->bool)->bool