(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-ssr-search-moved" "-w" "+deprecated-instance-without-locality" "-w" "+ambiguous-paths" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-deprecated-field-instance-without-locality" "-w" "+deprecated-tactic-notation" "-w" "-deprecated-since-8.19" "-w" "-deprecated-since-8.20" "-w" "-deprecated-from-Coq" "-w" "-deprecated-dirpath-Coq" "-w" "-notation-incompatible-prefix" "-w" "-deprecated-typeclasses-transparency-without-locality" "-w" "-notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/src" "Perennial" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp" "stdpp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_unstable" "stdpp.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_bitvector" "stdpp.bitvector" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/Goose" "Goose" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/record-update/src" "RecordUpdate" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coq-tactical/src" "Tactical" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris-named-props/src" "iris_named_props" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_trusted_code" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_code_axioms" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_partial_axioms" "New.code_axioms" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new" "New" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1066 lines to 167 lines, then from 180 lines to 368 lines, then from 373 lines to 168 lines, then from 181 lines to 855 lines, then from 857 lines to 177 lines, then from 190 lines to 549 lines, then from 554 lines to 194 lines, then from 207 lines to 743 lines, then from 748 lines to 248 lines, then from 261 lines to 446 lines, then from 451 lines to 249 lines, then from 262 lines to 842 lines, then from 847 lines to 260 lines, then from 273 lines to 624 lines, then from 624 lines to 278 lines, then from 291 lines to 478 lines, then from 483 lines to 279 lines, then from 292 lines to 558 lines, then from 563 lines to 279 lines, then from 292 lines to 689 lines, then from 694 lines to 309 lines, then from 322 lines to 1312 lines, then from 1316 lines to 426 lines, then from 439 lines to 919 lines, then from 924 lines to 474 lines, then from 487 lines to 1254 lines, then from 1259 lines to 659 lines, then from 660 lines to 533 lines, then from 546 lines to 841 lines, then from 846 lines to 542 lines, then from 555 lines to 674 lines, then from 679 lines to 553 lines, then from 566 lines to 969 lines, then from 974 lines to 588 lines, then from 601 lines to 766 lines, then from 771 lines to 587 lines, then from 600 lines to 772 lines, then from 777 lines to 589 lines, then from 602 lines to 962 lines, then from 967 lines to 603 lines, then from 616 lines to 1930 lines, then from 1935 lines to 642 lines, then from 655 lines to 2993 lines, then from 2998 lines to 1687 lines, then from 1700 lines to 3137 lines, then from 3142 lines to 2116 lines, then from 2113 lines to 2095 lines, then from 2108 lines to 2312 lines, then from 2317 lines to 2128 lines, then from 2141 lines to 3107 lines, then from 3112 lines to 2290 lines, then from 2303 lines to 2595 lines, then from 2600 lines to 2456 lines, then from 2469 lines to 2615 lines, then from 2620 lines to 2482 lines, then from 2495 lines to 2697 lines, then from 2702 lines to 2566 lines, then from 2579 lines to 2772 lines, then from 2777 lines to 2812 lines, then from 2813 lines to 2659 lines, then from 2672 lines to 2841 lines, then from 2846 lines to 2719 lines, then from 2732 lines to 2821 lines, then from 2826 lines to 2723 lines, then from 2736 lines to 3351 lines, then from 3356 lines to 3168 lines, then from 3151 lines to 2792 lines, then from 2805 lines to 3604 lines, then from 3608 lines to 3348 lines, then from 3321 lines to 2867 lines, then from 2880 lines to 3175 lines, then from 3180 lines to 2909 lines, then from 2922 lines to 3120 lines, then from 3125 lines to 2914 lines, then from 2927 lines to 3193 lines, then from 3198 lines to 2974 lines, then from 2987 lines to 3042 lines, then from 3047 lines to 3001 lines, then from 3011 lines to 2993 lines, then from 3006 lines to 3655 lines, then from 3660 lines to 2996 lines, then from 3009 lines to 3093 lines, then from 3099 lines to 3005 lines, then from 3019 lines to 3684 lines, then from 3690 lines to 3015 lines, then from 3029 lines to 3058 lines, then from 3064 lines to 3021 lines, then from 3035 lines to 3069 lines, then from 3075 lines to 3028 lines, then from 3042 lines to 3070 lines, then from 3076 lines to 3073 lines, then from 3075 lines to 3036 lines, then from 3049 lines to 3118 lines, then from 3124 lines to 3057 lines, then from 3071 lines to 3261 lines, then from 3267 lines to 3065 lines, then from 3079 lines to 3341 lines, then from 3347 lines to 3122 lines, then from 3136 lines to 3421 lines, then from 3427 lines to 3131 lines, then from 3145 lines to 3388 lines, then from 3394 lines to 3312 lines, then from 3313 lines to 3135 lines, then from 3148 lines to 3251 lines, then from 3257 lines to 3136 lines, then from 3150 lines to 3895 lines, then from 3901 lines to 3154 lines, then from 3168 lines to 6507 lines, then from 6513 lines to 3196 lines, then from 3211 lines to 3158 lines, then from 3171 lines to 4044 lines, then from 4050 lines to 3196 lines, then from 3210 lines to 3543 lines, then from 3549 lines to 3216 lines, then from 3230 lines to 3505 lines, then from 3511 lines to 3468 lines, then from 3467 lines to 3228 lines, then from 3241 lines to 4292 lines, then from 4297 lines to 3239 lines, then from 3253 lines to 3809 lines, then from 3815 lines to 3240 lines, then from 3254 lines to 5079 lines, then from 5085 lines to 4133 lines, then from 4119 lines to 3252 lines, then from 3265 lines to 3373 lines, then from 3379 lines to 3255 lines, then from 3269 lines to 3465 lines, then from 3471 lines to 3293 lines, then from 3307 lines to 3880 lines, then from 3886 lines to 3482 lines, then from 3496 lines to 3703 lines, then from 3708 lines to 3526 lines, then from 3541 lines to 3522 lines, then from 3535 lines to 3730 lines, then from 3736 lines to 3550 lines, then from 3564 lines to 4093 lines, then from 4099 lines to 3561 lines, then from 3575 lines to 4478 lines, then from 4484 lines to 4162 lines, then from 4158 lines to 3594 lines, then from 3607 lines to 3799 lines, then from 3805 lines to 3614 lines, then from 3628 lines to 4139 lines, then from 4145 lines to 3615 lines, then from 3634 lines to 3613 lines, then from 3626 lines to 8522 lines, then from 8527 lines to 3653 lines, then from 3667 lines to 3914 lines, then from 3920 lines to 3871 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.14.1
   coqtop version runner-t7b1znuaq-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfbe3) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
   Modules that could not be inlined: Ltac2.Array, Ltac2.Pattern, Ltac2.Ltac1
   Expected coqc runtime on this file: 2.530 sec *)








Require Stdlib.Init.Ltac.
Require Stdlib.QArith.QArith_base.
Require Stdlib.QArith.Qcanon.
Require Stdlib.Sorting.Permutation.
Require Stdlib.Logic.EqdepFacts.
Require Stdlib.PArith.PArith.
Require Stdlib.NArith.NArith.
Require Stdlib.ZArith.ZArith.
Require Stdlib.QArith.QArith.
Require Stdlib.Classes.Morphisms.
Require Stdlib.Classes.RelationClasses.
Require Stdlib.Lists.List.
Require Stdlib.Bool.Bool.
Require Stdlib.Setoids.Setoid.
Require Stdlib.Init.Peano.
Require Stdlib.Unicode.Utf8.
Require Stdlib.Program.Basics.
Require Stdlib.Program.Syntax.
Require Stdlib.ssr.ssrfun.
Require stdpp.options.
Require stdpp.base.
Require stdpp.proof_irrel.
Require stdpp.decidable.
Require Stdlib.micromega.Lia.
Require stdpp.tactics.
Require stdpp.option.
Require stdpp.well_founded.
Require stdpp.numbers.
Require stdpp.list.
Require stdpp.list_numbers.
Require stdpp.fin.
Require stdpp.countable.
Require Stdlib.Vectors.Vector.
Require stdpp.vector.
Require stdpp.finite.
Require Stdlib.ssr.ssreflect.
Require stdpp.orders.
Require stdpp.sets.
Require stdpp.relations.
Require stdpp.fin_sets.
Require stdpp.listset.
Require stdpp.lexico.
Require stdpp.prelude.
Require stdpp.ssreflect.
Require iris.prelude.options.
Require iris.prelude.prelude.
Require iris.algebra.ofe.
Require iris.algebra.monoid.
Require iris.algebra.cmra.
Require Stdlib.Strings.Ascii.
Require Stdlib.Strings.String.
Require Ltac2.Init.
Require Ltac2.Std.
Require Ltac2.Message.
Require Ltac2.Control.
Require Ltac2.Ltac1.
Require Ltac2.Pattern.
Require Ltac2.Int.
Require Ltac2.Bool.
Require Ltac2.Array.

Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.

Module Export stdpp_DOT_strings_WRAPPED.
Module Export strings.
Import Stdlib.Strings.Ascii.
Export stdpp.list.
Import stdpp.countable.
Import stdpp.options.




Export Stdlib.Strings.String (string(..)).
Export (notations) Stdlib.Strings.String.


String Notation string
  String.string_of_list_byte String.list_byte_of_string : stdpp_scope.

Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.



Local Definition bool_cons_pos (b : bool) (p : positive) : positive :=
  if b then p~1 else p~0.
Local Definition ascii_cons_pos (c : ascii) (p : positive) : positive :=
  match c with
  | Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
     bool_cons_pos b0 $ bool_cons_pos b1 $ bool_cons_pos b2 $
       bool_cons_pos b3 $ bool_cons_pos b4 $ bool_cons_pos b5 $
       bool_cons_pos b6 $ bool_cons_pos b7 p
  end.
Local Fixpoint string_to_pos (s : string) : positive :=
  match s with
  | EmptyString => 1
  | String c s => ascii_cons_pos c (string_to_pos s)
  end.


Local Fixpoint pos_to_string (p : positive) : string.
Admitted.

Local Lemma pos_to_string_string_to_pos s : pos_to_string (string_to_pos s) = s.
Admitted.

Module Export Ascii.
  Global Instance eq_dec : EqDecision ascii := ascii_dec.

  Global Program Instance countable : Countable ascii := {|
    encode a := string_to_pos (String a EmptyString);
    decode p := match pos_to_string p return _ with String a _ => Some a | _ => None end
  |}.
Admit Obligations.

  Definition is_nat (x : ascii) : option nat :=
    match x with
    | "0" => Some 0
    | "1" => Some 1
    | "2" => Some 2
    | "3" => Some 3
    | "4" => Some 4
    | "5" => Some 5
    | "6" => Some 6
    | "7" => Some 7
    | "8" => Some 8
    | "9" => Some 9
    | _ => None
    end%char.

  Definition is_space (x : ascii) : bool :=
    match x with
    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
    end%char.
End Ascii.

Module Export String.
  
  Notation app := String.append.

  
  Global Arguments app : simpl never.

  Global Instance eq_dec : EqDecision string.
Admitted.

  Global Instance inhabited : Inhabited string := populate "".

  Global Program Instance countable : Countable string := {|
    encode := string_to_pos;
    decode p := Some (pos_to_string p)
  |}.
  Solve Obligations with
    naive_solver eauto using pos_to_string_string_to_pos with f_equal.

  Definition le (s1 s2 : string) : Prop := String.leb s1 s2.

  Global Instance le_dec : RelDecision le.
Admitted.
  Global Instance le_pi s1 s2 : ProofIrrel (le s1 s2).
Admitted.

  Global Instance le_po : PartialOrder le.
Admitted.
  Global Instance le_total : Total le.
Admitted.

  Global Instance app_inj s1 : Inj (=) (=) (app s1).
Admitted.

  Fixpoint rev_app (s1 s2 : string) : string :=
    match s1 with
    | "" => s2
    | String a s1 => rev_app s1 (String a s2)
    end.
  Definition rev (s : string) : string := rev_app s "".

  
  Fixpoint words_go (cur : option string) (s : string) : list string :=
    match s with
    | "" => option_list (rev <$> cur)
    | String a s =>
       if Ascii.is_space a
       then option_list (rev <$> cur) ++ words_go None s
       else words_go (Some (from_option (String a) (String a "") cur)) s
    end.
  Definition words : string → list string := words_go None.
End String.

Infix "≤" := String.le : string_scope.
Notation "(≤)" := String.le (only parsing) : string_scope.
Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%string : string_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%string : string_scope.

Global Hint Extern 0 (_ ≤ _)%string => reflexivity : core.

End strings.

End stdpp_DOT_strings_WRAPPED.
Module Export stdpp_DOT_strings.
Module Export stdpp.
Module Export strings.
Include stdpp_DOT_strings_WRAPPED.strings.
End strings.

End stdpp.

End stdpp_DOT_strings.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Export stdpp.relations.

Class MapFold K A M := map_fold B : (K → A → B → B) → B → M → B.
Global Arguments map_fold {_ _ _ _ _} _ _ _.
Definition diag_None {A B C} (f : option A → option B → option C)
    (mx : option A) (my : option B) : option C.
Admitted.
Global Instance map_insert `{PartialAlter K A M} : Insert K A M.
Admitted.

Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
    PartialAlter K A (M A), OMap M, Merge M, ∀ A, MapFold K A (M A),
    EqDecision K} := {
  map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
  lookup_empty {A} i : (∅ : M A) !! i = None;
  lookup_partial_alter {A} f (m : M A) i :
    partial_alter f i m !! i = f (m !! i);
  lookup_partial_alter_ne {A} f (m : M A) i j :
    i ≠ j → partial_alter f i m !! j = m !! j;
  lookup_fmap {A B} (f : A → B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
  lookup_omap {A B} (f : A → option B) (m : M A) i :
    omap f m !! i = m !! i ≫= f;
  lookup_merge {A B C} (f : option A → option B → option C) (m1 : M A) (m2 : M B) i :
    merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i);
  map_fold_empty {A B} (f : K → A → B → B) (b : B) :
    map_fold f b ∅ = b;

  map_fold_fmap_ind {A} (P : M A → Prop) :
    P ∅ →
    (∀ i x m,
      m !! i = None →
      (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
        map_fold f b (<[i:=x']> (g <$> m)) = f i x' (map_fold f b (g <$> m))) →
      P m →
      P (<[i:=x]> m)) →
    ∀ m, P m;
}.
Global Instance map_singleton `{PartialAlter K A M, Empty M} :
  SingletonM K A M.
Admitted.
Global Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20.
Admitted.

Export stdpp.countable.

Record mapset' (Munit : Type) : Type :=
  Mapset { mapset_car: Munit }.
Notation mapset M := (mapset' (M unit)).

Section mapset.
Context `{FinMap K M}.
Global Instance mapset_elem_of: ElemOf K (mapset M).
admit.
Defined.
Global Instance mapset_singleton: Singleton K (mapset M).
admit.
Defined.

End mapset.

Local Open Scope positive_scope.

Local Notation "P ~ 0" := (λ p, P p~0) : function_scope.
Local Notation "P ~ 1" := (λ p, P p~1) : function_scope.

Inductive gmap_dep_ne (A : Type) (P : positive → Prop) :=
  | GNode001 : gmap_dep_ne A P~1  → gmap_dep_ne A P
  | GNode010 : P 1 → A → gmap_dep_ne A P
  | GNode011 : P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode100 : gmap_dep_ne A P~0 → gmap_dep_ne A P
  | GNode101 : gmap_dep_ne A P~0 → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode110 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P
  | GNode111 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P.

Variant gmap_dep (A : Type) (P : positive → Prop) :=
  | GEmpty : gmap_dep A P
  | GNodes : gmap_dep_ne A P → gmap_dep A P.

Record gmap_key K `{Countable K} (q : positive) :=
  GMapKey { _ : encode (A:=K) <$> decode q = Some q }.

Record gmap K `{Countable K} A := GMap { gmap_car : gmap_dep A (gmap_key K) }.
Global Instance gmap_lookup `{Countable K} {A} :
    Lookup K A (gmap K A).
Admitted.
Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A).
Admitted.
Global Instance gmap_partial_alter `{Countable K} {A} :
    PartialAlter K A (gmap K A).
Admitted.
Global Instance gmap_fmap `{Countable K} : FMap (gmap K).
Admitted.

