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.
Admitted.
Add Relation form eqderiv
transitivity proved by Equivalence_Transitive
as eqderiv.
Add Parametric Morphism Γ : (λ C, Γ ⟹ C) with signature
eqderiv ==> iff
as proper_deriv_concl.
Proof.
Admitted.
```

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?

eta-reduce `(λ C, Γ ⟹ C)`

to `f Γ`

where `f`

is the function that `⟹`

desugars to.

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`

.

Yes you'll need an equivalence relation on `list form`

, maybe `Forall2 eqderiv`

.

BTW for one less thing to fiddle with, you can remove `Add Relation`

, an `Equivalence`

instance subsumes it.

Last updated: Jun 18 2024 at 22:01 UTC