(* iris/algebra/stepindex.v *)
From iris.prelude Require Export prelude
From iris.prelude Require Import options

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;

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;
}.
Existing Class sidx.

Global ArgumentsSIdx _ {_ _ _ _} _.

Global Argumentssidx_car {_}.

Global Argumentssidx_lt {_}.

Global Argumentssidx_le {_}.

Global Argumentssidx_zero {_}.

Global Argumentssidx_succ {_} _.
Declare Scope sidx_scope.
Delimit Scope sidx_scope with sidx.
Bind Scope sidx_scope with sidx_car.

Local OpenScope sidx_scope.

Global HintExtern 0 (_ ≤ _)%sidx => reflexivity : core.

Class SIdxFinite(SI : sidx) :=
  finite_index n : n = 0ᵢ ∨ ∃ m, n = Sᵢ m.

Lemma lt_trans: Transitive (<).
  Proof. eapply sidx_mixin_lt_trans, sidx_mixin. Qed.

Lemma lt_wf: well_founded (<).
  Proof. eapply sidx_mixin_lt_wf, sidx_mixin. Qed.

Global Instancelt_trichotomy : TrichotomyT (<).
  Proof. eapply sidx_mixin_lt_trichotomy, sidx_mixin. Qed.

Lemma le_lteqn m : n ≤ m ↔ n < m ∨ n = m.
  Proof. eapply sidx_mixin_le_lteq, sidx_mixin. Qed.

Lemma nlt_0_rn : ¬ n < 0ᵢ.
  Proof. eapply sidx_mixin_nlt_0_r, sidx_mixin. Qed.

Lemma lt_succ_diag_rn : n < Sᵢ n.
  Proof. eapply sidx_mixin_lt_succ_diag_r, sidx_mixin. Qed.

Lemma le_succ_l_2n m : n < m → Sᵢ n ≤ m.
  Proof. eapply sidx_mixin_le_succ_l_2, sidx_mixin. Qed.

Lemma weak_casen : { m | n = Sᵢ m } + (∀ m, m < n → Sᵢ m < n).
  Proof. eapply sidx_mixin_weak_case, sidx_mixin. Qed.

Record limit(n : SI) := Limit {
    limit_gt_S m : m < n → Sᵢ m < n;
    limit_neq_0 : n ≠ 0ᵢ;
  }.

Global Instanceinhabited : Inhabited SI := populate 0ᵢ.

Global Instancelt_strict : StrictOrder (<).
  Proof.
    split; [|apply lt_trans].
    intros n Hn. induction (lt_wf n) as [n _ IH].
    by apply IH in Hn.
  Qed.

Global Instancele_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.

Lemma lt_le_incln m : n < m → n ≤ m.
  Proof. intros. apply le_lteq. auto. Qed.

Local HintResolve lt_le_incl : core.

Global Instancele_total : Total (≤).
  Proof. intros n m. destruct (trichotomy (<) n m); naive_solver. Qed.

Lemma lt_le_transn m p : n < m → m ≤ p → n < p.
  Proof. intros ? [| ->]%le_lteq; [|done]. by trans m. Qed.

Lemma le_lt_transn m p : n ≤ m → m < p → n < p.
  Proof. intros [| ->]%le_lteq ?; [|done]. by trans m. Qed.

Lemma le_succ_ln 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.

Lemma lt_succ_rn 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.

Lemma succ_le_monon m : n ≤ m ↔ Sᵢ n ≤ Sᵢ m.
  Proof. by rewrite le_succ_l lt_succ_r. Qed.

Lemma succ_lt_monon m : n < m ↔ Sᵢ n < Sᵢ m.
  Proof. by rewrite lt_succ_r le_succ_l. Qed.

Global Instancesucc_inj : Inj (=) (=) Sᵢ.
  Proof.
    intros n m Heq.
    apply (anti_symm (≤)); apply succ_le_mono; by rewrite Heq.
  Qed.

Lemma le_succ_diag_rn : n ≤ Sᵢ n.
  Proof. apply lt_le_incl, lt_succ_diag_r. Qed.

Lemma neq_0_lt_0n : n ≠ 0ᵢ ↔ 0ᵢ < n.
  Proof.
    split.
    - destruct (trichotomy (<) 0ᵢ n) as [|[|?%nlt_0_r]]; naive_solver.
    - intros ? ->. by destruct (nlt_0_r 0ᵢ).
  Qed.

Lemma lt_ge_casesn m : n < m ∨ m ≤ n.
  Proof.
    destruct (trichotomyT (<) n m) as [[| ->]|]; auto using lt_le_incl.
  Qed.

Lemma le_gt_casesn m : n ≤ m ∨ m < n.
  Proof. destruct (lt_ge_cases m n); auto. Qed.

Lemma le_ngtn 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.

Lemma lt_ngen 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.

Lemma le_neqn 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.

Lemma nlt_succ_rn m : ¬ m < Sᵢ n ↔ n < m.
  Proof. by rewrite -le_ngt le_succ_l. Qed.

Global Instanceeq_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.

Global Instancelt_dec : RelDecision (<) | 1000.
  Proof. apply _. Defined.

Global Instancele_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.

Lemma le_0_ln : 0ᵢ ≤ n.
  Proof. apply le_ngt, nlt_0_r. Qed.

Lemma le_0_rn : n ≤ 0ᵢ ↔ n = 0ᵢ.
  Proof. split; [|by intros ->]. intros. by apply (anti_symm (≤)), le_0_l. Qed.

Lemma neq_succ_0n : Sᵢ n ≠ 0ᵢ.
  Proof. apply neq_0_lt_0, lt_succ_r, le_0_l. Qed.

Lemma succ_neqn : n ≠ Sᵢ n.
  Proof.
    intros Hn. destruct (irreflexivity (<) n). rewrite {2}Hn.
    apply lt_succ_diag_r.
  Qed.

Lemma limit_0: ¬limit 0ᵢ.
  Proof. by intros [? []]. Qed.

Lemma limit_lt_0n : limit n → 0ᵢ < n.
  Proof. intros. apply neq_0_lt_0; intros ->. by apply limit_0. Qed.

Lemma limit_Sn : ¬limit (Sᵢ n).
  Proof.
    intros [Hlim _]. apply (irreflexivity (<) (Sᵢ n)), Hlim, lt_succ_diag_r.
  Qed.

Lemma limit_finite`{!SIdxFinite SI} n : ¬limit n.
  Proof.
    destruct (finite_index n) as [->|[m ->]]; auto using limit_0, limit_S.
  Qed.

Lemma casen : (n = 0ᵢ) + { m | n = Sᵢ m } + limit n.
  Proof.
    destruct (decide (n = 0ᵢ)); [by auto|].
    destruct (weak_case n); by auto using limit.
  Qed.

Lemma lt_succ_diag_r'n m : n = Sᵢ m → m < n.
  Proof. intros ->. apply lt_succ_diag_r. Qed.

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.

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.

Lemma rec_unfoldP 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.

Lemma rec_zeroP 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.

Lemma rec_succP 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.

Lemma rec_limP 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.