Add lemmas for list count and perm_eq

[cassiersg]

I needed these simple lemmas and they look like they might belong to the standard library.

[fdupress]

StdOrder eventually requires FinType, which uses lists to characterise finiteness. You can't require StdOrder in List. Do you see another way of getting those lemmas in?

[cassiersg]

Thanks @fdupress @strub for the comments. I addressed the StdOrder issue by re-proving the only lemma I used (IntOrder.ler_add) within the proof that used it. I'm not sure it that's the cleanest way?

[fdupress]

Can you check if Int.lez_add exists?

[fdupress]

Can you check if Int.lez_add exists? A lot of simple results on integers exist in Int (derived by smt) as they are needed to construct more complex theories.

But as soon as there is a generic notion of order and generic lemmas about it, it makes sense to instantiate it with Int to get all derived results. (This will, once they are ready, be done using type classes instead of cloning.)

[cassiersg]

Int.lez_add does not exist. Should I add it?

[strub]

You can also do that:

lemma le_in_count ['a] (p1 p2 : 'a -> bool) (s : 'a list) :
  (forall x, x \in s => p1 x => p2 x) =>
  count p1 s <= count p2 s.
proof. elim: s => //#. qed.

[strub]

To be clear, this is the kind of goals where SMT provers are stable.

[strub]

Squash, and we are good to go.

[cassiersg]

@strub done