more proof reuse

theories/examples/stack/proof_elim_graph.v

@@ -1736,7 +1736,7 @@ Proof.
       - by rewrite /G' /= SCSO.
       - (* stack_LIFO *)
         apply (stack_LIFO_insert_edge _ _ _ _ _ _ EqeVps EqeVs); [|done..]. clear.
-        intros u1 o1 [_ In1]%gcons_com_included [_ Lto1] _.
+        intros u1 o1 _ [_ In1]%gcons_com_included [_ Lto1] _ _ _ _.
         (* we know that psId is the biggest in G, so it cannot be smaller than o1 *)
         simpl in In1. subst psId. lia.
       - clear -SubM' SCMO. by  apply graph_insert_xo_eco.
@@ -2212,72 +2212,42 @@ Proof.
       - (* 5 *) by apply stack_empty_unmatched_push_insert_edge.
       - (* 6 *) by rewrite EqSo' EqCo' SCSO.
       - (* LIFO *)
-        rewrite /stack_LIFO.
-        (* TODO: remove some dups with treiber stack *)
-        (* the pair comes the from base stack, observation must be preserved *)
-        intros u1 o1 oV1 u2 o2 uV2 oV2. rewrite 2!elem_of_union 2!elem_of_singleton.
-        intros In1 In2 NEqu Eqo1 Equ2 Eqo2.
-        destruct In1 as [Eq1|In1]; [apply pair_inj in Eq1 as [-> ->]|];
-          (destruct In2 as [Eq2|In2]; [apply pair_inj in Eq2 as [-> ->]|]); [done|..].
-        + rewrite lookup_app_1_eq in Eqo1. inversion Eqo1. clear Eqo1. subst oV1.
-          destruct (NI _ _ In2). rewrite lookup_app_1_ne in Eqo2; [|done].
-          intros _ Lt'%(egcons_logview_closed _ EGCs _ _ Eqo2)%lookup_lt_is_Some _.
-          clear -Lt'; lia.
-        + (* TODO: use StackProps G' instead *)
-          rewrite lookup_app_1_ne in Equ2; [|done]. rewrite EqeVps in Equ2.
-          apply Some_inj in Equ2 as <-.
-          rewrite lookup_app_1_eq in Eqo2. apply Some_inj in Eqo2 as <-.
-          destruct (NI _ _ In1) as [_ ?]. rewrite lookup_app_1_ne in Eqo1; [|done].
-          simpl. intros Inu1. rewrite 2!elem_of_union elem_of_singleton.
-          intros InM InpsId.
-          assert (Leo1 := SCMO _ _ _ Eqo1 InpsId).
-          assert (NEqo1: psIde ≠ o1).
-          { clear -SCMA EqeVps Eqvv In1. intros <-.
-            specialize (SCMA _ _ In1) as [_ (_ & dV1 & v' & _ & EqdV1 & _ & Eqv' & _)].
-            rewrite EqeVps in EqdV1. apply Some_inj in EqdV1 as <-.
-            by rewrite Eqvv in Eqv'. }
-          destruct InM as [InM|[->|InM']]; [|done|]; last first.
-          { (* o1 eco psIde. But psIde eco o1, and psIde ≠ o1 ==> contradiction *)
-            assert (Leo1' := SCMO _ _ _ EqeVps InM').
-            clear -Leo1 Leo1' NEqo1. by apply NEqo1, (anti_symm Nat.le). }
-
-          rewrite -SCSO in In1.
-          destruct (StackProps_is_Some_so SP In1) as [[eu1 Eqeu1] [eo1 Eqeo1]].
-          have SR := In1. apply (stk_so_sim SP _ _ _ _ Eqeu1 Eqeo1) in SR.
-          inversion SR as [ub ob InSob|ux ox (InSox & IU & IO)];
-            clear SR; subst eu1 eo1.
-          { (* if (u1, o1) is a base stack pair, we piggyback on the base stack
-              LIFO *)
-            have InCob1 : (ub, ob) ∈ Gb'.(com).
-            { rewrite -(stk_cons_so_com _ SCb') Eqso. set_solver+InSob. }
-            have InCob2 : (psId, ppId) ∈ Gb'.(com).
-            { rewrite -(stk_cons_so_com _ SCb') Eqso. set_solver-. }
-            have NEqub : ub ≠ psId.
-            { clear -InSob FRSo. intros ->. by apply (FRSo _ InSob). }
-            destruct (StackProps_is_Some_l_1 SP Eqeo1) as [eVob EqeVob].
-            have EqeVob' :=
-              prefix_lookup _ _ _ _ EqeVob (graph_sqsubseteq_E _ _ SubGb).
-            apply (stk_cons_LIFO _ SCb' _ _ _ _ _ _ _ InCob1 InCob2 NEqub
-                    EqeVob' Eqps' Eqpp); simpl.
-            - apply (stk_base_stack_logview SP _ _ _ _ Eqeu1 EqTps _ _
-                      EqeVps Eqps Inu1).
-            - apply SubMb0. apply EL0 in InM as (eo & Eqeo & InMb0).
-              rewrite (prefix_lookup _ _ _ _ Eqeo LeT0) in Eqeo1.
-              clear -Eqeo1 InMb0. apply Some_inj in Eqeo1 as ->. done.
-            - apply (stk_base_stack_logview SP _ _ _ _ EqTps Eqeo1 _ _
-                        Eqo1 EqeVob InpsId). }
-          (* if (u1, o1) is an exchange pair, we know that o1 = S u1.
-            then, from psIde ≤ o1 and psIde ≠ o1 we know that psIde < o1,
-            thus psIde ≤ u1. But u1 eco psIde also gives us u1 ≤ psIde.
-            With u1 ≠ psIde ==> contradiction *)
-          assert (Eqo1' := stk_xchg_consec SP _ _ _ _ Eqeu1 Eqeo1 In1).
-          apply (SCMO _ _ _ EqeVps) in Inu1.
-          clear -Inu1 Eqo1' NEqu NEqo1 Leo1. lia.
-        + destruct (NI _ _ In1), (NI _ _ In2).
-          rewrite lookup_app_1_ne in Eqo1; [|done].
-          rewrite lookup_app_1_ne in Equ2; [|done].
-          rewrite lookup_app_1_ne in Eqo2; [|done].
-          revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply SCLIFO.
+        apply (stack_LIFO_insert_edge _ _ _ _ _ _ EqeVps Eqvv); [|done..].
+        intros u1 o1 oV1 In1 [Ltu1 Lto1] Eqo1 Inu1 InpsIde. destruct (NI _ _ In1).
+        rewrite 2!elem_of_union elem_of_singleton.
+        intros [InM|[->|InM']]; [|done|]; last first.
+        { (* o1 eco psIde. But psIde eco o1, and psIde ≠ o1 ==> contradiction *)
+          apply (SCMO _ _ _ EqeVps) in InM'. clear -Lto1 InM'. lia. }
+        rewrite -SCSO in In1.
+        destruct (StackProps_is_Some_so SP In1) as [[eu1 Eqeu1] [eo1 Eqeo1]].
+        have SR := In1. apply (stk_so_sim SP _ _ _ _ Eqeu1 Eqeo1) in SR.
+        inversion SR as [ub ob InSob|ux ox (InSox & IU & IO)];
+          clear SR; subst eu1 eo1.
+        { (* if (u1, o1) from the base stack, we piggyback on the base stack LIFO *)
+          have InCob1 : (ub, ob) ∈ Gb'.(com).
+          { rewrite -(stk_cons_so_com _ SCb') Eqso. set_solver+InSob. }
+          have InCob2 : (psId, ppId) ∈ Gb'.(com).
+          { rewrite -(stk_cons_so_com _ SCb') Eqso. set_solver-. }
+          have NEqub : ub ≠ psId.
+          { clear -InSob FRSo. intros ->. by apply (FRSo _ InSob). }
+          destruct (StackProps_is_Some_l_1 SP Eqeo1) as [eVob EqeVob].
+          have EqeVob' :=
+            prefix_lookup _ _ _ _ EqeVob (graph_sqsubseteq_E _ _ SubGb).
+          apply (stk_cons_LIFO _ SCb' _ _ _ _ _ _ _ InCob1 InCob2 NEqub
+                  EqeVob' Eqps' Eqpp); simpl.
+          - apply (stk_base_stack_logview SP _ _ _ _ Eqeu1 EqTps _ _
+                    EqeVps Eqps Inu1).
+          - apply SubMb0. apply EL0 in InM as (eo & Eqeo & InMb0).
+            rewrite (prefix_lookup _ _ _ _ Eqeo LeT0) in Eqeo1.
+            clear -Eqeo1 InMb0. apply Some_inj in Eqeo1 as ->. done.
+          - apply (stk_base_stack_logview SP _ _ _ _ EqTps Eqeo1 _ _
+                      Eqo1 EqeVob InpsIde). }
+        (* if (u1, o1) is an exchange pair, we know that o1 = S u1.
+          then, from psIde ≤ o1 and psIde ≠ o1 we know that psIde < o1,
+          thus psIde ≤ u1. But u1 eco psIde also gives us u1 ≤ psIde.
+          With u1 ≠ psIde ==> contradiction *)
+        assert (Eqo1' := stk_xchg_consec SP _ _ _ _ Eqeu1 Eqeo1 In1).
+        clear -Ltu1 Eqo1' Lto1. lia.
       - clear -SubM' SCMO. by apply graph_insert_xo_eco. }
 
     (* TODO: dup with push case also *)

theories/examples/stack/proof_treiber_graph.v

@@ -1850,8 +1850,8 @@ Proof.
     - (* LIFO *)
       apply (stack_LIFO_insert_edge _ _ _ _ _ _ Eqep Eqvp); [|done..].
       clear -SP2ORD2 SC2SO SC2MO Eqep EqTn NI.
-      intros u1 o1 In1 [Ltu1 Lto1]. rewrite 2!elem_of_union elem_of_singleton.
-      destruct (NI _ _ In1).
+      intros u1 o1 _ In1 [Ltu1 Lto1] _ _ _. destruct (NI _ _ In1).
+      rewrite 2!elem_of_union elem_of_singleton.
       intros [InM|[->|InM']]; [|done|].
       * (* psId is still in the stack, so it cannot get in between u1 and o1 *)
         rewrite -SC2SO in In1.

theories/examples/stack/spec_graph.v

@@ -589,7 +589,9 @@ Lemma stack_LIFO_insert_edge G e egV
   (Lt: bool_decide (e < length G.(Es))%nat) eV v :
   let G' := graph_insert_edge e egV G Lt in
   G.(Es) !! e = Some eV → eV.(ge_event) = Push v →
-  (∀ u1 o1, (u1, o1) ∈ G.(com) → (u1 < e < o1)%nat → o1 ∈ egV.(ge_lview) → False) →
+  (∀ u1 o1 oV1, (u1, o1) ∈ G.(com) → (u1 < e < o1)%nat →
+    G.(Es) !! o1 = Some oV1 →
+    u1 ∈ eV.(ge_lview) → e ∈ oV1.(ge_lview) → o1 ∈ egV.(ge_lview) → False) →
   eventgraph_consistent G → graph_xo_eco G.(Es) → stack_matches_value G →
   stack_LIFO G → stack_LIFO G'.
 Proof.
@@ -612,14 +614,13 @@ Proof.
     rewrite lookup_app_1_ne in Equ2; [|done].
     rewrite Eqe in Equ2. apply Some_inj in Equ2 as <-.
     intros Inu1 InM Ino1.
-    assert (Leu1 := MO _ _ _ Eqe Inu1).
-    assert (Leo1 := MO _ _ _ Eqo1 Ino1). clear Ino1.
+    assert (Leu1 := MO _ _ _ Eqe Inu1). assert (Leo1 := MO _ _ _ Eqo1 Ino1).
     assert (NEqo1: e ≠ o1).
     { clear -MA Eqe Eqv In1. intros <-.
       specialize (MA _ _ In1) as [_ (_ & dV1 & v' & _ & EqdV1 & _ & Eqv' & _)].
       rewrite Eqe in EqdV1. apply Some_inj in EqdV1 as <-.
       by rewrite Eqv in Eqv'. }
-    apply (LF' _ _ In1); [|done]. split; lia.
+    apply (LF' _ _ oV1 In1); [ |done..]. split; lia.
   - destruct (NI _ _ In1), (NI _ _ In2).
     rewrite lookup_app_1_ne in Eqo1; [|done].
     rewrite lookup_app_1_ne in Equ2; [|done].