phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/stepindex.v *)
Instance le_total : Total (≤).
Proof. intros n m. destruct (trichotomy (<) n m); naive_solver. Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_le_trans n m p : n < m → m ≤ p → n < p.
Proof. intros ? [| ->]%le_lteq; [|done]. by trans m. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_lt_trans n m p : n ≤ m → m < p → n < p.
Proof. intros [| ->]%le_lteq ?; [|done]. by trans m. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_succ_l n m : Sᵢ n ≤ m ↔ n < m.
Proof.
    split; [|apply le_succ_l_2].
    intros. eapply lt_le_trans; [|done]. apply lt_succ_diag_r.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_succ_r n m : n < Sᵢ m ↔ n ≤ m.
Proof.
    split.
    - intros. destruct (total (≤) n m) as [|[H1| ->]%le_lteq]; eauto.
      destruct (irreflexivity (<) n). eapply lt_le_trans; [done|].
      by apply le_succ_l.
    - intros. eapply le_lt_trans; [done|]. apply lt_succ_diag_r.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma succ_le_mono n m : n ≤ m ↔ Sᵢ n ≤ Sᵢ m.
Proof. by rewrite le_succ_l lt_succ_r. Qed.
(* iris/algebra/stepindex.v *)
Lemma succ_lt_mono n m : n < m ↔ Sᵢ n < Sᵢ m.
Proof. by rewrite lt_succ_r le_succ_l. Qed.
(* iris/algebra/stepindex.v *)
Instance succ_inj : Inj (=) (=) Sᵢ.
Proof.
    intros n m Heq.
    apply (anti_symm (≤)); apply succ_le_mono; by rewrite Heq.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma le_succ_diag_r n : n ≤ Sᵢ n.
Proof. apply lt_le_incl, lt_succ_diag_r. Qed.
(* iris/algebra/stepindex.v *)
Lemma neq_0_lt_0 n : n ≠ 0ᵢ ↔ 0ᵢ < n.
Proof.
    split.
    - destruct (trichotomy (<) 0ᵢ n) as [|[|?%nlt_0_r]]; naive_solver.
    - intros ? ->. by destruct (nlt_0_r 0ᵢ).
  Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_ge_cases n m : n < m ∨ m ≤ n.
Proof.
    destruct (trichotomyT (<) n m) as [[| ->]|]; auto using lt_le_incl.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma le_gt_cases n m : n ≤ m ∨ m < n.
Proof. destruct (lt_ge_cases m n); auto. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_ngt n m : n ≤ m ↔ ¬ m < n.
Proof.
    split.
    - intros ??. apply (irreflexivity (<) n); eauto using le_lt_trans.
    - intros ?. by destruct (lt_ge_cases m n).
  Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_nge n m : n < m ↔ ¬ m ≤ n.
Proof.
    split.
    - intros ??. apply (irreflexivity (<) n); eauto using lt_le_trans.
    - intros ?. by destruct (le_gt_cases m n).
  Qed.
(* iris/algebra/stepindex.v *)
Lemma le_neq n m : n < m ↔ n ≤ m ∧ n ≠ m.
Proof.
    split.
    - intros. split; [eauto using lt_le_incl|].
      intros ->. by apply (irreflexivity (<) m).
    - intros [? Heq]. apply lt_nge=> ?. by apply Heq, (anti_symm (≤)).
  Qed.
(* iris/algebra/stepindex.v *)
Lemma nlt_succ_r n m : ¬ m < Sᵢ n ↔ n < m.
Proof. by rewrite -le_ngt le_succ_l. Qed.
(* iris/algebra/stepindex.v *)
(* These instances have a very high cost, so that the default instances for
  [nat] are prefered over these ones in case of finite step indexing. *)
Instance eq_dec : EqDecision SI | 1000.
Proof.
    intros n m. destruct (trichotomyT (<) n m) as [[H| ->]|H].
    - right. intros ->. by apply (irreflexivity (<) m).
    - by left.
    - right. intros ->. by apply (irreflexivity (<) m).
  Qed.