Definition gset K `{Countable K} := mapset (gmap K).

Inductive coPset_raw :=
  | coPLeaf : bool → coPset_raw
  | coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
Fixpoint coPset_wf (t : coPset_raw) : bool.
Admitted.

Definition coPset := { t | coPset_wf t }.
Global Instance coPset_singleton : Singleton positive coPset.
Admitted.

Module Export iris_DOT_algebra_DOT_coPset_WRAPPED.
Module Export coPset.
Export iris.algebra.cmra.

Inductive coPset_disj :=
  | CoPset : coPset → coPset_disj
  | CoPsetBot : coPset_disj.

Section coPset_disj.
  Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid_instance : Valid coPset_disj.
Admitted.
Local Instance coPset_disj_op_instance : Op coPset_disj.
Admitted.
Local Instance coPset_disj_pcore_instance : PCore coPset_disj.
Admitted.

  Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
Admitted.
  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
End coPset_disj.

End coPset.
Module Export iris.
Module Export algebra.
Module Export coPset.
Include iris_DOT_algebra_DOT_coPset_WRAPPED.coPset.
End coPset.

Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).

Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).

Reserved Notation "⊢ Q" (at level 20, Q at level 200).
Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
Reserved Notation "P -∗ Q"
  (at level 99, Q at level 200, right associativity,
   format "'[' P  -∗  '/' '[' Q ']' ']'").

Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<pers>?' p  P").

Reserved Notation "▷ P" (at level 20, right associativity).
Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
   format "▷^ n  P").

Reserved Notation "'<affine>' P" (at level 20, right associativity).
Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<affine>?' p  P").

Reserved Notation "'<absorb>' P" (at level 20, right associativity).

Reserved Notation "□ P" (at level 20, right associativity).
Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'□?' p  P").

Reserved Notation "|==> Q" (at level 99, Q at level 200, format "'[  ' |==>  '/' Q ']'").
Reserved Notation "P ==∗ Q"
  (at level 99, Q at level 200, format "'[' P  ==∗  '/' Q ']'").

Reserved Notation "'[∗]' Ps" (at level 20).
Reserved Notation "'[∧' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x binder, right associativity,
   format "[∧  list]  x  ∈  l ,  P").

Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
  (at level 200, m at level 10, k binder, x binder, right associativity,
   format "[∗  map]  k ↦ x  ∈  m ,  P").
Delimit Scope bi_scope with I.

Section bi_mixin.
  Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
  Context (bi_entails : PROP → PROP → Prop).
  Context (bi_emp : PROP).
  Context (bi_pure : Prop → PROP).
  Context (bi_and : PROP → PROP → PROP).
  Context (bi_or : PROP → PROP → PROP).
  Context (bi_impl : PROP → PROP → PROP).
  Context (bi_forall : ∀ A, (A → PROP) → PROP).
  Context (bi_exist : ∀ A, (A → PROP) → PROP).
  Context (bi_sep : PROP → PROP → PROP).
  Context (bi_wand : PROP → PROP → PROP).

  Bind Scope bi_scope with PROP.
  Local Infix "⊢" := bi_entails.
  Local Notation "'emp'" := bi_emp : bi_scope.
  Local Notation "'True'" := (bi_pure True) : bi_scope.
  Local Notation "'False'" := (bi_pure False) : bi_scope.
  Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
  Local Infix "∧" := bi_and : bi_scope.
  Local Infix "∨" := bi_or : bi_scope.
  Local Infix "→" := bi_impl : bi_scope.
  Local Notation "∀ x .. y , P" :=
    (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.
  Local Notation "∃ x .. y , P" :=
    (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
  Local Infix "∗" := bi_sep : bi_scope.
  Local Infix "-∗" := bi_wand : bi_scope.

  Record BiMixin := {
    bi_mixin_entails_po : PreOrder bi_entails;
    bi_mixin_equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);

    bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
    bi_mixin_and_ne : NonExpansive2 bi_and;
    bi_mixin_or_ne : NonExpansive2 bi_or;
    bi_mixin_impl_ne : NonExpansive2 bi_impl;
    bi_mixin_forall_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A);
    bi_mixin_exist_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
    bi_mixin_sep_ne : NonExpansive2 bi_sep;
    bi_mixin_wand_ne : NonExpansive2 bi_wand;

    bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
    bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;

    bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P;
    bi_mixin_and_elim_r P Q : P ∧ Q ⊢ Q;
    bi_mixin_and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R;

    bi_mixin_or_intro_l P Q : P ⊢ P ∨ Q;
    bi_mixin_or_intro_r P Q : Q ⊢ P ∨ Q;
    bi_mixin_or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R;

    bi_mixin_impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R;
    bi_mixin_impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R;

    bi_mixin_forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a;
    bi_mixin_forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a;

    bi_mixin_exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a;
    bi_mixin_exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q;

    bi_mixin_sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q';
    bi_mixin_emp_sep_1 P : P ⊢ emp ∗ P;
    bi_mixin_emp_sep_2 P : emp ∗ P ⊢ P;
    bi_mixin_sep_comm' P Q : P ∗ Q ⊢ Q ∗ P;
    bi_mixin_sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R);
    bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
    bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
  }.

  Context (bi_persistently : PROP → PROP).
  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.

  Record BiPersistentlyMixin := {
    bi_mixin_persistently_ne : NonExpansive bi_persistently;

    bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;

    bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;

    bi_mixin_persistently_emp_2 : emp ⊢ <pers> emp;

    bi_mixin_persistently_and_2 (P Q : PROP) :
      (<pers> P) ∧ (<pers> Q) ⊢ <pers> (P ∧ Q);
    bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
      <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);

    bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;

    bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
  }.

  Context (bi_later : PROP → PROP).
  Local Notation "▷ P" := (bi_later P) : bi_scope.

  Record BiLaterMixin := {
    bi_mixin_later_ne : NonExpansive bi_later;

    bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
    bi_mixin_later_intro P : P ⊢ ▷ P;

    bi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
    bi_mixin_later_exist_false {A} (Φ : A → PROP) :
      (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
    bi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
    bi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
    bi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
    bi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;

    bi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
  }.
End bi_mixin.

  Universe Logic.

  Universe Quant.

Structure bi := Bi {
  bi_car :> Type@{Logic};
  bi_dist : Dist bi_car;
  bi_equiv : Equiv bi_car;
  bi_entails : bi_car → bi_car → Prop;
  bi_emp : bi_car;
  bi_pure : Prop → bi_car;
  bi_and : bi_car → bi_car → bi_car;
  bi_or : bi_car → bi_car → bi_car;
  bi_impl : bi_car → bi_car → bi_car;
  bi_forall : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
  bi_exist : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
  bi_sep : bi_car → bi_car → bi_car;
  bi_wand : bi_car → bi_car → bi_car;
  bi_persistently : bi_car → bi_car;
  bi_later : bi_car → bi_car;
  bi_ofe_mixin : OfeMixin bi_car;
  bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
  bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
                        bi_exist bi_sep bi_wand;
  bi_bi_persistently_mixin :
    BiPersistentlyMixin bi_entails bi_emp bi_and bi_exist bi_sep bi_persistently;
  bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                   bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
Bind Scope bi_scope with bi_car.
Coercion bi_ofeO (PROP : bi) : ofe.
exact (Ofe PROP (bi_ofe_mixin PROP)).
Defined.
Canonical Structure bi_ofeO.
Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
Global Arguments bi_emp {PROP} : simpl never, rename.
Global Arguments bi_pure {PROP} _%_stdpp : simpl never, rename.
Global Arguments bi_and {PROP} _ _ : simpl never, rename.
Global Arguments bi_or {PROP} _ _ : simpl never, rename.
Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
Global Arguments bi_forall {PROP _} _%_I : simpl never, rename.
Global Arguments bi_exist {PROP _} _%_I : simpl never, rename.
Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
Global Arguments bi_persistently {PROP} _ : simpl never, rename.
Global Arguments bi_later {PROP} _ : simpl never, rename.

Notation "'emp'" := (bi_emp) : bi_scope.
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
Notation "'True'" := (bi_pure True) : bi_scope.
Notation "'False'" := (bi_pure False) : bi_scope.
Infix "∧" := bi_and : bi_scope.
Infix "∨" := bi_or : bi_scope.
Infix "→" := bi_impl : bi_scope.
Infix "∗" := bi_sep : bi_scope.
Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
Notation "∀ x .. y , P" :=
  (bi_forall (λ x, .. (bi_forall (λ y, P%I)) ..)) : bi_scope.
Notation "∃ x .. y , P" :=
  (bi_exist (λ x, .. (bi_exist (λ y, P%I)) ..)) : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.

Notation "▷ P" := (bi_later P) : bi_scope.

Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.

Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop.
Admitted.

Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.

Notation "P -∗ Q" := (⊢ P -∗ Q) : stdpp_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.

Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
Notation "'<affine>' P" := (bi_affinely P) : bi_scope.

Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.

Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.

Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP.
Admitted.
Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP.
Admitted.
Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP.
Admitted.
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP.
Admitted.
Notation "□ P" := (bi_intuitionistically P) : bi_scope.
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP.
Admitted.
Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope.

Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
  match n with
  | O => P
  | S n' => ▷ ▷^n' P
  end
where "▷^ n P" := (bi_laterN n P) : bi_scope.

Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
  match mP with
  | None => Q
  | Some P => P -∗ Q
  end.

Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Section derived.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

Global Instance intuitionistically_affine P : Affine (□ P).
Admitted.

Global Instance bi_and_monoid : Monoid (@bi_and PROP).
Admitted.
Global Instance bi_sep_monoid : Monoid (@bi_sep PROP).
Admitted.
End derived.

Fixpoint big_opL {M : ofe} {o : M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
  match xs with
  | [] => monoid_unit
  | x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
  end.
Global Arguments big_opL {M} o {_ A} _ !_ /.
Local Definition big_opM_def {M : ofe} {o : M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
  (m : gmap K A) : M.
Admitted.
Local Definition big_opM_aux : seal (@big_opM_def).
Admitted.
Definition big_opM := big_opM_aux.(unseal).
Global Arguments big_opM {M} o {_ K _ _ A} _ _.

Section ofe.
Context {A : ofe}.
Local Instance list_dist : Dist (list A).
Admitted.

Definition list_ofe_mixin : OfeMixin (list A).
Admitted.
Canonical Structure listO := Ofe (list A) list_ofe_mixin.
End ofe.

Global Arguments listO : clear implicits.

Inductive gset_disj K `{Countable K} :=
  | GSet : gset K → gset_disj K
  | GSetBot : gset_disj K.

Section gset_disj.
  Context `{Countable K}.

  Canonical Structure gset_disjO := leibnizO (gset_disj K).
Local Instance gset_disj_valid_instance : Valid (gset_disj K).
Admitted.
Local Instance gset_disj_op_instance : Op (gset_disj K).
Admitted.
Local Instance gset_disj_pcore_instance : PCore (gset_disj K).
Admitted.

  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
Admitted.
  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.

  End gset_disj.
Global Arguments gset_disjR _ {_ _}.

Section ofe.
Context `{Countable K} {A : ofe}.
Local Instance gmap_dist : Dist (gmap K A).
Admitted.
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Admitted.
Canonical Structure gmapO : ofe.
exact (Ofe (gmap K A) gmap_ofe_mixin).
Defined.
End ofe.

