The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Christian,

  it is a bad interaction with unfolding: as you can see in ?X59 the inferred relation

for the rewritten subterm is the expansion of prv_Imp : (fun x y => prv (Imp x y)), 

and unification fails in this case. I would advise to phrase axFE using prv_imp instead

of prv (Imp FF s) and preserve this (definitional) abstraction throughout. 

 More in depth, the problem comes from a difference between CMorphisms and Morphisms:

the former does not enforce that the universe polymorphic [flip] constant is opaque for 

unifications done during proof search (using Typeclasses Opaque flip) while the non-polymorphic 

flip is, so the proof search is driven in a path where unifications fail because of the unfolding. 

You can simply set this command to restore compatibility (it's a bug that the polymorphic flip

is not declared opaque for resolution) and see where it gets you, but beware that rewriting with 

the "expanded" relation will probably get you in more trouble along the way. To debug this I compared the 

traces of resolution using [Set Typeclasses Debug] and [Set Typeclasses Debug Verbosity 2].

Hope this helps,

-- Matthieu

On Mon, Oct 9, 2017 at 4:36 PM Christian Doczkal <christian.doczkal AT ens-lyon.fr> wrote:

Hi Matthieu,

Thanks, for the pointers. That did get me started, but not quite off the
ground yet. I now have examples of (simple) rewrites that succeed in the
Prop and in the Type formulations. But the first thing involving
contravariance fails in the Type formulation. (I need preorders and
contravariant morphisms)

I get failures involving do_subrelation such as the one below. I
attached two files, the formulation in Prop where the rewrite works and
the one in Type where it fails.

Tactic failure: setoid rewrite failed: Unable to satisfy the following
constraints:
UNDEFINED EVARS:
 ?X57==[s |- crelation form] (internal placeholder) {?c}
 ?X58==[s |- crelation form] (internal placeholder) {?c0}
 ?X59==[s (do_subrelation:=do_subrelation)
         |- Proper
              ((fun x y : form => prv (x ---> y)) ==>
               ?X58@{__:=s} ==> ?X57@{__:=s}) Imp] (internal
placeholder) {?p}
 ?X60==[s |- ProperProxy ?X58@{__:=s} s] (internal placeholder) {?p0}
 ?X61==[s (do_subrelation:=do_subrelation)
         |- Proper (?X57@{__:=s} ==> flip arrow) prv] (internal
placeholder) {?p1}
.

I don't know enough about the internals of type class resolution to make
sense of this. Maybe you know what is going wrong here.

Best,
Christian

On 09/10/17 10:16, Matthieu Sozeau wrote:
> 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 <mailto: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
>