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.

[namasikanam]

@oskgo Thanks for your review. They make lots of sense to me and I learned something. I've resolved all your comments and updated my PR.

[namasikanam]

Hmmm...as now we strengthened two lemmas in stdlib, an external project (xmss) is broken. Shall I keep the original lemmas, rexpr_hmono_ltr and rexpr_hmono, or updated external projects which depend on these two lemmas?

[oskgo]

@namasikanam The external projects should be updated. I think @fdupress maintains xmss.

[fdupress]

I don't, but I keep it up to date.
I don't see the failure, though.

[namasikanam]

I don't, but I keep it up to date. I don't see the failure, though.

@fdupress You can see the failure through CI now.
https://github.com/EasyCrypt/easycrypt/actions/runs/27955903321/job/82726110975?pr=1053

I can also create a PR to XMSS by myself if you want.

[fdupress]

I don't, but I keep it up to date. I don't see the failure, though.

@fdupress You can see the failure through CI now. https://github.com/EasyCrypt/easycrypt/actions/runs/27955903321/job/82726110975?pr=1053

I can also create a PR to XMSS by myself if you want.

This is done. External CI works, but we'll need to synchronise the merging across the repos.

[fdupress]

Which we can't do because the local CI setup for the XMSS repo is still not fixed for compatibility with the external CI on breaking changes.

I'll reprioritise sorting this out.