The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Shouldn't all (or most) the things in theories/Logic/Decidable.v (and
all theorems of the form "Decidable.decidable P" for some P) be
transparent instead of opaque? The whole point of being decidable is
that you can _compute_ trough it, right?

The specific place where their being opaque annoys me _greatly_ is
that I define a very dependent type (in Prop) through a (somewhat)
complicated recursion. Along the way, I have proof obligations like
 n - m + m = m
of which I get rid of by omega.

But the _result_ of the computation (in Prop!) doesn't depend on the
particular proof of "n - m + m = m" taken. I need to prove this only
to prove that "vec T (n - m + m)" and "vec T n" are the same type, and
that thus I can make this particular recursive call. (See appendix for
definition of vec.)

So, I have basically my dependent type constructor as such:
 go : nat -> Prop.

Now, if I do "Eval compute in (go 2).", I get as a result 1140 lines
that whose shape is:

 match
  match
   Decidable.dec_not_not (2 = 2)
    (or_introl (2 = 2 -> False) (refl_equal 2))
    (fun H : 2 = 2 -> False => ...) in (_ = y) 
      return (y = 2)
  with
   | refl_equal => refl_equal 2
  end in (_ = y)
    return
           (...)
 with
  | refl_equal => (...)
 end le

When I see this, I think "(2=2) is decidable, so DECIDE IT, which will
make a redex and continue normalising!"


In order to get the results I want from my "go", I have modified Coq
so that everything is transparent (I have made "Qed" and "Save" do the
same thing as "Defined"), and now I get a much more reasonable result
from my "Eval compute in (go 2).".

(If you must know, it gives me:

  forall t t0 : nat, (pred t) <= t0 -> t <= (pred t0) -> t <= t0 :
  Prop

 which is much more readable than that 1140 lines thing with opaque
 decidable things!
)


But maybe I'm just being stupid and this is all my fault because I did
everything the wrong way. Or I misunderstand the problem. In this
case, please tell me and explain! I wanna learn.


Thanks in advance for your reactions,


APPENDIX
========

A bit more details on what I want to achieve. I want a dependent type
that for n m:nat, P an n-ary predicate over type T (of type
 T -> T -> ... -> T -> Prop) and f:T-T will be

 forall x_1 x_2 ... x_n : T,
   P (f x_1) x_2 x_3 ... x_{n} ->
   ... ->
   P x_1 ... x_{m-3} (f x_{m-2}) x_{m-1} ... x_{n} ->
   P x_1 ... x_{m-2} (f x_{m-1}) x_{m} ... x_{n} ->
   P x_1 ... x_{m-1} (f x_{m}) x_{m+1} ... x_{n} ->
   P x_1 ... x_{n}

I managed to write a function that produces this type. (The "go" above
is that function, with n=m and P:=le .) Internally, it uses an
auxiliary function that uses lists (called "vec") to store information
across recursive calls. Here's vec:

 Inductive vec : Type -> nat -> Type :=
  | vnil  : forall A:Type, vec A 0
  | vcons : forall A:Type, forall n:nat, A -> vec A n -> vec A (S n).


(
 My goal is to prove that if f is well-founded, then forall  T n P,

  (... that big type ....) -> forall x1 x2 ... xn, (P x1 x2 ... xn)
)


Now, I want to _use_ that function. But when fully applied, it doesn't
normalise to something reasonable, because of these opacity problems!

-- 
Lionel