(* iris/algebra/stepindex.v *)
Instance lt_dec : RelDecision (<) | 1000.
Proof. apply _. Defined.
(* iris/algebra/stepindex.v *)
Instance le_dec : RelDecision (≤) | 1000.
Proof.
    intros n m. destruct (trichotomyT (<) n m) as [[| ->]|]; [left; by auto..|].
    right. intro. destruct (irreflexivity (<) n); eauto using le_lt_trans.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma le_0_l n : 0ᵢ ≤ n.
Proof. apply le_ngt, nlt_0_r. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_0_r n : n ≤ 0ᵢ ↔ n = 0ᵢ.
Proof. split; [|by intros ->]. intros. by apply (anti_symm (≤)), le_0_l. Qed.
(* iris/algebra/stepindex.v *)
Lemma neq_succ_0 n : Sᵢ n ≠ 0ᵢ.
Proof. apply neq_0_lt_0, lt_succ_r, le_0_l. Qed.
(* iris/algebra/stepindex.v *)
Lemma succ_neq n : n ≠ Sᵢ n.
Proof.
    intros Hn. destruct (irreflexivity (<) n). rewrite {2}Hn.
    apply lt_succ_diag_r.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma limit_0 : ¬limit 0ᵢ.
Proof. by intros [? []]. Qed.
(* iris/algebra/stepindex.v *)
Lemma limit_lt_0 n : limit n → 0ᵢ < n.
Proof. intros. apply neq_0_lt_0; intros ->. by apply limit_0. Qed.
(* iris/algebra/stepindex.v *)
Lemma limit_S n : ¬limit (Sᵢ n).
Proof.
    intros [Hlim _]. apply (irreflexivity (<) (Sᵢ n)), Hlim, lt_succ_diag_r.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma limit_finite `{!SIdxFinite SI} n : ¬limit n.
Proof.
    destruct (finite_index n) as [->|[m ->]]; auto using limit_0, limit_S.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma case n : (n = 0ᵢ) + { m | n = Sᵢ m } + limit n.
Proof.
    destruct (decide (n = 0ᵢ)); [by auto|].
    destruct (weak_case n); by auto using limit.
  Qed.
(* iris/algebra/stepindex.v *)
(* We define the standard recursion scheme for ordinal induction (i.e.,
  transfinite induction) [rec] with the right "unfolding" lemmas:

    P 0 →
    (∀ i, P i → P (Sᵢ i)) →
    (∀ i, limit i, (∀ j, j < i → P j) → P i) →
    ∀ i, P i *)
Lemma lt_succ_diag_r' n m : n = Sᵢ m → m < n.
Proof. intros ->. apply lt_succ_diag_r. Qed.
(* iris/algebra/stepindex.v *)
Definition rec (P : SI → Type)
      (s : P 0ᵢ)
      (f : ∀ n, P n → P (Sᵢ n))
      (lim : ∀ n, limit n → (∀ m, m < n → P m) → P n) :
      ∀ n, P n
:=
    Fix lt_wf _ $ λ n IH,
      match case n with
      | inl (inl EQ) => eq_rect_r P s EQ
      | inl (inr (m ↾ EQ)) => eq_rect_r P (f m (IH m (lt_succ_diag_r' _ _ EQ))) EQ
      | inr Hlim => lim n Hlim IH
      end.
(* iris/algebra/stepindex.v *)
Definition rec_lim_ext {P : SI → Type}
      (lim : ∀ n, limit n → (∀ m, m < n → P m) → P n)
:=
    ∀ n Hn Hn' f g,
      (∀ m Hm, f m Hm = g m Hm) →
      lim n Hn f = lim n Hn' g.
(* iris/algebra/stepindex.v *)
Lemma rec_unfold P s f lim n :
    rec_lim_ext lim →
    rec P s f lim n =
      match case n with
      | inl (inl EQ) => eq_rect_r P s EQ
      | inl (inr (m ↾ EQ)) => eq_rect_r P (f m (rec P s f lim m)) EQ
      | inr Hlim => lim n Hlim (λ m _, rec P s f lim m)
      end.
Proof.
    intros Hext. unfold rec at 1. apply Fix_eq=> m g h EQ.
    destruct (case m) as [[?|[m' ->]]|?]; [done| |by auto].
    rewrite /eq_rect_r /= EQ //.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma rec_zero P s f lim : rec P s f lim 0ᵢ = s.
Proof.
    rewrite /rec /Fix. destruct (lt_wf 0ᵢ); simpl.
    destruct (case 0ᵢ) as [[H0|[m ?]]|?].
    - by rewrite (proof_irrel H0 (eq_refl _)).
    - by destruct (neq_succ_0 m).
    - by destruct limit_0.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma rec_succ P s f lim n :
    rec_lim_ext lim →
    rec P s f lim (Sᵢ n) = f n (rec P s f lim n).
Proof.
    intros Hext. rewrite rec_unfold //.
    destruct (case _) as [[?|[m Hm]]|?].
    - by destruct (neq_succ_0 n).
    - apply (inj _) in Hm as Hm'; subst. by rewrite (proof_irrel Hm (eq_refl _)).
    - by destruct (limit_S n).
  Qed.
(* iris/algebra/stepindex.v *)
Lemma rec_lim P s f lim n Hn :
    rec_lim_ext lim →
    rec P s f lim n = lim n Hn (λ m _, rec P s f lim m).
Proof.
    intros Hext. rewrite rec_unfold //.
    destruct (case _) as [[->|[m ->]]|[Hlim H0]].
    - by destruct limit_0.
    - by destruct (limit_S m).
    - by apply Hext.
  Qed.
(* iris/algebra/stepindex_finite.v *)
(* This file provides an instantiation of the [sidx] stepindex type for [nat],
which is the stepindex type traditionally used by Iris.

Side-effect: every development importing this file will automatically use finite
indices due to the declared instances and canonical structures for [sidx]. *)
Lemma nat_sidx_mixin : SIdxMixin lt le 0 S.
Proof.
  constructor; try lia.
  - apply _.
  - exact lt_wf.
  - intros m n. destruct (lt_eq_lt_dec m n); naive_solver.
  - intros [|n]; eauto with lia.
Qed.
(* iris/algebra/stepindex_finite.v *)
(* This declares the globally used index type to be [natSI]. All following
lemmas are implicitly specialized to [natSI]! *)
Canonical natSI : sidx
:= SIdx nat nat_sidx_mixin.
(* iris/algebra/stepindex_finite.v *)
Instance nat_sidx_finite : SIdxFinite natSI.
Proof. intros [|n]; eauto. Qed.
(* iris/algebra/stepindex_finite.v *)
(* Variants of lemmas with [S] and [≤] that use the definitions on [nat]
  directly. These are convenient in combination with [lia], which does not
  unfold the projections of the [sidx] class. *)
Lemma dist_later_S {A : ofe} (n : nat) (a b : A) :
    a ≡{n}≡ b ↔ dist_later (S n) a b.
Proof. apply dist_later_S. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma dist_S {A : ofe} n (x y : A) : x ≡{S n}≡ y → x ≡{n}≡ y.
Proof. apply dist_S. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma dist_le {A : ofe} (n m : nat) (x y : A) :
    x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y.
Proof. by apply dist_le. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma contractive_S {A B : ofe} (f : A → B) `{!Contractive f} (n : nat) x y :
    x ≡{n}≡ y → f x ≡{S n}≡ f y.
