The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Christian,

  indeed there is a variant of setoid_rewrite for computational relations,

which requires you to use the CMorphisms and CRelationClasses (C for computational) 

libraries instead of the usual Morphisms and RelationClasses libraries. 

Using the definitions in there you can define Proper instances for your

constants where the relation is computational (typically using iffT instead of iff, arrow instead

of logical implication), to be used by setoid_rewrite.

Hope this helps,

-- Matthieu

On Sun, Oct 8, 2017 at 11:40 PM Christian Doczkal <christian.doczkal AT ens-lyon.fr> wrote:

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