feat: Completeness for generic logics

Iris/Iris/Algebra/Frac.lean

@@ -19,6 +19,21 @@ This version follows Iris Rocq in fixing the underlying type of fractions to be
 
 @[expose] public section
 
+/-! ## Ordered-field lemmas for `Rat`
+
+This environment has no Mathlib, so `Rat` is missing the ordered-field API (and the
+`positivity`/`field_simp` tactics) needed to reason about division. These few lemmas fill the
+gap that the `Qp` API below relies on. -/
+namespace Rat
+
+protected theorem div_pos {a b : Rat} (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
+  rw [Rat.div_def]; exact Rat.mul_pos ha (Rat.inv_pos.mpr hb)
+
+protected theorem mul_div_cancel_left {a b : Rat} (ha : a ≠ 0) : a * (b / a) = b := by
+  rw [Rat.mul_comm, Rat.div_mul_cancel ha]
+
+end Rat
+
 namespace Iris
 
 /-- The type of positive rational numbers, used as fractions -/
@@ -42,6 +57,16 @@ def Qp.half (q : Qp) : Qp where
     let ⟨v, P⟩ := q
     grind
 
+/-- Division of fractions. -/
+def Qp.div (x y : Qp) : Qp := ⟨x.val / y.val, Rat.div_pos x.2 y.2⟩
+
+instance instHDivQpQpQp : HDiv Qp Qp Qp where
+  hDiv := Qp.div
+
+/-- `q` divided into `n > 0` equal positive parts. -/
+def Qp.divide_even (q : Qp) (n : Nat) (hn : 0 < n) : Qp :=
+  ⟨q.val / n, Rat.div_pos q.2 (by exact_mod_cast hn)⟩
+
 instance instCOFEQp : COFE Qp := COFE.ofDiscrete _ Eq_Equivalence
 
 instance instLeibnizQp : OFE.Leibniz Qp := ⟨id⟩
@@ -75,6 +100,9 @@ instance instCMRAQp : CMRA Qp where
 @[simp, grind =] theorem Qp.val_add (x y : Qp) : (x + y).val = x.val + y.val := rfl
 @[simp, grind =] theorem Qp.val_one : (1 : Qp).val = 1 := rfl
 @[simp, grind =] theorem Qp.val_half (q : Qp) : q.half.val = q.val / 2 := rfl
+@[simp, grind =] theorem Qp.val_div (x y : Qp) : (x / y).val = x.val / y.val := rfl
+@[simp, grind =] theorem Qp.val_divide_even (q : Qp) (n : Nat) (hn : 0 < n) :
+    (q.divide_even n hn).val = q.val / n := rfl
 @[simp, grind =] theorem Qp.val_op (x y : Qp) : (x • y).val = x.val + y.val := rfl
 @[simp, grind =] theorem Qp.validN_iff {n} {x : Qp} : ✓{n} x ↔ x.val ≤ 1 := Iff.rfl
 @[simp, grind =] theorem Qp.valid_iff {x : Qp} : ✓ x ↔ x.val ≤ 1 := Iff.rfl
@@ -87,6 +115,14 @@ instance instCMRAQp : CMRA Qp where
 /-- The whole fraction `1` is valid. -/
 @[simp, rocq_alias frac_valid_1] theorem Qp.valid_one : ✓ (1 : Qp) := by grind
 
+/-- Two halves make a whole. -/
+@[simp, grind =] theorem Qp.half_add_half (q : Qp) : q.half + q.half = q := Subtype.ext (by grind)
+
+/-- `a < b` iff `b` is `a` plus some positive remainder. -/
+theorem Qp.lt_iff_exists_add {a b : Qp} : a < b ↔ ∃ c : Qp, a + c = b := by
+  refine ⟨fun h => ⟨⟨b.val - a.val, by have := Qp.lt_iff.mp h; grind⟩, Subtype.ext (by grind)⟩, ?_⟩
+  rintro ⟨c, rfl⟩; have := c.2; grind
+
 #rocq_ignore frac_op_instance "Use CMRA instance"
 #rocq_ignore frac_pcore_instance "Use CMRA instance"
 #rocq_ignore frac_valid_instance "Use CMRA instance"

Iris/Iris/BI/BigOp/BigSepMap.lean

@@ -568,8 +568,22 @@ theorem bigSepM_impl_strong [DecidableEq K] {M₂ : Type _ → Type _} {V₂ : T
       refine sep_mono_right <| sep_mono_right (equiv_iff.mp <| bigOpM_eqv_of_perm Φ fun k => ?_).2
       by_cases hki : i = k <;> simp_all [get?_filter, get?_insert, get?_delete]
 
--- TODO: `big_sepM_kmap` and `big_sepM_map_seq` require map operations
--- which are not yet available in `PartialMap`.
+-- TODO: `big_sepM_kmap` requires map operations which are not yet available in `PartialMap`.
+
+theorem bigSepM_map_seq {M' : Type _ → Type _} [LawfulFiniteMap M' Nat] {V : Type _}
+    {Φ : Nat → V → PROP} {start : Nat} {l : List V} :
+    ([∗map] k ↦ v ∈ FiniteMap.map_seq (M := M') start l, Φ k v) ⊣⊢
+    ([∗list] i ↦ v ∈ l, Φ (start + i) v) := by
+  induction l generalizing start with
+  | nil => rw [LawfulFiniteMap.map_seq_nil]; simp
+  | cons v l ih =>
+      have hfun : (fun i (x : V) => Φ (start + 1 + i) x) = (fun i x => Φ (start + (i + 1)) x) := by
+        funext i x; congr 1; omega
+      have ih1 := ih (start := start + 1)
+      rw [hfun] at ih1
+      rw [LawfulFiniteMap.map_seq_cons]
+      exact (bigSepM_insert (by rw [LawfulFiniteMap.get?_map_seq, if_neg (by omega)])).trans
+        (sep_congr .rfl ih1)
 
 /-! ## Map–Set Interaction -/
 

Iris/Iris/BI/Lib/Fractional.lean

@@ -12,13 +12,115 @@ public import Iris.ProofMode
 @[expose] public section
 
 namespace Iris
-open Iris.Std BI OFE
+open Iris.Std BI OFE ProofMode
 
 @[rocq_alias Fractional]
 class Fractional [BI PROP] (Φ : Qp → PROP) where
   fractional p q : Φ (p + q) ⊣⊢ Φ p ∗ Φ q
 
 @[rocq_alias AsFractional]
-class AsFractional {PROP: Type u} [bi: BI PROP] (P : PROP) (Φ : Qp → PROP) (q : Qp) where
+class AsFractional {PROP : Type u} [BI PROP] (P : PROP) (Φ : Qp → PROP) (q : Qp) where
   as_fractional : P ⊣⊢ Φ q
   as_fractional_fractional : Fractional Φ
+
+section Lemmas
+variable {PROP : Type _} [BI PROP] {P P1 P2 : PROP} {Φ : Qp → PROP} {q q1 q2 : Qp}
+
+/-- Any `Φ q` of a fractional `Φ` is `AsFractional`. -/
+@[rocq_alias fractional_as_fractional]
+instance (priority := 100) fractional_as_fractional [h : Fractional Φ] (q : Qp) :
+    AsFractional (Φ q) Φ q where
+  as_fractional := .rfl
+  as_fractional_fractional := h
+
+/-- Split a fraction `q1 + q2` into the separating conjunction of its parts. -/
+@[rocq_alias fractional_split]
+theorem fractional_split [hP : AsFractional P Φ (q1 + q2)]
+    [hP1 : AsFractional P1 Φ q1] [hP2 : AsFractional P2 Φ q2] : P ⊣⊢ P1 ∗ P2 :=
+  have := hP.as_fractional_fractional
+  hP.as_fractional.trans <| (Fractional.fractional q1 q2).trans <|
+    sep_congr hP1.as_fractional.symm hP2.as_fractional.symm
+
+/-- Halve a fraction into two equal pieces. -/
+@[rocq_alias fractional_half]
+theorem fractional_half [hP : AsFractional P Φ q] [hP12 : AsFractional P1 Φ q.half] :
+    P ⊣⊢ P1 ∗ P1 :=
+  have := hP.as_fractional_fractional
+  hP.as_fractional.trans <| (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).trans <|
+    sep_congr hP12.as_fractional.symm hP12.as_fractional.symm
+
+/-- Merge two fractions back into their sum. -/
+@[rocq_alias fractional_merge]
+theorem fractional_merge [Fractional Φ]
+    [hP1 : AsFractional P1 Φ q1] [hP2 : AsFractional P2 Φ q2] : P1 ∗ P2 ⊢ Φ (q1 + q2) :=
+  (sep_mono hP1.as_fractional.1 hP2.as_fractional.1).trans (Fractional.fractional q1 q2).2
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias from_sep_fractional]
+instance (priority := default - 10) fromSepFractional [hP : AsFractional P Φ (q1 + q2)] :
+    FromSep P (Φ q1) (Φ q2) where
+  from_sep :=
+    have := hP.as_fractional_fractional
+    (Fractional.fractional q1 q2).2.trans hP.as_fractional.2
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_sep_fractional]
+instance (priority := default - 10) intoSepFractional [hP : AsFractional P Φ (q1 + q2)] :
+    IntoSep P (Φ q1) (Φ q2) where
+  into_sep :=
+    have := hP.as_fractional_fractional
+    hP.as_fractional.1.trans (Fractional.fractional q1 q2).1
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias from_sep_fractional_half]
+instance (priority := default - 10) fromSepFractionalHalf [hP : AsFractional P Φ q] :
+    FromSep P (Φ q.half) (Φ q.half) where
+  from_sep :=
+    have := hP.as_fractional_fractional
+    (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).2.trans hP.as_fractional.2
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_sep_fractional_half]
+instance (priority := default - 10) intoSepFractionalHalf [hP : AsFractional P Φ q] :
+    IntoSep P (Φ q.half) (Φ q.half) where
+  into_sep :=
+    have := hP.as_fractional_fractional
+    hP.as_fractional.1.trans (Qp.half_add_half q ▸ Fractional.fractional q.half q.half).1
+
+end Lemmas
+
+section Divide
+variable {PROP : Type _} [BI PROP]
+open BI.BigSepL
+
+/-- Whenever `q = (k+1) * r`, the fraction `Φ q` splits into `k+1` copies of `Φ r`. -/
+theorem fractional_bigSepL_replicate {Φ : Qp → PROP} [Fractional Φ] (r : Qp) :
+    ∀ (k : Nat) (q : Qp), q.val = ((k : Rat) + 1) * r.val →
+      Φ q ⊢ [∗list] _x ∈ List.replicate (k + 1) r, Φ r := by
+  intro k
+  induction k with
+  | zero =>
+    intro q hq
+    rw [show q = r from Subtype.ext (by grind)]
+    exact (bigSepL_singleton (Φ := fun _ _ => Φ r)).2
+  | succ k ih =>
+    intro q hq
+    have hval : q.val - r.val = ((k : Rat) + 1) * r.val := by grind
+    have hpos : (0 : Rat) < q.val - r.val := hval ▸ Rat.mul_pos (by grind) r.2
+    have hsum : r + (⟨q.val - r.val, hpos⟩ : Qp) = q := Subtype.ext (by grind)
+    rw [← hsum, List.replicate_succ]
+    exact ((Fractional.fractional r _).1.trans (sep_mono_right (ih _ hval))).trans
+      (bigSepL_cons (Φ := fun _ _ => Φ r)).2
+
+/-- Splitting `Φ q` into `n+1` equal pieces, each owning the fraction `q / (n+1)`. -/
+theorem fractional_divide_equal {Φ : Qp → PROP} [Fractional Φ] (q : Qp) (n : Nat) :
+    Φ q ⊢ [∗list] _x ∈ List.replicate (n + 1) (q.divide_even (n + 1) (Nat.succ_pos n)),
+      Φ (q.divide_even (n + 1) (Nat.succ_pos n)) := by
+  refine fractional_bigSepL_replicate _ n q ?_
+  have hne : ((n : Rat) + 1) ≠ 0 := by
+    have : (0 : Rat) ≤ (n : Rat) := by exact_mod_cast Nat.zero_le n
+    grind
+  have hcast : ((n + 1 : Nat) : Rat) = (n : Rat) + 1 := by grind
+  rw [Qp.val_divide_even, hcast, Rat.mul_div_cancel_left hne]
+
+end Divide