Proof. by apply contractive_S. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma conv_compl_S `{!Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
Proof. apply conv_compl_S. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma cmra_validN_S {A : cmra} n (x : A) : ✓{S n} x → ✓{n} x.
Proof. intros ?. by eapply cmra_validN_lt, SIdx.lt_succ_diag_r. Qed.
(* iris/algebra/stepindex_finite.v *)
Lemma cmra_includedN_S {A : cmra} n (x y : A) : x ≼{S n} y → x ≼{n} y.
Proof. apply cmra_includedN_S. Qed.
(* iris/algebra/stepindex_finite.v *)
(* We define [dist_later_fin], an equivalent (see dist_later_fin_iff) version
  of [dist_later] that uses a [match] on the step-index instead of the
  quantification over smaller step-indicies. The definition of [dist_later_fin]
  matches how [dist_later] used to be defined (i.e., with a [match] on the
  step-index), so [dist_later_fin] simplifies adapting existing Iris
  developments that used to rely on the reduction behavior of [dist_later].

  The "fin" indicates that when, in the future, the step-index is abstracted away,
  this equivalence will only hold for finite step-indices (as in, ordinals without
  "limit" steps such as natural numbers). *)
Definition dist_later_fin {A : ofe} (n : nat) (x y : A)
:=
    match n with 0 => True | S n => x ≡{n}≡ y end.
(* iris/algebra/stepindex_finite.v *)
Lemma dist_later_fin_iff {A : ofe} (n : nat) (x y : A):
    dist_later n x y ↔ dist_later_fin n x y.
Proof.
    destruct n; unfold dist_later_fin; first by split; eauto using dist_later_0.
    by rewrite dist_later_S.
  Qed.
(* iris/algebra/stepindex_finite.v *)
(* Shorthand for defining OFEs that only work for [natSI] *)
Lemma ofe_mixin_finite A `{!Equiv A, !Dist A} :
    (∀ x y : A, x ≡ y ↔ ∀ n, x ≡{n}≡ y) →
    (∀ n, Equivalence (@dist natSI A _ n)) →
    (∀ n (x y : A), x ≡{S n}≡ y → x ≡{n}≡ y) → (* [S] instead of [<] *)
    OfeMixin A.
