Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Opposite of the `transfer` method

Email Gateway (Aug 22 2022 at 20:07):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

I’m looking for a proof method that is like transfer but transforms
into the opposite direction.

Consider, for example, the following code:

axiomatization equivalence :: "[nat, nat] ⇒ bool" where
is_equi
valence:
"equivp equivalence"
and
is_compatible_with_plus
:
"⟦equivalence n n'; equivalence m m'⟧ ⟹
equivalence (n +
m) (n' + m')"

quotient_type abstract = nat / equivalence
using is_equivalence .

lift_definition abstract_plus :: "[abstract, abstract] ⇒ abstract"
is "(+)"
using is_compatible_with_plus .

The transfer method can replace equalities of abstract values by
equivalences of nat values:

lemma "abstract_plus a b = abstract_plus c d"
proof transfer
― ‹yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
oops

However, it does not perform the opposite conversion:

lemma "equivalence (a + b) (c + d)"
proof transfer
― ‹also yields \<^term>‹⋀a b c d. equivalence (a + b) (c + d)››
oops

Is there a proof method that replaces equivalences by equalities on a
corresponding quotient type? I know that there’s the transferred
attribute, but this works only for facts, not for goals.

The background of my question is that I’d like to employ the simplifier
for reasoning with arbitrary equivalences. The idea is to reduce a goal
that states an equivalence to a goal that states a corresponding
equality on a quotient type and then let the simplifier do equational
reasoning in that quotient type.

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:08):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
One step in the right direction might be to invoke the simplifier using
equations auto-generated by quotient_type and lift_definition, like
so:

lemma "equivalence (a + b) (c + d)"
proof (simp only: abstract.abs_eq_iff [THEN sym] abstract_plus.abs_eq [THEN sym])
― ‹yields \<^term>‹abstract_plus (abs_abstract a) (abs_abstract b) = abstract_plus (abs_abstract c) (abs_abstract d)››
oops

However, I wouldn’t like to specify the rewrite rules manually like in
this code snippet. Is there a way to automatically gather all
abs_eq_iff and abs_eq rules or perhaps only those that are related
to the equivalence relation used in the goal?

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:10):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Wolfgang,

Collecting the rewrite rules will not get you very far in general, because you need a
relational approach to deal with that; think of something like

list_all2 equivalence (map ((+) x) xs) (map ((+) y) ys)

That's why the transfer package uses a relation approach that is beyond the simplifier's
reach.

Now, unfortunately, the transfer package does not offer a proof method to from a raw type
(nat) to an abstract type. AFAIK the main reason for that is that it typically will not
work well. The transfer method assumes that only constants need to be replaced. This is
violated for lift_definition when the right-hand side is a compound term, which is the
usual case.

However, the whole machinery can also be made to work in the other directions; it's just
not implemented. Alternatively, you can manually define the reversed correspondence
relation rev_cr :: "nat => abstract => bool" as "rev_cr = conversep cr_abstract" and adapt
the transfer rules accordingly. But that's quite a bit of manual work.

Finally, the old quotient package by Cezary and Urban supports transferring in both
directions (Section 11.9.4 in isar-ref: quotient_definition instead of lift_definition,
methods lifting and descending). They also have the restriction in place that the raw term
must be a constant. Note however that this package is not so well integrated into the HOL
library as transfer.

Hope this helps,
Andreas

Email Gateway (Aug 22 2022 at 20:11):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi Wolfgang,

I’m unsure whether there is a proof method, however there is the “untransferred” attribute that
works in the opposite direction. So also transfer is to a certain extend bidirectional.

lemma "equivalence (a + b) (c + d)"
proof -
have "abstract_plus a b = abstract_plus c d" for a b c d sorry
from this[untransferred] show ?thesis .
qed

Perhaps this solves your goal.

Best,
René

Email Gateway (Aug 22 2022 at 20:11):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Dear Andreas,

thanks a lot for your response.

Collecting the rewrite rules will not get you very far in general,
because you need a relational approach to deal with that; think of
something like

list_all2 equivalence (map ((+) x) xs) (map ((+) y) ys)

That’s why the transfer package uses a relation approach that is
beyond the simplifier’s reach.

Well, in my use cases, premises and conclusions are always applications
of equivalence relations. I guess invoking those rewrite rules will work
for turning these applications of equivalence relations into equalities
on the quotient type. However, I’d still like to avoid this approach,
since it means too much manual work for my taste.

Finally, the old quotient package by Cezary and Urban supports
transferring in both directions (Section 11.9.4 in isar-ref:
quotient_definition instead of lift_definition, methods lifting
and descending).

I tried with the old quotient package, but it didn’t work for me.
Consider my example code adapted to the old package:

axiomatization equivalence :: "[nat, nat] ⇒ bool" where
is_equivalence:
"equivp equivalence"
and
is_compatible_with_plus:
"⟦equivalence n n'; equivalence m m'⟧ ⟹
equivalence (n + m) (n' + m')"

quotient_type abstract = nat / equivalence
using is_equivalence .

quotient_definition "abstract_plus :: [abstract, abstract] ⇒ abstract"
is "(+) :: [nat, nat] ⇒ nat"
using is_compatible_with_plus .

Now assume I have a goal equivalence (a + b) (c + d) and I want it to
be turned into the goal abstract_plus x y = abstract_plus z u. Neither
applying lifting nor applying descending does that: lifting leaves
the goal in place; descending just adds explicit universal
quantification of the variables via ⋀. What am I doing wrong here?

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:11):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi, René!

Thanks a lot for your response.

Technically, your solution would work. However, it would mean that the
user would have to add a considerable amount of boilerplate, because
stating the equations on the quotient types is necessary.

Maybe I should explain a bit more the background of my question.

I’m working with a process calculus. I have an algebraic data type
process of processes (or rather process terms) and several
bisimilarity relations, which describe different notions of behavioral
equivalence.

Most of the proofs I’m conducting are proofs of bisimilarities, proving
goals of the form p ∼ q where p and q are processes and (∼) is
one of the bisimilarity relations. In many of these proofs, I’m using
calculational reasoning, exploiting the fact that (∼) is transitive.

There are certain core facts about the bisimilarity relations that state
things like transitivity and commutativity of certain process operators
modulo bisimilarity, things like (p ∥ q) ∥ r ∼ p ∥ (q ∥ r) and p ∥ q ∼ q ∥ p. Having to apply these facts manually in the proofs is really
painful. My goal is to have a proof method that applies such technical
facts as rewrite rules, analogously to what the simplifier does with
equations.

For example, in a proof I might have something like the following:

from "p ∼ q ∥ r" have "p ∥ q ∼ r ∥ (q ∥ q)" sorry

I’d like to replace the sorry with something as simple as by simp.
While your approach would work, it would mean I had to add a quotient
type version of every single proof step.

Of course, it would be an option to translate the overall bisimilarity
goal of each proof into a goal about quotient type equations and then
reason in the quotient type throughout the proof. However, this would
feel quite unnatural to me. The main reason is that there’s not a single
best bisimilarity but there are multiple ones; so I would have to work
with several quotient types and convert back and forth between them.

I was considering using quotient types only internally as a means to
make the simplifier reason with arbitrary equivalences. The basic idea
is to translate both the goal and the rewrite rules (like p ∥ q ∼ q ∥ p) into statements that use equality on quotient types and then
employ the simplifier to solve the new goals entirely.

I’m wondering how others reason with equivalence relations. Somehow I
can’t imagine that a situation like mine is so rare; so I’d be surprised
if there isn’t an approach to performing “equivalence reasoning”
conveniently. Any hints?

All the best,
Wolfgang

Email Gateway (Aug 22 2022 at 20:11):

From: Peter Lammich <lammich@in.tum.de>

I’m wondering how others reason with equivalence relations. Somehow I
can’t imagine that a situation like mine is so rare; so I’d be
surprised
if there isn’t an approach to performing “equivalence reasoning”
conveniently. Any hints?

Coq has a setoid rewrite engine, which might be what you want here?.
The idea is to rewrite wrt arbitrary preorders.

Up to my knowledge, such a thing has not yet been implemented in
Isabelle (though I'm collecting possible applications, as I might
implement such a thing sooner or later ;) )

Email Gateway (Aug 22 2022 at 20:11):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Am Donnerstag, den 04.07.2019, 17:26 +0100 schrieb Peter Lammich:

I’m wondering how others reason with equivalence relations. Somehow
I can’t imagine that a situation like mine is so rare; so I’d be
surprised if there isn’t an approach to performing “equivalence
reasoning” conveniently. Any hints?

Coq has a setoid rewrite engine, which might be what you want here?

Well, I’d want something like that for Isabelle. 😉

I have a considerable amount of Isabelle code, which I wouldn’t like to
translate to Coq, for three reasons:

* The translation would take a lot of time.

* The translation would perhaps not be straightforward because of
Coq’s constructivity.

* Coq doesn’t have a proper proof language along the lines of Isar.

Up to my knowledge, such a thing has not yet been implemented in
Isabelle (though I’m collecting possible applications, as I might
implement such a thing sooner or later 😉).

Please implement it! :pray:

All the best,
Wolfgang

Last updated: Nov 21 2024 at 12:39 UTC