Section cmra.
Context `{Countable K} {A : cmra}.
Local Instance gmap_unit_instance : Unit (gmap K A).
Admitted.
Local Instance gmap_op_instance : Op (gmap K A).
Admitted.
Local Instance gmap_pcore_instance : PCore (gmap K A).
Admitted.
Local Instance gmap_valid_instance : Valid (gmap K A).
Admitted.
Local Instance gmap_validN_instance : ValidN (gmap K A).
Admitted.

Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
Admitted.
Canonical Structure gmapR := Cmra (gmap K A) gmap_cmra_mixin.

Lemma gmap_ucmra_mixin : UcmraMixin (gmap K A).
Admitted.
Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.

End cmra.
Global Arguments gmapUR _ {_ _} _.
Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps%I) : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" :=
  (big_opL bi_and (λ _ x, P%I) l) : bi_scope.

Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P%I) m) : bi_scope.

Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.

Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q) : stdpp_scope.

Record BiBUpdMixin (PROP : bi) 

[...]

 xs pat as p
    | _ => fail "iSpecialize:" t "should be a proof mode term"
    end
  end.

Tactic Notation "iPoseProofCore" open_constr(lem)
    "as" constr(p) tactic3(tac) :=
  iStartProof;
  let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
  let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
  let spec_tac Htmp :=
    lazymatch lem with
    | ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
    | _ => idtac
    end in
  lazymatch type of t with
  | ident =>
     let Htmp := iFresh in
     iPoseProofCoreHyp t as Htmp; spec_tac Htmp; [..|tac Htmp]
  | _ => iPoseProofCoreLem t as (fun Htmp => spec_tac Htmp; [..|tac Htmp])
  end.

Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
  eapply tac_or_destruct with H _ H1 H2 _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iOrDestruct:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoOr ?P _ _ => P end in
     fail "iOrDestruct: cannot destruct" P
    | pm_reduce;
      lazymatch goal with
      | |- False =>
        let H1 := pretty_ident H1 in
        let H2 := pretty_ident H2 in
        fail "iOrDestruct:" H1 "or" H2 "not fresh"
      |  _ => split
      end].

Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
  eapply tac_and_destruct with H _ H1 H2 _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iAndDestruct:" H "not found"
    |pm_reduce; tc_solve ||
     let P :=
       lazymatch goal with
       | |- IntoSep ?P _ _ => P
       | |- IntoAnd _ ?P _ _ => P
       end in
     fail "iAndDestruct: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
       | |- False =>
         let H1 := pretty_ident H1 in
         let H2 := pretty_ident H2 in
         fail "iAndDestruct:" H1 "or" H2 "not fresh"
       | _ => idtac
     end].

Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
  eapply tac_and_destruct_choice with H _ d H' _ _ _;
    [pm_reflexivity || fail "iAndDestructChoice:" H "not found"
    |pm_reduce; tc_solve ||
     let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
     fail "iAndDestructChoice: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iAndDestructChoice:" H' "not fresh"
     | _ => idtac
     end].

Ltac _iExists x :=
  iStartProof;
  eapply tac_exist;
    [tc_solve ||
     let P := match goal with |- FromExist ?P _ => P end in
     fail "iExists:" P "not an existential"
    |pm_prettify; eexists x
      ].

Tactic Notation "iExists" ne_uconstr_list_sep(xs,",") :=
  ltac1_list_iter _iExists xs.

Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
  eapply tac_exist_destruct with H _ Hx _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iExistDestruct:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoExist ?P _ _ => P end in
     fail "iExistDestruct: cannot destruct" P|];
    let name := lazymatch goal with
                | |- let _ := (λ name, _) in _ => name
                end in
    intros _;
    let y := fresh name in
    intros y; pm_reduce;
    lazymatch goal with
    | |- False =>
      let Hx := pretty_ident Hx in
      fail "iExistDestruct:" Hx "not fresh"
    | _ => revert y; intros x
    end.

Tactic Notation "iModIntro" uconstr(sel) :=
  iStartProof;
  notypeclasses refine (tac_modal_intro _ _ sel _ _ _ _ _ _ _ _ _ _ _ _ _ _);
    [tc_solve ||
     fail "iModIntro: the goal is not a modality"
    |tc_solve ||
     let s := lazymatch goal with |- IntoModalIntuitionisticEnv _ _ _ ?s => s end in
     lazymatch eval hnf in s with
     | MIEnvForall ?C => fail "iModIntro: intuitionistic context does not satisfy" C
     | MIEnvIsEmpty => fail "iModIntro: intuitionistic context is non-empty"
     end
    |tc_solve ||
     let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
     lazymatch eval hnf in s with
     | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
     | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
     end
    |pm_reduce; tc_solve ||
     fail "iModIntro: cannot filter spatial context when goal is not absorbing"
    |iSolveSideCondition
    |pm_prettify
      ].
Tactic Notation "iModIntro" := iModIntro _.

Tactic Notation "iModCore" constr(H) "as" constr(H') :=
  eapply tac_modal_elim with H H' _ _ _ _ _ _;
    [pm_reflexivity || fail "iMod:" H "not found"
    |tc_solve ||
     let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
     let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
     fail "iMod: cannot eliminate modality" P "in" Q
    |iSolveSideCondition
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iMod:" H' "not fresh"
     | _ => pm_prettify
     end].

Local Ltac ident_for_pat pat :=
  lazymatch pat with
  | IIdent ?x => x
  | _ => let x := iFresh in x
  end.

Local Ltac ident_for_pat_default pat default :=
  lazymatch pat with
  | IIdent ?x => x
  | _ =>
    lazymatch default with
    | IAnon _ => default
    | _ => let x := iFresh in x
    end
  end.

Local Ltac iDestructHypGo Hz pat0 pat :=
  lazymatch pat with
  | IFresh =>
     lazymatch Hz with
     | IAnon _ => idtac
     | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
     end
  | IDrop => iClearHyp Hz
  | IFrame => iFrameHyp Hz
  | IIdent Hz => idtac
  | IIdent ?y => iRename Hz into y
  | IList [[]] => iExFalso; iExact Hz

  | IList [[?pat1; IDrop]] =>
     let x := ident_for_pat_default pat1 Hz in
     iAndDestructChoice Hz as Left x;
     iDestructHypGo x pat0 pat1
  | IList [[IDrop; ?pat2]] =>
     let x := ident_for_pat_default pat2 Hz in
     iAndDestructChoice Hz as Right x;
     iDestructHypGo x pat0 pat2

  | IList [[IPure IGallinaAnon; ?pat2]] =>
     let x := ident_for_pat_default pat2 Hz in
     iExistDestruct Hz as ? x; iDestructHypGo x pat0 pat2
  | IList [[IPure (IGallinaNamed ?s); ?pat2]] =>
     let x := fresh in
     let y := ident_for_pat_default pat2 Hz in
     iExistDestruct Hz as x y;
     rename_by_string x s;
     iDestructHypGo y pat0 pat2
  | IList [[?pat1; ?pat2]] =>

     let x1 := ident_for_pat_default pat1 Hz in
     let x2 := ident_for_pat pat2 in
     iAndDestruct Hz as x1 x2;
     iDestructHypGo x1 pat0 pat1; iDestructHypGo x2 pat0 pat2
  | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
  | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"

  | IList [[?pat1];[?pat2]] =>
     let x1 := ident_for_pat_default pat1 Hz in
     let x2 := ident_for_pat_default pat2 Hz in
     iOrDestruct Hz as x1 x2;
     [iDestructHypGo x1 pat0 pat1|iDestructHypGo x2 pat0 pat2]

  | IList (_ :: _ :: _ :: _) => fail "iDestruct:" pat0 "has too many disjuncts"

  | IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"

  | IPure IGallinaAnon => iPure Hz as ?
  | IPure (IGallinaNamed ?s) =>
     let x := fresh in
     iPure Hz as x;
     rename_by_string x s
  | IRewrite Right => iPure Hz as ->
  | IRewrite Left => iPure Hz as <-
  | IIntuitionistic ?pat =>
    let x := ident_for_pat_default pat Hz in
    iIntuitionistic Hz as x; iDestructHypGo x pat0 pat
  | ISpatial ?pat =>
    let x := ident_for_pat_default pat Hz in
    iSpatial Hz as x; iDestructHypGo x pat0 pat
  | IModalElim ?pat =>
    let x := ident_for_pat_default pat Hz in
    iModCore Hz as x; iDestructHypGo x pat0 pat
  | _ => fail "iDestruct:" pat0 "is not supported due to" pat
  end.
Local Ltac iDestructHypFindPat Hgo pat found pats :=
  lazymatch pats with
  | [] =>
    lazymatch found with
    | true => pm_prettify
    | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
    end
  | ISimpl :: ?pats => simpl; iDestructHypFindPat Hgo pat found pats
  | IClear ?H :: ?pats => iClear H; iDestructHypFindPat Hgo pat found pats
  | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
  | ?pat1 :: ?pats =>
     lazymatch found with
     | false => iDestructHypGo Hgo pat pat1; iDestructHypFindPat Hgo pat true pats
     | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
     end
  end.

Ltac _iDestructHyp0 H pat :=
  let pats := intro_pat.parse pat in
  iDestructHypFindPat H pat false pats.
Ltac _iDestructHyp H xs pat :=
  ltac1_list_iter ltac:(fun x => iExistDestruct H as x H) xs;
  _iDestructHyp0 H pat.

Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
  _iDestructHyp0 H pat.

Ltac _iIntros_go pats startproof :=
  lazymatch pats with
  | [] =>
    lazymatch startproof with
    | true => iStartProof
    | false => idtac
    end

  | IPure (IGallinaNamed ?s) :: ?pats =>
     let i := fresh in
     iIntro (i);
     rename_by_string i s;
     _iIntros_go pats startproof
  | IPure IGallinaAnon :: ?pats => iIntro (?); _iIntros_go pats startproof
  | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; _iIntros_go pats false
  | IDrop :: ?pats => iIntro _; _iIntros_go pats startproof
  | IIdent ?H :: ?pats => iIntro H; _iIntros_go pats startproof

  | IPureIntro :: ?pats => iPureIntro; _iIntros_go pats false
  | IModalIntro :: ?pats => iModIntro; _iIntros_go pats false
  | IForall :: ?pats => repeat iIntroForall; _iIntros_go pats startproof
  | IAll :: ?pats => repeat (iIntroForall || iIntro); _iIntros_go pats startproof

  | ISimpl :: ?pats => simpl; _iIntros_go pats startproof
  | IClear ?H :: ?pats => iClear H; _iIntros_go pats false
  | IClearFrame ?H :: ?pats => iFrame H; _iIntros_go pats false
  | IDone :: ?pats => try done; _iIntros_go pats startproof

  | IIntuitionistic ?pat :: ?pats =>
     let H := iFresh in iIntro #H; iDestructHyp H as pat; _iIntros_go pats false
  | ?pat :: ?pats =>
     let H := iFresh in iIntro H; iDestructHyp H as pat; _iIntros_go pats false
  end.

Ltac _iIntros0 pat :=
  let pats := intro_pat.parse pat in

  lazymatch pats with
  | [] => idtac
  | _ => _iIntros_go pats true
  end.
Ltac _iIntros xs pat :=
  ltac1_list_iter ltac:(fun x => iIntro (x)) xs;
  _iIntros0 pat.
Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
  _iIntros xs pat.

Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
  let intro_destruct n :=
    let rec go n' :=
      lazymatch n' with
      | 0 => fail "iDestruct: cannot introduce" n "hypotheses"
      | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
      | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
      end in
    intros; go n in
  lazymatch type of lem with
  | nat => intro_destruct lem
  | Z =>

     let n := eval cbv in (Z.to_nat lem) in intro_destruct n
  | ident => tac lem
  | string => tac constr:(INamed lem)
  | _ => iPoseProofCore lem as p tac
  end.
Tactic Notation "iMod" open_constr(lem) "as" "(" ne_simple_intropattern_list(xs) ")"
    constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H as H; last _iDestructHyp H xs pat).

Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.

Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Admitted.
Global Hint Extern 0 (FromAssumption _ _ _) =>
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Admitted.
Global Hint Extern 0 (FromExist _ _) =>
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

Section class_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (⊢ P) P | 0.
Admitted.
Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Admitted.
Global Instance into_persistent_intuitionistically p P Q :
  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
Admitted.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Admitted.

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Admitted.

Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Admitted.

Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
Admitted.

Global Instance into_exist_exist {A} (Φ : A → PROP) name :
  AsIdentName Φ name → IntoExist (bi_exist Φ) Φ name.
Admitted.
End class_instances.

Section class_instances_updates.

Global Instance from_modal_bupd `{!BiBUpd PROP} P :
  FromModal True modality_id (|==> P) (|==> P) P.
Admitted.

Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Admitted.
End class_instances_updates.

Record agree (A : Type) : Type := {
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
}.
Global Arguments agree_car {_} _.
Definition to_agree {A} (a : A) : agree A.
Admitted.

Section agree.
Context {A : ofe}.
Local Instance agree_dist : Dist (agree A).
Admitted.
Local Instance agree_equiv : Equiv (agree A).
Admitted.

Definition agree_ofe_mixin : OfeMixin (agree A).
Admitted.
Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
Local Instance agree_validN_instance : ValidN (agree A).
Admitted.
Local Instance agree_valid_instance : Valid (agree A).
Admitted.

Local Program Instance agree_op_instance : Op (agree A) := λ x y,
  {| agree_car := agree_car x ++ agree_car y |}.
Admit Obligations.
Local Instance agree_pcore_instance : PCore (agree A).
Admitted.

Definition agree_cmra_mixin : CmraMixin (agree A).
Admitted.
Canonical Structure agreeR : cmra.
exact (Cmra (agree A) agree_cmra_mixin).
Defined.

End agree.
Global Arguments agreeR : clear implicits.

Notation frac := Qp (only parsing).
  Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac.
Admitted.
Local Instance frac_pcore_instance : PCore frac.
Admitted.
Local Instance frac_op_instance : Op frac.
Admitted.

  Definition frac_ra_mixin : RAMixin frac.
Admitted.
  Canonical Structure fracR := discreteR frac frac_ra_mixin.

Inductive dfrac :=
  | DfracOwn : Qp → dfrac
  | DfracDiscarded : dfrac
  | DfracBoth : Qp → dfrac.

Declare Custom Entry dfrac.
Notation "" := (DfracOwn 1) (in custom dfrac).

Structure view_rel (A : ofe) (B : ucmra) := ViewRel {
  view_rel_holds :> nat → A → B → Prop;
  view_rel_mono n1 n2 a1 a2 b1 b2 :
    view_rel_holds n1 a1 b1 →
    a1 ≡{n2}≡ a2 →
    b2 ≼{n2} b1 →
    n2 ≤ n1 →
    view_rel_holds n2 a2 b2;
  view_rel_validN n a b :
    view_rel_holds n a b → ✓{n} b;
  view_rel_unit n :
    ∃ a, view_rel_holds n a ε
}.
Global Arguments ViewRel {_ _} _ _.

Record view {A B} (rel : nat → A → B → Prop) :=
  View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.

Section ofe.
  Context {A B : ofe} (rel : nat → A → B → Prop).
Local Instance view_equiv : Equiv (view rel).
Admitted.
Local Instance view_dist : Dist (view rel).
Admitted.

  Definition view_ofe_mixin : OfeMixin (view rel).
Admitted.
  Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
End ofe.

Section cmra.
  Context {A B} (rel : view_rel A B).
Local Instance view_valid_instance : Valid (view rel).
Admitted.
Local Instance view_validN_instance : ValidN (view rel).
Admitted.
Local Instance view_pcore_instance : PCore (view rel).
Admitted.
Local Instance view_op_instance : Op (view rel).
Admitted.

  Lemma view_cmra_mixin : CmraMixin (view rel).
Admitted.
  Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Local Instance view_empty_instance : Unit (view rel).
Admitted.
  Lemma view_ucmra_mixin : UcmraMixin (view rel).
Admitted.
  Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.