Proof.
    intros; split; [done..|].
    intros n m x y Heq Hlt. induction Hlt; eauto.
  Qed.
(* iris/algebra/stepindex_finite.v *)
(* Shorthand for defining COFEs that only work for [natSI] *)
Definition cofe_finite {A} (compl : Compl A)
      (conv_compl: ∀ n c, compl c ≡{n}≡ c n) : Cofe A :=
    {| compl := compl; lbcompl n Hn := False_rect _ (SIdx.limit_finite _ Hn) |}.
Next Obligation. auto. Qed.
(* iris/algebra/stepindex_finite.v *)
(* For the goal [dist_later n x y], the tactic [dist_later_fin_intro] changes
the goal to [dist_later_fin] and takes care of the case where [n=0], such
that we are only left with the case where [n = S n'] for some [n']. Changing
[dist_later] to [dist_later_fin] enables reduction and thus works better with
custom versions of [dist] as used e.g. by LambdaRust. *)
Ltac dist_later_fin_intro
:=
  match goal with
  | |- @dist_later _ ?A _ ?n ?x ?y =>
      apply dist_later_fin_iff;
      destruct n as [|n]; [exact I|change (@dist natSI A _ n x y)]
  end.
(* iris/algebra/sts.v *)
Structure stsT
:= Sts {
  state : Type;
  token : Type;
  prim_step : relation state;
  tok : state → propset token;
}.
(* iris/algebra/sts.v *)
Notation states sts
:= (propset (state sts)).
(* iris/algebra/sts.v *)
Notation tokens sts
:= (propset (token sts)).
(* iris/algebra/sts.v *)
(* ** Step relations *)
Inductive step : relation (state sts * tokens sts)
:=
  | Step s1 s2 T1 T2 :
     prim_step s1 s2 → tok s1 ## T1 → tok s2 ## T2 →
     tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
(* iris/algebra/sts.v *)
Notation steps
:= (rtc step).
(* iris/algebra/sts.v *)
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop
:=
  (* Possible alternative definition: (tok s2) ## T) ∧ s \rightarrow s'.
     This is not equivalent, but it might be good enough? *)
  | Frame_step T1 T2 :
     T1 ## tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.
