coq - 用过滤器证明大小不等于 (size + 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

有一个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.

Answer 2

如果你想避免归纳和案例分析，而只使用rewrite，你可以使用iehas_predC和朋友。

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