Stream: Coq users

Topic: Cannot find Proper instance of Parametric Morphism

view this post on Zulip 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.
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?

view this post on Zulip Li-yao (Jun 15 2022 at 18:01):

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

view this post on Zulip 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.

view this post on Zulip Li-yao (Jun 15 2022 at 19:39):

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

view this post on Zulip 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: Apr 19 2024 at 12:02 UTC