Skip to content

Use solely canonical structures for language hierarchy.

Robbert Krebbers requested to merge ci/robbert/canonical_language into master

As @jung observed in !87 (merged), Coq is unable to infer CtxLanguage instances. This problem was there before already, and as such, we already duplicated lemmas like wp_bind a bunch of times. For example, in lifting we had:

Lemma wp_ectx_bind {E Φ} K e :
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.

The problem here is that we mixed canonical structures and type classes in a rather odd way for the hierarchy of languages (language, ectxLanguage, ectxiLanguage): language was a canonical structures, but ectxLanguage and ectxiLanguage were type classes.

In this MR, I have repaired this issue: I am now using solely canonical structures for the three layers of the language hierarchy.

FWIW: Similar to the canonical structures for OFEs, cameras, and soon BIs, I have also factored out the laws into a mixin.

Edited by Robbert Krebbers

Merge request reports