phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/proofmode_classes.v *)
(* The [IsOp a b1 b2] class is used in two directions: to "split" input [a] into
outputs [b1] and [b2], and to "merge" inputs [b1] and [b2] into output [a],
where in both cases we have [a ≡ b1 ⋅ b2].

Since the [IsOp a b1 b2] class is used in two directions, there are some
subtleties we need to account for:

- If we want to "merge", we want the "op" instance to be used *last*. That is,
  before using [IsOp (b1 ⋅ b2) b1 b2], we want to traverse the structure of the
  term to merge constructors, and we want it to combine terms like [q/2] and
  [q/2] into [q] instead of [q/2 ⋅ q/2].
- If we want to "split", we want the "op" instance to be used *first*. That is,
  we want to use [IsOp (b1 ⋅ b2) b1 b2] eagerly, so that for instance, a term
  like [q1 ⋅ q2] is turned into [q1] and [q2] and not two times [(q1 ⋅ q2) / 2].

To achieve this, there are various classes with different modes:

- [IsOp a b1 b2]. This class has no mode, so it can be used even to
  combine/merge evars. This class has only one direct instance
  [IsOp (a ⋅ b) a b] with cost 100 (so it is used last), ensuring that the
  "op" rule is used last when merging.
- [IsOp' a b1 b2]. This class requires either [a] OR both [b1] and [b2] to be inputs.
  All usual instances should be of this class to avoid loops.
- [IsOp'LR a b1 b2]. This class requires [a] to be an input and has just one
  instance [IsOp'LR (a ⋅ b) a b] with cost 0. This ensures that the "op"
  rule is used first when splitting. *)
Class IsOp {SI : sidx} {A : cmra} (a b1 b2 : A)
:= is_op : a ≡ b1 ⋅ b2.
(* iris/algebra/proofmode_classes.v *)
Instance is_op_op {SI : sidx} {A : cmra} (a b : A) : IsOp (a ⋅ b) a b | 100.
Proof. by rewrite /IsOp. Qed.
(* iris/algebra/proofmode_classes.v *)
Class IsOp' {SI : sidx} {A : cmra} (a b1 b2 : A)
:=
  #[global] is_op' :: IsOp a b1 b2.
(* iris/algebra/proofmode_classes.v *)
Class IsOp'LR {SI : sidx} {A : cmra} (a b1 b2 : A)
:= is_op_lr : IsOp a b1 b2.
(* iris/algebra/proofmode_classes.v *)
Instance is_op_lr_op {SI : sidx} {A : cmra} (a b : A) : IsOp'LR (a ⋅ b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
(* iris/algebra/proofmode_classes.v *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
Instance is_op_pair {SI : sidx} {A B : cmra} (a b1 b2 : A) (a' b1' b2' : B) :
  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
(* iris/algebra/proofmode_classes.v *)
Instance is_op_pair_core_id_l {SI : sidx} {A B : cmra} (a : A) (a' b1' b2' : B) :
  CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
(* iris/algebra/proofmode_classes.v *)
Instance is_op_pair_core_id_r {SI : sidx} {A B : cmra} (a b1 b2 : A) (a' : B) :
  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
(* iris/algebra/proofmode_classes.v *)
Instance is_op_Some {SI : sidx} {A : cmra} (a : A) b1 b2 :
  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
(* iris/algebra/reservation_map.v *)
(* The camera [reservation_map A] over a camera [A] extends [gmap positive A]
with a notion of "reservation tokens" for a (potentially infinite) set
[E : coPset] which represent the right to allocate a map entry at any position
[k ∈ E].  The key connectives are [reservation_map_data k a] (the "points-to"
assertion of this map), which associates data [a : A] with a key [k : positive],
and [reservation_map_token E] (the reservation token), which says
that no data has been associated with the indices in the mask [E]. The important
properties of this camera are:

- The lemma [reservation_map_token_union] enables one to split [reservation_map_token]
  w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
  [reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2].
- The lemma [reservation_map_alloc] provides a frame preserving update to
  associate data to a key: [reservation_map_token E ~~> reservation_map_data k a]
  provided [k ∈ E] and [✓ a].

In the future, it could be interesting to generalize this map to arbitrary key
types instead of hard-coding [positive]. *)
Record reservation_map (A : Type)
:= ReservationMap {
  reservation_map_data_proj : gmap positive A;
  reservation_map_token_proj : coPset_disj
}.
(* iris/algebra/reservation_map.v *)
Instance : Params (@ReservationMap) 1
:= {}.
(* iris/algebra/reservation_map.v *)
Instance : Params (@reservation_map_data_proj) 1
:= {}.
(* iris/algebra/reservation_map.v *)
Instance : Params (@reservation_map_token_proj) 1
:= {}.
(* iris/algebra/reservation_map.v *)
Definition reservation_map_data {SI : sidx} {A : cmra}
    (k : positive) (a : A) : reservation_map A
:=
  ReservationMap {[ k := a ]} ε.
(* iris/algebra/reservation_map.v *)
Definition reservation_map_token {SI : sidx} {A : cmra}
    (E : coPset) : reservation_map A
:=
  ReservationMap ∅ (CoPset E).
(* iris/algebra/reservation_map.v *)
Instance : Params (@reservation_map_data) 3
:= {}.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_equiv : Equiv (reservation_map A)
:= λ x y,
    reservation_map_data_proj x ≡ reservation_map_data_proj y ∧
    reservation_map_token_proj x = reservation_map_token_proj y.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_dist : Dist (reservation_map A)
:= λ n x y,
    reservation_map_data_proj x ≡{n}≡ reservation_map_data_proj y ∧
    reservation_map_token_proj x = reservation_map_token_proj y.
(* iris/algebra/reservation_map.v *)
Instance ReservationMap_ne :
    NonExpansive2 (@ReservationMap A).
Proof. by split. Qed.
(* iris/algebra/reservation_map.v *)
Instance ReservationMap_proper :
    Proper ((≡) ==> (=) ==> (≡)) (@ReservationMap A).
Proof. by split. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_proj_ne :
    NonExpansive (@reservation_map_data_proj A).
Proof. by destruct 1. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_proj_proper :
    Proper ((≡) ==> (≡)) (@reservation_map_data_proj A).
Proof. by destruct 1. Qed.
(* iris/algebra/reservation_map.v *)
Definition reservation_map_ofe_mixin : OfeMixin (reservation_map A).
Proof.
    by apply (iso_ofe_mixin
      (λ x, (reservation_map_data_proj x, reservation_map_token_proj x))).
  Qed.
(* iris/algebra/reservation_map.v *)
Canonical reservation_mapO
:=
    Ofe (reservation_map A) reservation_map_ofe_mixin.
(* iris/algebra/reservation_map.v *)
Instance ReservationMap_discrete a b :
    Discrete a → Discrete b → Discrete (ReservationMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete_0. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_ofe_discrete :
    OfeDiscrete A → OfeDiscrete reservation_mapO.
Proof. intros ? [??]; apply _. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_ne i :
    NonExpansive (@reservation_map_data SI A i).
Proof. solve_proper. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_proper k :
    Proper ((≡) ==> (≡)) (@reservation_map_data SI A k).
Proof. solve_proper. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_discrete k a :
    Discrete a → Discrete (reservation_map_data k a).
Proof. intros. apply ReservationMap_discrete; apply _. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_token_discrete E :
    Discrete (@reservation_map_token SI A E).
Proof. intros. apply ReservationMap_discrete; apply _. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_valid_instance : Valid (reservation_map A)
:= λ x,
    match reservation_map_token_proj x with
    | CoPset E =>
      ✓ (reservation_map_data_proj x) ∧
      (* dom (reservation_map_data_proj x) ⊥ E *)
      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
    | CoPsetInvalid => False
    end.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_validN_instance : ValidN (reservation_map A)
:= λ n x,
    match reservation_map_token_proj x with
    | CoPset E =>
      ✓{n} (reservation_map_data_proj x) ∧
      (* dom (reservation_map_data_proj x) ⊥ E *)
      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
    | CoPsetInvalid => False
    end.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_pcore_instance : PCore (reservation_map A)
:= λ x,
    Some (ReservationMap (core (reservation_map_data_proj x)) ε).
(* iris/algebra/reservation_map.v *)
Instance reservation_map_op_instance : Op (reservation_map A)
:= λ x y,
    ReservationMap (reservation_map_data_proj x ⋅ reservation_map_data_proj y)
                   (reservation_map_token_proj x ⋅ reservation_map_token_proj y).
(* iris/algebra/reservation_map.v *)
Definition reservation_map_valid_eq :
    valid = λ x, match reservation_map_token_proj x with
                 | CoPset E =>
                   ✓ (reservation_map_data_proj x) ∧
                   (* dom (reservation_map_data_proj x) ⊥ E *)
                   ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
                 | CoPsetInvalid => False
                 end
:= eq_refl _.
(* iris/algebra/reservation_map.v *)
Definition reservation_map_validN_eq :
    validN = λ n x, match reservation_map_token_proj x with
                    | CoPset E =>
                      ✓{n} (reservation_map_data_proj x) ∧
                      (* dom (reservation_map_data_proj x) ⊥ E *)
                      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
                    | CoPsetInvalid => False
                    end
:= eq_refl _.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_included x y :
    x ≼ y ↔
      reservation_map_data_proj x ≼ reservation_map_data_proj y ∧
      reservation_map_token_proj x ≼ reservation_map_token_proj y.
Proof.
    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (ReservationMap z1 z2); split; auto.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_data_proj_validN n x : ✓{n} x → ✓{n} reservation_map_data_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_token_proj_validN n x : ✓{n} x → ✓{n} reservation_map_token_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_cmra_mixin : CmraMixin (reservation_map A).
Proof.
    apply cmra_total_mixin.
    - eauto.
    - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
    - solve_proper.
    - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
      + by rewrite -Hm.
      + intros i. by rewrite -(dist_None n) -Hm dist_None.
    - pose 0ᵢ.
      intros [m [E|]]; rewrite reservation_map_valid_eq
        reservation_map_validN_eq /= ?cmra_valid_validN; naive_solver.
    - intros n m [k [E|]]; rewrite reservation_map_validN_eq /=;
        naive_solver eauto using cmra_validN_le.
    - split; simpl; [by rewrite assoc|by rewrite assoc_L].
    - split; simpl; [by rewrite comm|by rewrite comm_L].
    - split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
    - split; simpl; [by rewrite cmra_core_idemp|done].
    - intros ??; rewrite! reservation_map_included; intros [??].
      by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
    - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite reservation_map_validN_eq /=.
      rewrite {1}/op /cmra_op /=. case_decide; last done.
      intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
      intros i. move: (Hdisj i). rewrite lookup_op.
      case: (m1 !! i); case: (m2 !! i); set_solver.
    - intros n x y1 y2 ? [??]; simpl in *.
      destruct (cmra_extend n (reservation_map_data_proj x)
          (reservation_map_data_proj y1) (reservation_map_data_proj y2))
        as (m1&m2&?&?&?); auto using reservation_map_data_proj_validN.
      destruct (cmra_extend n (reservation_map_token_proj x)
          (reservation_map_token_proj y1) (reservation_map_token_proj y2))
        as (E1&E2&?&?&?); auto using reservation_map_token_proj_validN.
      by exists (ReservationMap m1 E1), (ReservationMap m2 E2).
  Qed.
(* iris/algebra/reservation_map.v *)
Canonical reservation_mapR
:=
    Cmra (reservation_map A) reservation_map_cmra_mixin.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_cmra_discrete :
    CmraDiscrete A → CmraDiscrete reservation_mapR.
Proof.
    split; first apply _.
    intros [m [E|]]; rewrite reservation_map_validN_eq reservation_map_valid_eq //=.
      by intros [?%cmra_discrete_valid ?].
  Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_empty_instance : Unit (reservation_map A)
:= ReservationMap ε ε.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_ucmra_mixin : UcmraMixin (reservation_map A).
Proof.
    split; simpl.
    - rewrite reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
    - split; simpl; [by rewrite left_id|by rewrite left_id_L].
    - do 2 constructor; [apply (core_id_core _)|done].
  Qed.
(* iris/algebra/reservation_map.v *)
Canonical reservation_mapUR
:=
    Ucmra (reservation_map A) reservation_map_ucmra_mixin.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_core_id k a :
    CoreId a → CoreId (reservation_map_data k a).
Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_data_valid k a : ✓ (reservation_map_data k a) ↔ ✓ a.
Proof. rewrite reservation_map_valid_eq /= singleton_valid. set_solver. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_token_valid E : ✓ (reservation_map_token E).
Proof. rewrite reservation_map_valid_eq /=. split; first done. by left. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_data_op k a b :
    reservation_map_data k (a ⋅ b) = reservation_map_data k a ⋅ reservation_map_data k b.
Proof.
      by rewrite {2}/op /reservation_map_op_instance /reservation_map_data /= singleton_op left_id_L.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_data_mono k a b :
    a ≼ b → reservation_map_data k a ≼ reservation_map_data k b.
Proof. intros [c ->]. by rewrite reservation_map_data_op. Qed.
(* iris/algebra/reservation_map.v *)
Instance reservation_map_data_is_op k a b1 b2 :
    IsOp a b1 b2 →
    IsOp' (reservation_map_data k a) (reservation_map_data k b1) (reservation_map_data k b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite reservation_map_data_op. Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_token_union E1 E2 :
    E1 ## E2 →
    reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2.
Proof.
    intros. by rewrite /op /reservation_map_op_instance
      /reservation_map_token /= coPset_disj_union // left_id_L.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_token_difference E1 E2 :
    E1 ⊆ E2 →
    reservation_map_token E2 = reservation_map_token E1 ⋅ reservation_map_token (E2 ∖ E1).
Proof.
    intros. rewrite -reservation_map_token_union; last set_solver.
      by rewrite -union_difference_L.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_token_valid_op E1 E2 :
    ✓ (reservation_map_token E1 ⋅ reservation_map_token E2) ↔ E1 ## E2.
Proof.
    rewrite reservation_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
    split; [done|]; intros _. split.
    - by rewrite left_id.
    - intros i. rewrite lookup_op lookup_empty. auto.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_alloc E k a :
    k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
Proof.
    intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
    rewrite reservation_map_validN_eq /= {1}/op {1}/cmra_op /=.
    case_decide; last done.
    rewrite !left_id_L. intros [Hmf Hdisj]; split.
    - destruct (Hdisj k) as [Hmfi|]; last set_solver.
      intros j. rewrite lookup_op.
      destruct (decide (k = j)) as [<-|].
      + rewrite Hmfi lookup_singleton_eq right_id_L. by apply cmra_valid_validN.
      + by rewrite lookup_singleton_ne // left_id_L.
    - intros j. destruct (decide (k = j)); first set_solver.
      rewrite lookup_op lookup_singleton_ne //.
      destruct (Hdisj j) as [Hmfi|?]; last set_solver. rewrite Hmfi. auto.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_updateP P (Q : reservation_map A → Prop) k a :
    a ~~>: P →
    (∀ a', P a' → Q (reservation_map_data k a')) →
    reservation_map_data k a ~~>: Q.
Proof.
    intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
    rewrite reservation_map_validN_eq /= left_id_L. intros [Hmf Hdisj].
    destruct (Hup n (mf !! k)) as (a'&?&?).
    { move: (Hmf (k)).
      by rewrite lookup_op lookup_singleton_eq Some_op_opM. }
    exists (reservation_map_data k a'); split; first by eauto.
    rewrite /= left_id_L. split.
    - intros j. destruct (decide (k = j)) as [<-|].
      + by rewrite lookup_op lookup_singleton_eq Some_op_opM.
      + rewrite lookup_op lookup_singleton_ne // left_id_L.
        move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
    - intros j. move: (Hdisj j).
      rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
  Qed.
(* iris/algebra/reservation_map.v *)
Lemma reservation_map_update k a b :
    a ~~> b →
    reservation_map_data k a ~~> reservation_map_data k b.
Proof.
    rewrite !cmra_update_updateP. eauto using reservation_map_updateP with subst.
  Qed.
(* iris/algebra/stepindex.v *)
(* An index type [I] comes with
- a well-founded strict linear order [sidx_lt] (written [i < j]),
- a total linear order [sidx_le] (written [i ≤ j]),
- a zero index [sidx_zero] (written [0ᵢ]),
- and a successor operation on indices [sidx_succ] (written [Sᵢ]).

The less-or-equal relation [≤] must be compatible with the less-than relation
[<] ([sidx_mixin_le_lteq]). That is, [i ≤ j] iff [i < j] or [i = j]. The [0ᵢ]
index has to be the smallest step-index (i.e., [¬ i ≺ zero] for all [i]) and the
successor operation [Sᵢ] should yield for a step-index [i] the least index
greater than [i]. The strict order [<] should be _computationally_ decidable,
and, finally, it should be computationally decidable whether a given step-index
is a limit index (i.e., it cannot be reached from any predecessor by applying
the successor operation).

The less-or-equal operation [sidx_le] is not strictly necessary since [i ≤ j]
is equivalent to [i < j] or [i = j]. We add it as an additional parameter to
this interface for engineering reasons: the addition of [sidx_le] simplifies
backwards compatibly to developments that assume step-indices are always natural
numbers and (implicitly) that [(i ≤ j)%sidx] unifies with [(i ≤ j)%nat] for
natural numbers. *)
Record SIdxMixin {I} (ilt ile : relation I) (zero : I) (succ : I → I)
:= {
  sidx_mixin_lt_trans : Transitive ilt;
  sidx_mixin_lt_wf : well_founded ilt;
  sidx_mixin_lt_trichotomy : TrichotomyT ilt;
  sidx_mixin_le_lteq n m : ile n m ↔ ilt n m ∨ n = m;
  sidx_mixin_nlt_0_r n : ¬ ilt n zero;
  sidx_mixin_lt_succ_diag_r n : ilt n (succ n);
  sidx_mixin_le_succ_l_2 n m : ilt n m → ile (succ n) m;
  (** An index is either a successor or a limit index. The second disjunct in
  [weak_case] considers [0ᵢ] to be a limit index, which is often not desired. So
  typically, instead of [weak_case] you want to use [Index.case] which has an
  explicit disjunct for [0ᵢ] and uses [Index.limit] to define limit indices,
  excluding [0ᵢ]. *)
  sidx_mixin_weak_case n : {m | n = succ m} + (∀ m, ilt m n → ilt (succ m) n);
}.
(* iris/algebra/stepindex.v *)
(* [sidx] is both a canonical structure and a typeclass.
When working with a concrete index type, we usually fix it globally. Declaring
an appropriate instance and structure enables Coq to infer the globally fixed
index type automatically in almost all places. For an example of how to
instantiate [sidx], see [stepindex_finite.v].

Using both a canonical structure and a type class is not very common. In this
case, it maximizes the inference that is done by Coq when we use the index type.
The fact that the step-index is a type class makes sure in, for example, lemma
statements that it will be inferred from the context automatically. It also
means that if we work with finite step-indices then the finite step-index
instance will be used by default as soon as we (or any of our dependencies)
import [stepindex_finite.v]. The canonical structure, on the other hand, makes
sure that the index type is inferred automatically as soon as we use either
natural numbers or ordinals as the step-index in a concrete lemma. *)
Structure sidx
:= SIdx {
  sidx_car :> Type;
  sidx_lt : relation sidx_car;
  sidx_le : relation sidx_car;
  sidx_zero : sidx_car;
  sidx_succ : sidx_car → sidx_car;
  sidx_mixin : SIdxMixin sidx_lt sidx_le sidx_zero sidx_succ;
}.
(* iris/algebra/stepindex.v *)
(* We cannot overload [0] and [S], so we define custom notations with an [i]
subscript. Overloading [0] is disallowed, one should use [Number Notation], but
that only works for "concrete" number types defined as an [Inductive] (not
"abstract" number types represented by a class). One also cannot overload [S]
since it is a constructor (of [nat]) and not a [Notation]. *)
Notation "0ᵢ"
:= sidx_zero (at level 0).
(* iris/algebra/stepindex.v *)
Notation "'Sᵢ'"
:= sidx_succ (at level 0).
(* iris/algebra/stepindex.v *)
(* The remaining operations have notations in the `%sidx` scope. *)
Notation "(<)"
:= sidx_lt (only parsing) : sidx_scope.
(* iris/algebra/stepindex.v *)
Notation "n < m"
:= (sidx_lt n m) : sidx_scope.
(* iris/algebra/stepindex.v *)
Notation "(≤)"
:= sidx_le (only parsing) : sidx_scope.
(* iris/algebra/stepindex.v *)
Notation "n ≤ m"
:= (sidx_le n m) : sidx_scope.
(* iris/algebra/stepindex.v *)
(* Finite indices are exactly the natural numbers *)
Class SIdxFinite (SI : sidx)
:=
  finite_index n : n = 0ᵢ ∨ ∃ m, n = Sᵢ m.
(* iris/algebra/stepindex.v *)
(* Not an [Instance], we get that via [StrictOrder]. *)
Lemma lt_trans : Transitive (<).
Proof. eapply sidx_mixin_lt_trans, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_wf : well_founded (<).
Proof. eapply sidx_mixin_lt_wf, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Instance lt_trichotomy : TrichotomyT (<).
Proof. eapply sidx_mixin_lt_trichotomy, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_lteq n m : n ≤ m ↔ n < m ∨ n = m.
Proof. eapply sidx_mixin_le_lteq, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma nlt_0_r n : ¬ n < 0ᵢ.
Proof. eapply sidx_mixin_nlt_0_r, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_succ_diag_r n : n < Sᵢ n.
Proof. eapply sidx_mixin_lt_succ_diag_r, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma le_succ_l_2 n m : n < m → Sᵢ n ≤ m.
Proof. eapply sidx_mixin_le_succ_l_2, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
Lemma weak_case n : { m | n = Sᵢ m } + (∀ m, m < n → Sᵢ m < n).
Proof. eapply sidx_mixin_weak_case, sidx_mixin. Qed.
(* iris/algebra/stepindex.v *)
(* [weak_case] allows us to decide whether a number is a limit index.
  However, according to [m < n → Sᵢ m < n] (right disjunct), 0 is a limit
  index. In many definitions and proofs (e.g., [case] and [rec]), it is helpful
  to think of 0 as a special case rather than a degenerate limit index. We
  therefore exclude 0 from the notion of limit indices. *)
Record limit (n : SI)
:= Limit {
    limit_gt_S m : m < n → Sᵢ m < n;
    limit_neq_0 : n ≠ 0ᵢ;
  }.
(* iris/algebra/stepindex.v *)
(* * Derived properties *)
Instance inhabited : Inhabited SI
:= populate 0ᵢ.
(* iris/algebra/stepindex.v *)
Instance lt_strict : StrictOrder (<).
Proof.
    split; [|apply lt_trans].
    intros n Hn. induction (lt_wf n) as [n _ IH].
    by apply IH in Hn.
  Qed.
(* iris/algebra/stepindex.v *)
Instance le_po : PartialOrder (≤).
Proof.
    split; [split|].
    - intros n. apply le_lteq. auto.
    - intros n m p. rewrite /sidx_le. rewrite !le_lteq.
      intros [Hnm|Hnm] [Hmp|Hmp]; subst; [|by eauto..].
      left. by etrans.
    - intros n m [H1| ->]%le_lteq [H2|H2]%le_lteq; [|by eauto..].
      destruct (irreflexivity (<) n). by trans m.
  Qed.
(* iris/algebra/stepindex.v *)
Lemma lt_le_incl n m : n < m → n ≤ m.
Proof. intros. apply le_lteq. auto. Qed.