more generic representation of bunches

allows us to remove a lot of duplication in the code
co-dan · Jul 15, 2023 · 30c22ff · 30c22ff
1 parent 369198a
commit 30c22ff
Show file tree

Hide file tree

Showing 8 changed files with 508 additions and 1,621 deletions.
diff --git a/theories/analytic_completion.v b/theories/analytic_completion.v
@@ -24,7 +24,7 @@ End analytic_completion.
 (** Example: restricted form of weakening: [a ∗ a ≤ a]
     and it's analytic presentation [a₁ * a₂ ≤ a₁ ∨ a₂] *)
 
-Example rule_restr_weakn : structural_rule := ([Var 0], TComma (Var 0) (Var 0)).
+Example rule_restr_weakn : structural_rule := ([Var 0], TBin Comma (Var 0) (Var 0)).
 Example rule_restr_weakn_a := analytic_completion rule_restr_weakn.
 Eval vm_compute in rule_restr_weakn_a.
 
@@ -56,7 +56,7 @@ Section analytic_completion_correct.
   Proof.
     rewrite /disj_ren_inverse /ren_inverse /linearize_bterm_ren /linearize_bterm.
     generalize 0.
-    induction T as [x | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 ]=>i; simpl.
+    induction T as [x | sp T1 IHT1 T2 IHT2 ]=>i; simpl.
     - apply (bi.exist_intro' _ _ i).
       apply bi.and_intro; eauto. apply bi.pure_intro.
       rewrite lookup_total_preimage. apply lookup_singleton.
@@ -86,45 +86,21 @@ Section analytic_completion_correct.
         apply bi.exist_mono'=>k. do 2 f_equiv.
         rewrite !lookup_total_preimage.
         intro. by apply lookup_union_Some_r. }
-    - specialize (IHT1 i).
-      destruct (linearize_pre T1 i) as [[i1 m1] T1'] eqn:Ht1.
-      specialize (IHT2 i1).
-      destruct (linearize_pre T2 i1) as [[i2 m2] T2'] eqn:Ht2. simpl.
-      assert (dom m1 = set_seq i (i1-i)) as Hm1.
-      { replace i1 with (fst $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        replace m1 with (snd $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        apply linearize_pre_dom. }
-      assert (dom m2 = set_seq i1 (i2-i1)) as Hm2.
-      { replace i2 with (fst $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        replace m2 with (snd $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        apply linearize_pre_dom. }
-      assert (m1 ##ₘ m2) as Hm1m2disj.
-      { apply map_disjoint_dom_2. rewrite Hm1 Hm2.
-        set_unfold. lia. }
-      f_equiv.
-      { rewrite IHT1 /=.
-        apply bterm_alg_act_mono=>j.
-        apply bi.exist_mono'=>k. do 2 f_equiv.
-        rewrite !lookup_total_preimage. intro. by apply lookup_union_Some_l. }
-      { rewrite IHT2 /=.
-        apply bterm_alg_act_mono=>j.
-        apply bi.exist_mono'=>k. do 2 f_equiv.
-        rewrite !lookup_total_preimage. intro. by apply lookup_union_Some_r. }
   Qed.
 
   Lemma bterm_alg_act_renaming'' Tz Xs :
     bterm_alg_act Tz (linearize_bterm_ren_act Xs) ≡ bterm_alg_act ((λ n, linearize_bterm_ren T !!! n) <$> Tz) Xs.
   Proof.
     rewrite /linearize_bterm_ren_act.
-    induction Tz as [x | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 ]; eauto; simpl; by f_equiv.
+    induction Tz as [x | [] T1 IHT1 T2 IHT2]; eauto; simpl; by f_equiv.
   Qed.
 
   Lemma bterm_alg_act_disj_ren_inverse_transform Tz Xs :
     bterm_alg_act Tz (disj_ren_inverse Xs) -∗ ∃ Tk, ⌜Tk ∈ transform_premise Tz⌝ ∧ bterm_alg_act Tk Xs.
   Proof.
     rewrite /disj_ren_inverse /transform_premise /linearize_bterm /linearize_bterm_ren.
     generalize 0.
-    induction Tz as [x | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 ]=>idx; simpl.
+    induction Tz as [x | sp T1 IHT1 T2 IHT2]=>idx; simpl.
     - apply bi.exist_elim=>k. apply bi.pure_elim_l=>Hk.
       apply (bi.exist_intro' _ _ (Var k)). apply bi.and_intro; eauto.
       apply bi.pure_intro. eapply elem_of_map_2. by rewrite lookup_total_singleton.
@@ -154,78 +130,54 @@ Section analytic_completion_correct.
         replace idx2 with (fst $ fst (linearize_pre T2 idx1)) by rewrite Ht2 //.
         apply linearize_pre_fv. }
 
-      rewrite IHT1 . rewrite bi.sep_exist_r. apply bi.exist_elim=>Tk1.
-      rewrite bi.sep_and_r. rewrite bi.pure_sep_l.
-      apply bi.pure_elim_l=>Hk1.
-      rewrite IHT2. rewrite comm. rewrite bi.sep_exist_r. apply bi.exist_elim=>Tk2.
-      rewrite bi.sep_and_r. rewrite bi.pure_sep_l.
-      apply bi.pure_elim_l=>Hk2. rewrite comm.
-      apply (bi.exist_intro' _ _ (TComma Tk1 Tk2)). apply bi.and_intro; simpl; last by f_equiv.
-      apply bi.pure_intro.
-      apply sets.elem_of_set_map_2. eexists _,_. repeat split; eauto.
-      + simpl in Hk1.
-        enough ((λ j : nat, ren_inverse !!! (m1 !!! j)) <$> T1' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T1'))
-          as <-; first done.
-        apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
-        rewrite !lookup_total_alt. f_equiv.
-        symmetry. apply lookup_union_l'. apply elem_of_dom.
-        set_unfold. naive_solver.
-      + simpl in Hk2.
-        enough ((λ j : nat, ren_inverse !!! (m2 !!! j)) <$> T2' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T2'))
-          as <-; first done.
-        apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
-        rewrite !lookup_total_alt. f_equiv.
-        symmetry. apply lookup_union_r. apply not_elem_of_dom.
-        set_unfold. intros Hx'. apply Hfv2 in Hx. apply Hm1 in Hx'. lia.
-    - specialize (IHT1 idx).
-      destruct (linearize_pre T1 idx) as [[idx1 m1] T1'] eqn:Ht1.
-      specialize (IHT2 idx1).
-      destruct (linearize_pre T2 idx1) as [[idx2 m2] T2'] eqn:Ht2.
-
-      assert (dom m1 = set_seq idx (idx1-idx)) as Hm1.
-      { replace idx1 with (fst $ fst (linearize_pre T1 idx)) by rewrite Ht1 //.
-        replace m1 with (snd $ fst (linearize_pre T1 idx)) by rewrite Ht1 //.
-        apply linearize_pre_dom. }
-      assert (dom m2 = set_seq idx1 (idx2-idx1)) as Hm2.
-      { replace idx2 with (fst $ fst (linearize_pre T2 idx1)) by rewrite Ht2 //.
-        replace m2 with (snd $ fst (linearize_pre T2 idx1)) by rewrite Ht2 //.
-        apply linearize_pre_dom. }
-      assert (m1 ##ₘ m2) as Hm1m2disj.
-      { apply map_disjoint_dom_2. rewrite Hm1 Hm2.
-        set_unfold. lia. }
-
-      assert (term_fv T1' ⊆ set_seq idx (idx1-idx)) as Hfv1.
-      { replace T1' with (snd (linearize_pre T1 idx)) by rewrite Ht1 //.
-        replace idx1 with (fst $ fst (linearize_pre T1 idx)) by rewrite Ht1 //.
-        apply linearize_pre_fv. }
-      assert (term_fv T2' ⊆ set_seq idx1 (idx2-idx1)) as Hfv2.
-      { replace T2' with (snd (linearize_pre T2 idx1)) by rewrite Ht2 //.
-        replace idx2 with (fst $ fst (linearize_pre T2 idx1)) by rewrite Ht2 //.
-        apply linearize_pre_fv. }
-
-      rewrite IHT1. rewrite bi.and_exist_r. apply bi.exist_elim=>Tk1.
-      rewrite -assoc.
-      apply bi.pure_elim_l=>Hk1.
-      rewrite IHT2. rewrite comm. rewrite bi.and_exist_r. apply bi.exist_elim=>Tk2.
-      rewrite -assoc.
-      apply bi.pure_elim_l=>Hk2. rewrite comm.
-      apply (bi.exist_intro' _ _ (TSemic Tk1 Tk2)). apply bi.and_intro; simpl; last by f_equiv.
-      apply bi.pure_intro.
-      apply sets.elem_of_set_map_2. eexists _,_. repeat split; eauto.
-      + simpl in Hk1.
-        enough ((λ j : nat, ren_inverse !!! (m1 !!! j)) <$> T1' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T1'))
-          as <-; first done.
-        apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
-        rewrite !lookup_total_alt. f_equiv.
-        symmetry. apply lookup_union_l'. apply elem_of_dom.
-        set_unfold. naive_solver.
-      + simpl in Hk2.
-        enough ((λ j : nat, ren_inverse !!! (m2 !!! j)) <$> T2' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T2'))
-          as <-; first done.
-        apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
-        rewrite !lookup_total_alt. f_equiv.
-        symmetry. apply lookup_union_r. apply not_elem_of_dom.
-        set_unfold. intros Hx'. apply Hfv2 in Hx. apply Hm1 in Hx'. lia.
+      rewrite IHT1.
+      destruct sp; simpl.
+      { rewrite bi.sep_exist_r. apply bi.exist_elim=>Tk1.
+        rewrite bi.sep_and_r. rewrite bi.pure_sep_l.
+        apply bi.pure_elim_l=>Hk1.
+        rewrite IHT2. rewrite comm. rewrite bi.sep_exist_r. apply bi.exist_elim=>Tk2.
+        rewrite bi.sep_and_r. rewrite bi.pure_sep_l.
+        apply bi.pure_elim_l=>Hk2. rewrite comm.
+        apply (bi.exist_intro' _ _ (TBin Comma Tk1 Tk2)). apply bi.and_intro; simpl; last by f_equiv.
+        apply bi.pure_intro.
+        apply sets.elem_of_set_map_2. eexists _,_. repeat split; eauto.
+        + simpl in Hk1.
+          enough ((λ j : nat, ren_inverse !!! (m1 !!! j)) <$> T1' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T1'))
+            as <-; first done.
+          apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
+          rewrite !lookup_total_alt. f_equiv.
+          symmetry. apply lookup_union_l'. apply elem_of_dom.
+          set_unfold. naive_solver.
+        + simpl in Hk2.
+          enough ((λ j : nat, ren_inverse !!! (m2 !!! j)) <$> T2' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T2'))
+            as <-; first done.
+          apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
+          rewrite !lookup_total_alt. f_equiv.
+          symmetry. apply lookup_union_r. apply not_elem_of_dom.
+          set_unfold. intros Hx'. apply Hfv2 in Hx. apply Hm1 in Hx'. lia. }
+      { rewrite bi.and_exist_r. apply bi.exist_elim=>Tk1.
+        rewrite -assoc.
+        apply bi.pure_elim_l=>Hk1.
+        rewrite IHT2. rewrite comm. rewrite bi.and_exist_r. apply bi.exist_elim=>Tk2.
+        rewrite -assoc.
+        apply bi.pure_elim_l=>Hk2. rewrite comm.
+        apply (bi.exist_intro' _ _ (TBin SemiC Tk1 Tk2)). apply bi.and_intro; simpl; last by f_equiv.
+        apply bi.pure_intro.
+        apply sets.elem_of_set_map_2. eexists _,_. repeat split; eauto.
+        + simpl in Hk1.
+          enough ((λ j : nat, ren_inverse !!! (m1 !!! j)) <$> T1' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T1'))
+            as <-; first done.
+          apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
+          rewrite !lookup_total_alt. f_equiv.
+          symmetry. apply lookup_union_l'. apply elem_of_dom.
+          set_unfold. naive_solver.
+        + simpl in Hk2.
+          enough ((λ j : nat, ren_inverse !!! (m2 !!! j)) <$> T2' = ((λ j : nat, ren_inverse !!! ((m1 ∪ m2) !!! j)) <$> T2'))
+            as <-; first done.
+          apply bterm_fmap_ext; last done. intros x Hx. f_equiv.
+          rewrite !lookup_total_alt. f_equiv.
+          symmetry. apply lookup_union_r. apply not_elem_of_dom.
+          set_unfold. intros Hx'. apply Hfv2 in Hx. apply Hm1 in Hx'. lia. }
   Qed.
 
   Lemma elem_of_map_ren_ren_inverse x y :
@@ -264,7 +216,7 @@ Section analytic_completion_correct.
     clear Hg. revert HHH.
     rewrite /(linearize_bterm_ren Tz) /(linearize_bterm Tz).
     generalize 0.
-    induction Tz as [x | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 ]=>i; simpl.
+    induction Tz as [x | sp T1 IHT1 T2 IHT2]=>i; simpl.
     - intros H1. f_equiv.
       etrans. { apply H1. by apply elem_of_singleton. }
       apply lookup_total_singleton.
@@ -300,46 +252,14 @@ Section analytic_completion_correct.
         - rewrite !lookup_total_alt. f_equiv.
           apply lookup_union_r. apply not_elem_of_dom.
           rewrite Hm1. set_unfold. naive_solver lia. }
-    - intros H1.
-      specialize (IHT1 i).
-      destruct (linearize_pre T1 i) as [[i1 m1] T1'] eqn:Ht1.
-      specialize (IHT2 i1).
-      destruct (linearize_pre T2 i1) as [[i2 m2] T2'] eqn:Ht2.
-      assert (term_fv T1' ⊆ set_seq i (i1-i)).
-      { replace T1' with (snd (linearize_pre T1 i)) by rewrite Ht1 //.
-        replace i1 with (fst $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        apply linearize_pre_fv. }
-      assert (term_fv T2' ⊆ set_seq i1 (i2-i1)).
-      { replace T2' with (snd (linearize_pre T2 i1)) by rewrite Ht2 //.
-        replace i2 with (fst $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        apply linearize_pre_fv. }
-      assert (dom m1 = set_seq i (i1-i)) as Hm1.
-      { replace i1 with (fst $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        replace m1 with (snd $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        apply linearize_pre_dom. }
-      assert (dom m2 = set_seq i1 (i2-i1)) as Hm2.
-      { replace i2 with (fst $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        replace m2 with (snd $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        apply linearize_pre_dom. }
-      simpl. f_equiv.
-      { apply IHT1. intros j Hj. simpl in *. trans ((m1 ∪ m2) !!! j).
-        - apply H1. set_solver.
-        - rewrite !lookup_total_alt. f_equiv.
-          apply lookup_union_l'.
-          apply elem_of_dom. rewrite Hm1. naive_solver. }
-      { apply IHT2. intros j Hj. simpl in *. trans ((m1 ∪ m2) !!! j).
-        - apply H1. set_solver.
-        - rewrite !lookup_total_alt. f_equiv.
-          apply lookup_union_r. apply not_elem_of_dom.
-          rewrite Hm1. set_unfold. naive_solver lia. }
   Qed.
 
   Lemma linearize_bterm_act_ren Xs:
     bterm_alg_act (linearize_bterm T) (linearize_bterm_ren_act Xs) ≡ bterm_alg_act T Xs.
   Proof.
     rewrite /linearize_bterm_ren_act /linearize_bterm_ren /linearize_bterm.
     generalize 0.
-    induction T as [x | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 ]=>i; simpl.
+    induction T as [x | sp T1 IHT1 T2 IHT2]=>i; simpl.
     - by rewrite lookup_total_singleton.
     - specialize (IHT1 i).
       destruct (linearize_pre T1 i) as [[i1 m1] T1'] eqn:Ht1.
@@ -373,38 +293,6 @@ Section analytic_completion_correct.
         assert ((m1 ∪ m2) !!! j = m2 !!! j) as ->; eauto.
         unfold lookup_total, map_lookup_total. f_equiv.
         apply lookup_union_r. apply not_elem_of_dom. rewrite Hm1. set_solver by lia.
-    - specialize (IHT1 i).
-      destruct (linearize_pre T1 i) as [[i1 m1] T1'] eqn:Ht1.
-      specialize (IHT2 i1).
-      destruct (linearize_pre T2 i1) as [[i2 m2] T2'] eqn:Ht2.
-      assert (term_fv T1' ⊆ set_seq i (i1-i)).
-      { replace T1' with (snd (linearize_pre T1 i)) by rewrite Ht1 //.
-        replace i1 with (fst $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        apply linearize_pre_fv. }
-      assert (term_fv T2' ⊆ set_seq i1 (i2-i1)).
-      { replace T2' with (snd (linearize_pre T2 i1)) by rewrite Ht2 //.
-        replace i2 with (fst $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        apply linearize_pre_fv. }
-      assert (dom m1 = set_seq i (i1-i)) as Hm1.
-      { replace i1 with (fst $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        replace m1 with (snd $ fst (linearize_pre T1 i)) by rewrite Ht1 //.
-        apply linearize_pre_dom. }
-      assert (dom m2 = set_seq i1 (i2-i1)) as Hm2.
-      { replace i2 with (fst $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        replace m2 with (snd $ fst (linearize_pre T2 i1)) by rewrite Ht2 //.
-        apply linearize_pre_dom. }
-      simpl. repeat split; eauto.
-      rewrite -IHT1 -IHT2. f_equiv.
-      + eapply bterm_alg_act_fv.
-        intros j Hj.
-        assert ((m1 ∪ m2) !!! j = m1 !!! j) as ->; eauto.
-        unfold lookup_total, map_lookup_total. f_equiv.
-        apply lookup_union_l', elem_of_dom. rewrite Hm1. set_solver by lia.
-      + eapply bterm_alg_act_fv.
-        intros j Hj.
-        assert ((m1 ∪ m2) !!! j = m2 !!! j) as ->; eauto.
-        unfold lookup_total, map_lookup_total. f_equiv.
-        apply lookup_union_r. apply not_elem_of_dom. rewrite Hm1. set_solver by lia.
   Qed.
 
 End analytic_completion_correct.