The Coq mailing list

["Zolt�n S. M�rk"<markzoli AT yahoo.com>]

I am experimenting with c-zar (oops, the Mathematical Proof Language ...), and
ran into the following phenomenon:

The following code works:
---------------------
Parameter S :  Set.

Parameter S_of_nat : nat -> S. 

Parameter combined : S -> S -> S.

Parameter has_property_X : S -> Prop.

Axiom general : forall (n : nat) (x : S), has_property_X x -> has_property_X
(combined (S_of_nat n) x).

Theorem particular : forall x : S, has_property_X x -> has_property_X 
(combined
(S_of_nat 0) x).
proof.
  thus thesis by general.
end proof.
Qed.
---------------------

However, if you replace the declaration of S_of_nat with a particular
definitioni, then the proof breaks:

...
Parameter some_element : S.
Definition S_of_nat (n : nat) : S := some_element.
...

"thus thesis by general" now claims insufficient justification. This 
particular
problem can be patched over by "Set Firstorder Depth 0". However, this patch
also fails if we introduce x and has_property_X x:

...
proof.
  let x : S.
  assume Hx : (has_property_X x).
...

Now "thus thesis by general" claims insufficient justification again, and this
time it cannot be helped, although this latter example will again work with an
opaque S_of_nat (even without Set Firstorder Depth 0). I ran into many 
variants
of what feels like this same phenomenon. For instance:

---
Parameter S :  Set.

Parameter S_of_nat : nat -> S. 

Parameter combined : S -> S -> S.

Parameter has_property_X : S -> Prop.

Axiom general : forall (n : nat) (x : S), has_property_X x -> has_property_X
(combined (S_of_nat n) x).

Parameter Sneg : S -> S.

Axiom negator : forall x : S, combined (S_of_nat 0) x = Sneg x.

Theorem particular : forall x : S, has_property_X x -> has_property_X (Sneg 
x).
proof.
  let x : S.
  assume Hx : (has_property_X x).
  have H:(combined (S_of_nat 0) x = Sneg x) by negator.
  have (has_property_X x) by Hx.
  then (has_property_X (combined (S_of_nat 0) x)) by general.
  then (has_property_X (Sneg x)) by H.
  hence thesis.
end proof.
Qed.
---

This works just fine, but if again you replace "Parameter S_of_nat : nat -> 
S."
with the definition
...
Parameter some_element : S.
Definition S_of_nat (n : nat) : S := some_element.
...

we find that " then (has_property_X (combined (S_of_nat 0) x)) by general."
claims insufficient justification.

Unless I am missing something very basic here, this is indeed a problem with
c-zar. One should not be able to break a proof by making an element of the
global context more specific; c-zar proofs should be more robust than that, as
per the mission statement. What are your thoughts? 

    M-