(* iris/algebra/sts.v *)
Notation frame_steps T
:= (rtc (frame_step T)).
(* iris/algebra/sts.v *)
(* ** Closure under frame steps *)
Record closed (S : states sts) (T : tokens sts) : Prop
:= Closed {
  closed_disjoint s : s ∈ S → tok s ## T;
  closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
}.
(* iris/algebra/sts.v *)
Definition up (s : state sts) (T : tokens sts) : states sts
:=
  {[ s' | frame_steps T s s' ]}.
(* iris/algebra/sts.v *)
Definition up_set (S : states sts) (T : tokens sts) : states sts
:=
  S ≫= λ s, up s T.
(* iris/algebra/sts.v *)
(* ** Setoids *)
Instance frame_step_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
Proof.
  intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
    eauto with sts; set_solver.
Qed.
(* iris/algebra/sts.v *)
Instance frame_step_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /set_equiv_subseteq [??]; split; by apply frame_step_mono. Qed.
(* iris/algebra/sts.v *)
Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
(* iris/algebra/sts.v *)
Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
(* iris/algebra/sts.v *)
Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof.
  intros s ? <- T T' HT ; apply elem_of_subseteq.
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply elem_of_PropSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
(* iris/algebra/sts.v *)
Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
Proof.
  by move=> ??? ?? /set_equiv_subseteq [??]; split; apply up_preserving.
Qed.
(* iris/algebra/sts.v *)
Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
Proof.
  intros S1 S2 HS T1 T2 HT. rewrite /up_set.
  f_equiv=> // s1 s2. by apply up_preserving.
Qed.
(* iris/algebra/sts.v *)
Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
Proof.
  move=> S1 S2 /set_equiv_subseteq [??] T1 T2 /set_equiv_subseteq [??];
    split; by apply up_set_preserving.
Qed.
(* iris/algebra/sts.v *)
(* ** Properties of closure under frame steps *)
Lemma closed_steps S T s1 s2 :
  closed S T → s1 ∈ S → frame_steps T s1 s2 → s2 ∈ S.
Proof. induction 3; eauto using closed_step. Qed.
(* iris/algebra/sts.v *)
Lemma closed_op T1 T2 S1 S2 :
  closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).
Proof.
  intros [? Hstep1] [? Hstep2]; split; [set_solver|].
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
  - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
  - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
Qed.
(* iris/algebra/sts.v *)
Lemma step_closed s1 s2 T1 T2 S Tf :
  step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ## Tf →
  s2 ∈ S ∧ T2 ## Tf ∧ tok s2 ## T2.
Proof.
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
  - set_solver -Hstep Hs1 Hs2.
Qed.
(* iris/algebra/sts.v *)
Lemma steps_closed s1 s2 T1 T2 S Tf :
  steps (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ## Tf →
  tok s1 ## T1 → s2 ∈ S ∧ T2 ## Tf ∧ tok s2 ## T2.
Proof.
  remember (s1,T1) as sT1 eqn:HsT1; remember (s2,T2) as sT2 eqn:HsT2.
  intros Hsteps; revert s1 T1 HsT1 s2 T2 HsT2.
  induction Hsteps as [?|? [s2 T2] ? Hstep Hsteps IH];
     intros s1 T1 HsT1 s2' T2' ?????; simplify_eq; first done.
  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); eauto.
Qed.
(* iris/algebra/sts.v *)
(* ** Properties of the closure operators *)
Lemma elem_of_up s T : s ∈ up s T.
Proof. constructor. Qed.
(* iris/algebra/sts.v *)
Lemma subseteq_up_set S T : S ⊆ up_set S T.
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
(* iris/algebra/sts.v *)
Lemma elem_of_up_set S T s : s ∈ S → s ∈ up_set S T.
Proof. apply subseteq_up_set. Qed.
(* iris/algebra/sts.v *)
Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
Proof. by rewrite /up_set set_bind_singleton. Qed.
(* iris/algebra/sts.v *)
Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ## T) → closed (up_set S T) T.
Proof.
  intros HS; unfold up_set; split.
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
    specialize (HS s' Hs'); clear Hs' S.
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
  - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.
    split; [eapply rtc_r|]; eauto.
