New lemmas for stdlib

[namasikanam]

This is the first part of the auxiliary lemmas used in the oram proofs. My current plan is to create 5 PRs (~2k LoC) in total.

I will make sure all the proofs are either written by human, or first generated by LLM and then carefully edited step by step by myself.

[oskgo]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

[namasikanam]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

Thanks. This makes lots of sense. I feel that I learned the proper way of handling option. I removed the all lemmas related to option except the following one, which I feel useful and I hope it's also useful for others.

lemma oget_ext ['a] (x y : 'a option) :
     x <> None
  => y <> None
  => oget x = oget y
  => x = y.
proof. by case x; case y. qed.

[oskgo]

Had a look at the rest now.

[oskgo]

This is only the non-negative case. It should be called something like exprE_ge0 instead.

[oskgo]

This is rexpr_hmono with a weaker side condition. Generally we prefer changing existing lemmas when a new one would be strictly more applicable. Also change rexpr_hmono_ltr to match the new rexpr_hmono.

[oskgo]

There should be a matching lemma for max.