## Stream: Coq users

### Topic: Cannot find Proper instance of Parametric Morphism

#### Pablo Donato (Jun 15 2022 at 17:34):

Hi all,

I'm trying to use generalized rewriting to simplify some proofs in a basic metatheory of sequent calculus. Basically I have an inductive predicate `deriv : list form -> form -> Prop` for derivability of a sequent, written `Γ ⟹ C`, and its symmetric closure `eqderiv : form -> form -> Prop` for equiderivability of formulas, written `A ⟺ B`.

What I want is to be able to rewrite any hypothesis or conclusion `A` occurring in a (derivability statement for a) sequent into `B`, whenever I have an assumption `HAB: A ⟺ B`. Focusing only on the conclusion part, I understand the following declarations should be enough:

``````Instance equiv_eqderiv : Equivalence eqderiv.
Proof.

transitivity proved by Equivalence_Transitive
as eqderiv.

Add Parametric Morphism Γ : (λ C, Γ ⟹ C) with signature
eqderiv ==> iff
as proper_deriv_concl.
Proof.
``````

But now if I try rewriting, Coq is unable to find the right Proper instance, even though I can easily apply it manually:

``````Lemma eqderiv_concl {A B Γ} :
A ⟺ B ->
Γ ⟹ A <->
Γ ⟹ B.
Proof.
move => HAB. split; move => H.
* Fail rewrite -HAB.
by apply (proper_deriv_concl _ A B HAB).
* Fail rewrite HAB.
by apply (proper_deriv_concl _ A B HAB).
Qed.
``````

My question is thus: how can I make Coq find the Proper instance? Should I declare the Parametric Morphism in a different way?

#### Li-yao (Jun 15 2022 at 18:01):

eta-reduce `(λ C, Γ ⟹ C)` to `f Γ` where `f` is the function that `⟹` desugars to.

#### Pablo Donato (Jun 15 2022 at 19:15):

oh that's weird, I thought I already tried this but indeed it works, thanks! I still have the problem if I want to rewrite an hypothesis though, since I cannot simply eta-reduce:

``````Add Parametric Morphism Γ C : (λ A, deriv (A :: Γ) C) with signature
eqderiv ==> iff
as proper_deriv_hyp.
``````

The error message is:

``````Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X413==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ |- relation (list form)]
(internal placeholder) {?r}
?X414==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ |- relation (list form)]
(internal placeholder) {?r0}
?X415==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ (do_subrelation:=do_subrelation)
|- Proper (eqderiv ==> ?r0 ==> ?r) cons] (internal placeholder) {?p}
?X416==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ |- ProperProxy ?r0 Γ]
(internal placeholder) {?p0}
?X417==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ |- relation form]
(internal placeholder) {?r1}
?X418==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ (do_subrelation:=do_subrelation)
|- Proper (?r ==> ?r1 ==> flip impl) deriv] (internal placeholder) {?p1}
?X419==[A B C Γ HAB H _pattern_value_ _rewrite_rule_ |- ProperProxy ?r1 C]
(internal placeholder) {?p2}
TYPECLASSES:?X413 ?X414 ?X415 ?X416 ?X417 ?X418 ?X419
SHELF:||
FUTURE GOALS STACK:?X419 ?X418 ?X417 ?X416 ?X415 ?X414 ?X413||?X392 ?X391 ?X390 ?X389
?X388 ?X387
.
``````

This suggests that I should declare Proper instances separately for `cons` and `deriv`. But It is not clear which signatures I want. For `cons` I tried to get the following lemma:

``````∀ (C A A' : form) (Γ Γ' : list form), A ⟺ B -> Γ = Γ' -> A :: Γ ⟹ C <-> A' :: Γ' ⟹ C
``````

with this morphism:

``````Add Parametric Morphism C : cons with signature
eqderiv ==> eq ==> (λ Γ Γ', Γ ⟹ C <-> Γ' ⟹ C)
as proper_cons.
``````

but I still get the same error message, and I don't know what signature I should put for `deriv`.

#### Li-yao (Jun 15 2022 at 19:39):

Yes you'll need an equivalence relation on `list form`, maybe `Forall2 eqderiv`.

#### Li-yao (Jun 15 2022 at 19:45):

BTW for one less thing to fiddle with, you can remove `Add Relation`, an `Equivalence` instance subsumes it.

Last updated: Sep 23 2023 at 14:01 UTC