General-purpose lemmas from building abstract interpreters. These are almost all lemmas about how existing constructions interact which each other or inversion principles. Not all are used in my codebase anymore, but I figure they're worth keeping around...
Changes:
Props/Leaf.v:
Correspondence with has_post: has_post_Leaf and has_post_Leaf_equiv. These make Props/Leaf.v depend on Props/HasPost.v; not sure where else to put them to avoid that.
Inversion lemmas for iter based based on invariants of body's leaves: Leaf_iter_inv, Leaf_interp_iter_inv, and Leaf_interp_state_iter_inv. The state version is quite juicy because it requires re-phrasing relations.
"Neutrality" of interp for Leaf, ie. x ∈ interp h t -> x ∈ t. This needs a special induction on t. Two versions: Leaf_interp_inv, Leaf_interp_state_inv.
Same for translate: Leaf_translate_inv.
Props/Finite.v:
all_finite_trigger (no hypothesis), any_finite_trigger (requires inhabitant).
all_finite_translate, any_finite_translate.
Core/Subevent.v:
Global instance void1 -< E.
Simplification lemmas for subevent ReSum_inl = inl1 and subevent ReSum_inr = inr1. These don't reduce with cbn (not sure why) so at least we can rewrite manually.
Eq/UpToTaus.v:
Specialization of eutt_eq_bind for the equality relation: eutt_eq_bind'.
A result on swapping RR for a super-relation over the diagonal when dealing with eutt RR t t: eutt_sub_self.
Interp/InterpFacts.v:
Variation of interp_iter' which uses eutt for the body and conclusion: interp_iter'_eutt.
translate_iter (not in TranslateFacts because uses the translate/interp correspondence).
Interp/StateFacts.v:
Specialization of eutt_interp_state_iter for equality (≈), in a way that is suitable to rewrite interp_state (iter ...): eutt_eq_interp_state_iter.
Variation of interp_state_iter' which uses eutt (instead of state_eq which is eq_itree): interp_state_iter'_eutt.
Interp/TranslateFacts.v:
An inversion lemma: translate_Vis_inv. There could probably be more.
Lysxia
commented
1 year ago
General-purpose lemmas from building abstract interpreters. These are almost all lemmas about how existing constructions interact which each other or inversion principles. Not all are used in my codebase anymore, but I figure they're worth keeping around...
Changes:
Props/Leaf.v:has_post:has_post_Leafandhas_post_Leaf_equiv. These makeProps/Leaf.vdepend onProps/HasPost.v; not sure where else to put them to avoid that.Leaf_iter_inv,Leaf_interp_iter_inv, andLeaf_interp_state_iter_inv. The state version is quite juicy because it requires re-phrasing relations.interpforLeaf, ie.x ∈ interp h t -> x ∈ t. This needs a special induction ont. Two versions:Leaf_interp_inv,Leaf_interp_state_inv.translate:Leaf_translate_inv.Props/Finite.v:all_finite_trigger(no hypothesis),any_finite_trigger(requires inhabitant).all_finite_translate,any_finite_translate.Core/Subevent.v:void1 -< E.subevent ReSum_inl = inl1andsubevent ReSum_inr = inr1. These don't reduce withcbn(not sure why) so at least we can rewrite manually.Eq/UpToTaus.v:eutt_eq_bindfor the equality relation:eutt_eq_bind'.RRfor a super-relation over the diagonal when dealing witheutt RR t t:eutt_sub_self.Interp/InterpFacts.v:interp_iter'which useseuttfor the body and conclusion:interp_iter'_eutt.translate_iter(not inTranslateFactsbecause uses the translate/interp correspondence).Interp/StateFacts.v:eutt_interp_state_iterfor equality (≈), in a way that is suitable to rewriteinterp_state (iter ...):eutt_eq_interp_state_iter.interp_state_iter'which useseutt(instead ofstate_eqwhich iseq_itree):interp_state_iter'_eutt.Interp/TranslateFacts.v:translate_Vis_inv. There could probably be more.