Unfinished WIP

theories/algebra/auth.v

@@ -244,6 +244,48 @@ Proof.
   split_and!; [by apply cmra_included_includedN|by apply cmra_valid_validN|done].
 Qed.
 
+    (* Print cmra_extend_included.
+
+     : ∀ M : cmraT, CmraSwappable M
+                    → ∀ (n : nat) (mx : option M) (z : M), 
+                    ✓{S n} mx
+                    → ✓{n} (z ⋅? mx)
+                      → {z' : M | ✓{S n} (z' ⋅? mx) ∧ z ≡{n}≡ z'} *)
+(* cmra_extend :
+∀ (A : cmraT) (n : nat) (x y1 y2 : A), ✓{n} x
+                                       → x ≡{n}≡ y1 ⋅ y2
+                                         → {z1 : A &
+                                           {z2 : A |
+                                           x ≡ z1 ⋅ z2
+                                           ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2}} *)
+
+Instance Swappable_authR `{CmraSwappable A}: CmraSwappable authR.
+Proof.
+  (* split; intros. *)
+  split => n [x|] [mza zao]; rewrite !auth_validN_eq /= ; first last.
+  - move: mza => [[za _ [Hle Hv] | // ] | _ Hv] /=.
+    + case: (cmra_extend_included n None za) => //= za' [Hza' Heq].
+      hnf in Hle.
+      (* Let's pretend the existential in Hle were a sigma. *)
+      have [zaf Hle']: { z | za ≡{n}≡ zao ⋅ z }. admit.
+      (* Fails: *)
+      (* case: (cmra_extend_included n None zao) => //= [| zao' [Hzao' Heqo]].
+      eauto using cmra_validN_includedN.
+      eexists (Auth (Excl' za') zao'); repeat split => //=; last by repeat f_equiv.
+      hnf in Hle |- *. *)
+      case: (cmra_extend n za' zao zaf); rewrite -?Heq // => zao' [zaf' [Heqo [??]]].
+      (* case: (cmra_extend_included n (Some zaf') zao') => /= [||za'' [??]]; rewrite /= ?Some_validN; try by setoid_subst; eauto using Some_validN, cmra_validN_S, cmra_validN_op_r.
+      eexists (Auth (Excl' za'') zao'); repeat split => //=; eauto using Some_validN, cmra_validN_S, cmra_validN_op_l, cmra_validN_op_r; last repeat f_equiv.
+      hnf; eauto.
+      exists ε. *)
+      case: (cmra_extend_included (S n) None za') => //= [za'' [Heq1 Heq2]].
+      (* rewrite /= ?Some_validN; try by setoid_subst; eauto using Some_validN, cmra_validN_S, cmra_validN_op_r. *)
+      eexists (Auth (Excl' za'') zao'); repeat split => //=; eauto using Some_validN, cmra_validN_S, cmra_validN_op_l, cmra_validN_op_r; last repeat f_equiv.
+      2: by rewrite Heq; apply dist_S.
+      hnf. exists zaf'. by setoid_subst.
+Abort.
+
+
 (* Not sure yet if this should hold. *)
 Instance Swappable_authR `{CmraSwappable A}: CmraSwappable authR.
 Proof.
@@ -256,6 +298,37 @@ Proof.
     + case: mx Hx {Hle Heqo} => [x|]; rewrite //= !Some_validN. apply authoritative_validN.
     + by case: mx Hx Heqo Hle => [x|] //=; rewrite ?Some_validN => ? <-.
     + exists (Auth z' (auth_own z)) => //=.
+      (* destruct mx; cbn in *; rewrite /= ?Some_validN. *)
+      repeat case_match; subst; split; destruct mx as [[[ca|] cao]|]; destruct z as [[a|] b]; destruct z'; cbn in *;
+      try cbv in Heqo; try cbv in Heqo0;
+      simplify_eq; try by [|inversion Heq].
+      *
+        cbv in Hz', Heq.
+        clear Heq Hz'.
+        all: split. all: try apply Hx.
+        destruct Hx as [Hx1 Hx2].
+        rewrite /auth_op /cmra_op /= in Hle Hx1 *.
+        all: rewrite /auth_op /cmra_op /= in Hle *.
+        admit.
+      *
+        apply (inj _) in Heq. inversion_clear Heq; setoid_subst.
+        cbv in Hz'. clear Hz'.
+        rewrite Some_validN /auth_op /cmra_op /= in Hx *.
+        move => /auth_own_validN /= Hx.
+        admit. (* This seems false. *)
+      * hnf in *.
+
+      (* destruct Hx. cbv in Hle, Hx.
+
+      cbv in Hx, Hz'.
+      cbn.
+      cbv.
+      1-3: admit.
+      cbv in Heqo0, Heqo; simplify_eq.
+      cbv in Heqo0, Heqo; simplify_eq. by inversion Heq.
+      by inversion Heq.
+      by inversion Heq.
+      inversion Heqo0; inversion Heqo. cbv in *. *)
     admit.
       (* repeat case_match; subst; split; destruct mx as [[[ca|] cao]|]; destruct z as [[a|] b]; cbn in *; setoid_subst => //.
   (* - case: (cmra_extend_included n (auth_own <$> mx) zamx) => /= [||z' [Hz' Heq]].