Qed.
(* iris/algebra/sts.v *)
Lemma closed_up s T : tok s ## T → closed (up s T) T.
Proof.
  intros; rewrite -(set_bind_singleton (λ s, up s T) s).
  apply closed_up_set; set_solver.
Qed.
(* iris/algebra/sts.v *)
Lemma closed_up_set_empty S : closed (up_set S ∅) ∅.
Proof. eauto using closed_up_set with sts. Qed.
(* iris/algebra/sts.v *)
Lemma closed_up_empty s : closed (up s ∅) ∅.
Proof. eauto using closed_up with sts. Qed.
(* iris/algebra/sts.v *)
Lemma up_closed S T : closed S T → up_set S T ≡ S.
Proof.
  intros ?; apply set_equiv_subseteq; split; auto using subseteq_up_set.
  intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
(* iris/algebra/sts.v *)
Lemma up_subseteq s T S : closed S T → s ∈ S → sts.up s T ⊆ S.
Proof. move=> ?? s' ?. eauto using closed_steps. Qed.
(* iris/algebra/sts.v *)
Lemma up_set_subseteq S1 T S2 : closed S2 T → S1 ⊆ S2 → sts.up_set S1 T ⊆ S2.
Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed.
(* iris/algebra/sts.v *)
Lemma up_op s T1 T2 : up s (T1 ∪ T2) ⊆ up s T1 ∩ up s T2.
Proof. (* Notice that the other direction does not hold. *)
  intros x Hx. split; eapply elem_of_PropSet, rtc_subrel; try exact Hx.
  - intros; eapply frame_step_mono; last first; try done. set_solver+.
  - intros; eapply frame_step_mono; last first; try done. set_solver+.
Qed.
(* iris/algebra/sts.v *)
(* The type of bounds we can give to the state of an STS. On paper, this is the
   type that we equip with an RA structure. In Coq we have to do some work to
   model composition only being defined under some non-computable conditions. *)
Inductive car (sts : stsT)
:=
  | auth : state sts → propset (token sts) → car sts
  | frag : propset (state sts) → propset (token sts) → car sts.
(* iris/algebra/sts.v *)
Notation stsT
:= sts.stsT.
(* iris/algebra/sts.v *)
Notation Sts
:= sts.Sts.
(* iris/algebra/sts.v *)
Inductive sts_car_equiv : Equiv (car sts)
:=
  | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
  | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
(* iris/algebra/sts.v *)
Instance sts_car_valid_instance : Valid (car sts)
:= λ x,
  match x with
  | auth s T => tok s ## T
  | frag S' T => closed S' T ∧ ∃ s, s ∈ S'
  end.
(* iris/algebra/sts.v *)
Instance sts_car_core_instance : PCore (car sts)
:= λ x,
  Some match x with
  | frag S' _ => frag (up_set S' ∅ ) ∅
  | auth s _  => frag (up s ∅) ∅
  end.
(* iris/algebra/sts.v *)
Inductive sts_car_disjoint_instance : Disjoint (car sts)
:=
  | frag_frag_disjoint S1 S2 T1 T2 :
     (∃ s, s ∈ S1 ∩ S2) → T1 ## T2 → frag S1 T1 ## frag S2 T2
  | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → auth s T1 ## frag S T2
  | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → frag S T1 ## auth s T2.
(* iris/algebra/sts.v *)
Instance sts_op_instance : Op (car sts)
:= λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
  | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
  | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
  | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
  end.
