The Coq mailing list

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

Theodoros G. Tsokos wrote:
> Dear all,
>
> thank you very much for your replies and your time.
>
> Yves Bertot wrote:
> > Long answer:
> >
> > ...
> > ...
> > ...
> >
> > I hope this helps,
> >
> > Yves
> Yes, it really helped my understanding (I hope ) in this topic. Thanks 
> for the long answer in specific, it was quite informative.
>
> However, I would like to rephrase, in a way, my question. I knew about 
> the option of creating a string_dec function of type forall x y: 
> string, {x=y}+{x<>y}, as in Yves' Semantics Survey. I'm concerned 
> about the *evaluation* of the clause as well. For example the following:
>
> Coq < Eval compute in (if (string_dec x y) then true else false).
>
> to give me false as an answer, whereas the
>
> Coq < Eval compute in (if (string_dec x x) then true else false).
>
> to give me true. However, in that way I don't get this result.
>
> Apologize for not setting it down properly in my first email, but my 
> aim is to be able to do that kind of evaluations/computations, in 
> order to get a *terminal* result from the evaluation.
>
> Thank you very much in advance again,
> Theo.
If you use the string package provided with Coq 8.1pl2
(I haven't installed the earlier version yet), you have the following 
behavior.

dizzy:~/talks bertot$ coqtop
Welcome to Coq 8.1pl2 (Oct. 2007)

Coq < Require Import String.
Warning: Notation _ ++ _ was already used in scope string_scope

Coq < Open Scope string_scope.

Coq < Definition x := "a first identifier".
x is defined

Coq < Definition y := "a second identifier".
y is defined

Coq < Eval compute in (if string_dec x x then true else false).
    = true
    : bool

Coq < Eval compute in (if string_dec x y then true else false).
    = false
    : bool

Now, if you want to keep x and y as variables, you can't expect 
"string_dec x y" to go
beyond evaluating as just "string_dec x y", because you don't know what 
may happen, see here:

Section my.
Variables x y : string.
Hypothesis x_is_y : x = y.
Definition f := if string_dec x y then true else false.

(* you think f should be true?  Well, you can prove it! *)

Lemma f_is_true : f = true.
Proof.
unfold f; case (string_dec x y); auto; intros x_is_not_y; case 
x_is_not_y; exact x_is_y.
Qed.

(* but you can also prove that f is false, here is how. *)

Hypothesis x_is_not_y : x <> y.
Lemma f_is_false : f = false.
Proof.
unfold f; case (string_dec x y); auto; intros; case x_is_not_y; exact 
x_is_y.
Qed.

(* Of course, we are in an inconsistent environment, but if you let 
inconsistent hypotheses
interfere with reduction, you cannot preserve strong normalization or 
the consistency of Coq. *)

(* Now if we leave the section, then two hypotheses are not valid 
anymore, so we are not
in an inconsistent state anymore. *)

End my.

(* Outside the section the various constants f, f_is_true, and 
f_is_false are all defined and meaningful!
 You can use Check to verify that we have the following types for the 
constant. *)


f : string -> string -> bool
f_is_true : forall x y : string, x = y -> f x y = true
f_is_false : forall x y : string, x <> y -> f x y = false

Conclusion: if you want string_dec to compute, you have to feed it with 
real data, not abstract variables.
Any logical hypothesis you make about a variable may be contradicted by 
some other hypothesis and
it would be foolish to let the evaluation mechanism depend on hypotheses 
too precisely.

Yves