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