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



Am Donnerstag, den 04.07.2019, 06:28 +0000 schrieb Thiemann, René:
> 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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.