Stream: General

Topic: Where is the `coinduction` proof method documented?

view this post on Zulip Wolfgang Jeltsch (Mar 30 2023 at 19:07):

The Isabelle/Isar Reference Manual documents the proof methods induct, induction, and coinduct. However, there is also the proof method coinduction. Compared to coinduct, coinduction seems to be superior; in particular, it can derive the bisimulation relation to use from the goal, something that coinduct apparently can’t do. I cannot remember having seen coinduction documented anywhere; I only encountered it in some AFP proof. Is there a documentation of coinduction somewhere?

view this post on Zulip Wolfgang Jeltsch (Mar 31 2023 at 20:20):

Oh, it seems that my coworker, @Javier Diaz, has already found it: it’s already cited in a paper we’re currently writing. :sweat_smile: Thank you, Javi, my related-work wonder. :grinning_face_with_smiling_eyes: The document I sought is the paper Truly Modular (Co)datatypes for Isabelle/HOL.

Last updated: Dec 07 2023 at 08:19 UTC