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



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! 🙏

All the best,
Wolfgang





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