From 7b97935614c270e91cf7d168e4fcd6dba9146850 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Tue, 3 Mar 2026 00:41:12 +0100 Subject: [PATCH 1/4] feat: Add BigOp algebra and monoid definitions --- src/Iris/Algebra/BigOp.lean | 764 +++++++++++++++++++++++++++++++++++ src/Iris/Algebra/Monoid.lean | 109 +++++ src/Iris/Std/List.lean | 101 +++++ src/Iris/Std/PartialMap.lean | 25 ++ 4 files changed, 999 insertions(+) create mode 100644 src/Iris/Algebra/BigOp.lean create mode 100644 src/Iris/Algebra/Monoid.lean create mode 100644 src/Iris/Std/List.lean diff --git a/src/Iris/Algebra/BigOp.lean b/src/Iris/Algebra/BigOp.lean new file mode 100644 index 000000000..2898b6268 --- /dev/null +++ b/src/Iris/Algebra/BigOp.lean @@ -0,0 +1,764 @@ +/- +Copyright (c) 2026 Zongyuan Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zongyuan Liu +-/ +import Iris.Algebra.Monoid +import Iris.Std.List +import Iris.Std.PartialMap + +namespace Iris.Algebra + +/-! # Big Operators + +This file defines big operators (fold operations) at the abstract OFE level. +These are parameterized by a monoid operation and include theorems about their properties. +-/ + +open OFE + +def bigOpL {M : Type u} {A : Type v} (op : M → M → M) (unit : M) + (Φ : Nat → A → M) (l : List A) : M := + match l with + | [] => unit + | x :: xs => op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs) + +namespace BigOpL + +variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit] + +omit [OFE M] [Monoid M op unit] in +@[simp] theorem nil (Φ : Nat → A → M) : + bigOpL op unit Φ ([] : List A) = unit := rfl + +omit [OFE M] [Monoid M op unit] in +@[simp] theorem cons (Φ : Nat → A → M) (x : A) (xs : List A) : + bigOpL op unit Φ (x :: xs) = op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs) := rfl + +@[simp] theorem singleton (Φ : Nat → A → M) (x : A) : + bigOpL op unit Φ [x] ≡ Φ 0 x := by + simp only [cons, nil] + exact Monoid.op_right_id _ + +theorem congr {Φ Ψ : Nat → A → M} {l : List A} + (h : ∀ i x, l[i]? = some x → Φ i x ≡ Ψ i x) : + bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := by + induction l generalizing Φ Ψ with + | nil => exact Equiv.rfl + | cons y ys ih => + simp only [cons] + exact Monoid.op_proper (h 0 y rfl) (ih fun i x hget => h (i + 1) x hget) + +theorem congr_ne {Φ Ψ : Nat → A → M} {l : List A} {n : Nat} + (h : ∀ i x, l[i]? = some x → Φ i x ≡{n}≡ Ψ i x) : + bigOpL op unit Φ l ≡{n}≡ bigOpL op unit Ψ l := by + induction l generalizing Φ Ψ with + | nil => exact Dist.rfl + | cons y ys ih => + simp only [cons] + exact Monoid.op_ne_dist (h 0 y rfl) (ih fun i x hget => h (i + 1) x hget) + +/-- Congruence when the functions are equivalent on all indices. -/ +theorem congr' {Φ Ψ : Nat → A → M} {l : List A} + (h : ∀ i x, Φ i x ≡ Ψ i x) : + bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := + congr (fun i x _ => h i x) + +theorem append (Φ : Nat → A → M) (l₁ l₂ : List A) : + bigOpL op unit Φ (l₁ ++ l₂) ≡ + op (bigOpL op unit Φ l₁) (bigOpL op unit (fun n => Φ (n + l₁.length)) l₂) := by + induction l₁ generalizing Φ with + | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _) + | cons x xs ih => + simp only [List.cons_append, cons, List.length_cons] + have ih' := ih (fun n => Φ (n + 1)) + calc op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) (xs ++ l₂)) + _ ≡ op (Φ 0 x) (op (bigOpL op unit (fun n => Φ (n + 1)) xs) + (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂)) := + Monoid.op_congr_r ih' + _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs)) + (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂) := + Equiv.symm (Monoid.op_assoc _ _ _) + _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs)) + (bigOpL op unit (fun n => Φ (n + (xs.length + 1))) l₂) := by + simp only [show ∀ n, n + xs.length + 1 = n + (xs.length + 1) from by omega]; exact Equiv.rfl + +theorem snoc (Φ : Nat → A → M) (l : List A) (x : A) : + bigOpL op unit Φ (l ++ [x]) ≡ op (bigOpL op unit Φ l) (Φ l.length x) := by + have h := @append M A _ op unit _ Φ l [x] + simp only [cons, nil, Nat.zero_add] at h + exact h.trans (Monoid.op_congr_r (Monoid.op_right_id _)) + +theorem unit_const (l : List A) : + bigOpL op unit (fun _ _ => unit) l ≡ unit := by + induction l with + | nil => exact Equiv.rfl + | cons _ _ ih => simp only [cons]; exact Equiv.trans (Monoid.op_left_id _) ih + +theorem op_distr (Φ Ψ : Nat → A → M) (l : List A) : + bigOpL op unit (fun i x => op (Φ i x) (Ψ i x)) l ≡ + op (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by + induction l generalizing Φ Ψ with + | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _) + | cons x xs ih => + simp only [cons] + exact Equiv.trans (Monoid.op_congr_r (ih _ _)) Monoid.op_op_swap + +theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) : + bigOpL op unit Φ (l.map h) ≡ bigOpL op unit (fun i x => Φ i (h x)) l := by + induction l generalizing Φ with + | nil => exact Equiv.rfl + | cons x xs ih => + simp only [List.map_cons, cons] + exact Monoid.op_proper Equiv.rfl (ih (fun n => Φ (n + 1))) + +omit [OFE M] [Monoid M op unit] in +theorem closed (P : M → Prop) (Φ : Nat → A → M) (l : List A) + (hunit : P unit) + (hop : ∀ x y, P x → P y → P (op x y)) + (hf : ∀ i x, l[i]? = some x → P (Φ i x)) : + P (bigOpL op unit Φ l) := by + induction l generalizing Φ with + | nil => exact hunit + | cons y ys ih => + simp only [cons] + exact hop _ _ (hf 0 y rfl) (ih _ fun i x hget => hf (i + 1) x hget) + +theorem perm (Φ : A → M) {l₁ l₂ : List A} (hp : l₁.Perm l₂) : + bigOpL op unit (fun _ => Φ) l₁ ≡ bigOpL op unit (fun _ => Φ) l₂ := by + induction hp with + | nil => exact Equiv.rfl + | cons _ _ ih => simp only [cons]; exact Monoid.op_congr_r ih + | swap _ _ _ => simp only [cons]; exact Monoid.op_swap_inner (unit := unit) + | trans _ _ ih1 ih2 => exact Equiv.trans ih1 ih2 + +theorem take_drop (Φ : Nat → A → M) (l : List A) (n : Nat) : + bigOpL op unit Φ l ≡ + op (bigOpL op unit Φ (l.take n)) (bigOpL op unit (fun k => Φ (n + k)) (l.drop n)) := by + by_cases hn : n ≤ l.length + · have h := @append M A _ op unit _ Φ (l.take n) (l.drop n) + simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at h + exact h + · simp only [Nat.not_le] at hn + simp only [List.drop_eq_nil_of_le (Nat.le_of_lt hn), List.take_of_length_le (Nat.le_of_lt hn), nil] + exact Equiv.symm (Monoid.op_right_id _) + +theorem filter_map {B : Type v} (h : A → Option B) (Φ : B → M) (l : List A) : + bigOpL op unit (fun _ => Φ) (l.filterMap h) ≡ + bigOpL op unit (fun _ x => (h x).elim unit Φ) l := by + induction l with + | nil => exact Equiv.rfl + | cons x xs ih => + simp only [List.filterMap_cons] + cases hx : h x <;> simp only [hx, Option.elim, cons] + · exact Equiv.trans ih (Equiv.symm (Monoid.op_left_id _)) + · exact Monoid.op_congr_r ih + +theorem bind {B : Type v} (h : A → List B) (Φ : B → M) (l : List A) : + bigOpL op unit (fun _ => Φ) (l.flatMap h) ≡ + bigOpL op unit (fun _ x => bigOpL op unit (fun _ => Φ) (h x)) l := by + induction l with + | nil => exact Equiv.rfl + | cons x xs ih => + simp only [List.flatMap_cons, cons] + exact Equiv.trans (append _ _ _) (Monoid.op_congr_r ih) + +omit [OFE M] [Monoid M op unit] in +theorem gen_proper_2 {B : Type v} (R : M → M → Prop) + (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) + (hunit : R unit unit) + (hop : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) + (hlen : l₁.length = l₂.length) + (hf : ∀ i, ∀ x y, l₁[i]? = some x → l₂[i]? = some y → R (Φ i x) (Ψ i y)) : + R (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + induction l₁ generalizing l₂ Φ Ψ with + | nil => + cases l₂ with + | nil => simp only [nil]; exact hunit + | cons _ _ => simp at hlen + | cons x xs ih => + cases l₂ with + | nil => simp at hlen + | cons y ys => + simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen + simp only [cons] + have h0 : R (Φ 0 x) (Ψ 0 y) := hf 0 x y rfl rfl + have htail : ∀ i, ∀ a b, xs[i]? = some a → ys[i]? = some b → + R (Φ (i + 1) a) (Ψ (i + 1) b) := fun i a b ha hb => hf (i + 1) a b ha hb + exact hop _ _ _ _ h0 (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen htail) + +omit [OFE M] [Monoid M op unit] in +theorem gen_proper (R : M → M → Prop) + (Φ Ψ : Nat → A → M) (l : List A) + (hR_refl : ∀ x, R x x) + (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) + (hf : ∀ k y, l[k]? = some y → R (Φ k y) (Ψ k y)) : + R (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by + apply gen_proper_2 (op := op) (unit := unit) R Φ Ψ l l + · exact hR_refl unit + · exact hR_op + · rfl + · intro k x y hx hy + rw [hx] at hy; cases hy + exact hf k x hx + +omit [OFE M] [Monoid M op unit] in +theorem ext {Φ Ψ : Nat → A → M} {l : List A} + (h : ∀ i x, l[i]? = some x → Φ i x = Ψ i x) : + bigOpL op unit Φ l = bigOpL op unit Ψ l := by + apply gen_proper + · intro _; rfl + · intros _ _ _ _ ha hb; rw [ha, hb] + · exact h + +omit [OFE M] [Monoid M op unit] in +theorem cons_int_l (Φ : Int → A → M) (x : A) (l : List A) : + bigOpL op unit (fun k => Φ k) (x :: l) = + op (Φ 0 x) (bigOpL op unit (fun k y => Φ (1 + (k : Int)) y) l) := by + simp only [cons] + apply congrArg + apply ext + intro i y hy + congr 1 + omega + +omit [OFE M] [Monoid M op unit] in +theorem cons_int_r (Φ : Int → A → M) (x : A) (l : List A) : + bigOpL op unit (fun k => Φ k) (x :: l) = + op (Φ 0 x) (bigOpL op unit (fun k y => Φ ((k : Int) + 1) y) l) := by + rfl + +theorem proper_2 [OFE A] (Φ Ψ : Nat → A → M) (l₁ l₂ : List A) + (hlen : l₁.length = l₂.length) + (hf : ∀ (k : Nat) (y₁ y₂ : A), l₁[k]? = some y₁ → l₂[k]? = some y₂ → Φ k y₁ ≡ Ψ k y₂) : + bigOpL op unit Φ l₁ ≡ bigOpL op unit Ψ l₂ := by + apply gen_proper_2 (op := op) (unit := unit) (· ≡ ·) Φ Ψ l₁ l₂ + · exact Equiv.rfl + · intros a a' b b' ha hb; exact Monoid.op_proper ha hb + · exact hlen + · intro k x y hx hy + exact hf k x y hx hy + +theorem zip_idx (Φ : A × Nat → M) (n : Nat) (l : List A) : + bigOpL op unit (fun _ => Φ) (l.zipIdx n) ≡ + bigOpL op unit (fun i x => Φ (x, n + i)) l := by + induction l generalizing n with + | nil => simp only [nil]; exact Equiv.rfl + | cons x xs ih => + simp only [cons, Nat.add_zero] + refine Monoid.op_proper Equiv.rfl (Equiv.trans (ih (n + 1)) (congr' fun i _ => ?_)) + simp only [Nat.add_assoc, Nat.add_comm 1 i]; exact Equiv.rfl + +theorem zip_idx_int (Φ : A × Int → M) (n : Int) (l : List A) : + bigOpL op unit (fun _ => Φ) (Std.List.zipIdxInt l n) ≡ + bigOpL op unit (fun i x => Φ (x, n + (i : Int))) l := by + unfold Std.List.zipIdxInt + suffices ∀ m, bigOpL op unit (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡ + bigOpL op unit (fun i x => Φ (x, m + (i : Int))) l by exact this n + intro m + induction l generalizing m with + | nil => simp only [List.mapIdx, nil]; exact Equiv.rfl + | cons x xs ih => + simp only [List.mapIdx_cons, cons] + apply Monoid.op_proper + · show Φ (x, (0 : Int) + m) ≡ Φ (x, m + (0 : Int)) + rw [Int.zero_add, Int.add_zero] + · have list_eq : (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) = + (List.mapIdx (fun i v => (v, ↑i + (m + 1))) xs) := by + apply List.ext_getElem (by simp only [List.length_mapIdx]) + intro n hn1 hn2 + simp only [List.getElem_mapIdx]; congr 1; omega + rw [list_eq] + exact (ih (m + 1)).trans (congr' fun i _ => by rw [show m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) from by omega]) + +theorem sep_zip_with {B C : Type _} + (f : A → B → C) (g1 : C → A) (g2 : C → B) + (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) + (hg1 : ∀ x y, g1 (f x y) = x) + (hg2 : ∀ x y, g2 (f x y) = y) + (hlen : l₁.length = l₂.length) : + bigOpL op unit (fun i c => op (Φ i (g1 c)) (Ψ i (g2 c))) (List.zipWith f l₁ l₂) ≡ + op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + induction l₁ generalizing l₂ Φ Ψ with + | nil => + cases l₂ with + | nil => simp only [List.zipWith_nil_left, nil]; exact Equiv.symm (Monoid.op_left_id _) + | cons _ _ => simp at hlen + | cons x xs ih => + cases l₂ with + | nil => simp at hlen + | cons y ys => + simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen + simp only [List.zipWith_cons_cons, cons, hg1, hg2] + exact Equiv.trans (Monoid.op_congr_r (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen)) Monoid.op_op_swap + +/-- Big op over zipped list with separated functions. -/ +theorem sep_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) + (hlen : l₁.length = l₂.length) : + bigOpL op unit (fun i xy => op (Φ i xy.1) (Ψ i xy.2)) (l₁.zip l₂) ≡ + op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + simp [List.zip] + exact sep_zip_with (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen + +variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] +variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂} +variable [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] +variable {B : Type w} + +/-- Monoid homomorphisms distribute over big ops. -/ +theorem commute {R : M₂ → M₂ → Prop} {f : M₁ → M₂} + (hom : MonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) + (Φ : Nat → B → M₁) (l : List B) : + R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by + induction l generalizing Φ with + | nil => simp only [nil]; exact hom.map_unit + | cons x xs ih => + simp only [cons] + exact hom.rel_trans (hom.homomorphism _ _) (hom.op_proper (hom.rel_refl _) (ih _)) + +/-- Weak monoid homomorphisms distribute over non-empty big ops. -/ +theorem commute_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} + (hom : WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) + (Φ : Nat → B → M₁) (l : List B) (hne : l ≠ []) : + R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by + induction l generalizing Φ with + | nil => exact absurd rfl hne + | cons x xs ih => + simp only [cons] + cases xs with + | nil => + simp only [nil] + haveI : NonExpansive f := hom.f_ne + exact (hom.rel_proper (NonExpansive.eqv (Monoid.op_right_id _)) + (Monoid.op_right_id _)).mpr (hom.rel_refl _) + | cons y ys => + exact hom.rel_trans (hom.homomorphism _ _) + (hom.op_proper (hom.rel_refl _) (ih _ (List.cons_ne_nil y ys))) + +end BigOpL + +namespace BigOpM + +open Iris.Std + +variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit] +variable {M' : Type _ → Type _} {K : Type _} {V : Type _} +variable [LawfulFiniteMap M' K] + +def bigOpM (Φ : K → V → M) (m : M' V) : M := + bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m) + +theorem bigOpM_equiv (Φ : K → V → M) (m₁ m₂ : M' V) + (h : PartialMap.equiv m₁ m₂) : + bigOpM (op := op) (unit := unit) Φ m₁ ≡ bigOpM (op := op) (unit := unit) Φ m₂ := by + simp only [bigOpM] + exact BigOpL.perm _ (LawfulFiniteMap.toList_perm_of_get?_eq h) + +omit [OFE M] [Monoid M op unit] in +@[simp] theorem empty (Φ : K → V → M) : + bigOpM (op := op) (unit := unit) Φ (∅ : M' V) = unit := by + show bigOpL op unit _ (toList (∅ : M' V)) = unit + rw [show toList (K := K) (∅ : M' V) = [] from toList_empty]; rfl + +theorem insert (Φ : K → V → M) (m : M' V) (i : K) (x : V) : + get? m i = none → + bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x) ≡ + op (Φ i x) (bigOpM (op := op) (unit := unit) Φ m) := by + intro hi + simp only [bigOpM] + exact BigOpL.perm _ (LawfulFiniteMap.toList_insert (v := x) hi) + +theorem delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : + get? m i = some x → + bigOpM (op := op) (unit := unit) Φ m ≡ + op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := by + intro hi + exact (bigOpM_equiv Φ m _ (fun k => (LawfulPartialMap.insert_delete_cancel hi k).symm)).trans + (insert Φ (Iris.Std.delete m i) i x (get?_delete_eq rfl)) + +variable {A : Type w} + +theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) + (Φ : K → A → M) (Ψ : K → B → M) (m1 : M' A) (m2 : M' B) + (hR_sub : ∀ x y, x ≡ y → R x y) + (hR_equiv : Equivalence R) + (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) + (hfg : ∀ k, + match get? m1 k, get? m2 k with + | some y1, some y2 => R (Φ k y1) (Ψ k y2) + | none, none => True + | _, _ => False) : + R (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Ψ m2) := by + let P1 : M' A → Prop := fun m1' => ∀ (m2' : M' B) (Φ' : K → A → M) (Ψ' : K → B → M), + (∀ k, match get? m1' k, get? m2' k with + | some y1, some y2 => R (Φ' k y1) (Ψ' k y2) + | none, none => True + | _, _ => False) → + R (bigOpM (op := op) (unit := unit) Φ' m1') (bigOpM (op := op) (unit := unit) Ψ' m2') + suffices h : P1 m1 from h m2 Φ Ψ hfg + have hequiv1 : ∀ (m₁ m₂ : M' A), PartialMap.equiv m₁ m₂ → P1 m₁ → P1 m₂ := + fun m₁ m₂ heq hP m2' Φ' Ψ' hfg' => + hR_equiv.trans (hR_sub _ _ (bigOpM_equiv Φ' m₁ m₂ heq).symm) + (hP m2' Φ' Ψ' (fun k => by rw [show get? m₁ k = get? m₂ k from heq k]; exact hfg' k)) + have hemp1 : P1 (∅ : M' A) := by + intro m2' Φ' Ψ' hfg' + let P2 : M' B → Prop := fun m2'' => ∀ (Φ'' : K → A → M) (Ψ'' : K → B → M), + (∀ k, match get? (∅ : M' A) k, get? m2'' k with + | some y1, some y2 => R (Φ'' k y1) (Ψ'' k y2) + | none, none => True + | _, _ => False) → + R (bigOpM (op := op) (unit := unit) Φ'' (∅ : M' A)) (bigOpM (op := op) (unit := unit) Ψ'' m2'') + suffices h2 : P2 m2' from h2 Φ' Ψ' hfg' + exact LawfulFiniteMap.induction_on (K := K) (P := P2) + (fun m₁ m₂ heq hP Φ'' Ψ'' hfg'' => + hR_equiv.trans (hP Φ'' Ψ'' (fun k => by rw [show get? m₁ k = get? m₂ k from heq k]; exact hfg'' k)) + (hR_sub _ _ (bigOpM_equiv Ψ'' m₁ m₂ heq))) + (fun _ _ _ => by + show R (bigOpM (op := op) (unit := unit) _ (∅ : M' A)) + (bigOpM (op := op) (unit := unit) _ (∅ : M' B)) + rw [empty, empty]; exact hR_sub unit unit Equiv.rfl) + (fun k _ _ _ _ Φ'' Ψ'' hfg'' => by + have := hfg'' k; simp only [show get? (∅ : M' A) k = none from get?_empty k, get?_insert_eq rfl] at this) + m2' + have hins1 : ∀ (i : K) (x : A) (m : M' A), get? m i = none → P1 m → P1 (Iris.Std.insert m i x) := by + intro k x1 m1' hm1'k IH m2' Φ' Ψ' hfg' + have hfg_k := hfg' k + rw [get?_insert_eq rfl] at hfg_k + cases hm2k : get? m2' k with + | none => rw [hm2k] at hfg_k; cases hfg_k + | some x2 => + rw [hm2k] at hfg_k + exact hR_equiv.trans (hR_sub _ _ (insert Φ' m1' k x1 hm1'k)) + (hR_equiv.trans (hR_op _ _ _ _ hfg_k (IH _ _ _ fun k' => by + by_cases hkk' : k = k' + · subst hkk'; rw [get?_delete_eq rfl, hm1'k]; trivial + · have := hfg' k'; rw [get?_insert_ne hkk'] at this; rwa [get?_delete_ne hkk'])) + (hR_sub _ _ (Equiv.symm (delete Ψ' m2' k x2 hm2k)))) + exact LawfulFiniteMap.induction_on (K := K) (P := P1) hequiv1 hemp1 hins1 m1 + +omit [Monoid M op unit] in +theorem gen_proper {M : Type u} {op : M → M → M} {unit : M} (R : M → M → Prop) + (Φ Ψ : K → V → M) (m : M' V) + (hR_refl : ∀ x, R x x) + (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) + (hf : ∀ k x, get? m k = some x → R (Φ k x) (Ψ k x)) : + R (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by + simp only [bigOpM] + apply BigOpL.gen_proper_2 (op := op) (unit := unit) R + · exact hR_refl unit + · exact hR_op + · rfl + · intro i x y hx hy + rw [hx] at hy; cases hy + exact hf x.1 x.2 (toList_get.mp (List.mem_iff_getElem?.mpr ⟨i, hx⟩)) + +theorem ext {M : Type u} (op : M → M → M) (unit : M) (Φ Ψ : K → V → M) (m : M' V) + (hf : ∀ k x, get? m k = some x → Φ k x = Ψ k x) : + bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Ψ m := by + apply gen_proper (R := (· = ·)) + · intro _; rfl + · intros _ _ _ _ ha hb; rw [ha, hb] + · exact hf + +theorem ne (Φ Ψ : K → V → M) (m : M' V) (n : Nat) + (hf : ∀ k x, get? m k = some x → Φ k x ≡{n}≡ Ψ k x) : + bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := by + apply gen_proper (R := (· ≡{n}≡ ·)) + · intro _; exact Dist.rfl + · intros a a' b b' ha hb; exact Monoid.op_ne_dist ha hb + · exact hf + +theorem proper (Φ Ψ : K → V → M) (m : M' V) + (hf : ∀ k x, get? m k = some x → Φ k x ≡ Ψ k x) : + bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := by + apply gen_proper (R := (· ≡ ·)) + · intro _; exact Equiv.rfl + · intros a a' b b' ha hb; exact Monoid.op_proper ha hb + · exact hf + +theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → M) (m1 m2 : M' A) + (hm : ∀ k, get? m1 k = get? m2 k) + (hf : ∀ k y1 y2, + get? m1 k = some y1 → + get? m2 k = some y2 → + y1 ≡ y2 → + Φ k y1 ≡ Ψ k y2) : + bigOpM (op := op) (unit := unit) Φ m1 ≡ bigOpM (op := op) (unit := unit) Ψ m2 := by + apply gen_proper_2 (R := (· ≡ ·)) + · intros _ _ h; exact h + · exact equiv_eqv + · intros a a' b b' ha hb; exact Monoid.op_proper ha hb + · intro k + have hlk := hm k + cases hm1k : get? m1 k with + | none => + rw [hm1k] at hlk + rw [← hlk] + trivial + | some y1 => + rw [hm1k] at hlk + cases hm2k : get? m2 k with + | none => rw [hm2k] at hlk; cases hlk + | some y2 => + rw [hm2k] at hlk + cases hlk + exact hf k y1 y1 hm1k hm2k Equiv.rfl + +theorem ne_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat) + (hf : ∀ k x, Φ k x ≡{n}≡ Ψ k x) : + bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := + ne _ _ _ _ fun k x _ => hf k x + +theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V) + (hf : ∀ k x, Φ k x ≡ Ψ k x) : + bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := + proper _ _ _ fun k x _ => hf k x + +omit [Monoid M op unit] in +theorem to_list (Φ : K → V → M) (m : M' V) : + bigOpM (op := op) (unit := unit) Φ m ≡ + bigOpL op unit (fun _ kx => Φ kx.1 kx.2) (toList (K := K) m) := by + rfl + +theorem of_list [DecidableEq K] (Φ : K → V → M) (l : List (K × V)) + (hnodup : NoDupKeys l) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.ofList l : M' V) ≡ + bigOpL op unit (fun _ kx => Φ kx.1 kx.2) l := by + simp only [bigOpM] + apply BigOpL.perm + exact LawfulFiniteMap.toList_ofList hnodup + +theorem singleton (Φ : K → V → M) (i : K) (x : V) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.singleton (M := M') i x) ≡ Φ i x := by + have h := insert (op := op) (unit := unit) Φ (∅ : M' V) i x (get?_empty i) + rw [empty] at h + exact h.trans (Monoid.op_right_id _) + +theorem unit_const [DecidableEq K] (m : M' V) : + bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m ≡ unit := by + let P : M' V → Prop := fun m' => bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m' ≡ unit + have hequiv : ∀ m₁ m₂ : M' V, PartialMap.equiv m₁ m₂ → P m₁ → P m₂ := + fun m₁ m₂ heq h => Equiv.trans (bigOpM_equiv _ m₁ m₂ heq).symm h + have hemp : P (∅ : M' V) := by show _ ≡ _; rw [empty] + have hins : ∀ i x m, get? m i = none → P m → P (Iris.Std.insert m i x) := + fun i x m' hm' IH => + let h_ins := insert (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m' i x hm' + Equiv.trans h_ins (Equiv.trans (Monoid.op_proper Equiv.rfl IH) (Monoid.op_left_id unit)) + show P m + exact LawfulFiniteMap.induction_on (K := K) (P := P) hequiv hemp hins m + +theorem map (h : V → B) (Φ : K → B → M) (m : M' V) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.map h m) ≡ + bigOpM (op := op) (unit := unit) (fun k v => Φ k (h v)) m := by + simp only [bigOpM] + exact (BigOpL.perm _ LawfulFiniteMap.toList_map).trans + (BigOpL.map (op := op) (unit := unit) (fun kv => (kv.1, h kv.2)) (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m)) + +theorem filter_map (h : V → Option V) (Φ : K → V → M) (m : M' V) + (hinj : Function.Injective h) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.filterMap h m) ≡ + bigOpM (op := op) (unit := unit) (fun k v => (h v).elim unit (Φ k)) m := by + simp only [bigOpM] + refine (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans ?_ + refine (BigOpL.filter_map (op := op) (unit := unit) (fun kv => (h kv.2).map (kv.1, ·)) + (fun kv => Φ kv.1 kv.2) (toList (K := K) m)).trans ?_ + exact BigOpL.congr' fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map] + +theorem insert_delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : + bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x) ≡ + op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := + (bigOpM_equiv Φ _ _ (fun k => (LawfulPartialMap.insert_delete (i := i) (x := x) (m := m) k).symm)).trans + (insert Φ (Iris.Std.delete m i) i x (get?_delete_eq rfl)) + +theorem insert_override (Φ : K → A → M) (m : M' A) (i : K) (x x' : A) : + get? m i = some x → Φ i x ≡ Φ i x' → + bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x') ≡ + bigOpM (op := op) (unit := unit) Φ m := by + intro hi hΦ + exact (insert_delete Φ m i x').trans + ((Monoid.op_proper hΦ.symm Equiv.rfl).trans (delete Φ m i x hi).symm) + +theorem fn_insert [DecidableEq K] {B : Type w} (g : K → V → B → M) (f : K → B) (m : M' V) + (i : K) (x : V) (b : B) (hi : get? m i = none) : + bigOpM (op := op) (unit := unit) (fun k y => g k y (if k = i then b else f k)) + (Iris.Std.insert m i x) ≡ + op (g i x b) (bigOpM (op := op) (unit := unit) (fun k y => g k y (f k)) m) := by + refine (insert _ m i x hi).trans (Monoid.op_proper (by simp) (proper _ _ _ fun k y hk => ?_)) + simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk] + +theorem fn_insert' [DecidableEq K] (f : K → M) (m : M' V) (i : K) (x : V) (P : M) + (hi : get? m i = none) : + bigOpM (op := op) (unit := unit) (fun k _ => if k = i then P else f k) + (Iris.Std.insert m i x) ≡ + op P (bigOpM (op := op) (unit := unit) (fun k _ => f k) m) := by + refine (insert _ m i x hi).trans (Monoid.op_proper (by simp) (proper _ _ _ fun k _ hk => ?_)) + simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk] + +private theorem filter_list_aux (Φ : K × V → M) (φ : K → V → Bool) (l : List (K × V)) : + bigOpL op unit (fun _ kv => Φ kv) (l.filter (fun kv => φ kv.1 kv.2)) ≡ + bigOpL op unit (fun _ kv => if φ kv.1 kv.2 then Φ kv else unit) l := by + induction l with + | nil => simp only [List.filter, BigOpL.nil]; exact Equiv.rfl + | cons kv kvs ih => + simp only [List.filter] + cases hp : φ kv.1 kv.2 with + | false => + simp only [BigOpL.cons, hp] + exact Equiv.trans ih (Equiv.symm (Monoid.op_left_id _)) + | true => + simp only [BigOpL.cons, hp] + exact Monoid.op_congr_r ih + +theorem filter' (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.filter φ m) ≡ + bigOpM (op := op) (unit := unit) (fun k x => if φ k x then Φ k x else unit) m := by + unfold bigOpM + have hperm := LawfulFiniteMap.toList_filter (M := M') (K := K) (V := V) (φ := φ) (m := m) + have heq : bigOpL op unit (fun _ kv => Φ kv.1 kv.2) + (toList (K := K) (PartialMap.filter φ m)) ≡ + bigOpL op unit (fun _ kv => Φ kv.1 kv.2) + ((toList (K := K) m).filter (fun kv => φ kv.1 kv.2)) := + BigOpL.perm _ hperm + refine Equiv.trans heq ?_ + exact filter_list_aux (fun kv => Φ kv.1 kv.2) φ (toList (K := K) m) + +theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : PartialMap.disjoint m1 m2) : + bigOpM (op := op) (unit := unit) Φ (m1 ∪ m2) ≡ + op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) := by + let P : M' V → Prop := fun m1 => + PartialMap.disjoint m1 m2 → + bigOpM (op := op) (unit := unit) Φ (PartialMap.union m1 m2) ≡ + op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) + have hequiv : ∀ m₁ m₂', PartialMap.equiv m₁ m₂' → P m₁ → P m₂' := by + intro m₁ m₂' heq hP hdisj' + have hunion : PartialMap.equiv (PartialMap.union m₁ m2) (PartialMap.union m₂' m2) := + fun k => by show get? _ k = get? _ k; rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k] + exact (bigOpM_equiv Φ _ _ hunion).symm.trans + ((hP fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩).trans + (Monoid.op_proper (bigOpM_equiv Φ m₁ m₂' heq) Equiv.rfl)) + suffices h : P m1 from h hdisj + have hemp : P (∅ : M' V) := fun _ => by + rw [empty] + exact (bigOpM_equiv Φ _ _ (fun k => by + show get? (PartialMap.union (∅ : M' V) m2) k = get? m2 k + rw [LawfulPartialMap.get?_union, show get? (∅ : M' V) k = none from get?_empty k]; simp)).trans + (Monoid.op_left_id _).symm + have hins : ∀ (i : K) (x : V) (m : M' V), get? m i = none → P m → P (Iris.Std.insert m i x) := by + intro i x m hi_none IH hdisj' + have hi_m2 : get? m2 i = none := by + have := (PartialMap.disjoint_iff _ m2).mp hdisj' i + cases this with + | inl h => rw [get?_insert_eq rfl] at h; cases h + | inr h => exact h + have hm_disj : PartialMap.disjoint m m2 := fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by + by_cases h : i = k + · subst h; rw [hi_none] at hk1; cases hk1 + · rwa [get?_insert_ne h], hk2⟩ + have h_none : get? (m ∪ m2) i = none := by + show get? (PartialMap.union m m2) i = none + rw [LawfulPartialMap.get?_union_none]; exact ⟨hi_none, hi_m2⟩ + exact (bigOpM_equiv Φ _ _ (fun k => (LawfulPartialMap.union_insert_left (i := i) (x := x) (m₁ := m) (m₂ := m2) k).symm)).trans + ((insert Φ (m ∪ m2) i x h_none).trans + ((Monoid.op_congr_r (IH hm_disj)).trans + ((Monoid.op_assoc _ _ _).symm.trans + (Monoid.op_congr_l (insert Φ m i x hi_none).symm)))) + exact LawfulFiniteMap.induction_on (K := K) (P := P) hequiv hemp hins m1 + +theorem op_distr (Φ Ψ : K → V → M) (m : M' V) : + bigOpM (op := op) (unit := unit) (fun k x => op (Φ k x) (Ψ k x)) m ≡ + op (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by + simp only [bigOpM] + exact BigOpL.op_distr (op := op) (unit := unit) + (fun _ kv => Φ kv.1 kv.2) (fun _ kv => Ψ kv.1 kv.2) (toList (K := K) m) + +private theorem closed_aux [DecidableEq K] (P : M → Prop) (Φ : K → V → M) + (hproper : ∀ x y, x ≡ y → (P x ↔ P y)) + (hunit : P unit) + (hop : ∀ x y, P x → P y → P (op x y)) : + ∀ (m' : M' V), (∀ k' x', get? m' k' = some x' → P (Φ k' x')) → + P (bigOpM (op := op) (unit := unit) Φ m') := by + intro m' hf' + let Q : M' V → Prop := fun m'' => (∀ k x, get? m'' k = some x → P (Φ k x)) → + P (bigOpM (op := op) (unit := unit) Φ m'') + have hequiv_Q : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → Q m₁ → Q m₂ := + fun m₁ m₂ heq hQ hf => (hproper _ _ (bigOpM_equiv Φ m₁ m₂ heq)).mp + (hQ fun k x hget => hf k x ((heq k) ▸ hget)) + have hemp_Q : Q (∅ : M' V) := fun _ => by + show P (bigOpM (op := op) (unit := unit) Φ (∅ : M' V)); rw [empty]; exact hunit + have hins_Q : ∀ i x m, get? m i = none → Q m → Q (Iris.Std.insert m i x) := by + intro k x m'' hm'' IH hf'' + exact (hproper _ _ (insert (op := op) (unit := unit) Φ m'' k x hm'')).mpr + (hop _ _ (hf'' _ _ (get?_insert_eq rfl)) (IH fun k' x' hget' => by + by_cases heq : k = k' + · subst heq; rw [hget'] at hm''; cases hm'' + · exact hf'' k' x' (by rw [get?_insert_ne heq]; exact hget'))) + exact (LawfulFiniteMap.induction_on (K := K) (P := Q) hequiv_Q hemp_Q hins_Q m') hf' + +theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V) + (hproper : ∀ x y, x ≡ y → (P x ↔ P y)) + (hunit : P unit) + (hop : ∀ x y, P x → P y → P (op x y)) + (hf : ∀ k x, get? m k = some x → P (Φ k x)) : + P (bigOpM (op := op) (unit := unit) Φ m) := + closed_aux P Φ hproper hunit hop m hf + +-- TODO: kmap and map_seq are skipped for now + +theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _} + (f : A → B → C) (g1 : C → A) (g2 : C → B) + (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) + (hg1 : ∀ x y, g1 (f x y) = x) + (hg2 : ∀ x y, g2 (f x y) = y) + (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) : + bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k (g1 xy)) (h2 k (g2 xy))) + (PartialMap.zipWith f m1 m2) ≡ + op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by + have h_op := @op_distr _ _ op unit _ _ _ _ _ + (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy)) (PartialMap.zipWith f m1 m2) + apply Equiv.trans h_op + have map_g1_eq : PartialMap.equiv (PartialMap.map g1 (PartialMap.zipWith f m1 m2)) m1 := by + intro k + simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith] + cases h1k : get? m1 k with + | none => simp [Option.bind] + | some a => + have := (hdom k).mp (by rw [h1k]; simp) + cases h2k : get? m2 k with + | none => rw [h2k] at this; simp at this + | some b => simp [Option.bind, Option.map, hg1] + have map_g2_eq : PartialMap.equiv (PartialMap.map g2 (PartialMap.zipWith f m1 m2)) m2 := by + intro k + simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith] + cases h1k : get? m1 k with + | none => + simp [Option.bind] + cases h2k : get? m2 k with + | none => rfl + | some b => + have := (hdom k).mpr (by rw [h2k]; simp) + rw [h1k] at this; simp at this + | some a => + cases h2k : get? m2 k with + | none => + have := (hdom k).mp (by rw [h1k]; simp) + rw [h2k] at this; simp at this + | some b => simp [Option.bind, Option.map, hg2] + apply Monoid.op_proper + · have h1_fmap := map (op := op) (unit := unit) g1 h1 (PartialMap.zipWith f m1 m2) + exact Equiv.trans (Equiv.symm h1_fmap) (bigOpM_equiv h1 _ _ map_g1_eq) + · have h2_fmap := map (op := op) (unit := unit) g2 h2 (PartialMap.zipWith f m1 m2) + exact Equiv.trans (Equiv.symm h2_fmap) (bigOpM_equiv h2 _ _ map_g2_eq) + +theorem sep_zip {A : Type _} {B : Type _} + (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) + (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) : + bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k xy.1) (h2 k xy.2)) + (PartialMap.zip m1 m2) ≡ + op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by + simp only [PartialMap.zip] + exact sep_zip_with (op := op) (unit := unit) Prod.mk Prod.fst Prod.snd h1 h2 m1 m2 + (fun _ _ => rfl) (fun _ _ => rfl) hdom + +end BigOpM + +end Iris.Algebra diff --git a/src/Iris/Algebra/Monoid.lean b/src/Iris/Algebra/Monoid.lean new file mode 100644 index 000000000..03fe30075 --- /dev/null +++ b/src/Iris/Algebra/Monoid.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 Zongyuan Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zongyuan Liu +-/ +import Iris.Algebra.OFE + +namespace Iris.Algebra + +/-! # Monoids for Big Operators + +- `Monoid` contains the laws and requires an OFE structure +- Use explicit `op` and `unit` parameters to support multiple monoids on the same type +-/ + +open OFE + +/-- A commutative monoid on an OFE, used for big operators. +The operation must be non-expansive, associative, commutative, and have a left identity. -/ +class Monoid (M : Type u) [OFE M] (op : M → M → M) (unit : outParam M) where + /-- The operation is non-expansive in both arguments -/ + op_ne : NonExpansive₂ op + /-- Associativity up to equivalence -/ + op_assoc : ∀ a b c : M, op (op a b) c ≡ op a (op b c) + /-- Commutativity up to equivalence -/ + op_comm : ∀ a b : M, op a b ≡ op b a + /-- Left identity up to equivalence -/ + op_left_id : ∀ a : M, op unit a ≡ a + +namespace Monoid + +attribute [simp] op_left_id + +variable {M : Type u} [OFE M] {op : M → M → M} + +/-- The operation is proper with respect to equivalence. -/ +theorem op_proper {unit : M} [Monoid M op unit] {a a' b b' : M} + (ha : a ≡ a') (hb : b ≡ b') : op a b ≡ op a' b' := by + haveI : NonExpansive₂ op := op_ne + exact NonExpansive₂.eqv ha hb + +/-- Right identity follows from commutativity and left identity. -/ +@[simp] theorem op_right_id {unit : M} [Monoid M op unit] (a : M) : op a unit ≡ a := + Equiv.trans (op_comm (unit := unit) a unit) (op_left_id a) + +/-- Congruence on the left argument. -/ +theorem op_congr_l {unit : M} [Monoid M op unit] {a a' b : M} (h : a ≡ a') : op a b ≡ op a' b := + op_proper (unit := unit) h Equiv.rfl + +/-- Congruence on the right argument. -/ +theorem op_congr_r {unit : M} [Monoid M op unit] {a b b' : M} (h : b ≡ b') : op a b ≡ op a b' := + op_proper (unit := unit) Equiv.rfl h + +/-- Rearrange `(a * b) * (c * d)` to `(a * c) * (b * d)`. -/ +theorem op_op_swap {unit : M} [Monoid M op unit] {a b c d : M} : + op (op a b) (op c d) ≡ op (op a c) (op b d) := + calc op (op a b) (op c d) + _ ≡ op a (op b (op c d)) := op_assoc a b (op c d) + _ ≡ op a (op (op b c) d) := op_congr_r (Equiv.symm (op_assoc b c d)) + _ ≡ op a (op (op c b) d) := op_congr_r (op_congr_l (op_comm b c)) + _ ≡ op a (op c (op b d)) := op_congr_r (op_assoc c b d) + _ ≡ op (op a c) (op b d) := Equiv.symm (op_assoc a c (op b d)) + +/-- Swap inner elements: `a * (b * c)` to `b * (a * c)`. -/ +theorem op_swap_inner {unit : M} [Monoid M op unit] {a b c : M} : + op a (op b c) ≡ op b (op a c) := + calc op a (op b c) + _ ≡ op (op a b) c := Equiv.symm (op_assoc a b c) + _ ≡ op (op b a) c := op_congr_l (op_comm a b) + _ ≡ op b (op a c) := op_assoc b a c + +/-- Non-expansiveness for dist. -/ +theorem op_ne_dist {unit : M} [Monoid M op unit] {n : Nat} {a a' b b' : M} + (ha : a ≡{n}≡ a') (hb : b ≡{n}≡ b') : op a b ≡{n}≡ op a' b' := by + haveI : NonExpansive₂ op := op_ne + exact NonExpansive₂.ne ha hb + +end Monoid + +/-! ## Monoid Homomorphisms -/ + +/-- A weak monoid homomorphism preserves the operation but not necessarily the unit. -/ +class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] + (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) + [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] + (R : M₂ → M₂ → Prop) (f : M₁ → M₂) where + /-- The relation is reflexive -/ + rel_refl : ∀ a : M₂, R a a + /-- The relation is transitive -/ + rel_trans : ∀ {a b c : M₂}, R a b → R b c → R a c + /-- The relation is proper with respect to equivalence -/ + rel_proper : ∀ {a a' b b' : M₂}, a ≡ a' → b ≡ b' → (R a b ↔ R a' b') + /-- The operation is proper with respect to R -/ + op_proper : ∀ {a a' b b' : M₂}, R a a' → R b b' → R (op₂ a b) (op₂ a' b') + /-- The function is non-expansive -/ + f_ne : NonExpansive f + /-- The homomorphism property -/ + homomorphism : ∀ x y, R (f (op₁ x y)) (op₂ (f x) (f y)) + +/-- A monoid homomorphism preserves both the operation and the unit. -/ +class MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] + (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) + [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] + (R : M₂ → M₂ → Prop) (f : M₁ → M₂) + extends WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f where + /-- The unit is preserved -/ + map_unit : R (f unit₁) unit₂ + +end Iris.Algebra diff --git a/src/Iris/Std/List.lean b/src/Iris/Std/List.lean new file mode 100644 index 000000000..355007111 --- /dev/null +++ b/src/Iris/Std/List.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Zongyuan Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zongyuan Liu +-/ + +/-! +# List Lemmas + +This file contains list theory lemmas that are standard properties +not available in Lean core. +-/ + +namespace Iris.Std.List + +/-- List equivalence relation parameterized by an element equivalence relation. + Corresponds to Rocq's `list_equiv`. -/ +inductive Equiv {α : Type _} (R : α → α → Prop) : List α → List α → Prop where + | nil : Equiv R [] [] + | cons {x y : α} {l k : List α} : R x y → Equiv R l k → Equiv R (x :: l) (y :: k) + +def zipIdxInt {α : Type _} (l : List α) (n : Int) : List (α × Int) := + l.mapIdx (fun i v => (v, (i : Int) + n)) + +/-- For a Nodup list, erasing an element removes it completely. -/ +theorem not_mem_erase_self_of_nodup {α : Type _} [DecidableEq α] (x : α) (l : List α) + (hnd : l.Nodup) : x ∉ l.erase x := by + induction l with + | nil => exact List.not_mem_nil + | cons y ys ih => + simp only [List.erase_cons] + rw [List.nodup_cons] at hnd + split + · next h => + have heq : y = x := eq_of_beq h + rw [← heq] + exact hnd.1 + · next h => + simp only [List.mem_cons] + intro hor + cases hor with + | inl heq => + have : (y == x) = true := beq_iff_eq.mpr heq.symm + exact absurd this h + | inr hmem => exact ih hnd.2 hmem + +/-- Two Nodup lists with the same membership are permutations of each other. + Corresponds to Rocq's `NoDup_Permutation`. -/ +theorem perm_of_nodup_of_mem_iff {α : Type _} [DecidableEq α] + {l₁ l₂ : List α} (hnd₁ : l₁.Nodup) (hnd₂ : l₂.Nodup) + (hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁.Perm l₂ := by + induction l₁ generalizing l₂ with + | nil => + cases l₂ with + | nil => exact List.Perm.refl [] + | cons y ys => + have : y ∈ ([] : List α) := (hmem y).mpr List.mem_cons_self + exact absurd this List.not_mem_nil + | cons x xs ih => + have hx_in_l₂ : x ∈ l₂ := (hmem x).mp List.mem_cons_self + have hperm₂ : l₂.Perm (x :: l₂.erase x) := List.perm_cons_erase hx_in_l₂ + rw [List.nodup_cons] at hnd₁ + have hx_notin_xs : x ∉ xs := hnd₁.1 + have hnd_xs : xs.Nodup := hnd₁.2 + have hnd_erase : (l₂.erase x).Nodup := hnd₂.erase x + have hmem_erase : ∀ y, y ∈ xs ↔ y ∈ l₂.erase x := by + intro y + constructor + · intro hy + have hne : y ≠ x := fun heq => hx_notin_xs (heq ▸ hy) + have hy_l₂ : y ∈ l₂ := (hmem y).mp (List.mem_cons_of_mem x hy) + exact (List.mem_erase_of_ne hne).mpr hy_l₂ + · intro hy + have hne : y ≠ x := by + intro heq + rw [heq] at hy + exact not_mem_erase_self_of_nodup x l₂ hnd₂ hy + have hy_l₂ : y ∈ l₂ := List.mem_of_mem_erase hy + have hy_l₁ : y ∈ x :: xs := (hmem y).mpr hy_l₂ + cases List.mem_cons.mp hy_l₁ with + | inl heq => exact absurd heq hne + | inr h => exact h + have hperm_xs : xs.Perm (l₂.erase x) := ih hnd_xs hnd_erase hmem_erase + exact (List.Perm.cons x hperm_xs).trans hperm₂.symm + + +theorem nodup_of_nodup_map_fst {α β : Type _} (l : List (α × β)) + (h : (l.map Prod.fst).Nodup) : l.Nodup := by + induction l with + | nil => exact List.nodup_nil + | cons x xs ih => + rw [List.nodup_cons] + constructor + · intro hx + rw [List.map_cons, List.nodup_cons] at h + have : x.1 ∈ xs.map Prod.fst := List.mem_map_of_mem (f := Prod.fst) hx + exact h.1 this + · rw [List.map_cons, List.nodup_cons] at h + exact ih h.2 + +end Iris.Std.List diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean index bb52582b3..d46e8af2d 100644 --- a/src/Iris/Std/PartialMap.lean +++ b/src/Iris/Std/PartialMap.lean @@ -823,6 +823,31 @@ theorem ofList_toList [DecidableEq K] {m : M V} : cases h ▸ toList_get.mp Hk · exact get?_ofList_some (toList_get.mpr h) toList_noDupKeys +private theorem induction_on_aux + {P : M V → Prop} + (hemp : P PartialMap.empty) + (hins : ∀ i x m, get? m i = none → P m → P (PartialMap.insert m i x)) + (l : List (K × V)) (hnd : NoDupKeys l) : P (ofList l) := by + induction l with + | nil => simpa [ofList] using hemp + | cons kv rest ih => + rw [ofList_cons] + apply hins kv.1 kv.2 + · have hnd_rest := noDupKeys_cons hnd + refine get?_ofList_none (M := M) ?_ hnd_rest + intro ⟨v, hv⟩ + have hnotin : kv.1 ∉ rest.map Prod.fst := + (List.nodup_cons.mp hnd).1 + exact hnotin (List.mem_map_of_mem (f := Prod.fst) (a := (kv.1, v)) hv) + · exact ih (noDupKeys_cons hnd) + +theorem induction_on [DecidableEq K] {P : M V → Prop} + (hequiv : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → P m₁ → P m₂) + (hemp : P PartialMap.empty) + (hins : ∀ i x m, get? m i = none → P m → P (PartialMap.insert m i x)) + (m : M V) : P m := + hequiv _ _ ofList_toList (induction_on_aux hemp hins (toList (K := K) m) toList_noDupKeys) + theorem mem_of_mem_ofList [DecidableEq K] {l : List (K × V)} {i : K} {x : V} (H : get? (ofList l : M V) i = some x) : (i, x) ∈ l := by induction l From 0ca2cac480d53025d4726c4d00ab2dc46ce06558 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Wed, 4 Mar 2026 20:59:31 +0100 Subject: [PATCH 2/4] Clean up --- src/Iris/Algebra/BigOp.lean | 483 ++++++++++++++--------------------- src/Iris/Std/List.lean | 79 +----- src/Iris/Std/PartialMap.lean | 23 +- 3 files changed, 207 insertions(+), 378 deletions(-) diff --git a/src/Iris/Algebra/BigOp.lean b/src/Iris/Algebra/BigOp.lean index 2898b6268..957076fe2 100644 --- a/src/Iris/Algebra/BigOp.lean +++ b/src/Iris/Algebra/BigOp.lean @@ -37,8 +37,7 @@ omit [OFE M] [Monoid M op unit] in @[simp] theorem singleton (Φ : Nat → A → M) (x : A) : bigOpL op unit Φ [x] ≡ Φ 0 x := by - simp only [cons, nil] - exact Monoid.op_right_id _ + simp only [cons, nil]; exact Monoid.op_right_id _ theorem congr {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, l[i]? = some x → Φ i x ≡ Ψ i x) : @@ -47,19 +46,21 @@ theorem congr {Φ Ψ : Nat → A → M} {l : List A} | nil => exact Equiv.rfl | cons y ys ih => simp only [cons] - exact Monoid.op_proper (h 0 y rfl) (ih fun i x hget => h (i + 1) x hget) + apply Monoid.op_proper (h 0 y rfl) + exact ih fun i x hget => h (i + 1) x hget -theorem congr_ne {Φ Ψ : Nat → A → M} {l : List A} {n : Nat} +theorem congr_dist {Φ Ψ : Nat → A → M} {l : List A} {n : Nat} (h : ∀ i x, l[i]? = some x → Φ i x ≡{n}≡ Ψ i x) : bigOpL op unit Φ l ≡{n}≡ bigOpL op unit Ψ l := by induction l generalizing Φ Ψ with | nil => exact Dist.rfl | cons y ys ih => simp only [cons] - exact Monoid.op_ne_dist (h 0 y rfl) (ih fun i x hget => h (i + 1) x hget) + apply Monoid.op_ne_dist (h 0 y rfl) + exact ih fun i x hget => h (i + 1) x hget /-- Congruence when the functions are equivalent on all indices. -/ -theorem congr' {Φ Ψ : Nat → A → M} {l : List A} +theorem congr_forall {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, Φ i x ≡ Ψ i x) : bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := congr (fun i x _ => h i x) @@ -68,41 +69,35 @@ theorem append (Φ : Nat → A → M) (l₁ l₂ : List A) : bigOpL op unit Φ (l₁ ++ l₂) ≡ op (bigOpL op unit Φ l₁) (bigOpL op unit (fun n => Φ (n + l₁.length)) l₂) := by induction l₁ generalizing Φ with - | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _) + | nil => simp only [nil]; exact (Monoid.op_left_id _).symm | cons x xs ih => simp only [List.cons_append, cons, List.length_cons] - have ih' := ih (fun n => Φ (n + 1)) - calc op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) (xs ++ l₂)) - _ ≡ op (Φ 0 x) (op (bigOpL op unit (fun n => Φ (n + 1)) xs) - (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂)) := - Monoid.op_congr_r ih' - _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs)) - (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂) := - Equiv.symm (Monoid.op_assoc _ _ _) - _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs)) - (bigOpL op unit (fun n => Φ (n + (xs.length + 1))) l₂) := by - simp only [show ∀ n, n + xs.length + 1 = n + (xs.length + 1) from by omega]; exact Equiv.rfl + apply (Monoid.op_congr_r (ih _)).trans + simp only [show ∀ n, n + xs.length + 1 = n + (xs.length + 1) from by omega] + exact (Monoid.op_assoc _ _ _).symm theorem snoc (Φ : Nat → A → M) (l : List A) (x : A) : bigOpL op unit Φ (l ++ [x]) ≡ op (bigOpL op unit Φ l) (Φ l.length x) := by - have h := @append M A _ op unit _ Φ l [x] - simp only [cons, nil, Nat.zero_add] at h - exact h.trans (Monoid.op_congr_r (Monoid.op_right_id _)) + have := @append _ _ _ op unit _ Φ l [x] + simp only [cons, nil, Nat.zero_add] at this + exact this.trans (Monoid.op_congr_r (Monoid.op_right_id _)) -theorem unit_const (l : List A) : +theorem const_unit (l : List A) : bigOpL op unit (fun _ _ => unit) l ≡ unit := by induction l with | nil => exact Equiv.rfl - | cons _ _ ih => simp only [cons]; exact Equiv.trans (Monoid.op_left_id _) ih + | cons _ _ ih => + simp only [cons] + exact (Monoid.op_left_id _).trans ih -theorem op_distr (Φ Ψ : Nat → A → M) (l : List A) : +theorem op_distrib (Φ Ψ : Nat → A → M) (l : List A) : bigOpL op unit (fun i x => op (Φ i x) (Ψ i x)) l ≡ op (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by induction l generalizing Φ Ψ with | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _) | cons x xs ih => simp only [cons] - exact Equiv.trans (Monoid.op_congr_r (ih _ _)) Monoid.op_op_swap + exact (Monoid.op_congr_r (ih _ _)).trans Monoid.op_op_swap theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) : bigOpL op unit Φ (l.map h) ≡ bigOpL op unit (fun i x => Φ i (h x)) l := by @@ -110,7 +105,7 @@ theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) : | nil => exact Equiv.rfl | cons x xs ih => simp only [List.map_cons, cons] - exact Monoid.op_proper Equiv.rfl (ih (fun n => Φ (n + 1))) + exact Monoid.op_proper Equiv.rfl (ih _) omit [OFE M] [Monoid M op unit] in theorem closed (P : M → Prop) (Φ : Nat → A → M) (l : List A) @@ -136,9 +131,9 @@ theorem take_drop (Φ : Nat → A → M) (l : List A) (n : Nat) : bigOpL op unit Φ l ≡ op (bigOpL op unit Φ (l.take n)) (bigOpL op unit (fun k => Φ (n + k)) (l.drop n)) := by by_cases hn : n ≤ l.length - · have h := @append M A _ op unit _ Φ (l.take n) (l.drop n) - simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at h - exact h + · have := @append M A _ op unit _ Φ (l.take n) (l.drop n) + simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at this + exact this · simp only [Nat.not_le] at hn simp only [List.drop_eq_nil_of_le (Nat.le_of_lt hn), List.take_of_length_le (Nat.le_of_lt hn), nil] exact Equiv.symm (Monoid.op_right_id _) @@ -161,7 +156,7 @@ theorem bind {B : Type v} (h : A → List B) (Φ : B → M) (l : List A) : | nil => exact Equiv.rfl | cons x xs ih => simp only [List.flatMap_cons, cons] - exact Equiv.trans (append _ _ _) (Monoid.op_congr_r ih) + exact (append _ _ _).trans (Monoid.op_congr_r ih) omit [OFE M] [Monoid M op unit] in theorem gen_proper_2 {B : Type v} (R : M → M → Prop) @@ -182,10 +177,8 @@ theorem gen_proper_2 {B : Type v} (R : M → M → Prop) | cons y ys => simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen simp only [cons] - have h0 : R (Φ 0 x) (Ψ 0 y) := hf 0 x y rfl rfl - have htail : ∀ i, ∀ a b, xs[i]? = some a → ys[i]? = some b → - R (Φ (i + 1) a) (Ψ (i + 1) b) := fun i a b ha hb => hf (i + 1) a b ha hb - exact hop _ _ _ _ h0 (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen htail) + exact hop _ _ _ _ (hf 0 x y rfl rfl) + (ih _ _ _ hlen fun i a b ha hb => hf (i + 1) a b ha hb) omit [OFE M] [Monoid M op unit] in theorem gen_proper (R : M → M → Prop) @@ -194,67 +187,38 @@ theorem gen_proper (R : M → M → Prop) (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) (hf : ∀ k y, l[k]? = some y → R (Φ k y) (Ψ k y)) : R (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by - apply gen_proper_2 (op := op) (unit := unit) R Φ Ψ l l - · exact hR_refl unit - · exact hR_op - · rfl - · intro k x y hx hy - rw [hx] at hy; cases hy - exact hf k x hx + apply gen_proper_2 (op := op) (unit := unit) R Φ Ψ l l (hR_refl unit) hR_op rfl + intro k x y hx hy; rw [hx] at hy; cases hy; exact hf k x hx omit [OFE M] [Monoid M op unit] in theorem ext {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, l[i]? = some x → Φ i x = Ψ i x) : - bigOpL op unit Φ l = bigOpL op unit Ψ l := by - apply gen_proper - · intro _; rfl - · intros _ _ _ _ ha hb; rw [ha, hb] - · exact h - -omit [OFE M] [Monoid M op unit] in -theorem cons_int_l (Φ : Int → A → M) (x : A) (l : List A) : - bigOpL op unit (fun k => Φ k) (x :: l) = - op (Φ 0 x) (bigOpL op unit (fun k y => Φ (1 + (k : Int)) y) l) := by - simp only [cons] - apply congrArg - apply ext - intro i y hy - congr 1 - omega - -omit [OFE M] [Monoid M op unit] in -theorem cons_int_r (Φ : Int → A → M) (x : A) (l : List A) : - bigOpL op unit (fun k => Φ k) (x :: l) = - op (Φ 0 x) (bigOpL op unit (fun k y => Φ ((k : Int) + 1) y) l) := by - rfl + bigOpL op unit Φ l = bigOpL op unit Ψ l := + gen_proper (· = ·) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) h theorem proper_2 [OFE A] (Φ Ψ : Nat → A → M) (l₁ l₂ : List A) (hlen : l₁.length = l₂.length) (hf : ∀ (k : Nat) (y₁ y₂ : A), l₁[k]? = some y₁ → l₂[k]? = some y₂ → Φ k y₁ ≡ Ψ k y₂) : bigOpL op unit Φ l₁ ≡ bigOpL op unit Ψ l₂ := by - apply gen_proper_2 (op := op) (unit := unit) (· ≡ ·) Φ Ψ l₁ l₂ - · exact Equiv.rfl - · intros a a' b b' ha hb; exact Monoid.op_proper ha hb - · exact hlen - · intro k x y hx hy - exact hf k x y hx hy - -theorem zip_idx (Φ : A × Nat → M) (n : Nat) (l : List A) : + exact gen_proper_2 (op := op) (unit := unit) (· ≡ ·) Φ Ψ l₁ l₂ Equiv.rfl + (fun _ _ _ _ => Monoid.op_proper) hlen hf + +theorem zipIdx (Φ : A × Nat → M) (n : Nat) (l : List A) : bigOpL op unit (fun _ => Φ) (l.zipIdx n) ≡ bigOpL op unit (fun i x => Φ (x, n + i)) l := by induction l generalizing n with | nil => simp only [nil]; exact Equiv.rfl | cons x xs ih => simp only [cons, Nat.add_zero] - refine Monoid.op_proper Equiv.rfl (Equiv.trans (ih (n + 1)) (congr' fun i _ => ?_)) - simp only [Nat.add_assoc, Nat.add_comm 1 i]; exact Equiv.rfl + exact Monoid.op_proper Equiv.rfl + ((ih (n + 1)).trans (congr_forall fun i _ => by simp [Nat.add_assoc, Nat.add_comm 1 i])) -theorem zip_idx_int (Φ : A × Int → M) (n : Int) (l : List A) : +theorem zipIdxInt (Φ : A × Int → M) (n : Int) (l : List A) : bigOpL op unit (fun _ => Φ) (Std.List.zipIdxInt l n) ≡ bigOpL op unit (fun i x => Φ (x, n + (i : Int))) l := by unfold Std.List.zipIdxInt suffices ∀ m, bigOpL op unit (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡ - bigOpL op unit (fun i x => Φ (x, m + (i : Int))) l by exact this n + bigOpL op unit (fun i x => Φ (x, m + (i : Int))) l from this n intro m induction l generalizing m with | nil => simp only [List.mapIdx, nil]; exact Equiv.rfl @@ -263,15 +227,16 @@ theorem zip_idx_int (Φ : A × Int → M) (n : Int) (l : List A) : apply Monoid.op_proper · show Φ (x, (0 : Int) + m) ≡ Φ (x, m + (0 : Int)) rw [Int.zero_add, Int.add_zero] - · have list_eq : (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) = - (List.mapIdx (fun i v => (v, ↑i + (m + 1))) xs) := by + · rw [show (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) = + (List.mapIdx (fun i v => (v, ↑i + (m + 1))) xs) from by apply List.ext_getElem (by simp only [List.length_mapIdx]) intro n hn1 hn2 - simp only [List.getElem_mapIdx]; congr 1; omega - rw [list_eq] - exact (ih (m + 1)).trans (congr' fun i _ => by rw [show m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) from by omega]) + simp only [List.getElem_mapIdx]; congr 1; omega] + apply (ih (m + 1)).trans + apply congr_forall fun i _ => ?_ + rw [show m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) from by omega] -theorem sep_zip_with {B C : Type _} +theorem op_zipWith {B C : Type _} (f : A → B → C) (g1 : C → A) (g2 : C → B) (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) (hg1 : ∀ x y, g1 (f x y) = x) @@ -290,15 +255,15 @@ theorem sep_zip_with {B C : Type _} | cons y ys => simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen simp only [List.zipWith_cons_cons, cons, hg1, hg2] - exact Equiv.trans (Monoid.op_congr_r (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen)) Monoid.op_op_swap + exact (Monoid.op_congr_r (ih _ _ _ hlen)).trans Monoid.op_op_swap /-- Big op over zipped list with separated functions. -/ -theorem sep_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) +theorem op_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) (hlen : l₁.length = l₂.length) : bigOpL op unit (fun i xy => op (Φ i xy.1) (Ψ i xy.2)) (l₁.zip l₂) ≡ op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by - simp [List.zip] - exact sep_zip_with (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen + simp only [List.zip] + exact op_zipWith (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂} @@ -306,7 +271,7 @@ variable [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] variable {B : Type w} /-- Monoid homomorphisms distribute over big ops. -/ -theorem commute {R : M₂ → M₂ → Prop} {f : M₁ → M₂} +theorem hom {R : M₂ → M₂ → Prop} {f : M₁ → M₂} (hom : MonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) (Φ : Nat → B → M₁) (l : List B) : R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by @@ -314,10 +279,11 @@ theorem commute {R : M₂ → M₂ → Prop} {f : M₁ → M₂} | nil => simp only [nil]; exact hom.map_unit | cons x xs ih => simp only [cons] - exact hom.rel_trans (hom.homomorphism _ _) (hom.op_proper (hom.rel_refl _) (ih _)) + apply hom.rel_trans (hom.homomorphism _ _) + exact hom.op_proper (hom.rel_refl _) (ih _) /-- Weak monoid homomorphisms distribute over non-empty big ops. -/ -theorem commute_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} +theorem hom_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} (hom : WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) (Φ : Nat → B → M₁) (l : List B) (hne : l ≠ []) : R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by @@ -329,11 +295,12 @@ theorem commute_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} | nil => simp only [nil] haveI : NonExpansive f := hom.f_ne - exact (hom.rel_proper (NonExpansive.eqv (Monoid.op_right_id _)) - (Monoid.op_right_id _)).mpr (hom.rel_refl _) + apply (hom.rel_proper (NonExpansive.eqv (Monoid.op_right_id _)) + (Monoid.op_right_id _)).mpr + exact hom.rel_refl _ | cons y ys => - exact hom.rel_trans (hom.homomorphism _ _) - (hom.op_proper (hom.rel_refl _) (ih _ (List.cons_ne_nil y ys))) + apply hom.rel_trans (hom.homomorphism _ _) + exact hom.op_proper (hom.rel_refl _) (ih _ (List.cons_ne_nil y ys)) end BigOpL @@ -348,7 +315,7 @@ variable [LawfulFiniteMap M' K] def bigOpM (Φ : K → V → M) (m : M' V) : M := bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m) -theorem bigOpM_equiv (Φ : K → V → M) (m₁ m₂ : M' V) +theorem equiv (Φ : K → V → M) (m₁ m₂ : M' V) (h : PartialMap.equiv m₁ m₂) : bigOpM (op := op) (unit := unit) Φ m₁ ≡ bigOpM (op := op) (unit := unit) Φ m₂ := by simp only [bigOpM] @@ -373,8 +340,8 @@ theorem delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : bigOpM (op := op) (unit := unit) Φ m ≡ op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := by intro hi - exact (bigOpM_equiv Φ m _ (fun k => (LawfulPartialMap.insert_delete_cancel hi k).symm)).trans - (insert Φ (Iris.Std.delete m i) i x (get?_delete_eq rfl)) + apply (BigOpM.equiv Φ m _ (fun k => (LawfulPartialMap.insert_delete_cancel hi k).symm)).trans + exact insert Φ (Iris.Std.delete m i) _ _ (get?_delete_eq rfl) variable {A : Type w} @@ -396,11 +363,11 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) | _, _ => False) → R (bigOpM (op := op) (unit := unit) Φ' m1') (bigOpM (op := op) (unit := unit) Ψ' m2') suffices h : P1 m1 from h m2 Φ Ψ hfg - have hequiv1 : ∀ (m₁ m₂ : M' A), PartialMap.equiv m₁ m₂ → P1 m₁ → P1 m₂ := - fun m₁ m₂ heq hP m2' Φ' Ψ' hfg' => - hR_equiv.trans (hR_sub _ _ (bigOpM_equiv Φ' m₁ m₂ heq).symm) - (hP m2' Φ' Ψ' (fun k => by rw [show get? m₁ k = get? m₂ k from heq k]; exact hfg' k)) - have hemp1 : P1 (∅ : M' A) := by + apply LawfulFiniteMap.induction_on (K := K) (P := P1) + · intro m₁ m₂ heq hP m2' Φ' Ψ' hfg' + apply hR_equiv.trans (hR_sub _ _ (BigOpM.equiv Φ' m₁ m₂ heq).symm) + exact hP m2' Φ' Ψ' (fun k => by rw [heq k]; exact hfg' k) + · show P1 (∅ : M' A) intro m2' Φ' Ψ' hfg' let P2 : M' B → Prop := fun m2'' => ∀ (Φ'' : K → A → M) (Ψ'' : K → B → M), (∀ k, match get? (∅ : M' A) k, get? m2'' k with @@ -409,32 +376,33 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) | _, _ => False) → R (bigOpM (op := op) (unit := unit) Φ'' (∅ : M' A)) (bigOpM (op := op) (unit := unit) Ψ'' m2'') suffices h2 : P2 m2' from h2 Φ' Ψ' hfg' - exact LawfulFiniteMap.induction_on (K := K) (P := P2) - (fun m₁ m₂ heq hP Φ'' Ψ'' hfg'' => - hR_equiv.trans (hP Φ'' Ψ'' (fun k => by rw [show get? m₁ k = get? m₂ k from heq k]; exact hfg'' k)) - (hR_sub _ _ (bigOpM_equiv Ψ'' m₁ m₂ heq))) - (fun _ _ _ => by - show R (bigOpM (op := op) (unit := unit) _ (∅ : M' A)) - (bigOpM (op := op) (unit := unit) _ (∅ : M' B)) - rw [empty, empty]; exact hR_sub unit unit Equiv.rfl) - (fun k _ _ _ _ Φ'' Ψ'' hfg'' => by - have := hfg'' k; simp only [show get? (∅ : M' A) k = none from get?_empty k, get?_insert_eq rfl] at this) - m2' - have hins1 : ∀ (i : K) (x : A) (m : M' A), get? m i = none → P1 m → P1 (Iris.Std.insert m i x) := by - intro k x1 m1' hm1'k IH m2' Φ' Ψ' hfg' + apply LawfulFiniteMap.induction_on (K := K) (P := P2) + · intro m₁ m₂ heq hP Φ'' Ψ'' hfg'' + apply hR_equiv.trans (hP Φ'' Ψ'' (fun k => by rw [heq k]; exact hfg'' k)) + exact hR_sub _ _ (BigOpM.equiv Ψ'' m₁ m₂ heq) + · show P2 (∅ : M' B) + intro _ _ _ + show R (bigOpM (op := op) _ (∅ : M' A)) (bigOpM (op := op) _ (∅ : M' B)) + rw [empty, empty]; exact hR_sub unit unit Equiv.rfl + · intro k _ _ _ _ Φ'' Ψ'' hfg'' + have := hfg'' k + rw [show get? (∅ : M' A) k = none from get?_empty k, get?_insert_eq rfl] at this + exact this.elim + · intro k x1 m1' hm1'k IH m2' Φ' Ψ' hfg' have hfg_k := hfg' k rw [get?_insert_eq rfl] at hfg_k cases hm2k : get? m2' k with | none => rw [hm2k] at hfg_k; cases hfg_k | some x2 => rw [hm2k] at hfg_k - exact hR_equiv.trans (hR_sub _ _ (insert Φ' m1' k x1 hm1'k)) - (hR_equiv.trans (hR_op _ _ _ _ hfg_k (IH _ _ _ fun k' => by - by_cases hkk' : k = k' - · subst hkk'; rw [get?_delete_eq rfl, hm1'k]; trivial - · have := hfg' k'; rw [get?_insert_ne hkk'] at this; rwa [get?_delete_ne hkk'])) - (hR_sub _ _ (Equiv.symm (delete Ψ' m2' k x2 hm2k)))) - exact LawfulFiniteMap.induction_on (K := K) (P := P1) hequiv1 hemp1 hins1 m1 + refine hR_equiv.trans (hR_sub _ _ (insert Φ' m1' k x1 hm1'k)) ?_ + apply hR_equiv.trans _ (hR_sub _ _ (Equiv.symm (delete Ψ' m2' k x2 hm2k))) + apply hR_op _ _ _ _ hfg_k + apply IH + intro k' + by_cases hkk' : k = k' + · subst hkk'; rw [get?_delete_eq rfl, hm1'k]; trivial + · have := hfg' k'; rw [get?_insert_ne hkk'] at this; rwa [get?_delete_ne hkk'] omit [Monoid M op unit] in theorem gen_proper {M : Type u} {op : M → M → M} {unit : M} (R : M → M → Prop) @@ -444,37 +412,24 @@ theorem gen_proper {M : Type u} {op : M → M → M} {unit : M} (R : M → M → (hf : ∀ k x, get? m k = some x → R (Φ k x) (Ψ k x)) : R (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by simp only [bigOpM] - apply BigOpL.gen_proper_2 (op := op) (unit := unit) R - · exact hR_refl unit - · exact hR_op - · rfl - · intro i x y hx hy - rw [hx] at hy; cases hy - exact hf x.1 x.2 (toList_get.mp (List.mem_iff_getElem?.mpr ⟨i, hx⟩)) + apply BigOpL.gen_proper_2 (op := op) (unit := unit) R _ _ _ _ (hR_refl unit) hR_op rfl + intro i x y hx hy; rw [hx] at hy; cases hy + exact hf x.1 x.2 (toList_get.mp (List.mem_iff_getElem?.mpr ⟨i, hx⟩)) theorem ext {M : Type u} (op : M → M → M) (unit : M) (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, get? m k = some x → Φ k x = Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Ψ m := by - apply gen_proper (R := (· = ·)) - · intro _; rfl - · intros _ _ _ _ ha hb; rw [ha, hb] - · exact hf + bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Ψ m := + gen_proper (R := (· = ·)) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) hf -theorem ne (Φ Ψ : K → V → M) (m : M' V) (n : Nat) +theorem dist (Φ Ψ : K → V → M) (m : M' V) (n : Nat) (hf : ∀ k x, get? m k = some x → Φ k x ≡{n}≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := by - apply gen_proper (R := (· ≡{n}≡ ·)) - · intro _; exact Dist.rfl - · intros a a' b b' ha hb; exact Monoid.op_ne_dist ha hb - · exact hf + bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := + gen_proper (R := (· ≡{n}≡ ·)) _ _ _ (fun _ => Dist.rfl) (fun _ _ _ _ => Monoid.op_ne_dist) hf theorem proper (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, get? m k = some x → Φ k x ≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := by - apply gen_proper (R := (· ≡ ·)) - · intro _; exact Equiv.rfl - · intros a a' b b' ha hb; exact Monoid.op_proper ha hb - · exact hf + bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := + gen_proper (R := (· ≡ ·)) _ _ _ (fun _ => Equiv.rfl) (fun _ _ _ _ => Monoid.op_proper) hf theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → M) (m1 m2 : M' A) (hm : ∀ k, get? m1 k = get? m2 k) @@ -484,30 +439,21 @@ theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → y1 ≡ y2 → Φ k y1 ≡ Ψ k y2) : bigOpM (op := op) (unit := unit) Φ m1 ≡ bigOpM (op := op) (unit := unit) Ψ m2 := by - apply gen_proper_2 (R := (· ≡ ·)) - · intros _ _ h; exact h - · exact equiv_eqv - · intros a a' b b' ha hb; exact Monoid.op_proper ha hb - · intro k - have hlk := hm k - cases hm1k : get? m1 k with - | none => - rw [hm1k] at hlk - rw [← hlk] - trivial - | some y1 => - rw [hm1k] at hlk - cases hm2k : get? m2 k with - | none => rw [hm2k] at hlk; cases hlk - | some y2 => - rw [hm2k] at hlk - cases hlk - exact hf k y1 y1 hm1k hm2k Equiv.rfl - -theorem ne_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat) + apply gen_proper_2 (R := (· ≡ ·)) _ _ _ _ (fun _ _ h => h) equiv_eqv (fun _ _ _ _ => Monoid.op_proper) + intro k + have hlk := hm k + cases hm1k : get? m1 k with + | none => rw [hm1k] at hlk; rw [← hlk]; trivial + | some y1 => + rw [hm1k] at hlk + cases hm2k : get? m2 k with + | none => rw [hm2k] at hlk; cases hlk + | some y2 => rw [hm2k] at hlk; cases hlk; exact hf k y1 y1 hm1k hm2k Equiv.rfl + +theorem dist_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat) (hf : ∀ k x, Φ k x ≡{n}≡ Ψ k x) : bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := - ne _ _ _ _ fun k x _ => hf k x + dist _ _ _ _ fun k x _ => hf k x theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, Φ k x ≡ Ψ k x) : @@ -517,66 +463,58 @@ theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V) omit [Monoid M op unit] in theorem to_list (Φ : K → V → M) (m : M' V) : bigOpM (op := op) (unit := unit) Φ m ≡ - bigOpL op unit (fun _ kx => Φ kx.1 kx.2) (toList (K := K) m) := by - rfl + bigOpL op unit (fun _ kx => Φ kx.1 kx.2) (toList (K := K) m) := by rfl theorem of_list [DecidableEq K] (Φ : K → V → M) (l : List (K × V)) (hnodup : NoDupKeys l) : bigOpM (op := op) (unit := unit) Φ (PartialMap.ofList l : M' V) ≡ bigOpL op unit (fun _ kx => Φ kx.1 kx.2) l := by - simp only [bigOpM] - apply BigOpL.perm - exact LawfulFiniteMap.toList_ofList hnodup + simp only [bigOpM]; exact BigOpL.perm _ (LawfulFiniteMap.toList_ofList hnodup) theorem singleton (Φ : K → V → M) (i : K) (x : V) : bigOpM (op := op) (unit := unit) Φ (PartialMap.singleton (M := M') i x) ≡ Φ i x := by - have h := insert (op := op) (unit := unit) Φ (∅ : M' V) i x (get?_empty i) - rw [empty] at h - exact h.trans (Monoid.op_right_id _) + rw [show PartialMap.singleton (M := M') i x = Iris.Std.insert (∅ : M' V) i x from rfl] + apply (insert Φ (∅ : M' V) i x (get?_empty i)).trans + rw [empty]; exact Monoid.op_right_id _ -theorem unit_const [DecidableEq K] (m : M' V) : +theorem const_unit [DecidableEq K] (m : M' V) : bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m ≡ unit := by let P : M' V → Prop := fun m' => bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m' ≡ unit - have hequiv : ∀ m₁ m₂ : M' V, PartialMap.equiv m₁ m₂ → P m₁ → P m₂ := - fun m₁ m₂ heq h => Equiv.trans (bigOpM_equiv _ m₁ m₂ heq).symm h - have hemp : P (∅ : M' V) := by show _ ≡ _; rw [empty] - have hins : ∀ i x m, get? m i = none → P m → P (Iris.Std.insert m i x) := - fun i x m' hm' IH => - let h_ins := insert (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m' i x hm' - Equiv.trans h_ins (Equiv.trans (Monoid.op_proper Equiv.rfl IH) (Monoid.op_left_id unit)) - show P m - exact LawfulFiniteMap.induction_on (K := K) (P := P) hequiv hemp hins m + show P m; apply LawfulFiniteMap.induction_on (K := K) (P := P) + · intro m₁ m₂ heq h; exact (BigOpM.equiv _ _ _ heq).symm.trans h + · show P (∅ : M' V); show _ ≡ _; rw [empty] + · intro i x m' hm' IH + exact (insert _ _ _ _ hm').trans ((Monoid.op_proper Equiv.rfl IH).trans (Monoid.op_left_id _)) theorem map (h : V → B) (Φ : K → B → M) (m : M' V) : bigOpM (op := op) (unit := unit) Φ (PartialMap.map h m) ≡ bigOpM (op := op) (unit := unit) (fun k v => Φ k (h v)) m := by simp only [bigOpM] exact (BigOpL.perm _ LawfulFiniteMap.toList_map).trans - (BigOpL.map (op := op) (unit := unit) (fun kv => (kv.1, h kv.2)) (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m)) + (BigOpL.map (op := op) _ _ (toList (K := K) m)) theorem filter_map (h : V → Option V) (Φ : K → V → M) (m : M' V) (hinj : Function.Injective h) : bigOpM (op := op) (unit := unit) Φ (PartialMap.filterMap h m) ≡ bigOpM (op := op) (unit := unit) (fun k v => (h v).elim unit (Φ k)) m := by simp only [bigOpM] - refine (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans ?_ - refine (BigOpL.filter_map (op := op) (unit := unit) (fun kv => (h kv.2).map (kv.1, ·)) - (fun kv => Φ kv.1 kv.2) (toList (K := K) m)).trans ?_ - exact BigOpL.congr' fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map] + exact (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans + ((BigOpL.filter_map (op := op) _ _ _).trans + (BigOpL.congr_forall fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map])) theorem insert_delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x) ≡ - op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := - (bigOpM_equiv Φ _ _ (fun k => (LawfulPartialMap.insert_delete (i := i) (x := x) (m := m) k).symm)).trans - (insert Φ (Iris.Std.delete m i) i x (get?_delete_eq rfl)) + op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := by + exact (BigOpM.equiv _ _ _ fun k => (LawfulPartialMap.insert_delete k).symm).trans + (insert _ _ _ _ (get?_delete_eq rfl)) theorem insert_override (Φ : K → A → M) (m : M' A) (i : K) (x x' : A) : get? m i = some x → Φ i x ≡ Φ i x' → bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x') ≡ bigOpM (op := op) (unit := unit) Φ m := by intro hi hΦ - exact (insert_delete Φ m i x').trans - ((Monoid.op_proper hΦ.symm Equiv.rfl).trans (delete Φ m i x hi).symm) + apply (insert_delete Φ m i x').trans + exact (Monoid.op_proper hΦ.symm Equiv.rfl).trans (delete Φ m i x hi).symm theorem fn_insert [DecidableEq K] {B : Type w} (g : K → V → B → M) (f : K → B) (m : M' V) (i : K) (x : V) (b : B) (hi : get? m i = none) : @@ -594,11 +532,17 @@ theorem fn_insert' [DecidableEq K] (f : K → M) (m : M' V) (i : K) (x : V) (P : refine (insert _ m i x hi).trans (Monoid.op_proper (by simp) (proper _ _ _ fun k _ hk => ?_)) simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk] -private theorem filter_list_aux (Φ : K × V → M) (φ : K → V → Bool) (l : List (K × V)) : - bigOpL op unit (fun _ kv => Φ kv) (l.filter (fun kv => φ kv.1 kv.2)) ≡ - bigOpL op unit (fun _ kv => if φ kv.1 kv.2 then Φ kv else unit) l := by +theorem filter (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) : + bigOpM (op := op) (unit := unit) Φ (PartialMap.filter φ m) ≡ + bigOpM (op := op) (unit := unit) (fun k x => if φ k x then Φ k x else unit) m := by + unfold bigOpM + refine (BigOpL.perm _ LawfulFiniteMap.toList_filter).trans ?_ + suffices ∀ l : List (K × V), + bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (l.filter (fun kv => φ kv.1 kv.2)) ≡ + bigOpL op unit (fun _ kv => if φ kv.1 kv.2 then Φ kv.1 kv.2 else unit) l from this _ + intro l induction l with - | nil => simp only [List.filter, BigOpL.nil]; exact Equiv.rfl + | nil => exact Equiv.rfl | cons kv kvs ih => simp only [List.filter] cases hp : φ kv.1 kv.2 with @@ -606,22 +550,9 @@ private theorem filter_list_aux (Φ : K × V → M) (φ : K → V → Bool) (l : simp only [BigOpL.cons, hp] exact Equiv.trans ih (Equiv.symm (Monoid.op_left_id _)) | true => - simp only [BigOpL.cons, hp] + simp only [BigOpL.cons, hp, ite_true] exact Monoid.op_congr_r ih -theorem filter' (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.filter φ m) ≡ - bigOpM (op := op) (unit := unit) (fun k x => if φ k x then Φ k x else unit) m := by - unfold bigOpM - have hperm := LawfulFiniteMap.toList_filter (M := M') (K := K) (V := V) (φ := φ) (m := m) - have heq : bigOpL op unit (fun _ kv => Φ kv.1 kv.2) - (toList (K := K) (PartialMap.filter φ m)) ≡ - bigOpL op unit (fun _ kv => Φ kv.1 kv.2) - ((toList (K := K) m).filter (fun kv => φ kv.1 kv.2)) := - BigOpL.perm _ hperm - refine Equiv.trans heq ?_ - exact filter_list_aux (fun kv => Φ kv.1 kv.2) φ (toList (K := K) m) - theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : PartialMap.disjoint m1 m2) : bigOpM (op := op) (unit := unit) Φ (m1 ∪ m2) ≡ op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) := by @@ -629,82 +560,68 @@ theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : Parti PartialMap.disjoint m1 m2 → bigOpM (op := op) (unit := unit) Φ (PartialMap.union m1 m2) ≡ op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) - have hequiv : ∀ m₁ m₂', PartialMap.equiv m₁ m₂' → P m₁ → P m₂' := by - intro m₁ m₂' heq hP hdisj' - have hunion : PartialMap.equiv (PartialMap.union m₁ m2) (PartialMap.union m₂' m2) := - fun k => by show get? _ k = get? _ k; rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k] - exact (bigOpM_equiv Φ _ _ hunion).symm.trans - ((hP fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩).trans - (Monoid.op_proper (bigOpM_equiv Φ m₁ m₂' heq) Equiv.rfl)) suffices h : P m1 from h hdisj - have hemp : P (∅ : M' V) := fun _ => by - rw [empty] - exact (bigOpM_equiv Φ _ _ (fun k => by - show get? (PartialMap.union (∅ : M' V) m2) k = get? m2 k - rw [LawfulPartialMap.get?_union, show get? (∅ : M' V) k = none from get?_empty k]; simp)).trans - (Monoid.op_left_id _).symm - have hins : ∀ (i : K) (x : V) (m : M' V), get? m i = none → P m → P (Iris.Std.insert m i x) := by - intro i x m hi_none IH hdisj' - have hi_m2 : get? m2 i = none := by - have := (PartialMap.disjoint_iff _ m2).mp hdisj' i - cases this with + apply LawfulFiniteMap.induction_on (K := K) (P := P) + · intro m₁ m₂' heq hP hdisj' + refine Equiv.trans ?_ ((hP fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩).trans + (Monoid.op_proper (BigOpM.equiv Φ m₁ m₂' heq) Equiv.rfl)) + apply Equiv.symm + apply BigOpM.equiv Φ _ _ fun k => ?_ + show get? _ k = get? _ k + rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k] + · show P (∅ : M' V) + intro _; rw [empty] + refine Equiv.trans ?_ (Monoid.op_left_id _).symm + apply BigOpM.equiv Φ _ _ + intro k; show get? (PartialMap.union (∅ : M' V) m2) k = get? m2 k + rw [LawfulPartialMap.get?_union, show get? (∅ : M' V) k = none from get?_empty k]; simp + · intro i x m hi_none IH hdisj' + apply (BigOpM.equiv Φ _ _ fun k => (LawfulPartialMap.union_insert_left k).symm).trans + apply (insert Φ (m ∪ m2) i x (by + show get? (PartialMap.union m m2) i = none + rw [LawfulPartialMap.get?_union_none] + refine ⟨hi_none, ?_⟩ + cases (PartialMap.disjoint_iff _ m2).mp hdisj' i with | inl h => rw [get?_insert_eq rfl] at h; cases h - | inr h => exact h - have hm_disj : PartialMap.disjoint m m2 := fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by + | inr h => exact h)).trans + apply (Monoid.op_congr_r (IH fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by by_cases h : i = k · subst h; rw [hi_none] at hk1; cases hk1 - · rwa [get?_insert_ne h], hk2⟩ - have h_none : get? (m ∪ m2) i = none := by - show get? (PartialMap.union m m2) i = none - rw [LawfulPartialMap.get?_union_none]; exact ⟨hi_none, hi_m2⟩ - exact (bigOpM_equiv Φ _ _ (fun k => (LawfulPartialMap.union_insert_left (i := i) (x := x) (m₁ := m) (m₂ := m2) k).symm)).trans - ((insert Φ (m ∪ m2) i x h_none).trans - ((Monoid.op_congr_r (IH hm_disj)).trans - ((Monoid.op_assoc _ _ _).symm.trans - (Monoid.op_congr_l (insert Φ m i x hi_none).symm)))) - exact LawfulFiniteMap.induction_on (K := K) (P := P) hequiv hemp hins m1 - -theorem op_distr (Φ Ψ : K → V → M) (m : M' V) : + · rwa [get?_insert_ne h], hk2⟩)).trans + exact (Monoid.op_assoc _ _ _).symm.trans (Monoid.op_congr_l (insert Φ m i x hi_none).symm) + +theorem op_distrib (Φ Ψ : K → V → M) (m : M' V) : bigOpM (op := op) (unit := unit) (fun k x => op (Φ k x) (Ψ k x)) m ≡ op (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by - simp only [bigOpM] - exact BigOpL.op_distr (op := op) (unit := unit) - (fun _ kv => Φ kv.1 kv.2) (fun _ kv => Ψ kv.1 kv.2) (toList (K := K) m) - -private theorem closed_aux [DecidableEq K] (P : M → Prop) (Φ : K → V → M) - (hproper : ∀ x y, x ≡ y → (P x ↔ P y)) - (hunit : P unit) - (hop : ∀ x y, P x → P y → P (op x y)) : - ∀ (m' : M' V), (∀ k' x', get? m' k' = some x' → P (Φ k' x')) → - P (bigOpM (op := op) (unit := unit) Φ m') := by - intro m' hf' - let Q : M' V → Prop := fun m'' => (∀ k x, get? m'' k = some x → P (Φ k x)) → - P (bigOpM (op := op) (unit := unit) Φ m'') - have hequiv_Q : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → Q m₁ → Q m₂ := - fun m₁ m₂ heq hQ hf => (hproper _ _ (bigOpM_equiv Φ m₁ m₂ heq)).mp - (hQ fun k x hget => hf k x ((heq k) ▸ hget)) - have hemp_Q : Q (∅ : M' V) := fun _ => by - show P (bigOpM (op := op) (unit := unit) Φ (∅ : M' V)); rw [empty]; exact hunit - have hins_Q : ∀ i x m, get? m i = none → Q m → Q (Iris.Std.insert m i x) := by - intro k x m'' hm'' IH hf'' - exact (hproper _ _ (insert (op := op) (unit := unit) Φ m'' k x hm'')).mpr - (hop _ _ (hf'' _ _ (get?_insert_eq rfl)) (IH fun k' x' hget' => by - by_cases heq : k = k' - · subst heq; rw [hget'] at hm''; cases hm'' - · exact hf'' k' x' (by rw [get?_insert_ne heq]; exact hget'))) - exact (LawfulFiniteMap.induction_on (K := K) (P := Q) hequiv_Q hemp_Q hins_Q m') hf' + simp only [bigOpM]; exact BigOpL.op_distrib _ _ _ theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V) (hproper : ∀ x y, x ≡ y → (P x ↔ P y)) (hunit : P unit) (hop : ∀ x y, P x → P y → P (op x y)) (hf : ∀ k x, get? m k = some x → P (Φ k x)) : - P (bigOpM (op := op) (unit := unit) Φ m) := - closed_aux P Φ hproper hunit hop m hf + P (bigOpM (op := op) (unit := unit) Φ m) := by + let Q : M' V → Prop := fun m'' => (∀ k x, get? m'' k = some x → P (Φ k x)) → + P (bigOpM (op := op) (unit := unit) Φ m'') + suffices h : Q m from h hf + apply LawfulFiniteMap.induction_on (K := K) (P := Q) + · intro m₁ m₂ heq hQ hf' + apply (hproper _ _ (BigOpM.equiv Φ m₁ m₂ heq)).mp + exact hQ fun k x hget => hf' k x ((heq k) ▸ hget) + · show Q (∅ : M' V) + intro _; show P (bigOpM Φ (∅ : M' V)); rw [empty]; exact hunit + · intro k x m'' hm'' IH hf'' + apply (hproper _ _ (insert Φ m'' k x hm'')).mpr + apply hop _ _ (hf'' _ _ (get?_insert_eq rfl)) + apply IH; intro k' x' hget' + by_cases heq : k = k' + · subst heq; rw [hget'] at hm''; cases hm'' + · apply hf'' k' x' + rw [get?_insert_ne heq]; exact hget' -- TODO: kmap and map_seq are skipped for now -theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _} +theorem op_zipWith {A : Type _} {B : Type _} {C : Type _} (f : A → B → C) (g1 : C → A) (g2 : C → B) (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) (hg1 : ∀ x y, g1 (f x y) = x) @@ -713,10 +630,11 @@ theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _} bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k (g1 xy)) (h2 k (g2 xy))) (PartialMap.zipWith f m1 m2) ≡ op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by - have h_op := @op_distr _ _ op unit _ _ _ _ _ - (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy)) (PartialMap.zipWith f m1 m2) - apply Equiv.trans h_op - have map_g1_eq : PartialMap.equiv (PartialMap.map g1 (PartialMap.zipWith f m1 m2)) m1 := by + refine (op_distrib (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy)) + (PartialMap.zipWith f m1 m2)).trans ?_ + apply Monoid.op_proper + · refine (map g1 h1 (PartialMap.zipWith f m1 m2)).symm.trans ?_ + apply BigOpM.equiv h1 _ _ intro k simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith] cases h1k : get? m1 k with @@ -726,7 +644,8 @@ theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _} cases h2k : get? m2 k with | none => rw [h2k] at this; simp at this | some b => simp [Option.bind, Option.map, hg1] - have map_g2_eq : PartialMap.equiv (PartialMap.map g2 (PartialMap.zipWith f m1 m2)) m2 := by + · refine (map g2 h2 (PartialMap.zipWith f m1 m2)).symm.trans ?_ + apply BigOpM.equiv h2 _ _ intro k simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith] cases h1k : get? m1 k with @@ -743,21 +662,15 @@ theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _} have := (hdom k).mp (by rw [h1k]; simp) rw [h2k] at this; simp at this | some b => simp [Option.bind, Option.map, hg2] - apply Monoid.op_proper - · have h1_fmap := map (op := op) (unit := unit) g1 h1 (PartialMap.zipWith f m1 m2) - exact Equiv.trans (Equiv.symm h1_fmap) (bigOpM_equiv h1 _ _ map_g1_eq) - · have h2_fmap := map (op := op) (unit := unit) g2 h2 (PartialMap.zipWith f m1 m2) - exact Equiv.trans (Equiv.symm h2_fmap) (bigOpM_equiv h2 _ _ map_g2_eq) -theorem sep_zip {A : Type _} {B : Type _} +theorem op_zip {A : Type _} {B : Type _} (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) : bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k xy.1) (h2 k xy.2)) (PartialMap.zip m1 m2) ≡ op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by simp only [PartialMap.zip] - exact sep_zip_with (op := op) (unit := unit) Prod.mk Prod.fst Prod.snd h1 h2 m1 m2 - (fun _ _ => rfl) (fun _ _ => rfl) hdom + exact op_zipWith _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hdom end BigOpM diff --git a/src/Iris/Std/List.lean b/src/Iris/Std/List.lean index 355007111..4f1aa8d80 100644 --- a/src/Iris/Std/List.lean +++ b/src/Iris/Std/List.lean @@ -13,8 +13,7 @@ not available in Lean core. namespace Iris.Std.List -/-- List equivalence relation parameterized by an element equivalence relation. - Corresponds to Rocq's `list_equiv`. -/ +/-- List equivalence relation parameterized by an element equivalence relation. -/ inductive Equiv {α : Type _} (R : α → α → Prop) : List α → List α → Prop where | nil : Equiv R [] [] | cons {x y : α} {l k : List α} : R x y → Equiv R l k → Equiv R (x :: l) (y :: k) @@ -22,80 +21,4 @@ inductive Equiv {α : Type _} (R : α → α → Prop) : List α → List α → def zipIdxInt {α : Type _} (l : List α) (n : Int) : List (α × Int) := l.mapIdx (fun i v => (v, (i : Int) + n)) -/-- For a Nodup list, erasing an element removes it completely. -/ -theorem not_mem_erase_self_of_nodup {α : Type _} [DecidableEq α] (x : α) (l : List α) - (hnd : l.Nodup) : x ∉ l.erase x := by - induction l with - | nil => exact List.not_mem_nil - | cons y ys ih => - simp only [List.erase_cons] - rw [List.nodup_cons] at hnd - split - · next h => - have heq : y = x := eq_of_beq h - rw [← heq] - exact hnd.1 - · next h => - simp only [List.mem_cons] - intro hor - cases hor with - | inl heq => - have : (y == x) = true := beq_iff_eq.mpr heq.symm - exact absurd this h - | inr hmem => exact ih hnd.2 hmem - -/-- Two Nodup lists with the same membership are permutations of each other. - Corresponds to Rocq's `NoDup_Permutation`. -/ -theorem perm_of_nodup_of_mem_iff {α : Type _} [DecidableEq α] - {l₁ l₂ : List α} (hnd₁ : l₁.Nodup) (hnd₂ : l₂.Nodup) - (hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁.Perm l₂ := by - induction l₁ generalizing l₂ with - | nil => - cases l₂ with - | nil => exact List.Perm.refl [] - | cons y ys => - have : y ∈ ([] : List α) := (hmem y).mpr List.mem_cons_self - exact absurd this List.not_mem_nil - | cons x xs ih => - have hx_in_l₂ : x ∈ l₂ := (hmem x).mp List.mem_cons_self - have hperm₂ : l₂.Perm (x :: l₂.erase x) := List.perm_cons_erase hx_in_l₂ - rw [List.nodup_cons] at hnd₁ - have hx_notin_xs : x ∉ xs := hnd₁.1 - have hnd_xs : xs.Nodup := hnd₁.2 - have hnd_erase : (l₂.erase x).Nodup := hnd₂.erase x - have hmem_erase : ∀ y, y ∈ xs ↔ y ∈ l₂.erase x := by - intro y - constructor - · intro hy - have hne : y ≠ x := fun heq => hx_notin_xs (heq ▸ hy) - have hy_l₂ : y ∈ l₂ := (hmem y).mp (List.mem_cons_of_mem x hy) - exact (List.mem_erase_of_ne hne).mpr hy_l₂ - · intro hy - have hne : y ≠ x := by - intro heq - rw [heq] at hy - exact not_mem_erase_self_of_nodup x l₂ hnd₂ hy - have hy_l₂ : y ∈ l₂ := List.mem_of_mem_erase hy - have hy_l₁ : y ∈ x :: xs := (hmem y).mpr hy_l₂ - cases List.mem_cons.mp hy_l₁ with - | inl heq => exact absurd heq hne - | inr h => exact h - have hperm_xs : xs.Perm (l₂.erase x) := ih hnd_xs hnd_erase hmem_erase - exact (List.Perm.cons x hperm_xs).trans hperm₂.symm - - -theorem nodup_of_nodup_map_fst {α β : Type _} (l : List (α × β)) - (h : (l.map Prod.fst).Nodup) : l.Nodup := by - induction l with - | nil => exact List.nodup_nil - | cons x xs ih => - rw [List.nodup_cons] - constructor - · intro hx - rw [List.map_cons, List.nodup_cons] at h - have : x.1 ∈ xs.map Prod.fst := List.mem_map_of_mem (f := Prod.fst) hx - exact h.1 this - · rw [List.map_cons, List.nodup_cons] at h - exact ih h.2 - end Iris.Std.List diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean index d46e8af2d..b0225d47d 100644 --- a/src/Iris/Std/PartialMap.lean +++ b/src/Iris/Std/PartialMap.lean @@ -823,31 +823,24 @@ theorem ofList_toList [DecidableEq K] {m : M V} : cases h ▸ toList_get.mp Hk · exact get?_ofList_some (toList_get.mpr h) toList_noDupKeys -private theorem induction_on_aux - {P : M V → Prop} +theorem induction_on [DecidableEq K] {P : M V → Prop} + (hequiv : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → P m₁ → P m₂) (hemp : P PartialMap.empty) (hins : ∀ i x m, get? m i = none → P m → P (PartialMap.insert m i x)) - (l : List (K × V)) (hnd : NoDupKeys l) : P (ofList l) := by + (m : M V) : P m := by + apply hequiv _ _ ofList_toList + suffices ∀ l, NoDupKeys l → P (ofList l) from this _ toList_noDupKeys + intro l hnd induction l with | nil => simpa [ofList] using hemp | cons kv rest ih => rw [ofList_cons] apply hins kv.1 kv.2 - · have hnd_rest := noDupKeys_cons hnd - refine get?_ofList_none (M := M) ?_ hnd_rest + · refine get?_ofList_none (M := M) ?_ (noDupKeys_cons hnd) intro ⟨v, hv⟩ - have hnotin : kv.1 ∉ rest.map Prod.fst := - (List.nodup_cons.mp hnd).1 - exact hnotin (List.mem_map_of_mem (f := Prod.fst) (a := (kv.1, v)) hv) + exact (List.nodup_cons.mp hnd).1 (List.mem_map_of_mem (f := Prod.fst) (a := (kv.1, v)) hv) · exact ih (noDupKeys_cons hnd) -theorem induction_on [DecidableEq K] {P : M V → Prop} - (hequiv : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → P m₁ → P m₂) - (hemp : P PartialMap.empty) - (hins : ∀ i x m, get? m i = none → P m → P (PartialMap.insert m i x)) - (m : M V) : P m := - hequiv _ _ ofList_toList (induction_on_aux hemp hins (toList (K := K) m) toList_noDupKeys) - theorem mem_of_mem_ofList [DecidableEq K] {l : List (K × V)} {i : K} {x : V} (H : get? (ofList l : M V) i = some x) : (i, x) ∈ l := by induction l From d8215c1696db5b46ffdc32e01bcaefc454b6999f Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Wed, 4 Mar 2026 21:01:35 +0100 Subject: [PATCH 3/4] Update PORTING.md --- PORTING.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/PORTING.md b/PORTING.md index 8d7045bfb..4e2a8e486 100644 --- a/PORTING.md +++ b/PORTING.md @@ -17,7 +17,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p - [x] Updates - [x] Functors - [ ] `big_op.v` - - TBD (Zongyuan?) + - [x] Lists + - [x] Maps + - [ ] Sets + - [ ] Multisets + - [ ] Homomorphisms - [ ] `cmra.v` - [x] Lemmas - [ ] Total CMRA construction @@ -72,7 +76,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p - [ ] `max_prefix_list.v` - [ ] Lemmas - [ ] Functors -- [ ] `monoid.v` +- [x] `monoid.v` - [ ] `mra.v` - [x] `numbers.v` - [ ] `ofe.v` @@ -430,5 +434,3 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p - [ ] `language.v` - [ ] `ectx_language.v` - [ ] `ectxi_language.v` - - From fd9c6532a5ca0f0d268e19e07721fbd501bf4e09 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Thu, 5 Mar 2026 11:10:15 +0100 Subject: [PATCH 4/4] Add notations --- src/Iris/Algebra/BigOp.lean | 412 ++++++++++++++++++----------------- src/Iris/Algebra/Monoid.lean | 24 +- 2 files changed, 227 insertions(+), 209 deletions(-) diff --git a/src/Iris/Algebra/BigOp.lean b/src/Iris/Algebra/BigOp.lean index 957076fe2..be936bfb3 100644 --- a/src/Iris/Algebra/BigOp.lean +++ b/src/Iris/Algebra/BigOp.lean @@ -16,103 +16,125 @@ These are parameterized by a monoid operation and include theorems about their p -/ open OFE +open Iris.Std -def bigOpL {M : Type u} {A : Type v} (op : M → M → M) (unit : M) +def bigOpL {M : Type u} {A : Type v} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit] (Φ : Nat → A → M) (l : List A) : M := match l with | [] => unit - | x :: xs => op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs) + | x :: xs => op (Φ 0 x) (bigOpL op (fun n => Φ (n + 1)) xs) + +def bigOpM {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit] +{K : Type _} {V : Type _} (Φ : K → V → M) {M' : Type _ → Type _} [LawfulFiniteMap M' K] +(m : M' V) : M := + bigOpL op (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m) + +/-- Big op over list with index: `[^ op list] k ↦ x ∈ l, P` -/ +scoped syntax atomic("[^") term " list]" ident " ↦ " ident " ∈ " term ", " term : term +/-- Big op over list without index: `[^ op list] x ∈ l, P` -/ +scoped syntax atomic("[^") term " list]" ident " ∈ " term ", " term : term + +/-- Big op over map with key: `[^ op map] k ↦ x ∈ m, P` -/ +scoped syntax atomic("[^") term " map]" ident " ↦ " ident " ∈ " term ", " term : term +/-- Big op over map without key: `[^ op map] x ∈ m, P` -/ +scoped syntax atomic("[^") term " map]" ident " ∈ " term ", " term : term + +scoped macro_rules + | `([^ $o list] $k ↦ $x ∈ $l, $P) => `(bigOpL $o (fun $k $x => $P) $l) + | `([^ $o list] $x ∈ $l, $P) => `(bigOpL $o (fun _ $x => $P) $l) + | `([^ $o map] $k ↦ $x ∈ $m, $P) => `(bigOpM $o (fun $k $x => $P) $m) + | `([^ $o map] $x ∈ $m, $P) => `(bigOpM $o (fun _ $x => $P) $m) namespace BigOpL -variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit] +variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit] -omit [OFE M] [Monoid M op unit] in @[simp] theorem nil (Φ : Nat → A → M) : - bigOpL op unit Φ ([] : List A) = unit := rfl + ([^ op list] k ↦ x ∈ ([] : List A), Φ k x) = unit := rfl -omit [OFE M] [Monoid M op unit] in -@[simp] theorem cons (Φ : Nat → A → M) (x : A) (xs : List A) : - bigOpL op unit Φ (x :: xs) = op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs) := rfl +@[simp] theorem cons (Φ : Nat → A → M) (a : A) (as : List A) : + ([^ op list] k ↦ x ∈ a :: as, Φ k x) = op (Φ 0 a) ([^ op list] k ↦ x ∈ as, Φ (k + 1) x) := rfl -@[simp] theorem singleton (Φ : Nat → A → M) (x : A) : - bigOpL op unit Φ [x] ≡ Φ 0 x := by - simp only [cons, nil]; exact Monoid.op_right_id _ +@[simp] theorem singleton (Φ : Nat → A → M) (a : A) : + ([^ op list] k ↦ x ∈ [a], Φ k x) ≡ Φ 0 a := by + simp only [cons, nil]; exact MonoidOps.op_right_id _ theorem congr {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, l[i]? = some x → Φ i x ≡ Ψ i x) : - bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := by + ([^ op list] k ↦ x ∈ l, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Ψ k x) := by induction l generalizing Φ Ψ with | nil => exact Equiv.rfl | cons y ys ih => simp only [cons] - apply Monoid.op_proper (h 0 y rfl) + apply MonoidOps.op_proper (h 0 y rfl) exact ih fun i x hget => h (i + 1) x hget theorem congr_dist {Φ Ψ : Nat → A → M} {l : List A} {n : Nat} (h : ∀ i x, l[i]? = some x → Φ i x ≡{n}≡ Ψ i x) : - bigOpL op unit Φ l ≡{n}≡ bigOpL op unit Ψ l := by + ([^ op list] k ↦ x ∈ l, Φ k x) ≡{n}≡ ([^ op list] k ↦ x ∈ l, Ψ k x) := by induction l generalizing Φ Ψ with | nil => exact Dist.rfl | cons y ys ih => simp only [cons] - apply Monoid.op_ne_dist (h 0 y rfl) + apply MonoidOps.op_ne_dist (h 0 y rfl) exact ih fun i x hget => h (i + 1) x hget /-- Congruence when the functions are equivalent on all indices. -/ theorem congr_forall {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, Φ i x ≡ Ψ i x) : - bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := + ([^ op list] k ↦ x ∈ l, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Ψ k x) := congr (fun i x _ => h i x) theorem append (Φ : Nat → A → M) (l₁ l₂ : List A) : - bigOpL op unit Φ (l₁ ++ l₂) ≡ - op (bigOpL op unit Φ l₁) (bigOpL op unit (fun n => Φ (n + l₁.length)) l₂) := by + ([^ op list] k ↦ x ∈ l₁ ++ l₂, Φ k x) ≡ + op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Φ (k + l₁.length) x) := by induction l₁ generalizing Φ with - | nil => simp only [nil]; exact (Monoid.op_left_id _).symm + | nil => simp only [nil]; exact (MonoidOps.op_left_id _).symm | cons x xs ih => simp only [List.cons_append, cons, List.length_cons] - apply (Monoid.op_congr_r (ih _)).trans + apply (MonoidOps.op_congr_r (ih _)).trans simp only [show ∀ n, n + xs.length + 1 = n + (xs.length + 1) from by omega] - exact (Monoid.op_assoc _ _ _).symm + exact (MonoidOps.op_assoc _ _ _).symm -theorem snoc (Φ : Nat → A → M) (l : List A) (x : A) : - bigOpL op unit Φ (l ++ [x]) ≡ op (bigOpL op unit Φ l) (Φ l.length x) := by - have := @append _ _ _ op unit _ Φ l [x] +theorem snoc (Φ : Nat → A → M) (l : List A) (a : A) : + ([^ op list] k ↦ x ∈ l ++ [a], Φ k x) ≡ op ([^ op list] k ↦ x ∈ l, Φ k x) (Φ l.length a) := by + have := append (op := op) Φ l [a] simp only [cons, nil, Nat.zero_add] at this - exact this.trans (Monoid.op_congr_r (Monoid.op_right_id _)) + refine this.trans ?_ + exact MonoidOps.op_congr_r (MonoidOps.op_right_id _) theorem const_unit (l : List A) : - bigOpL op unit (fun _ _ => unit) l ≡ unit := by + ([^ op list] _x ∈ l, unit) ≡ unit := by induction l with | nil => exact Equiv.rfl | cons _ _ ih => simp only [cons] - exact (Monoid.op_left_id _).trans ih + refine (MonoidOps.op_left_id _).trans ?_ + exact ih theorem op_distrib (Φ Ψ : Nat → A → M) (l : List A) : - bigOpL op unit (fun i x => op (Φ i x) (Ψ i x)) l ≡ - op (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by + ([^ op list] k ↦ x ∈ l, op (Φ k x) (Ψ k x)) ≡ + op ([^ op list] k ↦ x ∈ l, Φ k x) ([^ op list] k ↦ x ∈ l, Ψ k x) := by induction l generalizing Φ Ψ with - | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _) + | nil => simp only [nil]; exact Equiv.symm (MonoidOps.op_left_id _) | cons x xs ih => simp only [cons] - exact (Monoid.op_congr_r (ih _ _)).trans Monoid.op_op_swap + refine (MonoidOps.op_congr_r (ih _ _)).trans ?_ + exact MonoidOps.op_op_swap theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) : - bigOpL op unit Φ (l.map h) ≡ bigOpL op unit (fun i x => Φ i (h x)) l := by + ([^ op list] k ↦ x ∈ l.map h, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Φ k (h x)) := by induction l generalizing Φ with | nil => exact Equiv.rfl | cons x xs ih => simp only [List.map_cons, cons] - exact Monoid.op_proper Equiv.rfl (ih _) + exact MonoidOps.op_proper Equiv.rfl (ih _) -omit [OFE M] [Monoid M op unit] in theorem closed (P : M → Prop) (Φ : Nat → A → M) (l : List A) (hunit : P unit) (hop : ∀ x y, P x → P y → P (op x y)) (hf : ∀ i x, l[i]? = some x → P (Φ i x)) : - P (bigOpL op unit Φ l) := by + P ([^ op list] k ↦ x ∈ l, Φ k x) := by induction l generalizing Φ with | nil => exact hunit | cons y ys ih => @@ -120,52 +142,52 @@ theorem closed (P : M → Prop) (Φ : Nat → A → M) (l : List A) exact hop _ _ (hf 0 y rfl) (ih _ fun i x hget => hf (i + 1) x hget) theorem perm (Φ : A → M) {l₁ l₂ : List A} (hp : l₁.Perm l₂) : - bigOpL op unit (fun _ => Φ) l₁ ≡ bigOpL op unit (fun _ => Φ) l₂ := by + ([^ op list] x ∈ l₁, Φ x) ≡ ([^ op list] x ∈ l₂, Φ x) := by induction hp with | nil => exact Equiv.rfl - | cons _ _ ih => simp only [cons]; exact Monoid.op_congr_r ih - | swap _ _ _ => simp only [cons]; exact Monoid.op_swap_inner (unit := unit) + | cons _ _ ih => simp only [cons]; exact MonoidOps.op_congr_r ih + | swap _ _ _ => simp only [cons]; exact MonoidOps.op_swap_inner (unit := unit) | trans _ _ ih1 ih2 => exact Equiv.trans ih1 ih2 theorem take_drop (Φ : Nat → A → M) (l : List A) (n : Nat) : - bigOpL op unit Φ l ≡ - op (bigOpL op unit Φ (l.take n)) (bigOpL op unit (fun k => Φ (n + k)) (l.drop n)) := by + ([^ op list] k ↦ x ∈ l, Φ k x) ≡ + op ([^ op list] k ↦ x ∈ l.take n, Φ k x) ([^ op list] k ↦ x ∈ l.drop n, Φ (n + k) x) := by by_cases hn : n ≤ l.length - · have := @append M A _ op unit _ Φ (l.take n) (l.drop n) + · have := append (op := op) Φ (l.take n) (l.drop n) simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at this exact this · simp only [Nat.not_le] at hn simp only [List.drop_eq_nil_of_le (Nat.le_of_lt hn), List.take_of_length_le (Nat.le_of_lt hn), nil] - exact Equiv.symm (Monoid.op_right_id _) + exact Equiv.symm (MonoidOps.op_right_id _) theorem filter_map {B : Type v} (h : A → Option B) (Φ : B → M) (l : List A) : - bigOpL op unit (fun _ => Φ) (l.filterMap h) ≡ - bigOpL op unit (fun _ x => (h x).elim unit Φ) l := by + ([^ op list] x ∈ l.filterMap h, Φ x) ≡ + ([^ op list] x ∈ l, (h x).elim unit Φ) := by induction l with | nil => exact Equiv.rfl | cons x xs ih => simp only [List.filterMap_cons] cases hx : h x <;> simp only [hx, Option.elim, cons] - · exact Equiv.trans ih (Equiv.symm (Monoid.op_left_id _)) - · exact Monoid.op_congr_r ih + · exact Equiv.trans ih (Equiv.symm (MonoidOps.op_left_id _)) + · exact MonoidOps.op_congr_r ih theorem bind {B : Type v} (h : A → List B) (Φ : B → M) (l : List A) : - bigOpL op unit (fun _ => Φ) (l.flatMap h) ≡ - bigOpL op unit (fun _ x => bigOpL op unit (fun _ => Φ) (h x)) l := by + ([^ op list] x ∈ l.flatMap h, Φ x) ≡ + ([^ op list] x ∈ l, [^ op list] y ∈ h x, Φ y) := by induction l with | nil => exact Equiv.rfl | cons x xs ih => simp only [List.flatMap_cons, cons] - exact (append _ _ _).trans (Monoid.op_congr_r ih) + refine (append _ _ _).trans ?_ + exact MonoidOps.op_congr_r ih -omit [OFE M] [Monoid M op unit] in theorem gen_proper_2 {B : Type v} (R : M → M → Prop) (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) (hunit : R unit unit) (hop : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) (hlen : l₁.length = l₂.length) (hf : ∀ i, ∀ x y, l₁[i]? = some x → l₂[i]? = some y → R (Φ i x) (Ψ i y)) : - R (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + R ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by induction l₁ generalizing l₂ Φ Ψ with | nil => cases l₂ with @@ -180,51 +202,48 @@ theorem gen_proper_2 {B : Type v} (R : M → M → Prop) exact hop _ _ _ _ (hf 0 x y rfl rfl) (ih _ _ _ hlen fun i a b ha hb => hf (i + 1) a b ha hb) -omit [OFE M] [Monoid M op unit] in theorem gen_proper (R : M → M → Prop) (Φ Ψ : Nat → A → M) (l : List A) (hR_refl : ∀ x, R x x) (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) (hf : ∀ k y, l[k]? = some y → R (Φ k y) (Ψ k y)) : - R (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by - apply gen_proper_2 (op := op) (unit := unit) R Φ Ψ l l (hR_refl unit) hR_op rfl + R ([^ op list] k ↦ x ∈ l, Φ k x) ([^ op list] k ↦ x ∈ l, Ψ k x) := by + apply gen_proper_2 R Φ Ψ l l (hR_refl unit) hR_op rfl intro k x y hx hy; rw [hx] at hy; cases hy; exact hf k x hx -omit [OFE M] [Monoid M op unit] in theorem ext {Φ Ψ : Nat → A → M} {l : List A} (h : ∀ i x, l[i]? = some x → Φ i x = Ψ i x) : - bigOpL op unit Φ l = bigOpL op unit Ψ l := + ([^ op list] k ↦ x ∈ l, Φ k x) = ([^ op list] k ↦ x ∈ l, Ψ k x) := gen_proper (· = ·) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) h theorem proper_2 [OFE A] (Φ Ψ : Nat → A → M) (l₁ l₂ : List A) (hlen : l₁.length = l₂.length) (hf : ∀ (k : Nat) (y₁ y₂ : A), l₁[k]? = some y₁ → l₂[k]? = some y₂ → Φ k y₁ ≡ Ψ k y₂) : - bigOpL op unit Φ l₁ ≡ bigOpL op unit Ψ l₂ := by - exact gen_proper_2 (op := op) (unit := unit) (· ≡ ·) Φ Ψ l₁ l₂ Equiv.rfl - (fun _ _ _ _ => Monoid.op_proper) hlen hf + ([^ op list] k ↦ x ∈ l₁, Φ k x) ≡ ([^ op list] k ↦ x ∈ l₂, Ψ k x) := + gen_proper_2 (· ≡ ·) Φ Ψ l₁ l₂ Equiv.rfl (fun _ _ _ _ => MonoidOps.op_proper) hlen hf theorem zipIdx (Φ : A × Nat → M) (n : Nat) (l : List A) : - bigOpL op unit (fun _ => Φ) (l.zipIdx n) ≡ - bigOpL op unit (fun i x => Φ (x, n + i)) l := by + ([^ op list] x ∈ l.zipIdx n, Φ x) ≡ + ([^ op list] k ↦ x ∈ l, Φ (x, n + k)) := by induction l generalizing n with | nil => simp only [nil]; exact Equiv.rfl | cons x xs ih => simp only [cons, Nat.add_zero] - exact Monoid.op_proper Equiv.rfl + exact MonoidOps.op_proper Equiv.rfl ((ih (n + 1)).trans (congr_forall fun i _ => by simp [Nat.add_assoc, Nat.add_comm 1 i])) theorem zipIdxInt (Φ : A × Int → M) (n : Int) (l : List A) : - bigOpL op unit (fun _ => Φ) (Std.List.zipIdxInt l n) ≡ - bigOpL op unit (fun i x => Φ (x, n + (i : Int))) l := by + ([^ op list] x ∈ Std.List.zipIdxInt l n, Φ x) ≡ + ([^ op list] k ↦ x ∈ l, Φ (x, n + (k : Int))) := by unfold Std.List.zipIdxInt - suffices ∀ m, bigOpL op unit (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡ - bigOpL op unit (fun i x => Φ (x, m + (i : Int))) l from this n + suffices ∀ m, bigOpL op (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡ + bigOpL op (fun i x => Φ (x, m + (i : Int))) l from this n intro m induction l generalizing m with | nil => simp only [List.mapIdx, nil]; exact Equiv.rfl | cons x xs ih => simp only [List.mapIdx_cons, cons] - apply Monoid.op_proper + apply MonoidOps.op_proper · show Φ (x, (0 : Int) + m) ≡ Φ (x, m + (0 : Int)) rw [Int.zero_add, Int.add_zero] · rw [show (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) = @@ -236,18 +255,18 @@ theorem zipIdxInt (Φ : A × Int → M) (n : Int) (l : List A) : apply congr_forall fun i _ => ?_ rw [show m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) from by omega] -theorem op_zipWith {B C : Type _} +theorem sep_zipWith {B C : Type _} (f : A → B → C) (g1 : C → A) (g2 : C → B) (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) (hg1 : ∀ x y, g1 (f x y) = x) (hg2 : ∀ x y, g2 (f x y) = y) (hlen : l₁.length = l₂.length) : - bigOpL op unit (fun i c => op (Φ i (g1 c)) (Ψ i (g2 c))) (List.zipWith f l₁ l₂) ≡ - op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + ([^ op list] k ↦ c ∈ List.zipWith f l₁ l₂, op (Φ k (g1 c)) (Ψ k (g2 c))) ≡ + op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by induction l₁ generalizing l₂ Φ Ψ with | nil => cases l₂ with - | nil => simp only [List.zipWith_nil_left, nil]; exact Equiv.symm (Monoid.op_left_id _) + | nil => simp only [List.zipWith_nil_left, nil]; exact Equiv.symm (MonoidOps.op_left_id _) | cons _ _ => simp at hlen | cons x xs ih => cases l₂ with @@ -255,26 +274,27 @@ theorem op_zipWith {B C : Type _} | cons y ys => simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen simp only [List.zipWith_cons_cons, cons, hg1, hg2] - exact (Monoid.op_congr_r (ih _ _ _ hlen)).trans Monoid.op_op_swap + refine (MonoidOps.op_congr_r (ih _ _ _ hlen)).trans ?_ + exact MonoidOps.op_op_swap /-- Big op over zipped list with separated functions. -/ -theorem op_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) +theorem sep_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B) (hlen : l₁.length = l₂.length) : - bigOpL op unit (fun i xy => op (Φ i xy.1) (Ψ i xy.2)) (l₁.zip l₂) ≡ - op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by + ([^ op list] k ↦ xy ∈ l₁.zip l₂, op (Φ k xy.1) (Ψ k xy.2)) ≡ + op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by simp only [List.zip] - exact op_zipWith (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen + exact sep_zipWith (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂} -variable [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] +variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] variable {B : Type w} /-- Monoid homomorphisms distribute over big ops. -/ theorem hom {R : M₂ → M₂ → Prop} {f : M₁ → M₂} (hom : MonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) (Φ : Nat → B → M₁) (l : List B) : - R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by + R (f ([^ op₁ list] k ↦ x ∈ l, Φ k x)) ([^ op₂ list] k ↦ x ∈ l, f (Φ k x)) := by induction l generalizing Φ with | nil => simp only [nil]; exact hom.map_unit | cons x xs ih => @@ -286,7 +306,7 @@ theorem hom {R : M₂ → M₂ → Prop} {f : M₁ → M₂} theorem hom_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} (hom : WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f) (Φ : Nat → B → M₁) (l : List B) (hne : l ≠ []) : - R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by + R (f ([^ op₁ list] k ↦ x ∈ l, Φ k x)) ([^ op₂ list] k ↦ x ∈ l, f (Φ k x)) := by induction l generalizing Φ with | nil => exact absurd rfl hne | cons x xs ih => @@ -295,8 +315,8 @@ theorem hom_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂} | nil => simp only [nil] haveI : NonExpansive f := hom.f_ne - apply (hom.rel_proper (NonExpansive.eqv (Monoid.op_right_id _)) - (Monoid.op_right_id _)).mpr + apply (hom.rel_proper (NonExpansive.eqv (MonoidOps.op_right_id _)) + (MonoidOps.op_right_id _)).mpr exact hom.rel_refl _ | cons y ys => apply hom.rel_trans (hom.homomorphism _ _) @@ -306,46 +326,40 @@ end BigOpL namespace BigOpM -open Iris.Std +open scoped PartialMap -variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit] +variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit] variable {M' : Type _ → Type _} {K : Type _} {V : Type _} variable [LawfulFiniteMap M' K] -def bigOpM (Φ : K → V → M) (m : M' V) : M := - bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m) - theorem equiv (Φ : K → V → M) (m₁ m₂ : M' V) - (h : PartialMap.equiv m₁ m₂) : - bigOpM (op := op) (unit := unit) Φ m₁ ≡ bigOpM (op := op) (unit := unit) Φ m₂ := by + (h : m₁ ≡ₘ m₂) : + ([^ op map] k ↦ x ∈ m₁, Φ k x) ≡ ([^ op map] k ↦ x ∈ m₂, Φ k x) := by simp only [bigOpM] exact BigOpL.perm _ (LawfulFiniteMap.toList_perm_of_get?_eq h) -omit [OFE M] [Monoid M op unit] in @[simp] theorem empty (Φ : K → V → M) : - bigOpM (op := op) (unit := unit) Φ (∅ : M' V) = unit := by - show bigOpL op unit _ (toList (∅ : M' V)) = unit + ([^ op map] k ↦ x ∈ (∅ : M' V), Φ k x) = unit := by + show bigOpL op _ (toList (∅ : M' V)) = unit rw [show toList (K := K) (∅ : M' V) = [] from toList_empty]; rfl theorem insert (Φ : K → V → M) (m : M' V) (i : K) (x : V) : get? m i = none → - bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x) ≡ - op (Φ i x) (bigOpM (op := op) (unit := unit) Φ m) := by + ([^ op map] k ↦ v ∈ PartialMap.insert m i x, Φ k v) ≡ + op (Φ i x) ([^ op map] k ↦ v ∈ m, Φ k v) := by intro hi simp only [bigOpM] exact BigOpL.perm _ (LawfulFiniteMap.toList_insert (v := x) hi) theorem delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : get? m i = some x → - bigOpM (op := op) (unit := unit) Φ m ≡ - op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := by + ([^ op map] k ↦ v ∈ m, Φ k v) ≡ + op (Φ i x) ([^ op map] k ↦ v ∈ PartialMap.delete m i, Φ k v) := by intro hi apply (BigOpM.equiv Φ m _ (fun k => (LawfulPartialMap.insert_delete_cancel hi k).symm)).trans - exact insert Φ (Iris.Std.delete m i) _ _ (get?_delete_eq rfl) - -variable {A : Type w} + exact insert Φ (PartialMap.delete m i) _ _ (get?_delete_eq rfl) -theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) +theorem gen_proper_2 [DecidableEq K] {A : Type _} {B : Type _} (R : M → M → Prop) (Φ : K → A → M) (Ψ : K → B → M) (m1 : M' A) (m2 : M' B) (hR_sub : ∀ x y, x ≡ y → R x y) (hR_equiv : Equivalence R) @@ -355,13 +369,13 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) | some y1, some y2 => R (Φ k y1) (Ψ k y2) | none, none => True | _, _ => False) : - R (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Ψ m2) := by + R ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Ψ k x) := by let P1 : M' A → Prop := fun m1' => ∀ (m2' : M' B) (Φ' : K → A → M) (Ψ' : K → B → M), (∀ k, match get? m1' k, get? m2' k with | some y1, some y2 => R (Φ' k y1) (Ψ' k y2) | none, none => True | _, _ => False) → - R (bigOpM (op := op) (unit := unit) Φ' m1') (bigOpM (op := op) (unit := unit) Ψ' m2') + R ([^ op map] k ↦ x ∈ m1', Φ' k x) ([^ op map] k ↦ x ∈ m2', Ψ' k x) suffices h : P1 m1 from h m2 Φ Ψ hfg apply LawfulFiniteMap.induction_on (K := K) (P := P1) · intro m₁ m₂ heq hP m2' Φ' Ψ' hfg' @@ -374,7 +388,7 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) | some y1, some y2 => R (Φ'' k y1) (Ψ'' k y2) | none, none => True | _, _ => False) → - R (bigOpM (op := op) (unit := unit) Φ'' (∅ : M' A)) (bigOpM (op := op) (unit := unit) Ψ'' m2'') + R ([^ op map] k ↦ x ∈ (∅ : M' A), Φ'' k x) ([^ op map] k ↦ x ∈ m2'', Ψ'' k x) suffices h2 : P2 m2' from h2 Φ' Ψ' hfg' apply LawfulFiniteMap.induction_on (K := K) (P := P2) · intro m₁ m₂ heq hP Φ'' Ψ'' hfg'' @@ -382,7 +396,7 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) exact hR_sub _ _ (BigOpM.equiv Ψ'' m₁ m₂ heq) · show P2 (∅ : M' B) intro _ _ _ - show R (bigOpM (op := op) _ (∅ : M' A)) (bigOpM (op := op) _ (∅ : M' B)) + show R ([^ op map] k ↦ x ∈ (∅ : M' A), _) ([^ op map] k ↦ x ∈ (∅ : M' B), _) rw [empty, empty]; exact hR_sub unit unit Equiv.rfl · intro k _ _ _ _ Φ'' Ψ'' hfg'' have := hfg'' k @@ -404,32 +418,33 @@ theorem gen_proper_2 [DecidableEq K] {B : Type w} (R : M → M → Prop) · subst hkk'; rw [get?_delete_eq rfl, hm1'k]; trivial · have := hfg' k'; rw [get?_insert_ne hkk'] at this; rwa [get?_delete_ne hkk'] -omit [Monoid M op unit] in -theorem gen_proper {M : Type u} {op : M → M → M} {unit : M} (R : M → M → Prop) +theorem gen_proper {M : Type u} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit] + (R : M → M → Prop) (Φ Ψ : K → V → M) (m : M' V) (hR_refl : ∀ x, R x x) (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b')) (hf : ∀ k x, get? m k = some x → R (Φ k x) (Ψ k x)) : - R (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by + R ([^ op map] k ↦ x ∈ m, Φ k x) ([^ op map] k ↦ x ∈ m, Ψ k x) := by simp only [bigOpM] - apply BigOpL.gen_proper_2 (op := op) (unit := unit) R _ _ _ _ (hR_refl unit) hR_op rfl + apply BigOpL.gen_proper_2 R _ _ _ _ (hR_refl unit) hR_op rfl intro i x y hx hy; rw [hx] at hy; cases hy exact hf x.1 x.2 (toList_get.mp (List.mem_iff_getElem?.mpr ⟨i, hx⟩)) -theorem ext {M : Type u} (op : M → M → M) (unit : M) (Φ Ψ : K → V → M) (m : M' V) +theorem ext {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit] + (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, get? m k = some x → Φ k x = Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Ψ m := + ([^ op map] k ↦ x ∈ m, Φ k x) = ([^ op map] k ↦ x ∈ m, Ψ k x) := gen_proper (R := (· = ·)) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) hf theorem dist (Φ Ψ : K → V → M) (m : M' V) (n : Nat) (hf : ∀ k x, get? m k = some x → Φ k x ≡{n}≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := - gen_proper (R := (· ≡{n}≡ ·)) _ _ _ (fun _ => Dist.rfl) (fun _ _ _ _ => Monoid.op_ne_dist) hf + ([^ op map] k ↦ x ∈ m, Φ k x) ≡{n}≡ ([^ op map] k ↦ x ∈ m, Ψ k x) := + gen_proper (R := (· ≡{n}≡ ·)) _ _ _ (fun _ => Dist.rfl) (fun _ _ _ _ => MonoidOps.op_ne_dist) hf theorem proper (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, get? m k = some x → Φ k x ≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := - gen_proper (R := (· ≡ ·)) _ _ _ (fun _ => Equiv.rfl) (fun _ _ _ _ => Monoid.op_proper) hf + ([^ op map] k ↦ x ∈ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, Ψ k x) := + gen_proper (R := (· ≡ ·)) _ _ _ (fun _ => Equiv.rfl) (fun _ _ _ _ => MonoidOps.op_proper) hf theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → M) (m1 m2 : M' A) (hm : ∀ k, get? m1 k = get? m2 k) @@ -438,8 +453,8 @@ theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → get? m2 k = some y2 → y1 ≡ y2 → Φ k y1 ≡ Ψ k y2) : - bigOpM (op := op) (unit := unit) Φ m1 ≡ bigOpM (op := op) (unit := unit) Ψ m2 := by - apply gen_proper_2 (R := (· ≡ ·)) _ _ _ _ (fun _ _ h => h) equiv_eqv (fun _ _ _ _ => Monoid.op_proper) + ([^ op map] k ↦ x ∈ m1, Φ k x) ≡ ([^ op map] k ↦ x ∈ m2, Ψ k x) := by + apply gen_proper_2 (R := (· ≡ ·)) _ _ _ _ (fun _ _ h => h) equiv_eqv (fun _ _ _ _ => MonoidOps.op_proper) intro k have hlk := hm k cases hm1k : get? m1 k with @@ -452,94 +467,96 @@ theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → theorem dist_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat) (hf : ∀ k x, Φ k x ≡{n}≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := - dist _ _ _ _ fun k x _ => hf k x + ([^ op map] k ↦ x ∈ m, Φ k x) ≡{n}≡ ([^ op map] k ↦ x ∈ m, Ψ k x) := + dist _ _ _ _ fun k x _ => hf k x theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V) (hf : ∀ k x, Φ k x ≡ Ψ k x) : - bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := - proper _ _ _ fun k x _ => hf k x + ([^ op map] k ↦ x ∈ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, Ψ k x) := + proper _ _ _ fun k x _ => hf k x -omit [Monoid M op unit] in theorem to_list (Φ : K → V → M) (m : M' V) : - bigOpM (op := op) (unit := unit) Φ m ≡ - bigOpL op unit (fun _ kx => Φ kx.1 kx.2) (toList (K := K) m) := by rfl + ([^ op map] k ↦ x ∈ m, Φ k x) ≡ + ([^ op list] kx ∈ toList (K := K) m, Φ kx.1 kx.2) := by rfl theorem of_list [DecidableEq K] (Φ : K → V → M) (l : List (K × V)) (hnodup : NoDupKeys l) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.ofList l : M' V) ≡ - bigOpL op unit (fun _ kx => Φ kx.1 kx.2) l := by - simp only [bigOpM]; exact BigOpL.perm _ (LawfulFiniteMap.toList_ofList hnodup) + ([^ op map] k ↦ x ∈ (PartialMap.ofList l : M' V), Φ k x) ≡ + ([^ op list] kx ∈ l, Φ kx.1 kx.2) := by + simp only [bigOpM] + exact BigOpL.perm _ (LawfulFiniteMap.toList_ofList hnodup) theorem singleton (Φ : K → V → M) (i : K) (x : V) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.singleton (M := M') i x) ≡ Φ i x := by - rw [show PartialMap.singleton (M := M') i x = Iris.Std.insert (∅ : M' V) i x from rfl] + ([^ op map] k ↦ v ∈ ({[i := x]} : M' V), Φ k v) ≡ Φ i x := by + rw [show ({[i := x]} : M' V) = PartialMap.insert (∅ : M' V) i x from rfl] apply (insert Φ (∅ : M' V) i x (get?_empty i)).trans - rw [empty]; exact Monoid.op_right_id _ + rw [empty]; exact MonoidOps.op_right_id _ theorem const_unit [DecidableEq K] (m : M' V) : - bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m ≡ unit := by - let P : M' V → Prop := fun m' => bigOpM (op := op) (unit := unit) (fun (_ : K) (_ : V) => unit) m' ≡ unit + bigOpM op (fun (_ : K) _ => unit) m ≡ unit := by + let P : M' V → Prop := fun m' => bigOpM op (fun (_ : K) (_ : V) => unit) m' ≡ unit show P m; apply LawfulFiniteMap.induction_on (K := K) (P := P) - · intro m₁ m₂ heq h; exact (BigOpM.equiv _ _ _ heq).symm.trans h + · intro m₁ m₂ heq h + refine (BigOpM.equiv _ _ _ heq).symm.trans ?_ + exact h · show P (∅ : M' V); show _ ≡ _; rw [empty] · intro i x m' hm' IH - exact (insert _ _ _ _ hm').trans ((Monoid.op_proper Equiv.rfl IH).trans (Monoid.op_left_id _)) + refine (insert _ _ _ _ hm').trans ?_ + refine (MonoidOps.op_proper Equiv.rfl IH).trans ?_ + exact MonoidOps.op_left_id _ theorem map (h : V → B) (Φ : K → B → M) (m : M' V) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.map h m) ≡ - bigOpM (op := op) (unit := unit) (fun k v => Φ k (h v)) m := by + ([^ op map] k ↦ x ∈ PartialMap.map h m, Φ k x) ≡ + ([^ op map] k ↦ v ∈ m, Φ k (h v)) := by simp only [bigOpM] - exact (BigOpL.perm _ LawfulFiniteMap.toList_map).trans - (BigOpL.map (op := op) _ _ (toList (K := K) m)) + refine (BigOpL.perm _ LawfulFiniteMap.toList_map).trans ?_ + exact BigOpL.map (op := op) _ _ (toList (K := K) m) theorem filter_map (h : V → Option V) (Φ : K → V → M) (m : M' V) (hinj : Function.Injective h) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.filterMap h m) ≡ - bigOpM (op := op) (unit := unit) (fun k v => (h v).elim unit (Φ k)) m := by + ([^ op map] k ↦ x ∈ PartialMap.filterMap h m, Φ k x) ≡ + ([^ op map] k ↦ v ∈ m, (h v).elim unit (Φ k)) := by simp only [bigOpM] - exact (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans - ((BigOpL.filter_map (op := op) _ _ _).trans - (BigOpL.congr_forall fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map])) + refine (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans ?_ + refine (BigOpL.filter_map (op := op) _ _ _).trans ?_ + exact BigOpL.congr_forall fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map] theorem insert_delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) : - bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x) ≡ - op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (Iris.Std.delete m i)) := by - exact (BigOpM.equiv _ _ _ fun k => (LawfulPartialMap.insert_delete k).symm).trans - (insert _ _ _ _ (get?_delete_eq rfl)) + ([^ op map] k ↦ v ∈ PartialMap.insert m i x, Φ k v) ≡ + op (Φ i x) ([^ op map] k ↦ v ∈ PartialMap.delete m i, Φ k v) := by + refine (BigOpM.equiv _ _ _ fun k => (LawfulPartialMap.insert_delete k).symm).trans ?_ + exact insert _ _ _ _ (get?_delete_eq rfl) theorem insert_override (Φ : K → A → M) (m : M' A) (i : K) (x x' : A) : get? m i = some x → Φ i x ≡ Φ i x' → - bigOpM (op := op) (unit := unit) Φ (Iris.Std.insert m i x') ≡ - bigOpM (op := op) (unit := unit) Φ m := by + ([^ op map] k ↦ v ∈ PartialMap.insert m i x', Φ k v) ≡ + ([^ op map] k ↦ v ∈ m, Φ k v) := by intro hi hΦ - apply (insert_delete Φ m i x').trans - exact (Monoid.op_proper hΦ.symm Equiv.rfl).trans (delete Φ m i x hi).symm + refine (insert_delete Φ m i x').trans ?_ + refine (MonoidOps.op_proper hΦ.symm Equiv.rfl).trans ?_ + exact (delete Φ m i x hi).symm theorem fn_insert [DecidableEq K] {B : Type w} (g : K → V → B → M) (f : K → B) (m : M' V) (i : K) (x : V) (b : B) (hi : get? m i = none) : - bigOpM (op := op) (unit := unit) (fun k y => g k y (if k = i then b else f k)) - (Iris.Std.insert m i x) ≡ - op (g i x b) (bigOpM (op := op) (unit := unit) (fun k y => g k y (f k)) m) := by - refine (insert _ m i x hi).trans (Monoid.op_proper (by simp) (proper _ _ _ fun k y hk => ?_)) + ([^ op map] k ↦ y ∈ PartialMap.insert m i x, g k y (if k = i then b else f k)) ≡ + op (g i x b) ([^ op map] k ↦ y ∈ m, g k y (f k)) := by + refine (insert _ m i x hi).trans (MonoidOps.op_proper (by simp) (proper _ _ _ fun k y hk => ?_)) simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk] theorem fn_insert' [DecidableEq K] (f : K → M) (m : M' V) (i : K) (x : V) (P : M) (hi : get? m i = none) : - bigOpM (op := op) (unit := unit) (fun k _ => if k = i then P else f k) - (Iris.Std.insert m i x) ≡ - op P (bigOpM (op := op) (unit := unit) (fun k _ => f k) m) := by - refine (insert _ m i x hi).trans (Monoid.op_proper (by simp) (proper _ _ _ fun k _ hk => ?_)) + ([^ op map] k ↦ _v ∈ PartialMap.insert m i x, if k = i then P else f k) ≡ + op P ([^ op map] k ↦ _v ∈ m, f k) := by + refine (insert _ m i x hi).trans (MonoidOps.op_proper (by simp) (proper _ _ _ fun k _ hk => ?_)) simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk] theorem filter (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) : - bigOpM (op := op) (unit := unit) Φ (PartialMap.filter φ m) ≡ - bigOpM (op := op) (unit := unit) (fun k x => if φ k x then Φ k x else unit) m := by + ([^ op map] k ↦ x ∈ PartialMap.filter φ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, if φ k x then Φ k x else unit) := by unfold bigOpM refine (BigOpL.perm _ LawfulFiniteMap.toList_filter).trans ?_ suffices ∀ l : List (K × V), - bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (l.filter (fun kv => φ kv.1 kv.2)) ≡ - bigOpL op unit (fun _ kv => if φ kv.1 kv.2 then Φ kv.1 kv.2 else unit) l from this _ + bigOpL op (fun _ kv => Φ kv.1 kv.2) (l.filter (fun kv => φ kv.1 kv.2)) ≡ + bigOpL op (fun _ kv => if φ kv.1 kv.2 then Φ kv.1 kv.2 else unit) l from this _ intro l induction l with | nil => exact Equiv.rfl @@ -548,51 +565,54 @@ theorem filter (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) : cases hp : φ kv.1 kv.2 with | false => simp only [BigOpL.cons, hp] - exact Equiv.trans ih (Equiv.symm (Monoid.op_left_id _)) + exact Equiv.trans ih (Equiv.symm (MonoidOps.op_left_id _)) | true => simp only [BigOpL.cons, hp, ite_true] - exact Monoid.op_congr_r ih + exact MonoidOps.op_congr_r ih -theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : PartialMap.disjoint m1 m2) : - bigOpM (op := op) (unit := unit) Φ (m1 ∪ m2) ≡ - op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) := by +theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : m1 ##ₘ m2) : + ([^ op map] k ↦ x ∈ m1 ∪ m2, Φ k x) ≡ op ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Φ k x) := by let P : M' V → Prop := fun m1 => PartialMap.disjoint m1 m2 → - bigOpM (op := op) (unit := unit) Φ (PartialMap.union m1 m2) ≡ - op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) + ([^ op map] k ↦ x ∈ PartialMap.union m1 m2, Φ k x) ≡ + op ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Φ k x) suffices h : P m1 from h hdisj apply LawfulFiniteMap.induction_on (K := K) (P := P) · intro m₁ m₂' heq hP hdisj' - refine Equiv.trans ?_ ((hP fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩).trans - (Monoid.op_proper (BigOpM.equiv Φ m₁ m₂' heq) Equiv.rfl)) - apply Equiv.symm - apply BigOpM.equiv Φ _ _ fun k => ?_ - show get? _ k = get? _ k - rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k] + have hdisj'' : PartialMap.disjoint m₁ m2 := + fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩ + have hunion_eq := BigOpM.equiv (op := op) (unit := unit) + Φ (PartialMap.union m₁ m2) (PartialMap.union m₂' m2) + (fun k => by rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k]) + refine hunion_eq.symm.trans ?_ + refine (hP hdisj'').trans ?_ + exact MonoidOps.op_proper (BigOpM.equiv Φ m₁ m₂' heq) Equiv.rfl · show P (∅ : M' V) intro _; rw [empty] - refine Equiv.trans ?_ (Monoid.op_left_id _).symm + refine Equiv.trans ?_ (MonoidOps.op_left_id _).symm apply BigOpM.equiv Φ _ _ intro k; show get? (PartialMap.union (∅ : M' V) m2) k = get? m2 k rw [LawfulPartialMap.get?_union, show get? (∅ : M' V) k = none from get?_empty k]; simp · intro i x m hi_none IH hdisj' - apply (BigOpM.equiv Φ _ _ fun k => (LawfulPartialMap.union_insert_left k).symm).trans - apply (insert Φ (m ∪ m2) i x (by - show get? (PartialMap.union m m2) i = none + have hi_union : get? (PartialMap.union m m2) i = none := by rw [LawfulPartialMap.get?_union_none] refine ⟨hi_none, ?_⟩ cases (PartialMap.disjoint_iff _ m2).mp hdisj' i with | inl h => rw [get?_insert_eq rfl] at h; cases h - | inr h => exact h)).trans - apply (Monoid.op_congr_r (IH fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by + | inr h => exact h + have hdisj_inner : PartialMap.disjoint m m2 := fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by by_cases h : i = k · subst h; rw [hi_none] at hk1; cases hk1 - · rwa [get?_insert_ne h], hk2⟩)).trans - exact (Monoid.op_assoc _ _ _).symm.trans (Monoid.op_congr_l (insert Φ m i x hi_none).symm) + · rwa [get?_insert_ne h], hk2⟩ + refine (BigOpM.equiv Φ _ _ fun k => (LawfulPartialMap.union_insert_left k).symm).trans ?_ + refine (insert Φ (m ∪ m2) i x hi_union).trans ?_ + refine (MonoidOps.op_congr_r (IH hdisj_inner)).trans ?_ + refine (MonoidOps.op_assoc _ _ _).symm.trans ?_ + exact MonoidOps.op_congr_l (insert Φ m i x hi_none).symm theorem op_distrib (Φ Ψ : K → V → M) (m : M' V) : - bigOpM (op := op) (unit := unit) (fun k x => op (Φ k x) (Ψ k x)) m ≡ - op (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by + ([^ op map] k ↦ x ∈ m, op (Φ k x) (Ψ k x)) ≡ + op ([^ op map] k ↦ x ∈ m, Φ k x) ([^ op map] k ↦ x ∈ m, Ψ k x) := by simp only [bigOpM]; exact BigOpL.op_distrib _ _ _ theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V) @@ -600,16 +620,16 @@ theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V) (hunit : P unit) (hop : ∀ x y, P x → P y → P (op x y)) (hf : ∀ k x, get? m k = some x → P (Φ k x)) : - P (bigOpM (op := op) (unit := unit) Φ m) := by + P ([^ op map] k ↦ x ∈ m, Φ k x) := by let Q : M' V → Prop := fun m'' => (∀ k x, get? m'' k = some x → P (Φ k x)) → - P (bigOpM (op := op) (unit := unit) Φ m'') + P ([^ op map] k ↦ x ∈ m'', Φ k x) suffices h : Q m from h hf apply LawfulFiniteMap.induction_on (K := K) (P := Q) · intro m₁ m₂ heq hQ hf' apply (hproper _ _ (BigOpM.equiv Φ m₁ m₂ heq)).mp exact hQ fun k x hget => hf' k x ((heq k) ▸ hget) · show Q (∅ : M' V) - intro _; show P (bigOpM Φ (∅ : M' V)); rw [empty]; exact hunit + intro _; show P ([^ op map] k ↦ x ∈ (∅ : M' V), Φ k x); rw [empty]; exact hunit · intro k x m'' hm'' IH hf'' apply (hproper _ _ (insert Φ m'' k x hm'')).mpr apply hop _ _ (hf'' _ _ (get?_insert_eq rfl)) @@ -621,18 +641,17 @@ theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V) -- TODO: kmap and map_seq are skipped for now -theorem op_zipWith {A : Type _} {B : Type _} {C : Type _} +theorem sep_zipWith {A : Type _} {B : Type _} {C : Type _} (f : A → B → C) (g1 : C → A) (g2 : C → B) (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) (hg1 : ∀ x y, g1 (f x y) = x) (hg2 : ∀ x y, g2 (f x y) = y) (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) : - bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k (g1 xy)) (h2 k (g2 xy))) - (PartialMap.zipWith f m1 m2) ≡ - op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by + ([^ op map] k ↦ xy ∈ PartialMap.zipWith f m1 m2, op (h1 k (g1 xy)) (h2 k (g2 xy))) ≡ + op ([^ op map] k ↦ x ∈ m1, h1 k x) ([^ op map] k ↦ x ∈ m2, h2 k x) := by refine (op_distrib (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy)) (PartialMap.zipWith f m1 m2)).trans ?_ - apply Monoid.op_proper + apply MonoidOps.op_proper · refine (map g1 h1 (PartialMap.zipWith f m1 m2)).symm.trans ?_ apply BigOpM.equiv h1 _ _ intro k @@ -663,14 +682,13 @@ theorem op_zipWith {A : Type _} {B : Type _} {C : Type _} rw [h2k] at this; simp at this | some b => simp [Option.bind, Option.map, hg2] -theorem op_zip {A : Type _} {B : Type _} +theorem sep_zip {A : Type _} {B : Type _} (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B) (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) : - bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k xy.1) (h2 k xy.2)) - (PartialMap.zip m1 m2) ≡ - op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by + ([^ op map] k ↦ xy ∈ PartialMap.zip m1 m2, op (h1 k xy.1) (h2 k xy.2)) ≡ + op ([^ op map] k ↦ x ∈ m1, h1 k x) ([^ op map] k ↦ x ∈ m2, h2 k x) := by simp only [PartialMap.zip] - exact op_zipWith _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hdom + exact sep_zipWith _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hdom end BigOpM diff --git a/src/Iris/Algebra/Monoid.lean b/src/Iris/Algebra/Monoid.lean index 03fe30075..459b3250e 100644 --- a/src/Iris/Algebra/Monoid.lean +++ b/src/Iris/Algebra/Monoid.lean @@ -17,7 +17,7 @@ open OFE /-- A commutative monoid on an OFE, used for big operators. The operation must be non-expansive, associative, commutative, and have a left identity. -/ -class Monoid (M : Type u) [OFE M] (op : M → M → M) (unit : outParam M) where +class MonoidOps {M : Type u} [OFE M] (op : M → M → M) (unit : outParam M) where /-- The operation is non-expansive in both arguments -/ op_ne : NonExpansive₂ op /-- Associativity up to equivalence -/ @@ -27,32 +27,32 @@ class Monoid (M : Type u) [OFE M] (op : M → M → M) (unit : outParam M) where /-- Left identity up to equivalence -/ op_left_id : ∀ a : M, op unit a ≡ a -namespace Monoid +namespace MonoidOps attribute [simp] op_left_id variable {M : Type u} [OFE M] {op : M → M → M} /-- The operation is proper with respect to equivalence. -/ -theorem op_proper {unit : M} [Monoid M op unit] {a a' b b' : M} +theorem op_proper {unit : M} [MonoidOps op unit] {a a' b b' : M} (ha : a ≡ a') (hb : b ≡ b') : op a b ≡ op a' b' := by haveI : NonExpansive₂ op := op_ne exact NonExpansive₂.eqv ha hb /-- Right identity follows from commutativity and left identity. -/ -@[simp] theorem op_right_id {unit : M} [Monoid M op unit] (a : M) : op a unit ≡ a := +@[simp] theorem op_right_id {unit : M} [MonoidOps op unit] (a : M) : op a unit ≡ a := Equiv.trans (op_comm (unit := unit) a unit) (op_left_id a) /-- Congruence on the left argument. -/ -theorem op_congr_l {unit : M} [Monoid M op unit] {a a' b : M} (h : a ≡ a') : op a b ≡ op a' b := +theorem op_congr_l {unit : M} [MonoidOps op unit] {a a' b : M} (h : a ≡ a') : op a b ≡ op a' b := op_proper (unit := unit) h Equiv.rfl /-- Congruence on the right argument. -/ -theorem op_congr_r {unit : M} [Monoid M op unit] {a b b' : M} (h : b ≡ b') : op a b ≡ op a b' := +theorem op_congr_r {unit : M} [MonoidOps op unit] {a b b' : M} (h : b ≡ b') : op a b ≡ op a b' := op_proper (unit := unit) Equiv.rfl h /-- Rearrange `(a * b) * (c * d)` to `(a * c) * (b * d)`. -/ -theorem op_op_swap {unit : M} [Monoid M op unit] {a b c d : M} : +theorem op_op_swap {unit : M} [MonoidOps op unit] {a b c d : M} : op (op a b) (op c d) ≡ op (op a c) (op b d) := calc op (op a b) (op c d) _ ≡ op a (op b (op c d)) := op_assoc a b (op c d) @@ -62,7 +62,7 @@ theorem op_op_swap {unit : M} [Monoid M op unit] {a b c d : M} : _ ≡ op (op a c) (op b d) := Equiv.symm (op_assoc a c (op b d)) /-- Swap inner elements: `a * (b * c)` to `b * (a * c)`. -/ -theorem op_swap_inner {unit : M} [Monoid M op unit] {a b c : M} : +theorem op_swap_inner {unit : M} [MonoidOps op unit] {a b c : M} : op a (op b c) ≡ op b (op a c) := calc op a (op b c) _ ≡ op (op a b) c := Equiv.symm (op_assoc a b c) @@ -70,19 +70,19 @@ theorem op_swap_inner {unit : M} [Monoid M op unit] {a b c : M} : _ ≡ op b (op a c) := op_assoc b a c /-- Non-expansiveness for dist. -/ -theorem op_ne_dist {unit : M} [Monoid M op unit] {n : Nat} {a a' b b' : M} +theorem op_ne_dist {unit : M} [MonoidOps op unit] {n : Nat} {a a' b b' : M} (ha : a ≡{n}≡ a') (hb : b ≡{n}≡ b') : op a b ≡{n}≡ op a' b' := by haveI : NonExpansive₂ op := op_ne exact NonExpansive₂.ne ha hb -end Monoid +end MonoidOps /-! ## Monoid Homomorphisms -/ /-- A weak monoid homomorphism preserves the operation but not necessarily the unit. -/ class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) - [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] + [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] (R : M₂ → M₂ → Prop) (f : M₁ → M₂) where /-- The relation is reflexive -/ rel_refl : ∀ a : M₂, R a a @@ -100,7 +100,7 @@ class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M /-- A monoid homomorphism preserves both the operation and the unit. -/ class MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) - [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂] + [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] (R : M₂ → M₂ → Prop) (f : M₁ → M₂) extends WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f where /-- The unit is preserved -/