(* iris/algebra/sts.v *)
Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s).
Proof. by constructor. Qed.
(* iris/algebra/sts.v *)
Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts).
Proof. by constructor. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_equivalence: Equivalence ((≡) : relation (car sts)).
Proof.
  split.
  - by intros []; constructor.
  - by destruct 1; constructor.
  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed.
(* iris/algebra/sts.v *)
Instance sts_car_op_proper : Proper ((≡@{car sts}) ==> (≡) ==> (≡)) (⋅).
Proof. by do 2 destruct 1; constructor; setoid_subst. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_core_proper : Proper ((≡@{car sts}) ==> (≡)) core.
Proof. by destruct 1; constructor; setoid_subst. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_valid_proper : Proper ((≡@{car sts}) ==> impl) valid.
Proof. by destruct 1; simpl; intros ?; setoid_subst. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_valid_proper' : Proper ((≡@{car sts}) ==> iff) valid.
Proof. by split; apply: sts_car_valid_proper. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_disjoint_proper (x : car sts) :
  Proper ((≡) ==> impl) (disjoint x).
Proof.
  by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
Qed.
(* iris/algebra/sts.v *)
Instance sts_car_disjoint_symmetric : Symmetric (@disjoint (car sts) _).
Proof. destruct 1; constructor; auto with sts. Qed.
(* iris/algebra/sts.v *)
Instance sts_car_disjoint_proper' :
  Proper ((≡@{car sts}) ==> (≡) ==> iff) disjoint.
Proof.
  intros x1 x2 Hx y1 y2 Hy; split.
  - by rewrite Hy (symmetry_iff (##) x1) (symmetry_iff (##) x2) Hx.
  - by rewrite -Hy (symmetry_iff (##) x2) (symmetry_iff (##) x1) -Hx.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_core_valid (x : car sts) :
  ✓ x → ✓ core x.
Proof.
  destruct x; naive_solver eauto using closed_up, closed_up_set,
      elem_of_up, elem_of_up_set with sts.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_op_valid (x y : car sts) :
  ✓ x → ✓ y → x ## y → ✓ (x ⋅ y).
Proof.
  destruct 3; simpl in *; destruct_and?; eauto using closed_op;
      select (closed _ _) (fun H => destruct H); set_solver.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_op_assoc (x y z : car sts) :
  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z.
Proof.
  destruct x, y, z; intros _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_op_comm (x y : car sts) :
  ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x.
Proof. destruct 3; constructor; auto with sts. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_disjoint_ll (x y z : car sts) :
  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z.
Proof.
  destruct 4; inversion_clear 1; constructor; auto with sts.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_disjoint_rl (x y z : car sts) :
  ✓ x → ✓ y → ✓ z → y ## z → x ## y ⋅ z → x ## y.
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply sts_car_disjoint_ll. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_disjoint_lr (x y z : car sts) :
  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → y ## z.
Proof. intros ????. rewrite sts_car_op_comm //. by apply sts_car_disjoint_ll. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_disjoint_move_l (x y z : car sts) :
    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## y ⋅ z.
Proof. destruct 4; inversion_clear 1; constructor; auto with sts. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_disjoint_move_r (a b c : car sts) :
  ✓ a → ✓ b → ✓ c → b ## c → a ## b ⋅ c → a ⋅ b ## c.
Proof.
  intros; symmetry; rewrite sts_car_op_comm; eauto using sts_car_disjoint_rl.
  apply sts_car_disjoint_move_l; auto; by rewrite sts_car_op_comm.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_core_disjoint_l (x : car sts) : ✓ x → core x ## x.
Proof. destruct x; constructor; eauto with sts. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_core_l (x : car sts) : ✓ x → core x ⋅ x ≡ x.
Proof. destruct x; constructor; eauto with sts. Qed.
(* iris/algebra/sts.v *)
Lemma sts_car_core_idemp (x : car sts) : ✓ x → core (core x) ≡ core x.
Proof.
  destruct x as [s T|S T]; constructor; auto with sts.
  + rewrite (up_closed (up _ _)); auto using closed_up with sts.
  + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
Qed.