Доказательство того, что размер с фильтром не равен (размер + 1)

Question

Имея эту теорему:

Lemma all_count T (a : pred T) s :
  all a s = (count a s == size s).
Proof.
  elim: s=> [| x xs IH] //. case E: (a x)=> /=; rewrite E.
- rewrite addnC. rewrite addn1. rewrite eqSS. by rewrite -IH.
- rewrite addnC=> /=. rewrite addn0. rewrite -size_filter.

Я получил это состояние:

T : Type
a : pred T
x : T
xs : seq T
IH : all a xs = (count a xs == size xs)
E : a x = false
============================
false = (size [seq x <- xs | a x] == (size xs).+1)

Как я могу доказать, что size [seq x <- xs | a x] всегда меньше (size xs).+1)? Таким образом, их равенство всегда ложно.

Answer 1

Если вы хотите избежать индукционного и тематического анализа и использовать только перезапись, вы можете использовать has_predC и друзей.

Proof.
    rewrite -(negbK (all a s)) -has_predC has_count -eqn0Ngt 
       -(count_predC a) -{1}(@addn0 (count a s)) eqn_add2l //.
Qed.

Answer 2

Существует лемма count_size, которая говорит, что count a xs <= size xs. Тогда достаточно использовать ltnn : forall n, (n < n) = false:

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.

Lemma all_count T (a : pred T) s :
  all a s = (count a s == size s).
Proof.
  elim: s=> [| x xs IH] //. case E: (a x)=> /=; rewrite E.
- rewrite addnC. rewrite addn1. rewrite eqSS. by rewrite -IH.
- rewrite addnC=> /=. rewrite addn0.
  by case: (count a xs =P (size xs).+1) (count_size a xs) => // ->; rewrite ltnn.
Qed.