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



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

On 03/07/2019 23:52, Wolfgang Jeltsch wrote:
Am Mittwoch, den 03.07.2019, 23:03 +0300 schrieb Wolfgang Jeltsch:
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_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 .

     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

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







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