The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

I've been using dependent types to specify properties of various
things. So, for example, I might use the Inductive type sig and
construct inhabitants of that type using the exist constructor.

But when checking equality between two inhabitants I want to check
only the equality of the witnesses, not equality of the proof that
each witness satisfies that property.

I find myself forced to define equality in the way I need for every
such type that arises. Here is an example below.

Inductive equal_mod_sig (B : Set) (P : B -> Prop) (equalB : B -> B -> Prop) : 
si
g P -> sig P -> Prop :=
 | Equal_mod_sig : forall (b b' : B) (p : P b) (p' : P b'),
       equalB b b' -> equal_mod_sig
                                   equalB
                                   (exist P b p)
                                   (exist P b' p').

Then I prove that if equality between the witnesses is decidable then
my equality is decidable.

Lemma equal_mod_sig_dec : forall (B : Set) (P : B -> Prop) (equalB : B -> B 
-> P
rop),
 (forall (b b' : B), {equalB b b'} + {~ (equalB b b')}) ->
    (forall (s s' : sig P), {equal_mod_sig equalB s s'} + {~ (equal_mod_sig 
equ
alB s s')}).
....

Is there a general way to ignore proofs when deciding equality...or is
my current approach actually necessary?

Note that this arises in multiple other contexts as well, this is just
one example. Also, it gets a little more tedious since I want to prove
that each equality that I have so defined is in fact an equivalence
relation.

-mulhern