Computing correctly with inductive relations
Zoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos · 2022
Inductive relations are the predominant way of writing specifications in mechanized proof developments. Compared to purely functional specifications, they enjoy increased expressive power and facilitate more compositional reasoning. However, inductive relations also come with a significant drawback: they can’t be used for computation.