End cmra.
Definition viewO_map {A A' B B' : ofe}
    {rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
    (f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel'.
Admitted.
Definition auth_view_rel_raw {A : ucmra} (n : nat) (a b : A) : Prop.
Admitted.
Lemma auth_view_rel_raw_mono (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
  auth_view_rel_raw n1 a1 b1 →
  a1 ≡{n2}≡ a2 →
  b2 ≼{n2} b1 →
  n2 ≤ n1 →
  auth_view_rel_raw n2 a2 b2.
Admitted.
Lemma auth_view_rel_raw_valid (A : ucmra) n (a b : A) :
  auth_view_rel_raw n a b → ✓{n} b.
Admitted.
Lemma auth_view_rel_raw_unit (A : ucmra) n :
  ∃ a : A, auth_view_rel_raw n a ε.
Admitted.
Canonical Structure auth_view_rel {A : ucmra} : view_rel A A.
exact (ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
          (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A)).
Defined.

Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
Definition authR (A : ucmra) : cmra.
exact (viewR (A:=A) (B:=A) auth_view_rel).
Defined.
Definition authUR (A : ucmra) : ucmra.
exact (viewUR (A:=A) (B:=A) auth_view_rel).
Defined.
Definition auth_auth {A: ucmra} : dfrac → A → auth A.
Admitted.
Definition auth_frag {A: ucmra} : A → auth A.
Admitted.

Notation "● dq a" := (auth_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "● dq  a").
Notation "◯ a" := (auth_frag a) (at level 20).

Program Definition authURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Admit Obligations.

Program Definition authRF (F : urFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Solve Obligations with apply authURF.

Record uPred (M : ucmra) : Type := UPred {
  uPred_holds : nat → M → Prop;

  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.

Local Coercion uPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred.

Section cofe.
  Context {M : ucmra}.
Local Instance uPred_equiv : Equiv (uPred M).
Admitted.
Local Instance uPred_dist : Dist (uPred M).
Admitted.
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
Admitted.
Canonical Structure uPredO : ofe.
exact (Ofe (uPred M) uPred_ofe_mixin).
Defined.

  Program Definition uPred_compl : Compl uPredO := λ c,
    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
Admit Obligations.
  Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
Admit Obligations.
End cofe.
Global Arguments uPredO : clear implicits.

Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
Global Hint Resolve uPred_mono : uPred_def.

Local Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x := φ |}.
Solve Obligations with done.
Local Definition uPred_pure_aux : seal (@uPred_pure_def).
Admitted.
Definition uPred_pure := uPred_pure_aux.(unseal).
Global Arguments uPred_pure {M}.

Local Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x ∧ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_and_aux : seal (@uPred_and_def).
Admitted.
Definition uPred_and := uPred_and_aux.(unseal).
Global Arguments uPred_and {M}.

Local Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x ∨ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_or_aux : seal (@uPred_or_def).
Admitted.
Definition uPred_or := uPred_or_aux.(unseal).
Global Arguments uPred_or {M}.

Local Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Admit Obligations.
Local Definition uPred_impl_aux : seal (@uPred_impl_def).
Admitted.
Definition uPred_impl := uPred_impl_aux.(unseal).
Global Arguments uPred_impl {M}.

Local Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
  {| uPred_holds n x := ∀ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_forall_aux : seal (@uPred_forall_def).
Admitted.
Definition uPred_forall := uPred_forall_aux.(unseal).

Local Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
  {| uPred_holds n x := ∃ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_exist_aux : seal (@uPred_exist_def).
Admitted.
Definition uPred_exist := uPred_exist_aux.(unseal).

Local Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Admit Obligations.
Local Definition uPred_sep_aux : seal (@uPred_sep_def).
Admitted.
Definition uPred_sep := uPred_sep_aux.(unseal).
Global Arguments uPred_sep {M}.

Local Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Admit Obligations.
Local Definition uPred_wand_aux : seal (@uPred_wand_def).
Admitted.
Definition uPred_wand := uPred_wand_aux.(unseal).
Global Arguments uPred_wand {M}.

Local Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.

Local Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (core x) |}.
Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
Local Definition uPred_persistently_aux : seal (@uPred_persistently_def).
Admitted.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
Global Arguments uPred_persistently {M}.

Local Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Admit Obligations.
Local Definition uPred_later_aux : seal (@uPred_later_def).
Admitted.
Definition uPred_later := uPred_later_aux.(unseal).
Global Arguments uPred_later {M}.
Definition uPred_emp {M} : uPred M.
Admitted.

Lemma uPred_bi_mixin (M : ucmra) :
  BiMixin
    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
Admitted.

Lemma uPred_bi_persistently_mixin (M : ucmra) :
  BiPersistentlyMixin
    uPred_entails uPred_emp uPred_and
    (@uPred_exist M) uPred_sep uPred_persistently.
Admitted.

Lemma uPred_bi_later_mixin (M : ucmra) :
  BiLaterMixin
    uPred_entails uPred_pure uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
Admitted.
Canonical Structure uPredI (M : ucmra) : bi.
exact ({| bi_ofe_mixin := ofe_mixin_of (uPred M);
     bi_bi_mixin := uPred_bi_mixin M;
     bi_bi_later_mixin := uPred_bi_later_mixin M;
     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}).
Defined.
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M).
Admitted.

Structure gFunctor := GFunctor {
  gFunctor_F :> rFunctor;
  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.

Record gFunctors := GFunctors {
  gFunctors_len : nat;
  gFunctors_lookup : fin gFunctors_len → gFunctor
}.

Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).

Definition gname := positive.
Definition iResUR (Σ : gFunctors) : ucmra.
Admitted.
  Notation iProp Σ := (uPred (iResUR Σ)).
  Notation iPropO Σ := (uPredO (iResUR Σ)).

Class inG (Σ : gFunctors) (A : cmra) := InG {
  inG_id : gid Σ;
  inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
  inG_prf : A = inG_apply (iPropO Σ) _;
}.
Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ.
Admitted.
Local Definition own_aux : seal (@own_def).
Admitted.
Definition own := own_aux.(unseal).
Global Arguments own {Σ A _} γ a.

Section cmra_mlist.

  Context (A: Type) `{EqDecision A}.
  Implicit Types (D: list A).

  Inductive mlist :=
    | MList D : mlist
    | MListBot : mlist.

  Inductive mlist_equiv : Equiv mlist :=
    | MList_equiv D1 D2:
        D1 = D2 → MList D1 ≡ MList D2
    | MListBot_equiv : MListBot ≡ MListBot.

  Existing Instance mlist_equiv.
  Local Instance mlist_equiv_Equivalence : @Equivalence mlist equiv.
Admitted.
Canonical Structure mlistC : ofe.
exact (discreteO mlist).
Defined.
Local Instance mlist_valid : Valid mlist.
Admitted.
Local Instance mlist_op : Op mlist.
Admitted.
Local Instance mlist_PCore : PCore mlist.
Admitted.
Local Instance mlist_unit : Unit mlist.
Admitted.

  Definition mlist_ra_mixin : RAMixin mlist.
Admitted.

  Canonical Structure mlistR := discreteR mlist mlist_ra_mixin.

  Definition mlist_ucmra_mixin : UcmraMixin mlist.
Admitted.

  Canonical Structure mlistUR :=
    Ucmra mlist mlist_ucmra_mixin.

End cmra_mlist.

Global Arguments MList {_} _.

Definition fmlistUR (A: Type) {Heq: EqDecision A} := authUR (mlistUR A).
Class fmlistG (A: Type) {Heq: EqDecision A} Σ :=
  { #[global] fmlist_inG :: inG Σ (fmlistUR A) }.

Section fmlist_props.
Context `{fmlistG A Σ}.
Definition fmlist_lb γ l := own γ (◯ (MList l)).
Definition fmlist_idx γ i a := (∃ l, ⌜ l !! i = Some a ⌝ ∗ fmlist_lb γ l)%I.

End fmlist_props.
Local Instance nat_valid_instance : Valid nat.
Admitted.
Local Instance nat_pcore_instance : PCore nat.
Admitted.
Local Instance nat_op_instance : Op nat.
Admitted.
  Lemma nat_ra_mixin : RAMixin nat.
Admitted.
Canonical Structure natR : cmra.
exact (discreteR nat nat_ra_mixin).
Defined.
Local Instance nat_unit_instance : Unit nat.
Admitted.
  Lemma nat_ucmra_mixin : UcmraMixin nat.
Admitted.
Canonical Structure natUR : ucmra.
exact (Ucmra nat nat_ucmra_mixin).
Defined.

Class lcGpreS (Σ : gFunctors) := LcGpreS {
  #[local] lcGpreS_inG :: inG Σ (authR natUR)
}.

Class lcGS (Σ : gFunctors) := LcGS {
  #[local] lcGS_inG :: inG Σ (authR natUR);
  lcGS_name : gname;
}.
Import iris.algebra.coPset.

Inductive bi_schema :=
| bi_sch_emp : bi_schema
| bi_sch_pure : Prop → bi_schema
| bi_sch_and : bi_schema → bi_schema → bi_schema
| bi_sch_or : bi_schema → bi_schema → bi_schema
| bi_sch_forall : ∀ A, (A → bi_schema) → bi_schema
| bi_sch_exist : ∀ A, (A → bi_schema) → bi_schema
| bi_sch_sep : bi_schema → bi_schema → bi_schema
| bi_sch_wand : bi_schema → bi_schema → bi_schema
| bi_sch_persistently : bi_schema → bi_schema
| bi_sch_later : bi_schema → bi_schema
| bi_sch_bupd : bi_schema → bi_schema

| bi_sch_var_fixed : nat → bi_schema
| bi_sch_var_mut : nat → bi_schema
| bi_sch_wsat : bi_schema
| bi_sch_ownE : (nat → coPset) → bi_schema.

Canonical Structure bi_schemaO := leibnizO bi_schema.

Record invariant_level_names := { invariant_name : gname; }.

Global Instance invariant_level_names_eq_dec : EqDecision (invariant_level_names).
Admitted.
  Class invGpreS (Σ : gFunctors) : Set := WsatPreG {
    #[global] inv_inPreG :: inG Σ (authR (gmapUR positive
                                    (prodR (agreeR (prodO (listO (laterO (iPropO Σ))) bi_schemaO))
                                           (optionR (prodR fracR (agreeR (listO (laterO (iPropO Σ)))))))));
    #[global] enabled_inPreG :: inG Σ coPset_disjR;
    #[global] disabled_inPreG :: inG Σ (gset_disjR positive);
    #[global] mlist_inPreG :: fmlistG (invariant_level_names) Σ;
    inv_lcPreG : lcGpreS Σ;
  }.

  Class invGS (Σ : gFunctors) : Set := WsatG {
    #[global] inv_inG :: invGpreS Σ;
    #[global] invGS_lc :: lcGS Σ;
    inv_list_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.

Definition invariant_unfold {Σ} {n} sch (Ps : vec (iProp Σ) n) : agree (list (later (iPropO Σ)) * bi_schema) :=
  to_agree ((λ P, Next P) <$> (vec_to_list Ps), sch).
Definition inv_mut_unfold {Σ} {n} q (Ps : vec (iProp Σ) n) : option (frac * (agree (list (later (iPropO Σ))))) :=
  Some (q%Qp, to_agree ((λ P, Next P) <$> (vec_to_list Ps))).
Definition ownI `{!invGS Σ} {n} (lvl: nat) (i : positive) (sch: bi_schema) (Ps : vec (iProp Σ) n) : iProp Σ :=
  (∃ γs, fmlist_idx inv_list_name lvl γs ∗
         own (invariant_name γs) (◯ {[ i := (invariant_unfold sch Ps, ε) ]})).

Definition ownI_mut `{!invGS Σ} {n} (lvl: nat) (i : positive) q (Qs : vec (iProp Σ) n) : iProp Σ :=
  (∃ (l: agree (list (later (iPropO Σ)) * bi_schema)) γs, fmlist_idx inv_list_name lvl γs ∗
         own (invariant_name γs) (◯ {[ i := (l, inv_mut_unfold q Qs) ]})).
Definition ownE `{!invGS Σ} (E : coPset) : iProp Σ.
Admitted.
Definition ownD `{!invGS Σ} (E : gset positive) : iProp Σ.
Admitted.

Definition inv_cmra_fmap `{!invGS Σ} (v: (list (iProp Σ) * bi_schema) * list (iProp Σ)) :=
  let '((Ps, sch), Qs) := v in
  (invariant_unfold sch (list_to_vec Ps), inv_mut_unfold 1%Qp (list_to_vec Qs)).

Fixpoint bi_schema_pre `{!invGS Σ} n (Ps Ps_mut: list (iProp Σ)) wsat (sch: bi_schema) :=
  match sch with
  | bi_sch_emp => emp
  | bi_sch_pure φ => ⌜φ⌝
  | bi_sch_and sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∧ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_or sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∨ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_forall A sch => ∀ (a: A),  bi_schema_pre n Ps Ps_mut wsat (sch a)
  | bi_sch_exist A sch => ∃ (a: A),  bi_schema_pre n Ps Ps_mut wsat (sch a)
  | bi_sch_sep sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∗ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_wand sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 -∗ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_persistently sch => <pers> bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_later sch => ▷ bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_bupd sch => |==> bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_var_fixed i =>
    match (Ps !! i) with
    | None => emp
    | Some P => P
    end
  | bi_sch_var_mut i =>
    match (Ps_mut !! i) with
    | None => emp
    | Some P => P
    end
  | bi_sch_wsat => wsat
  | bi_sch_ownE E => ownE (E n)
  end%I.

Definition wsat_pre `{!invGS Σ} n bi_schema_interp :=
  (∃ I : gmap positive ((list (iProp Σ) * bi_schema) * list (iProp Σ)),
        (∃ γs, fmlist_idx inv_list_name n γs ∗
             own (invariant_name γs) (● (inv_cmra_fmap <$> I : gmap _ _))) ∗
        [∗ map] i ↦ Qs ∈ I, (bi_schema_interp (bi_later <$> Qs.1.1) (bi_later <$> Qs.2) Qs.1.2 ∗
                             ownI_mut n i (1/2)%Qp (list_to_vec Qs.2) ∗
                             ownD {[i]}) ∨
                            ownE {[i]})%I.

Fixpoint bi_schema_interp `{!invGS Σ} n (Ps Ps_mut: list (iProp Σ)) sch {struct n} :=
  match n with
  | O => bi_schema_pre O Ps Ps_mut True%I sch
  | S n' => bi_schema_pre (S n') Ps Ps_mut (wsat_pre n' (bi_schema_interp n') ∗ wsat n')%I sch
  end
  with
  wsat `{!invGS Σ} n :=
  match n with
    | S n =>
  (∃ I : gmap positive ((list (iProp Σ) * bi_schema) * list (iProp Σ)),
        (∃ γs, fmlist_idx inv_list_name n γs ∗
             own (invariant_name γs) (● (inv_cmra_fmap <$> I : gmap _ _))) ∗
        [∗ map] i ↦ Qs ∈ I, (bi_schema_interp n (bi_later <$> Qs.1.1) (bi_later <$> Qs.2) Qs.1.2 ∗
                             ownI_mut n i (1/2)%Qp (list_to_vec Qs.2) ∗
                             ownD {[i]}) ∨
                            ownE {[i]})
    ∗ wsat n
    | O => True
  end%I.

Section wsat.
Context `{!invGS Σ}.

Lemma ownI_alloc {n m} φ sch lvl (Ps: vec _ n) (Ps_mut: vec _ m):
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat (S lvl) ∗
  bi_schema_interp lvl (bi_later <$> (vec_to_list Ps)) (bi_later <$> (vec_to_list Ps_mut)) sch ==∗
  ∃ i, ⌜φ i⌝ ∗ wsat (S lvl) ∗ ownI lvl i sch Ps ∗ ownI_mut lvl i (1/2)%Qp Ps_mut.
Admitted.

End wsat.

Section schema_test_mut.
Context `{!invGS Σ}.
Definition bi_sch_bupd_factory (Q P: bi_schema) : bi_schema.
Admitted.

Definition ownI_full_bupd_factory lvl i q Q P :=
  (∃ n (Qs: vec _ n), ownI lvl i (bi_sch_bupd_factory (bi_sch_var_mut O) (bi_sch_var_fixed O)) (list_to_vec [P]) ∗
   ownI_mut lvl i q Qs ∗ ⌜ default True%I (vec_to_list Qs !! 0) = Q ⌝)%I.

Lemma ownI_bupd_factory_alloc lvl φ Q P :
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat (S lvl) ∗ (▷ Q ∗ □ (▷ Q ==∗ ▷ Q ∗ ▷ P))
       ==∗ ∃ i, ⌜φ i⌝ ∗ wsat (S lvl) ∗ ownI_full_bupd_factory lvl i (1/2)%Qp Q P.
Proof.
  iIntros (?) "(Hw&(HQ&#Hfactory))".
iMod (ownI_alloc with "[$Hw HQ]") as (i) "(?&?&?&?)"; eauto; last first.
  {
 iModIntro.
iExists i.
iFrame.
instantiate (1:= list_to_vec [Q]).
rewrite //=.
}
  repeat (rewrite ?bi_schema_interp_unfold //=).

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-ssr-search-moved" "-w" "+deprecated-instance-without-locality" "-w" "+ambiguous-paths" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-deprecated-field-instance-without-locality" "-w" "+deprecated-tactic-notation" "-w" "-deprecated-since-8.19" "-w" "-deprecated-since-8.20" "-w" "-deprecated-from-Coq" "-w" "-deprecated-dirpath-Coq" "-w" "-notation-incompatible-prefix" "-w" "-deprecated-typeclasses-transparency-without-locality" "-w" "-notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/src" "Perennial" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp" "stdpp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_unstable" "stdpp.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_bitvector" "stdpp.bitvector" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/Goose" "Goose" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/record-update/src" "RecordUpdate" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coq-tactical/src" "Tactical" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris-named-props/src" "iris_named_props" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_trusted_code" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_code_axioms" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_partial_axioms" "New.code_axioms" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new" "New" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1066 lines to 167 lines, then from 180 lines to 368 lines, then from 373 lines to 168 lines, then from 181 lines to 855 lines, then from 857 lines to 177 lines, then from 190 lines to 549 lines, then from 554 lines to 194 lines, then from 207 lines to 743 lines, then from 748 lines to 248 lines, then from 261 lines to 446 lines, then from 451 lines to 249 lines, then from 262 lines to 842 lines, then from 847 lines to 260 lines, then from 273 lines to 624 lines, then from 624 lines to 278 lines, then from 291 lines to 478 lines, then from 483 lines to 279 lines, then from 292 lines to 558 lines, then from 563 lines to 279 lines, then from 292 lines to 689 lines, then from 694 lines to 309 lines, then from 322 lines to 1312 lines, then from 1316 lines to 426 lines, then from 439 lines to 919 lines, then from 924 lines to 474 lines, then from 487 lines to 1254 lines, then from 1259 lines to 659 lines, then from 660 lines to 533 lines, then from 546 lines to 841 lines, then from 846 lines to 542 lines, then from 555 lines to 674 lines, then from 679 lines to 553 lines, then from 566 lines to 969 lines, then from 974 lines to 588 lines, then from 601 lines to 766 lines, then from 771 lines to 587 lines, then from 600 lines to 772 lines, then from 777 lines to 589 lines, then from 602 lines to 962 lines, then from 967 lines to 603 lines, then from 616 lines to 1930 lines, then from 1935 lines to 642 lines, then from 655 lines to 2993 lines, then from 2998 lines to 1687 lines, then from 1700 lines to 3137 lines, then from 3142 lines to 2116 lines, then from 2113 lines to 2095 lines, then from 2108 lines to 2312 lines, then from 2317 lines to 2128 lines, then from 2141 lines to 3107 lines, then from 3112 lines to 2290 lines, then from 2303 lines to 2595 lines, then from 2600 lines to 2456 lines, then from 2469 lines to 2615 lines, then from 2620 lines to 2482 lines, then from 2495 lines to 2697 lines, then from 2702 lines to 2566 lines, then from 2579 lines to 2772 lines, then from 2777 lines to 2812 lines, then from 2813 lines to 2659 lines, then from 2672 lines to 2841 lines, then from 2846 lines to 2719 lines, then from 2732 lines to 2821 lines, then from 2826 lines to 2723 lines, then from 2736 lines to 3351 lines, then from 3356 lines to 3168 lines, then from 3151 lines to 2792 lines, then from 2805 lines to 3604 lines, then from 3608 lines to 3348 lines, then from 3321 lines to 2867 lines, then from 2880 lines to 3175 lines, then from 3180 lines to 2909 lines, then from 2922 lines to 3120 lines, then from 3125 lines to 2914 lines, then from 2927 lines to 3193 lines, then from 3198 lines to 2974 lines, then from 2987 lines to 3042 lines, then from 3047 lines to 3001 lines, then from 3011 lines to 2993 lines, then from 3006 lines to 3655 lines, then from 3660 lines to 2996 lines, then from 3009 lines to 3093 lines, then from 3099 lines to 3005 lines, then from 3019 lines to 3684 lines, then from 3690 lines to 3015 lines, then from 3029 lines to 3058 lines, then from 3064 lines to 3021 lines, then from 3035 lines to 3069 lines, then from 3075 lines to 3028 lines, then from 3042 lines to 3070 lines, then from 3076 lines to 3073 lines, then from 3075 lines to 3036 lines, then from 3049 lines to 3118 lines, then from 3124 lines to 3057 lines, then from 3071 lines to 3261 lines, then from 3267 lines to 3065 lines, then from 3079 lines to 3341 lines, then from 3347 lines to 3122 lines, then from 3136 lines to 3421 lines,

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-ssr-search-moved" "-w" "+deprecated-instance-without-locality" "-w" "+ambiguous-paths" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-deprecated-field-instance-without-locality" "-w" "+deprecated-tactic-notation" "-w" "-deprecated-since-8.19" "-w" "-deprecated-since-8.20" "-w" "-deprecated-from-Coq" "-w" "-deprecated-dirpath-Coq" "-w" "-notation-incompatible-prefix" "-w" "-deprecated-typeclasses-transparency-without-locality" "-w" "-notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/src" "Perennial" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp" "stdpp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_unstable" "stdpp.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_bitvector" "stdpp.bitvector" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/Goose" "Goose" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/record-update/src" "RecordUpdate" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coq-tactical/src" "Tactical" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris-named-props/src" "iris_named_props" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_trusted_code" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_code_axioms" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_partial_axioms" "New.code_axioms" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new" "New" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1066 lines to 167 lines, then from 180 lines to 368 lines, then from 373 lines to 168 lines, then from 181 lines to 855 lines, then from 857 lines to 177 lines, then from 190 lines to 549 lines, then from 554 lines to 194 lines, then from 207 lines to 743 lines, then from 748 lines to 248 lines, then from 261 lines to 446 lines, then from 451 lines to 249 lines, then from 262 lines to 842 lines, then from 847 lines to 260 lines, then from 273 lines to 624 lines, then from 624 lines to 278 lines, then from 291 lines to 478 lines, then from 483 lines to 279 lines, then from 292 lines to 558 lines, then from 563 lines to 279 lines, then from 292 lines to 689 lines, then from 694 lines to 309 lines, then from 322 lines to 1312 lines, then from 1316 lines to 426 lines, then from 439 lines to 919 lines, then from 924 lines to 474 lines, then from 487 lines to 1254 lines, then from 1259 lines to 659 lines, then from 660 lines to 533 lines, then from 546 lines to 841 lines, then from 846 lines to 542 lines, then from 555 lines to 674 lines, then from 679 lines to 553 lines, then from 566 lines to 969 lines, then from 974 lines to 588 lines, then from 601 lines to 766 lines, then from 771 lines to 587 lines, then from 600 lines to 772 lines, then from 777 lines to 589 lines, then from 602 lines to 962 lines, then from 967 lines to 603 lines, then from 616 lines to 1930 lines, then from 1935 lines to 642 lines, then from 655 lines to 2993 lines, then from 2998 lines to 1687 lines, then from 1700 lines to 3137 lines, then from 3142 lines to 2116 lines, then from 2113 lines to 2095 lines, then from 2108 lines to 2312 lines, then from 2317 lines to 2128 lines, then from 2141 lines to 3107 lines, then from 3112 lines to 2290 lines, then from 2303 lines to 2595 lines, then from 2600 lines to 2456 lines, then from 2469 lines to 2615 lines, then from 2620 lines to 2482 lines, then from 2495 lines to 2697 lines, then from 2702 lines to 2566 lines, then from 2579 lines to 2772 lines, then from 2777 lines to 2812 lines, then from 2813 lines to 2659 lines, then from 2672 lines to 2841 lines, then from 2846 lines to 2719 lines, then from 2732 lines to 2821 lines, then from 2826 lines to 2723 lines, then from 2736 lines to 3351 lines, then from 3356 lines to 3168 lines, then from 3151 lines to 2792 lines, then from 2805 lines to 3604 lines, then from 3608 lines to 3348 lines, then from 3321 lines to 2867 lines, then from 2880 lines to 3175 lines, then from 3180 lines to 2909 lines, then from 2922 lines to 3120 lines, then from 3125 lines to 2914 lines, then from 2927 lines to 3193 lines, then from 3198 lines to 2974 lines, then from 2987 lines to 3042 lines, then from 3047 lines to 3001 lines, then from 3011 lines to 2993 lines, then from 3006 lines to 3655 lines, then from 3660 lines to 2996 lines, then from 3009 lines to 3093 lines, then from 3099 lines to 3005 lines, then from 3019 lines to 3684 lines, then from 3690 lines to 3015 lines, then from 3029 lines to 3058 lines, then from 3064 lines to 3021 lines, then from 3035 lines to 3069 lines, then from 3075 lines to 3028 lines, then from 3042 lines to 3070 lines, then from 3076 lines to 3073 lines, then from 3075 lines to 3036 lines, then from 3049 lines to 3118 lines, then from 3124 lines to 3057 lines, then from 3071 lines to 3261 lines, then from 3267 lines to 3065 lines, then from 3079 lines to 3341 lines, then from 3347 lines to 3122 lines, then from 3136 lines to 3421 lines, then from 3427 lines to 3131 lines, then from 3145 lines to 3388 lines, then from 3394 lines to 3312 lines, then from 3313 lines to 3135 lines, then from 3148 lines to 3251 lines, then from 3257 lines to 3136 lines, then from 3150 lines to 3895 lines, then from 3901 lines to 3154 lines, then from 3168 lines to 6507 lines, then from 6513 lines to 3196 lines, then from 3211 lines to 3158 lines, then from 3171 lines to 4044 lines, then from 4050 lines to 3196 lines, then from 3210 lines to 3543 lines, then from 3549 lines to 3216 lines, then from 3230 lines to 3505 lines, then from 3511 lines to 3468 lines, then from 3467 lines to 3228 lines, then from 3241 lines to 4292 lines, then from 4297 lines to 3239 lines, then from 3253 lines to 3809 lines, then from 3815 lines to 3240 lines, then from 3254 lines to 5079 lines, then from 5085 lines to 4133 lines, then from 4119 lines to 3252 lines, then from 3265 lines to 3373 lines, then from 3379 lines to 3255 lines, then from 3269 lines to 3465 lines, then from 3471 lines to 3293 lines, then from 3307 lines to 3880 lines, then from 3886 lines to 3482 lines, then from 3496 lines to 3703 lines, then from 3708 lines to 3526 lines, then from 3541 lines to 3522 lines, then from 3535 lines to 3730 lines, then from 3736 lines to 3550 lines, then from 3564 lines to 4093 lines, then from 4099 lines to 3561 lines, then from 3575 lines to 4478 lines, then from 4484 lines to 4162 lines, then from 4158 lines to 3594 lines, then from 3607 lines to 3799 lines, then from 3805 lines to 3614 lines, then from 3628 lines to 4139 lines, then from 4145 lines to 3615 lines, then from 3634 lines to 3613 lines, then from 3626 lines to 8522 lines, then from 8527 lines to 3653 lines, then from 3667 lines to 3914 lines, then from 3920 lines to 3871 lines, then from 3864 lines to 3690 lines, then from 3703 lines to 5752 lines, then from 5758 lines to 3949 lines, then from 3963 lines to 4076 lines, then from 4082 lines to 4065 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.14.1
   coqtop version runner-t7b1znuaq-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfbe3) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
   Modules that could not be inlined: Ltac2.Array, Ltac2.Pattern, Ltac2.Ltac1
   Expected coqc runtime on this file: 2.569 sec *)








Require Stdlib.Init.Ltac.
Require Stdlib.Bool.Bool.
Require Stdlib.Classes.Morphisms.
Require Stdlib.Classes.RelationClasses.
Require Stdlib.Init.Peano.
Require Stdlib.Lists.List.
Require Stdlib.Logic.EqdepFacts.
Require Stdlib.NArith.NArith.
Require Stdlib.PArith.PArith.
Require Stdlib.Program.Basics.
Require Stdlib.Program.Syntax.
Require Stdlib.QArith.QArith.
Require Stdlib.QArith.QArith_base.
Require Stdlib.QArith.Qcanon.
Require Stdlib.Setoids.Setoid.
Require Stdlib.Sorting.Permutation.
Require Stdlib.Unicode.Utf8.
Require Stdlib.Vectors.Vector.
Require Stdlib.ZArith.ZArith.
Require Stdlib.micromega.Lia.
Require Stdlib.ssr.ssreflect.
Require Stdlib.ssr.ssrfun.
Require stdpp.options.
Require iris.prelude.options.
Require stdpp.base.
Require stdpp.proof_irrel.
Require stdpp.well_founded.
Require stdpp.decidable.
Require stdpp.tactics.
Require stdpp.fin.
Require stdpp.option.
Require stdpp.orders.
Require stdpp.numbers.
Require stdpp.lexico.
Require stdpp.list.
Require stdpp.list_numbers.
Require stdpp.countable.
Require stdpp.vector.
Require stdpp.finite.
Require stdpp.sets.
Require stdpp.listset.
Require stdpp.relations.
Require stdpp.fin_sets.
Require stdpp.prelude.
Require stdpp.ssreflect.
Require iris.prelude.prelude.
Require iris.algebra.ofe.
Require Stdlib.Strings.String.
Require Ltac2.Init.
Require Ltac2.Std.
Require Ltac2.Message.
Require Ltac2.Control.
Require Ltac2.Ltac1.
Require Ltac2.Pattern.
Require Ltac2.Int.
Require Ltac2.Bool.
Require Ltac2.Array.

Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.

Module Export iris_DOT_algebra_DOT_monoid_WRAPPED.
Module Export monoid.
Export iris.algebra.ofe.
Import iris.prelude.options.


Class Monoid {M : ofe} (o : M → M → M) := {
  monoid_unit : M;
  monoid_ne : NonExpansive2 o;
  monoid_assoc : Assoc (≡) o;
  monoid_comm : Comm (≡) o;
  monoid_left_id : LeftId (≡) monoid_unit o;
}.
Lemma monoid_proper {M : ofe} {o : M → M → M} `{!Monoid o} : Proper ((≡) ==> (≡) ==> (≡)) o.
Admitted.
Lemma monoid_right_id {M : ofe} {o : M → M → M} `{!Monoid o} : RightId (≡) monoid_unit o.
Admitted.


Class WeakMonoidHomomorphism {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
    (R : relation M2) (f : M1 → M2) := {
  monoid_homomorphism_rel_po : PreOrder R;
  monoid_homomorphism_rel_proper : Proper ((≡) ==> (≡) ==> iff) R;
  monoid_homomorphism_op_proper : Proper (R ==> R ==> R) o2;
  monoid_homomorphism_ne : NonExpansive f;
  monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
}.

Class MonoidHomomorphism {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
    (R : relation M2) (f : M1 → M2) := {
  #[global] monoid_homomorphism_weak :: WeakMonoidHomomorphism o1 o2 R f;
  monoid_homomorphism_unit : R (f monoid_unit) monoid_unit
}.

Lemma weak_monoid_homomorphism_proper
  `{WeakMonoidHomomorphism M1 M2 o1 o2 R f} : Proper ((≡) ==> (≡)) f.
Admitted.

End monoid.

End iris_DOT_algebra_DOT_monoid_WRAPPED.
Module Export iris.
Module Export algebra.
Module Export monoid.
Include iris_DOT_algebra_DOT_monoid_WRAPPED.monoid.
End monoid.

Module Export iris_DOT_algebra_DOT_cmra_WRAPPED.
Module Export cmra.
Export iris.algebra.monoid.

Class PCore (A : Type) := pcore : A → option A.

Class Op (A : Type) := op : A → A → A.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.

Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.

Class ValidN (A : Type) := validN : nat → A → Prop.
Notation "✓{ n } x" := (validN n x)
  (at level 20, n at next level, format "✓{ n }  x").

Class Valid (A : Type) := valid : A → Prop.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.

Definition includedN `{!Dist A, !Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
  (at level 70, n at next level, format "x  ≼{ n }  y") : stdpp_scope.
Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.

Section mixin.
  Record CmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {

    mixin_cmra_op_ne (x : A) : NonExpansive (op x);
    mixin_cmra_pcore_ne n (x y : A) cx :
      x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
    mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);

    mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
    mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;

    mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
    mixin_cmra_comm : Comm (≡@{A}) (⋅);
    mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
    mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
    mixin_cmra_pcore_mono (x y : A) cx :
      x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
    mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
    mixin_cmra_extend n (x y1 y2 : A) :
      ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
      { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
  }.
End mixin.

#[projections(primitive=no)]
Structure cmra := Cmra' {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_pcore : PCore cmra_car;
  cmra_op : Op cmra_car;
  cmra_valid : Valid cmra_car;
  cmra_validN : ValidN cmra_car;
  cmra_ofe_mixin : OfeMixin cmra_car;
  cmra_mixin : CmraMixin cmra_car;
}.
Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.

Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).

Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
Coercion cmra_ofeO (A : cmra) : ofe.
exact (Ofe A (cmra_ofe_mixin A)).
Defined.
Canonical Structure cmra_ofeO.
Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac.
exact (cmra_mixin Ac).
Defined.
Notation cmra_mixin_of A :=
  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).

Definition core {A} `{!PCore A} (x : A) : A.
Admitted.

Class Unit (A : Type) := ε : A.

Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
  mixin_ucmra_unit_valid : ✓ (ε : A);
  mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
  mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.

#[projections(primitive=no)]
Structure ucmra := Ucmra' {
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
  ucmra_pcore : PCore ucmra_car;
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_unit : Unit ucmra_car;
  ucmra_ofe_mixin : OfeMixin ucmra_car;
  ucmra_cmra_mixin : CmraMixin ucmra_car;
  ucmra_mixin : UcmraMixin ucmra_car;
}.
Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
Notation Ucmra A m :=
  (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).

Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
Coercion ucmra_ofeO (A : ucmra) : ofe.
exact (Ofe A (ucmra_ofe_mixin A)).
Defined.
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmra) : cmra.
exact (Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A)).
Defined.
Canonical Structure ucmra_cmraR.

