The Coq mailing list

[Bjarke Dahl Ebert <ebert AT irisa.fr>]

Hello Coq Club.

I have a problem regarding the interrelations between values of
Prop-kind and values of Set-kind.

In my application, I deal with functions of type (sig A P). In a certain
proof I come to the following subgoal:
  (cp1 (exist nat (bounds_pred b1) x0 y0))
    =(cp1 (exist nat [x1:nat](bounds_pred b1 x1) x0 y))

where cp1 has Set-kind.

The (bounds_pred b1) =? [x1:nat](bounds_pred b1 x1) is not a problem
here. Coq can see that they are equal by eta-reduction.

The problem is y0 =? y.

In fact, I might in the concrete situation be able to prove that y==y0,
but I don't want to. I want the head equality to hold whether or not
y==y0 holds. Because, y and y0 are just two proofs of the fact
(bounds_pred b1 x0), and for proofs we should not care about their
value, only their type (and the fact that they exist -- i.e. the
inhabitation of the type).

And if I understand it correctly, the type checker of Coq will not allow
us to define a function cp1 of Set-kind that depends on the value of a
Prop-term. But is the fact, that such functions cannot exist, a theorem
in Coq?

So far, I have just taken this as an axiom:

(* All functions on (sig A P) factorizes through proj1_sig *)
Axiom Prop_Set_confinement : 
    (A,B:Set) (P:A->Prop)
    (f:(sig A P)->B) (x1,x2:(sig A P)) 
    (proj1_sig A P x1)=(proj1_sig A P x2) -> (f x1)=(f x2).

which states that a Set-function on a (sig A P) domain depends only on
the A-art.


My questions are:
 1. Is the statement of the axiom wrong?
 2. Is the statement provable in Coq without the need of this axiom?



Kind regards,
Bjarke Ebert


-- 
IRISA-INRIA, Campus de Beaulieu, 35042 Rennes cedex, France
Home page: http://www.irisa.fr/compose/ebert/