The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello everyone,

Is it possible to use setoid rewriting when constructing inhabitants of
type families (X -> Type).

I have some developments proving meta-theoretic properties of proof
systems (e.g., Hilbert style systems or sequent systems). So far I've
been formalizing proof systems as inductive predicates of type:

        formula (or sequent) -> Prop

The main reason for this is that I make extensive use of setoid
rewriting to replace formulas by provably equivalent ones.

However, treating proofs of deeply embedded calculi as computational
objects seems more natural to me. Moreover, this allow defining
functions from proofs to nat (e.g, for the size of a proof). However, I
would still want to use setoid rewriting where the shape of the proof is
irrelevant.

I recall being told that prior to the introduction of universe
polymorphism, setoid could not be used for type families. So now that we
have universe polymorphism, is this reasonable now? If so, what would I
need to do to set this up?

Thanks in advance,
Christian