feat: Big ops

[lzy0505]

Port of big_op.v and its dependencies.

TODO:

• Use a concrete map to replace/instantiate the finite map interface
• Simplify the finite set interface and instantiate it
• Port missing lemmas
• Document differences in lemma statements
• Clean up proofs

Missing lemmas (could be incomplete, double-check)

• big_sepL
  • big_sepL_nil_persistent
  • big_sepL_nil_affine
  • big_sepL_timeless
  • big_sepL_timeless'
  • big_sepL_timeless_id
  • big_sepL_zip_seqZ
• big_sepL2
  • big_sepL2_proper_2
  • big_sepL2_closed
  • big_sepL2_nil_persistent
  • big_sepL2_persistent
  • big_sepL2_nil_affine
  • big_sepL2_affine
  • big_sepL2_nil_timeless
  • big_sepL2_timeless
  • big_sepL2_timeless'
  • big_sepL2_later_1
  • big_sepL2_later
  • big_sepL2_laterN_1
  • big_sepL2_laterN
• big_andL
  • big_andL_submseteq
  • big_andL_ne
  • big_andL_mono'
  • big_andL_id_mono'
  • big_andL_nil_absorbing
  • big_andL_absorbing
  • big_andL_absorbing'
  • big_andL_nil_persistent
  • big_andL_persistent
  • big_andL_timeless
  • big_andL_timeless'
• big_opL
  • big_orL_ne
  • big_orL_nil_timeless
  • big_orL_timeless
  • big_orL_timeless'
  • big_orL_zip_seqZ
• big_sepM
  • big_sepM_empty_timeless
  • big_sepM_timeless
  • big_sepM_timeless'
• big_andM
  • big_andM_empty_timeless
  • big_andM_timeless
  • big_andM_timeless'
  • big_andM_fn_insert
  • big_andM_fn_insert'
• big_sepS
  • big_sepS_empty_timeless
  • big_sepS_timeless
  • big_sepS_timeless'
• All of big_sepMS
• All of big_sepM2

[ahuoguo]

the following corresponds to dom_insert in stdpp:

theorem domSet_insert_l (m : M V) (i : K) (v: V):
  (domSet (insert m i v)) ≡ (singleton i : S) ∪ domSet m := by
  intros j
  rw [← elem_of_domSet]
  rw [mem_union]
  simp only [FiniteMapLaws.lookup_insert_Some]
  rw [← elem_of_domSet]
  by_cases h : i = j
  · rw [h]
    apply Iff.intro
    · intro _
      left
      exact (mem_singleton j j).mpr rfl
    · intro _
      exact ⟨v, Or.inl ⟨rfl, rfl⟩⟩
  · apply Iff.intro
    · intro ⟨x, hx⟩
      cases hx with
      | inl hl => exact absurd hl.1 h
      | inr hr => exact Or.inr ⟨x, hr.2⟩
    · intro hor
      cases hor with
      | inl hl =>
        refine absurd hl ?_
        intro _
        exact (h ((mem_singleton j i).mp hl).symm)
      | inr hr =>
        have ⟨x, hx⟩ := hr
        exact ⟨x, Or.inr ⟨h, hx⟩⟩