Class CmraMorphism {A B : cmra} (f : A → B) := {
  #[global] cmra_morphism_ne :: NonExpansive f;
  cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
  cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
  cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.

Section cmra.
Context {A : cmra}.
Implicit Types x y z : A.

Section total_core.
  Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Admitted.
  Lemma cmra_core_monoN n x y : x ≼{n} y → core x ≼{n} core y.
Admitted.
End total_core.
End cmra.

Section ucmra.
  Context {A : ucmra}.

  Lemma ucmra_unit_validN n : ✓{n} (ε:A).
Admitted.
End ucmra.

Record rFunctor := RFunctor {
  rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmra;
  rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
  rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
  rFunctor_map_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
    rFunctor_map (cid,cid) x ≡ x;
  rFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
  rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (rFunctor_map fg)
}.

Class rFunctorContractive (F : rFunctor) :=
  #[global] rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
    Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
Definition rFunctor_apply (F: rFunctor) (A: ofe) `{!Cofe A} : cmra.
Admitted.

Record urFunctor := URFunctor {
  urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmra;
  urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
  urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
  urFunctor_map_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
    urFunctor_map (cid,cid) x ≡ x;
  urFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
  urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (urFunctor_map fg)
}.

Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {

  ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
  ra_core_proper (x y : A) cx :
    x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy;
  ra_validN_proper : Proper ((≡@{A}) ==> impl) valid;

  ra_assoc : Assoc (≡@{A}) (⋅);
  ra_comm : Comm (≡@{A}) (⋅);
  ra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
  ra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
  ra_pcore_mono (x y : A) cx :
    x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
  ra_valid_op_l (x y : A) : ✓ (x ⋅ y) → ✓ x
}.

Section discrete.
  Context `{!Equiv A, !PCore A, !Op A, !Valid A} (Heq : @Equivalence A (≡)).
  Context (ra_mix : RAMixin A).
  Existing Instances discrete_dist.
Local Instance discrete_validN_instance : ValidN A.
Admitted.
  Definition discrete_cmra_mixin : CmraMixin A.
Admitted.
End discrete.

Notation discreteR A ra_mix :=
  (Cmra A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
  (only parsing).

Section prod.
  Context {A B : cmra}.
Local Instance prod_op_instance : Op (A * B).
Admitted.
Local Instance prod_pcore_instance : PCore (A * B).
Admitted.
Local Instance prod_valid_instance : Valid (A * B).
Admitted.
Local Instance prod_validN_instance : ValidN (A * B).
Admitted.

  Definition prod_cmra_mixin : CmraMixin (A * B).
Admitted.
  Canonical Structure prodR := Cmra (prod A B) prod_cmra_mixin.
End prod.

Global Arguments prodR : clear implicits.

Section option.
  Context {A : cmra}.
Local Instance option_valid_instance : Valid (option A).
Admitted.
Local Instance option_validN_instance : ValidN (option A).
Admitted.
Local Instance option_pcore_instance : PCore (option A).
Admitted.
Local Instance option_op_instance : Op (option A).
Admitted.

  Lemma option_cmra_mixin : CmraMixin (option A).
Admitted.
  Canonical Structure optionR := Cmra (option A) option_cmra_mixin.
Local Instance option_unit_instance : Unit (option A).
Admitted.
  Lemma option_ucmra_mixin : UcmraMixin optionR.
Admitted.
  Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
End option.

Global Arguments optionR : clear implicits.

End cmra.
Module Export iris.
Module Export algebra.
Module Export cmra.
Include iris_DOT_algebra_DOT_cmra_WRAPPED.cmra.
End cmra.
Import Stdlib.Strings.Ascii.

Export Stdlib.Strings.String (string(..)).

String Notation string
  String.string_of_list_byte String.list_byte_of_string : stdpp_scope.

Module Export Ascii.
Definition is_nat (x : ascii) : option nat.
exact (match x with
    | "0" => Some 0
    | "1" => Some 1
    | "2" => Some 2
    | "3" => Some 3
    | "4" => Some 4
    | "5" => Some 5
    | "6" => Some 6
    | "7" => Some 7
    | "8" => Some 8
    | "9" => Some 9
    | _ => None
    end%char).
Defined.
Definition is_space (x : ascii) : bool.
exact (match x with
    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
    end%char).
Defined.

Module Export String.
Fixpoint rev_app (s1 s2 : string) : string.
exact (match s1 with
    | "" => s2
    | String a s1 => rev_app s1 (String a s2)
    end).
Defined.
Definition rev (s : string) : string.
exact (rev_app s "").
Defined.

Class MapFold K A M := map_fold B : (K → A → B → B) → B → M → B.
Global Arguments map_fold {_ _ _ _ _} _ _ _.
Definition diag_None {A B C} (f : option A → option B → option C)
    (mx : option A) (my : option B) : option C.
Admitted.
Global Instance map_insert `{PartialAlter K A M} : Insert K A M.
Admitted.

Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
    PartialAlter K A (M A), OMap M, Merge M, ∀ A, MapFold K A (M A),
    EqDecision K} := {
  map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
  lookup_empty {A} i : (∅ : M A) !! i = None;
  lookup_partial_alter {A} f (m : M A) i :
    partial_alter f i m !! i = f (m !! i);
  lookup_partial_alter_ne {A} f (m : M A) i j :
    i ≠ j → partial_alter f i m !! j = m !! j;
  lookup_fmap {A B} (f : A → B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
  lookup_omap {A B} (f : A → option B) (m : M A) i :
    omap f m !! i = m !! i ≫= f;
  lookup_merge {A B C} (f : option A → option B → option C) (m1 : M A) (m2 : M B) i :
    merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i);
  map_fold_empty {A B} (f : K → A → B → B) (b : B) :
    map_fold f b ∅ = b;

  map_fold_fmap_ind {A} (P : M A → Prop) :
    P ∅ →
    (∀ i x m,
      m !! i = None →
      (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
        map_fold f b (<[i:=x']> (g <$> m)) = f i x' (map_fold f b (g <$> m))) →
      P m →
      P (<[i:=x]> m)) →
    ∀ m, P m;
}.
Global Instance map_singleton `{PartialAlter K A M, Empty M} :
  SingletonM K A M.
Admitted.
Global Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20.
Admitted.

Export stdpp.countable.

Record mapset' (Munit : Type) : Type :=
  Mapset { mapset_car: Munit }.
Notation mapset M := (mapset' (M unit)).

Section mapset.
Context `{FinMap K M}.
Global Instance mapset_elem_of: ElemOf K (mapset M).
admit.
Defined.
Global Instance mapset_singleton: Singleton K (mapset M).
admit.
Defined.

End mapset.

Local Open Scope positive_scope.

Local Notation "P ~ 0" := (λ p, P p~0) : function_scope.
Local Notation "P ~ 1" := (λ p, P p~1) : function_scope.

Inductive gmap_dep_ne (A : Type) (P : positive → Prop) :=
  | GNode001 : gmap_dep_ne A P~1  → gmap_dep_ne A P
  | GNode010 : P 1 → A → gmap_dep_ne A P
  | GNode011 : P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode100 : gmap_dep_ne A P~0 → gmap_dep_ne A P
  | GNode101 : gmap_dep_ne A P~0 → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode110 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P
  | GNode111 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P.

Variant gmap_dep (A : Type) (P : positive → Prop) :=
  | GEmpty : gmap_dep A P
  | GNodes : gmap_dep_ne A P → gmap_dep A P.

Record gmap_key K `{Countable K} (q : positive) :=
  GMapKey { _ : encode (A:=K) <$> decode q = Some q }.

Record gmap K `{Countable K} A := GMap { gmap_car : gmap_dep A (gmap_key K) }.
Global Instance gmap_lookup `{Countable K} {A} :
    Lookup K A (gmap K A).
Admitted.
Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A).
Admitted.
Global Instance gmap_partial_alter `{Countable K} {A} :
    PartialAlter K A (gmap K A).
Admitted.
Global Instance gmap_fmap `{Countable K} : FMap (gmap K).
Admitted.

Definition gset K `{Countable K} := mapset (gmap K).

Inductive coPset_raw :=
  | coPLeaf : bool → coPset_raw
  | coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
Fixpoint coPset_wf (t : coPset_raw) : bool.
Admitted.

Definition coPset := { t | coPset_wf t }.
Global Instance coPset_singleton : Singleton positive coPset.
Admitted.

Module Export iris_DOT_algebra_DOT_coPset_WRAPPED.
Module Export coPset.
Export iris.algebra.cmra.

Inductive coPset_disj :=
  | CoPset : coPset → coPset_disj
  | CoPsetBot : coPset_disj.

Section coPset_disj.
  Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid_instance : Valid coPset_disj.
Admitted.
Local Instance coPset_disj_op_instance : Op coPset_disj.
Admitted.
Local Instance coPset_disj_pcore_instance : PCore coPset_disj.
Admitted.

  Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
Admitted.
  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
End coPset_disj.

End coPset.
Module Export iris.
Module Export algebra.
Module Export coPset.
Include iris_DOT_algebra_DOT_coPset_WRAPPED.coPset.
End coPset.

Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).

Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).

Reserved Notation "⊢ Q" (at level 20, Q at level 200).
Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
Reserved Notation "P -∗ Q"
  (at level 99, Q at level 200, right associativity,
   format "'[' P  -∗  '/' '[' Q ']' ']'").

Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<pers>?' p  P").

Reserved Notation "▷ P" (at level 20, right associativity).
Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
   format "▷^ n  P").

Reserved Notation "'<affine>' P" (at level 20, right associativity).
Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<affine>?' p  P").

Reserved Notation "'<absorb>' P" (at level 20, right associativity).

Reserved Notation "□ P" (at level 20, right associativity).
Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'□?' p  P").

Reserved Notation "|==> Q" (at level 99, Q at level 200, format "'[  ' |==>  '/' Q ']'").
Reserved Notation "P ==∗ Q"
  (at level 99, Q at level 200, format "'[' P  ==∗  '/' Q ']'").

Reserved Notation "'[∗]' Ps" (at level 20).
Reserved Notation "'[∧' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x binder, right associativity,
   format "[∧  list]  x  ∈  l ,  P").

Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
  (at level 200, m at level 10, k binder, x binder, right associativity,
   format "[∗  map]  k ↦ x  ∈  m ,  P").
Delimit Scope bi_scope with I.

Section bi_mixin.
  Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
  Context (bi_entails : PROP → PROP → Prop).
  Context (bi_emp : PROP).
  Context (bi_pure : Prop → PROP).
  Context (bi_and : PROP → PROP → PROP).
  Context (bi_or : PROP → PROP → PROP).
  Context (bi_impl : PROP → PROP → PROP).
  Context (bi_forall : ∀ A, (A → PROP) → PROP).
  Context (bi_exist : ∀ A, (A → PROP) → PROP).
  Context (bi_sep : PROP → PROP → PROP).
  Context (bi_wand : PROP → PROP → PROP).

  Bind Scope bi_scope with PROP.
  Local Infix "⊢" := bi_entails.
  Local Notation "'emp'" := bi_emp : bi_scope.
  Local Notation "'True'" := (bi_pure True) : bi_scope.
  Local Notation "'False'" := (bi_pure False) : bi_scope.
  Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
  Local Infix "∧" := bi_and : bi_scope.
  Local Infix "∨" := bi_or : bi_scope.
  Local Infix "→" := bi_impl : bi_scope.
  Local Notation "∀ x .. y , P" :=
    (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.
  Local Notation "∃ x .. y , P" :=
    (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
  Local Infix "∗" := bi_sep : bi_scope.
  Local Infix "-∗" := bi_wand : bi_scope.

  Record BiMixin := {
    bi_mixin_entails_po : PreOrder bi_entails;
    bi_mixin_equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);

    bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
    bi_mixin_and_ne : NonExpansive2 bi_and;
    bi_mixin_or_ne : NonExpansive2 bi_or;
    bi_mixin_impl_ne : NonExpansive2 bi_impl;
    bi_mixin_forall_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A);
    bi_mixin_exist_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
    bi_mixin_sep_ne : NonExpansive2 bi_sep;
    bi_mixin_wand_ne : NonExpansive2 bi_wand;

    bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
    bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;

    bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P;
    bi_mixin_and_elim_r P Q : P ∧ Q ⊢ Q;
    bi_mixin_and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R;

    bi_mixin_or_intro_l P Q : P ⊢ P ∨ Q;
    bi_mixin_or_intro_r P Q : Q ⊢ P ∨ Q;
    bi_mixin_or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R;

    bi_mixin_impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R;
    bi_mixin_impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R;

    bi_mixin_forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a;
    bi_mixin_forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a;

    bi_mixin_exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a;
    bi_mixin_exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q;

    bi_mixin_sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q';
    bi_mixin_emp_sep_1 P : P ⊢ emp ∗ P;
    bi_mixin_emp_sep_2 P : emp ∗ P ⊢ P;
    bi_mixin_sep_comm' P Q : P ∗ Q ⊢ Q ∗ P;
    bi_mixin_sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R);
    bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
    bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
  }.

  Context (bi_persistently : PROP → PROP).
  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.

  Record BiPersistentlyMixin := {
    bi_mixin_persistently_ne : NonExpansive bi_persistently;

    bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;

    bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;

    bi_mixin_persistently_emp_2 : emp ⊢ <pers> emp;

    bi_mixin_persistently_and_2 (P Q : PROP) :
      (<pers> P) ∧ (<pers> Q) ⊢ <pers> (P ∧ Q);
    bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
      <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);

    bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;

    bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
  }.

  Context (bi_later : PROP → PROP).
  Local Notation "▷ P" := (bi_later P) : bi_scope.

  Record BiLaterMixin := {
    bi_mixin_later_ne : NonExpansive bi_later;

    bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
    bi_mixin_later_intro P : P ⊢ ▷ P;

    bi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
    bi_mix

[...]

 xs pat as p
    | _ => fail "iSpecialize:" t "should be a proof mode term"
    end
  end.

Tactic Notation "iPoseProofCore" open_constr(lem)
    "as" constr(p) tactic3(tac) :=
  iStartProof;
  let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
  let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
  let spec_tac Htmp :=
    lazymatch lem with
    | ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
    | _ => idtac
    end in
  lazymatch type of t with
  | ident =>
     let Htmp := iFresh in
     iPoseProofCoreHyp t as Htmp; spec_tac Htmp; [..|tac Htmp]
  | _ => iPoseProofCoreLem t as (fun Htmp => spec_tac Htmp; [..|tac Htmp])
  end.

Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
  eapply tac_or_destruct with H _ H1 H2 _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iOrDestruct:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoOr ?P _ _ => P end in
     fail "iOrDestruct: cannot destruct" P
    | pm_reduce;
      lazymatch goal with
      | |- False =>
        let H1 := pretty_ident H1 in
        let H2 := pretty_ident H2 in
        fail "iOrDestruct:" H1 "or" H2 "not fresh"
      |  _ => split
      end].

Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
  eapply tac_and_destruct with H _ H1 H2 _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iAndDestruct:" H "not found"
    |pm_reduce; tc_solve ||
     let P :=
       lazymatch goal with
       | |- IntoSep ?P _ _ => P
       | |- IntoAnd _ ?P _ _ => P
       end in
     fail "iAndDestruct: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
       | |- False =>
         let H1 := pretty_ident H1 in
         let H2 := pretty_ident H2 in
         fail "iAndDestruct:" H1 "or" H2 "not fresh"
       | _ => idtac
     end].

Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
  eapply tac_and_destruct_choice with H _ d H' _ _ _;
    [pm_reflexivity || fail "iAndDestructChoice:" H "not found"
    |pm_reduce; tc_solve ||
     let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
     fail "iAndDestructChoice: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iAndDestructChoice:" H' "not fresh"
     | _ => idtac
     end].

Ltac _iExists x :=
  iStartProof;
  eapply tac_exist;
    [tc_solve ||
     let P := match goal with |- FromExist ?P _ => P end in
     fail "iExists:" P "not an existential"
    |pm_prettify; eexists x
      ].

Tactic Notation "iExists" ne_uconstr_list_sep(xs,",") :=
  ltac1_list_iter _iExists xs.

Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
  eapply tac_exist_destruct with H _ Hx _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iExistDestruct:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoExist ?P _ _ => P end in
     fail "iExistDestruct: cannot destruct" P|];
    let name := lazymatch goal with
                | |- let _ := (λ name, _) in _ => name
                end in
    intros _;
    let y := fresh name in
    intros y; pm_reduce;
    lazymatch goal with
    | |- False =>
      let Hx := pretty_ident Hx in
      fail "iExistDestruct:" Hx "not fresh"
    | _ => revert y; intros x
    end.

Tactic Notation "iModIntro" uconstr(sel) :=
  iStartProof;
  notypeclasses refine (tac_modal_intro _ _ sel _ _ _ _ _ _ _ _ _ _ _ _ _ _);
    [tc_solve ||
     fail "iModIntro: the goal is not a modality"
    |tc_solve ||
     let s := lazymatch goal with |- IntoModalIntuitionisticEnv _ _ _ ?s => s end in
     lazymatch eval hnf in s with
     | MIEnvForall ?C => fail "iModIntro: intuitionistic context does not satisfy" C
     | MIEnvIsEmpty => fail "iModIntro: intuitionistic context is non-empty"
     end
    |tc_solve ||
     let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
     lazymatch eval hnf in s with
     | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
     | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
     end
    |pm_reduce; tc_solve ||
     fail "iModIntro: cannot filter spatial context when goal is not absorbing"
    |iSolveSideCondition
    |pm_prettify
      ].
Tactic Notation "iModIntro" := iModIntro _.

Tactic Notation "iModCore" constr(H) "as" constr(H') :=
  eapply tac_modal_elim with H H' _ _ _ _ _ _;
    [pm_reflexivity || fail "iMod:" H "not found"
    |tc_solve ||
     let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
     let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
     fail "iMod: cannot eliminate modality" P "in" Q
    |iSolveSideCondition
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iMod:" H' "not fresh"
     | _ => pm_prettify
     end].

Local Ltac ident_for_pat pat :=
  lazymatch pat with
  | IIdent ?x => x
  | _ => let x := iFresh in x
  end.

Local Ltac ident_for_pat_default pat default :=
  lazymatch pat with
  | IIdent ?x => x
  | _ =>
    lazymatch default with
    | IAnon _ => default
    | _ => let x := iFresh in x
    end
  end.

Local Ltac iDestructHypGo Hz pat0 pat :=
  lazymatch pat with
  | IFresh =>
     lazymatch Hz with
     | IAnon _ => idtac
     | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
     end
  | IDrop => iClearHyp Hz
  | IFrame => iFrameHyp Hz
  | IIdent Hz => idtac
  | IIdent ?y => iRename Hz into y
  | IList [[]] => iExFalso; iExact Hz

  | IList [[?pat1; IDrop]] =>
     let x := ident_for_pat_default pat1 Hz in
     iAndDestructChoice Hz as Left x;
     iDestructHypGo x pat0 pat1
  | IList [[IDrop; ?pat2]] =>
     let x := ident_for_pat_default pat2 Hz in
     iAndDestructChoice Hz as Right x;
     iDestructHypGo x pat0 pat2

  | IList [[IPure IGallinaAnon; ?pat2]] =>
     let x := ident_for_pat_default pat2 Hz in
     iExistDestruct Hz as ? x; iDestructHypGo x pat0 pat2
  | IList [[IPure (IGallinaNamed ?s); ?pat2]] =>
     let x := fresh in
     let y := ident_for_pat_default pat2 Hz in
     iExistDestruct Hz as x y;
     rename_by_string x s;
     iDestructHypGo y pat0 pat2
  | IList [[?pat1; ?pat2]] =>

     let x1 := ident_for_pat_default pat1 Hz in
     let x2 := ident_for_pat pat2 in
     iAndDestruct Hz as x1 x2;
     iDestructHypGo x1 pat0 pat1; iDestructHypGo x2 pat0 pat2
  | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
  | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"

  | IList [[?pat1];[?pat2]] =>
     let x1 := ident_for_pat_default pat1 Hz in
     let x2 := ident_for_pat_default pat2 Hz in
     iOrDestruct Hz as x1 x2;
     [iDestructHypGo x1 pat0 pat1|iDestructHypGo x2 pat0 pat2]

  | IList (_ :: _ :: _ :: _) => fail "iDestruct:" pat0 "has too many disjuncts"

  | IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"

  | IPure IGallinaAnon => iPure Hz as ?
  | IPure (IGallinaNamed ?s) =>
     let x := fresh in
     iPure Hz as x;
     rename_by_string x s
  | IRewrite Right => iPure Hz as ->
  | IRewrite Left => iPure Hz as <-
  | IIntuitionistic ?pat =>
    let x := ident_for_pat_default pat Hz in
    iIntuitionistic Hz as x; iDestructHypGo x pat0 pat
  | ISpatial ?pat =>
    let x := ident_for_pat_default pat Hz in
    iSpatial Hz as x; iDestructHypGo x pat0 pat
  | IModalElim ?pat =>
    let x := ident_for_pat_default pat Hz in
    iModCore Hz as x; iDestructHypGo x pat0 pat
  | _ => fail "iDestruct:" pat0 "is not supported due to" pat
  end.
Local Ltac iDestructHypFindPat Hgo pat found pats :=
  lazymatch pats with
  | [] =>
    lazymatch found with
    | true => pm_prettify
    | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
    end
  | ISimpl :: ?pats => simpl; iDestructHypFindPat Hgo pat found pats
  | IClear ?H :: ?pats => iClear H; iDestructHypFindPat Hgo pat found pats
  | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
  | ?pat1 :: ?pats =>
     lazymatch found with
     | false => iDestructHypGo Hgo pat pat1; iDestructHypFindPat Hgo pat true pats
     | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
     end
  end.

Ltac _iDestructHyp0 H pat :=
  let pats := intro_pat.parse pat in
  iDestructHypFindPat H pat false pats.
Ltac _iDestructHyp H xs pat :=
  ltac1_list_iter ltac:(fun x => iExistDestruct H as x H) xs;
  _iDestructHyp0 H pat.

Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
  _iDestructHyp0 H pat.

Ltac _iIntros_go pats startproof :=
  lazymatch pats with
  | [] =>
    lazymatch startproof with
    | true => iStartProof
    | false => idtac
    end

  | IPure (IGallinaNamed ?s) :: ?pats =>
     let i := fresh in
     iIntro (i);
     rename_by_string i s;
     _iIntros_go pats startproof
  | IPure IGallinaAnon :: ?pats => iIntro (?); _iIntros_go pats startproof
  | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; _iIntros_go pats false
  | IDrop :: ?pats => iIntro _; _iIntros_go pats startproof
  | IIdent ?H :: ?pats => iIntro H; _iIntros_go pats startproof

  | IPureIntro :: ?pats => iPureIntro; _iIntros_go pats false
  | IModalIntro :: ?pats => iModIntro; _iIntros_go pats false
  | IForall :: ?pats => repeat iIntroForall; _iIntros_go pats startproof
  | IAll :: ?pats => repeat (iIntroForall || iIntro); _iIntros_go pats startproof

  | ISimpl :: ?pats => simpl; _iIntros_go pats startproof
  | IClear ?H :: ?pats => iClear H; _iIntros_go pats false
  | IClearFrame ?H :: ?pats => iFrame H; _iIntros_go pats false
  | IDone :: ?pats => try done; _iIntros_go pats startproof

  | IIntuitionistic ?pat :: ?pats =>
     let H := iFresh in iIntro #H; iDestructHyp H as pat; _iIntros_go pats false
  | ?pat :: ?pats =>
     let H := iFresh in iIntro H; iDestructHyp H as pat; _iIntros_go pats false
  end.

Ltac _iIntros0 pat :=
  let pats := intro_pat.parse pat in

  lazymatch pats with
  | [] => idtac
  | _ => _iIntros_go pats true
  end.
Ltac _iIntros xs pat :=
  ltac1_list_iter ltac:(fun x => iIntro (x)) xs;
  _iIntros0 pat.
Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
  _iIntros xs pat.

Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
  let intro_destruct n :=
    let rec go n' :=
      lazymatch n' with
      | 0 => fail "iDestruct: cannot introduce" n "hypotheses"
      | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
      | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
      end in
    intros; go n in
  lazymatch type of lem with
  | nat => intro_destruct lem
  | Z =>

     let n := eval cbv in (Z.to_nat lem) in intro_destruct n
  | ident => tac lem
  | string => tac constr:(INamed lem)
  | _ => iPoseProofCore lem as p tac
  end.
Tactic Notation "iMod" open_constr(lem) "as" "(" ne_simple_intropattern_list(xs) ")"
    constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H as H; last _iDestructHyp H xs pat).

Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.

Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Admitted.
Global Hint Extern 0 (FromAssumption _ _ _) =>
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Admitted.
Global Hint Extern 0 (FromExist _ _) =>
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

Section class_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (⊢ P) P | 0.
Admitted.
Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Admitted.
Global Instance into_persistent_intuitionistically p P Q :
  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
Admitted.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Admitted.

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Admitted.

Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Admitted.

Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
Admitted.

Global Instance into_exist_exist {A} (Φ : A → PROP) name :
  AsIdentName Φ name → IntoExist (bi_exist Φ) Φ name.
Admitted.
End class_instances.

Section class_instances_updates.

Global Instance from_modal_bupd `{!BiBUpd PROP} P :
  FromModal True modality_id (|==> P) (|==> P) P.
Admitted.

Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Admitted.
End class_instances_updates.

Record agree (A : Type) : Type := {
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
}.
Global Arguments agree_car {_} _.
Definition to_agree {A} (a : A) : agree A.
Admitted.

Section agree.
Context {A : ofe}.
Local Instance agree_dist : Dist (agree A).
Admitted.
Local Instance agree_equiv : Equiv (agree A).
Admitted.

Definition agree_ofe_mixin : OfeMixin (agree A).
Admitted.
Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
Local Instance agree_validN_instance : ValidN (agree A).
Admitted.
Local Instance agree_valid_instance : Valid (agree A).
Admitted.

Local Program Instance agree_op_instance : Op (agree A) := λ x y,
  {| agree_car := agree_car x ++ agree_car y |}.
Admit Obligations.
Local Instance agree_pcore_instance : PCore (agree A).
Admitted.

Definition agree_cmra_mixin : CmraMixin (agree A).
Admitted.
Canonical Structure agreeR : cmra.
exact (Cmra (agree A) agree_cmra_mixin).
Defined.

End agree.
Global Arguments agreeR : clear implicits.

Notation frac := Qp (only parsing).
  Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac.
Admitted.
Local Instance frac_pcore_instance : PCore frac.
Admitted.
Local Instance frac_op_instance : Op frac.
Admitted.

  Definition frac_ra_mixin : RAMixin frac.
Admitted.
  Canonical Structure fracR := discreteR frac frac_ra_mixin.

Inductive dfrac :=
  | DfracOwn : Qp → dfrac
  | DfracDiscarded : dfrac
  | DfracBoth : Qp → dfrac.

Declare Custom Entry dfrac.
Notation "" := (DfracOwn 1) (in custom dfrac).

Structure view_rel (A : ofe) (B : ucmra) := ViewRel {
  view_rel_holds :> nat → A → B → Prop;
  view_rel_mono n1 n2 a1 a2 b1 b2 :
    view_rel_holds n1 a1 b1 →
    a1 ≡{n2}≡ a2 →
    b2 ≼{n2} b1 →
    n2 ≤ n1 →
    view_rel_holds n2 a2 b2;
  view_rel_validN n a b :
    view_rel_holds n a b → ✓{n} b;
  view_rel_unit n :
    ∃ a, view_rel_holds n a ε
}.
Global Arguments ViewRel {_ _} _ _.

Record view {A B} (rel : nat → A → B → Prop) :=
  View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.

Section ofe.
  Context {A B : ofe} (rel : nat → A → B → Prop).
Local Instance view_equiv : Equiv (view rel).
Admitted.
Local Instance view_dist : Dist (view rel).
Admitted.

  Definition view_ofe_mixin : OfeMixin (view rel).
Admitted.
  Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
End ofe.

Section cmra.
  Context {A B} (rel : view_rel A B).
Local Instance view_valid_instance : Valid (view rel).
Admitted.
Local Instance view_validN_instance : ValidN (view rel).
Admitted.
Local Instance view_pcore_instance : PCore (view rel).
Admitted.
Local Instance view_op_instance : Op (view rel).
Admitted.

  Lemma view_cmra_mixin : CmraMixin (view rel).
Admitted.
  Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Local Instance view_empty_instance : Unit (view rel).
Admitted.
  Lemma view_ucmra_mixin : UcmraMixin (view rel).
Admitted.
  Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.

End cmra.
Definition viewO_map {A A' B B' : ofe}
    {rel : nat → A → B → Prop} {rel' : nat → A' → B' → Prop}
    (f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel'.
Admitted.
Definition auth_view_rel_raw {A : ucmra} (n : nat) (a b : A) : Prop.
Admitted.
Lemma auth_view_rel_raw_mono (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
  auth_view_rel_raw n1 a1 b1 →
  a1 ≡{n2}≡ a2 →
  b2 ≼{n2} b1 →
  n2 ≤ n1 →
  auth_view_rel_raw n2 a2 b2.
Admitted.
Lemma auth_view_rel_raw_valid (A : ucmra) n (a b : A) :
  auth_view_rel_raw n a b → ✓{n} b.
Admitted.
Lemma auth_view_rel_raw_unit (A : ucmra) n :
  ∃ a : A, auth_view_rel_raw n a ε.
Admitted.
Canonical Structure auth_view_rel {A : ucmra} : view_rel A A.
exact (ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
          (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A)).
Defined.

Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
Definition authR (A : ucmra) : cmra.
exact (viewR (A:=A) (B:=A) auth_view_rel).
Defined.
Definition authUR (A : ucmra) : ucmra.
exact (viewUR (A:=A) (B:=A) auth_view_rel).
Defined.
Definition auth_auth {A: ucmra} : dfrac → A → auth A.
Admitted.
Definition auth_frag {A: ucmra} : A → auth A.
Admitted.

Notation "● dq a" := (auth_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "● dq  a").
Notation "◯ a" := (auth_frag a) (at level 20).

Program Definition authURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Admit Obligations.

Program Definition authRF (F : urFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Solve Obligations with apply authURF.

Record uPred (M : ucmra) : Type := UPred {
  uPred_holds : nat → M → Prop;

  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.

Local Coercion uPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred.

Section cofe.
  Context {M : ucmra}.
Local Instance uPred_equiv : Equiv (uPred M).
Admitted.
Local Instance uPred_dist : Dist (uPred M).
Admitted.
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
Admitted.
Canonical Structure uPredO : ofe.
exact (Ofe (uPred M) uPred_ofe_mixin).
Defined.

  Program Definition uPred_compl : Compl uPredO := λ c,
    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
Admit Obligations.
  Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
Admit Obligations.
End cofe.
Global Arguments uPredO : clear implicits.

Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
Global Hint Resolve uPred_mono : uPred_def.

Local Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x := φ |}.
Solve Obligations with done.
Local Definition uPred_pure_aux : seal (@uPred_pure_def).
Admitted.
Definition uPred_pure := uPred_pure_aux.(unseal).
Global Arguments uPred_pure {M}.

Local Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x ∧ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_and_aux : seal (@uPred_and_def).
Admitted.
Definition uPred_and := uPred_and_aux.(unseal).
Global Arguments uPred_and {M}.

Local Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x ∨ Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_or_aux : seal (@uPred_or_def).
Admitted.
Definition uPred_or := uPred_or_aux.(unseal).
Global Arguments uPred_or {M}.

Local Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Admit Obligations.
Local Definition uPred_impl_aux : seal (@uPred_impl_def).
Admitted.
Definition uPred_impl := uPred_impl_aux.(unseal).
Global Arguments uPred_impl {M}.

Local Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
  {| uPred_holds n x := ∀ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_forall_aux : seal (@uPred_forall_def).
Admitted.
Definition uPred_forall := uPred_forall_aux.(unseal).

Local Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
  {| uPred_holds n x := ∃ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Local Definition uPred_exist_aux : seal (@uPred_exist_def).
Admitted.
Definition uPred_exist := uPred_exist_aux.(unseal).

Local Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Admit Obligations.
Local Definition uPred_sep_aux : seal (@uPred_sep_def).
Admitted.
Definition uPred_sep := uPred_sep_aux.(unseal).
Global Arguments uPred_sep {M}.

Local Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Admit Obligations.
Local Definition uPred_wand_aux : seal (@uPred_wand_def).
Admitted.
Definition uPred_wand := uPred_wand_aux.(unseal).
Global Arguments uPred_wand {M}.

Local Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.

Local Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (core x) |}.
Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
Local Definition uPred_persistently_aux : seal (@uPred_persistently_def).
Admitted.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
Global Arguments uPred_persistently {M}.

Local Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Admit Obligations.
Local Definition uPred_later_aux : seal (@uPred_later_def).
Admitted.
Definition uPred_later := uPred_later_aux.(unseal).
Global Arguments uPred_later {M}.
Definition uPred_emp {M} : uPred M.
Admitted.

Lemma uPred_bi_mixin (M : ucmra) :
  BiMixin
    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
Admitted.

Lemma uPred_bi_persistently_mixin (M : ucmra) :
  BiPersistentlyMixin
    uPred_entails uPred_emp uPred_and
    (@uPred_exist M) uPred_sep uPred_persistently.
Admitted.

Lemma uPred_bi_later_mixin (M : ucmra) :
  BiLaterMixin
    uPred_entails uPred_pure uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
Admitted.
Canonical Structure uPredI (M : ucmra) : bi.
exact ({| bi_ofe_mixin := ofe_mixin_of (uPred M);
     bi_bi_mixin := uPred_bi_mixin M;
     bi_bi_later_mixin := uPred_bi_later_mixin M;
     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}).
Defined.
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M).
Admitted.

Structure gFunctor := GFunctor {
  gFunctor_F :> rFunctor;
  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.

Record gFunctors := GFunctors {
  gFunctors_len : nat;
  gFunctors_lookup : fin gFunctors_len → gFunctor
}.

Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).

Definition gname := positive.
Definition iResUR (Σ : gFunctors) : ucmra.
Admitted.
  Notation iProp Σ := (uPred (iResUR Σ)).
  Notation iPropO Σ := (uPredO (iResUR Σ)).

Class inG (Σ : gFunctors) (A : cmra) := InG {
  inG_id : gid Σ;
  inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
  inG_prf : A = inG_apply (iPropO Σ) _;
}.
Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ.
Admitted.
Local Definition own_aux : seal (@own_def).
Admitted.
Definition own := own_aux.(unseal).
Global Arguments own {Σ A _} γ a.

Section cmra_mlist.

  Context (A: Type) `{EqDecision A}.
  Implicit Types (D: list A).

  Inductive mlist :=
    | MList D : mlist
    | MListBot : mlist.

  Inductive mlist_equiv : Equiv mlist :=
    | MList_equiv D1 D2:
        D1 = D2 → MList D1 ≡ MList D2
    | MListBot_equiv : MListBot ≡ MListBot.

  Existing Instance mlist_equiv.
  Local Instance mlist_equiv_Equivalence : @Equivalence mlist equiv.
Admitted.
Canonical Structure mlistC : ofe.
exact (discreteO mlist).
Defined.
Local Instance mlist_valid : Valid mlist.
Admitted.
Local Instance mlist_op : Op mlist.
Admitted.
Local Instance mlist_PCore : PCore mlist.
Admitted.
Local Instance mlist_unit : Unit mlist.
Admitted.

  Definition mlist_ra_mixin : RAMixin mlist.
Admitted.

  Canonical Structure mlistR := discreteR mlist mlist_ra_mixin.

  Definition mlist_ucmra_mixin : UcmraMixin mlist.
Admitted.

  Canonical Structure mlistUR :=
    Ucmra mlist mlist_ucmra_mixin.

End cmra_mlist.

Global Arguments MList {_} _.

Definition fmlistUR (A: Type) {Heq: EqDecision A} := authUR (mlistUR A).
Class fmlistG (A: Type) {Heq: EqDecision A} Σ :=
  { #[global] fmlist_inG :: inG Σ (fmlistUR A) }.

Section fmlist_props.
Context `{fmlistG A Σ}.
Definition fmlist_lb γ l := own γ (◯ (MList l)).
Definition fmlist_idx γ i a := (∃ l, ⌜ l !! i = Some a ⌝ ∗ fmlist_lb γ l)%I.

End fmlist_props.
Local Instance nat_valid_instance : Valid nat.
Admitted.
Local Instance nat_pcore_instance : PCore nat.
Admitted.
Local Instance nat_op_instance : Op nat.
Admitted.
  Lemma nat_ra_mixin : RAMixin nat.
Admitted.
Canonical Structure natR : cmra.
exact (discreteR nat nat_ra_mixin).
Defined.
Local Instance nat_unit_instance : Unit nat.
Admitted.
  Lemma nat_ucmra_mixin : UcmraMixin nat.
Admitted.
Canonical Structure natUR : ucmra.
exact (Ucmra nat nat_ucmra_mixin).
Defined.

Class lcGpreS (Σ : gFunctors) := LcGpreS {
  #[local] lcGpreS_inG :: inG Σ (authR natUR)
}.

Class lcGS (Σ : gFunctors) := LcGS {
  #[local] lcGS_inG :: inG Σ (authR natUR);
  lcGS_name : gname;
}.
Import iris.algebra.coPset.

Inductive bi_schema :=
| bi_sch_emp : bi_schema
| bi_sch_pure : Prop → bi_schema
| bi_sch_and : bi_schema → bi_schema → bi_schema
| bi_sch_or : bi_schema → bi_schema → bi_schema
| bi_sch_forall : ∀ A, (A → bi_schema) → bi_schema
| bi_sch_exist : ∀ A, (A → bi_schema) → bi_schema
| bi_sch_sep : bi_schema → bi_schema → bi_schema
| bi_sch_wand : bi_schema → bi_schema → bi_schema
| bi_sch_persistently : bi_schema → bi_schema
| bi_sch_later : bi_schema → bi_schema
| bi_sch_bupd : bi_schema → bi_schema

| bi_sch_var_fixed : nat → bi_schema
| bi_sch_var_mut : nat → bi_schema
| bi_sch_wsat : bi_schema
| bi_sch_ownE : (nat → coPset) → bi_schema.

Canonical Structure bi_schemaO := leibnizO bi_schema.

Record invariant_level_names := { invariant_name : gname; }.

Global Instance invariant_level_names_eq_dec : EqDecision (invariant_level_names).
Admitted.
  Class invGpreS (Σ : gFunctors) : Set := WsatPreG {
    #[global] inv_inPreG :: inG Σ (authR (gmapUR positive
                                    (prodR (agreeR (prodO (listO (laterO (iPropO Σ))) bi_schemaO))
                                           (optionR (prodR fracR (agreeR (listO (laterO (iPropO Σ)))))))));
    #[global] enabled_inPreG :: inG Σ coPset_disjR;
    #[global] disabled_inPreG :: inG Σ (gset_disjR positive);
    #[global] mlist_inPreG :: fmlistG (invariant_level_names) Σ;
    inv_lcPreG : lcGpreS Σ;
  }.

  Class invGS (Σ : gFunctors) : Set := WsatG {
    #[global] inv_inG :: invGpreS Σ;
    #[global] invGS_lc :: lcGS Σ;
    inv_list_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.

Definition invariant_unfold {Σ} {n} sch (Ps : vec (iProp Σ) n) : agree (list (later (iPropO Σ)) * bi_schema) :=
  to_agree ((λ P, Next P) <$> (vec_to_list Ps), sch).
Definition inv_mut_unfold {Σ} {n} q (Ps : vec (iProp Σ) n) : option (frac * (agree (list (later (iPropO Σ))))) :=
  Some (q%Qp, to_agree ((λ P, Next P) <$> (vec_to_list Ps))).
Definition ownI `{!invGS Σ} {n} (lvl: nat) (i : positive) (sch: bi_schema) (Ps : vec (iProp Σ) n) : iProp Σ :=
  (∃ γs, fmlist_idx inv_list_name lvl γs ∗
         own (invariant_name γs) (◯ {[ i := (invariant_unfold sch Ps, ε) ]})).

Definition ownI_mut `{!invGS Σ} {n} (lvl: nat) (i : positive) q (Qs : vec (iProp Σ) n) : iProp Σ :=
  (∃ (l: agree (list (later (iPropO Σ)) * bi_schema)) γs, fmlist_idx inv_list_name lvl γs ∗
         own (invariant_name γs) (◯ {[ i := (l, inv_mut_unfold q Qs) ]})).
Definition ownE `{!invGS Σ} (E : coPset) : iProp Σ.
Admitted.
Definition ownD `{!invGS Σ} (E : gset positive) : iProp Σ.
Admitted.

Definition inv_cmra_fmap `{!invGS Σ} (v: (list (iProp Σ) * bi_schema) * list (iProp Σ)) :=
  let '((Ps, sch), Qs) := v in
  (invariant_unfold sch (list_to_vec Ps), inv_mut_unfold 1%Qp (list_to_vec Qs)).

Fixpoint bi_schema_pre `{!invGS Σ} n (Ps Ps_mut: list (iProp Σ)) wsat (sch: bi_schema) :=
  match sch with
  | bi_sch_emp => emp
  | bi_sch_pure φ => ⌜φ⌝
  | bi_sch_and sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∧ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_or sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∨ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_forall A sch => ∀ (a: A),  bi_schema_pre n Ps Ps_mut wsat (sch a)
  | bi_sch_exist A sch => ∃ (a: A),  bi_schema_pre n Ps Ps_mut wsat (sch a)
  | bi_sch_sep sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 ∗ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_wand sch1 sch2 => bi_schema_pre n Ps Ps_mut wsat sch1 -∗ bi_schema_pre n Ps Ps_mut wsat sch2
  | bi_sch_persistently sch => <pers> bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_later sch => ▷ bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_bupd sch => |==> bi_schema_pre n Ps Ps_mut wsat sch
  | bi_sch_var_fixed i =>
    match (Ps !! i) with
    | None => emp
    | Some P => P
    end
  | bi_sch_var_mut i =>
    match (Ps_mut !! i) with
    | None => emp
    | Some P => P
    end
  | bi_sch_wsat => wsat
  | bi_sch_ownE E => ownE (E n)
  end%I.

Definition wsat_pre `{!invGS Σ} n bi_schema_interp :=
  (∃ I : gmap positive ((list (iProp Σ) * bi_schema) * list (iProp Σ)),
        (∃ γs, fmlist_idx inv_list_name n γs ∗
             own (invariant_name γs) (● (inv_cmra_fmap <$> I : gmap _ _))) ∗
        [∗ map] i ↦ Qs ∈ I, (bi_schema_interp (bi_later <$> Qs.1.1) (bi_later <$> Qs.2) Qs.1.2 ∗
                             ownI_mut n i (1/2)%Qp (list_to_vec Qs.2) ∗
                             ownD {[i]}) ∨
                            ownE {[i]})%I.

Fixpoint bi_schema_interp `{!invGS Σ} n (Ps Ps_mut: list (iProp Σ)) sch {struct n} :=
  match n with
  | O => bi_schema_pre O Ps Ps_mut True%I sch
  | S n' => bi_schema_pre (S n') Ps Ps_mut (wsat_pre n' (bi_schema_interp n') ∗ wsat n')%I sch
  end
  with
  wsat `{!invGS Σ} n :=
  match n with
    | S n =>
  (∃ I : gmap positive ((list (iProp Σ) * bi_schema) * list (iProp Σ)),
        (∃ γs, fmlist_idx inv_list_name n γs ∗
             own (invariant_name γs) (● (inv_cmra_fmap <$> I : gmap _ _))) ∗
        [∗ map] i ↦ Qs ∈ I, (bi_schema_interp n (bi_later <$> Qs.1.1) (bi_later <$> Qs.2) Qs.1.2 ∗
                             ownI_mut n i (1/2)%Qp (list_to_vec Qs.2) ∗
                             ownD {[i]}) ∨
                            ownE {[i]})
    ∗ wsat n
    | O => True
  end%I.

Section wsat.
Context `{!invGS Σ}.

Lemma ownI_alloc {n m} φ sch lvl (Ps: vec _ n) (Ps_mut: vec _ m):
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat (S lvl) ∗
  bi_schema_interp lvl (bi_later <$> (vec_to_list Ps)) (bi_later <$> (vec_to_list Ps_mut)) sch ==∗
  ∃ i, ⌜φ i⌝ ∗ wsat (S lvl) ∗ ownI lvl i sch Ps ∗ ownI_mut lvl i (1/2)%Qp Ps_mut.
Admitted.

End wsat.

Section schema_test_mut.
Context `{!invGS Σ}.
Definition bi_sch_bupd_factory (Q P: bi_schema) : bi_schema.
Admitted.

Definition ownI_full_bupd_factory lvl i q Q P :=
  (∃ n (Qs: vec _ n), ownI lvl i (bi_sch_bupd_factory (bi_sch_var_mut O) (bi_sch_var_fixed O)) (list_to_vec [P]) ∗
   ownI_mut lvl i q Qs ∗ ⌜ default True%I (vec_to_list Qs !! 0) = Q ⌝)%I.

Lemma ownI_bupd_factory_alloc lvl φ Q P :
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat (S lvl) ∗ (▷ Q ∗ □ (▷ Q ==∗ ▷ Q ∗ ▷ P))
       ==∗ ∃ i, ⌜φ i⌝ ∗ wsat (S lvl) ∗ ownI_full_bupd_factory lvl i (1/2)%Qp Q P.
Proof.
  iIntros (?) "(Hw&(HQ&#Hfactory))".
iMod (ownI_alloc with "[$Hw HQ]") as (i) "(?&?&?&?)"; eauto; last first.
  {
 iModIntro.
iExists i.
iFrame.
instantiate (1:= list_to_vec [Q]).
rewrite //=.
}
  repeat (rewrite ?bi_schema_interp_unfold //=).

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-ssr-search-moved" "-w" "+deprecated-instance-without-locality" "-w" "+ambiguous-paths" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-deprecated-field-instance-without-locality" "-w" "+deprecated-tactic-notation" "-w" "-deprecated-since-8.19" "-w" "-deprecated-since-8.20" "-w" "-deprecated-from-Coq" "-w" "-deprecated-dirpath-Coq" "-w" "-notation-incompatible-prefix" "-w" "-deprecated-typeclasses-transparency-without-locality" "-w" "-notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/src" "Perennial" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp" "stdpp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_unstable" "stdpp.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_bitvector" "stdpp.bitvector" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/Goose" "Goose" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/record-update/src" "RecordUpdate" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coq-tactical/src" "Tactical" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris-named-props/src" "iris_named_props" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_trusted_code" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_code_axioms" "New.code" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new_partial_axioms" "New.code_axioms" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/new" "New" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1066 lines to 167 lines, then from 180 lines to 368 lines, then from 373 lines to 168 lines, then from 181 lines to 855 lines, then from 857 lines to 177 lines, then from 190 lines to 549 lines, then from 554 lines to 194 lines, then from 207 lines to 743 lines, then from 748 lines to 248 lines, then from 261 lines to 446 lines, then from 451 lines to 249 lines, then from 262 lines to 842 lines, then from 847 lines to 260 lines, then from 273 lines to 624 lines, then from 624 lines to 278 lines, then from 291 lines to 478 lines, then from 483 lines to 279 lines, then from 292 lines to 558 lines, then from 563 lines to 279 lines, then from 292 lines to 689 lines, then from 694 lines to 309 lines, then from 322 lines to 1312 lines, then from 1316 lines to 426 lines, then from 439 lines to 919 lines, then from 924 lines to 474 lines, then from 487 lines to 1254 lines, then from 1259 lines to 659 lines, then from 660 lines to 533 lines, then from 546 lines to 841 lines, then from 846 lines to 542 lines, then from 555 lines to 674 lines, then from 679 lines to 553 lines, then from 566 lines to 969 lines, then from 974 lines to 588 lines, then from 601 lines to 766 lines, then from 771 lines to 587 lines, then from 600 lines to 772 lines, then from 777 lines to 589 lines, then from 602 lines to 962 lines, then from 967 lines to 603 lines, then from 616 lines to 1930 lines, then from 1935 lines to 642 lines, then from 655 lines to 2993 lines, then from 2998 lines to 1687 lines, then from 1700 lines to 3137 lines, then from 3142 lines to 2116 lines, then from 2113 lines to 2095 lines, then from 2108 lines to 2312 lines, then from 2317 lines to 2128 lines, then from 2141 lines to 3107 lines, then from 3112 lines to 2290 lines, then from 2303 lines to 2595 lines, then from 2600 lines to 2456 lines, then from 2469 lines to 2615 lines, then from 2620 lines to 2482 lines, then from 2495 lines to 2697 lines, then from 2702 lines to 2566 lines, then from 2579 lines to 2772 lines, then from 2777 lines to 2812 lines, then from 2813 lines to 2659 lines, then from 2672 lines to 2841 lines, then from 2846 lines to 2719 lines, then from 2732 lines to 2821 lines, then from 2826 lines to 2723 lines, then from 2736 lines to 3351 lines, then from 3356 lines to 3168 lines, then from 3151 lines to 2792 lines, then from 2805 lines to 3604 lines, then from 3608 lines to 3348 lines, then from 3321 lines to 2867 lines, then from 2880 lines to 3175 lines, then from 3180 lines to 2909 lines, then from 2922 lines to 3120 lines, then from 3125 lines to 2914 lines, then from 2927 lines to 3193 lines, then from 3198 lines to 2974 lines, then from 2987 lines to 3042 lines, then from 3047 lines to 3001 lines, then from 3011 lines to 2993 lines, then from 3006 lines to 3655 lines, then from 3660 lines to 2996 lines, then from 3009 lines to 3093 lines, then from 3099 lines to 3005 lines, then from 3019 lines to 3684 lines, then from 3690 lines to 3015 lines, then from 3029 lines to 3058 lines, then from 3064 lines to 3021 lines, then from 3035 lines to 3069 lines, then from 3075 lines to 3028 lines, then from 3042 lines to 3070 lines, then from 3076 lines to 3073 lines, then from 3075 lines to 3036 lines, then from 3049 lines to 3118 lines, then from 3124 lines to 3057 lines, then from 3071 lines to 3261 lines, then from 3267 lines to 3065 lines, then from 3079 lines to 3341 lines, then from 3347 lines to 3122 lines, then from 3136 lines to 3421 lines,