Skip to content

Rewrite cross split lemmas so they can more easily be used for forward reasoning.

Robbert Krebbers requested to merge robbert/cross_split into master

Before our cross split lemmas looked like (we have such lemmas for Permutation, Qp, and maps):

  la ++ lb ≡ₚ l →
  lc ++ ld ≡ₚ l →
  ∃ lac lad lbc lbd,
    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.

This MR changes them to look like:

  la ++ lb ≡ₚ lc ++ ld →
  ∃ lac lad lbc lbd,
    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.

The explicit l in the old lemma statement was rather annoying. First, it made the proof longer (we immediately substituted it). Second, it made the lemma harder to use because you cannot use it with apply .. in .. or the % introduction pattern. Example in Iron that shows that the new lemma is easier:

diff --git a/theories/iron_logic/iron.v b/theories/iron_logic/iron.v
index 2723897..f8864da 100644
--- a/theories/iron_logic/iron.v
+++ b/theories/iron_logic/iron.v
@@ -171,8 +171,7 @@ Proof.
   rewrite /Uniform=> HP1 HP2 π1 π2. rewrite !fracPred_at_sep. apply (anti_symm _).
   - apply bi.exist_elim=> -[π1'|]; apply bi.exist_elim=> -[π2'|];
       apply bi.pure_elim_l; rewrite ?(inj_iff Some) //.
-    + intros. destruct (Qp_cross_split (π1 + π2) π1 π2 π1' π2')
-        as (π'&π''&π'''&π''''&<-&<-&<-&<-)=> //.
+    + intros (π'&π''&π'''&π''''&<-&<-&<-&<-)%Qp_cross_split.

Merge request reports