lambda - Coq：如何证明列表中不同元素的大小小于列表的长度

Question

我想用下面的引理来证明强形式鸽洞原理。

Parameter A:Type.
Parameter  var_dec : forall (x y : A),{x=y}+{~x=y}. 

Definition included (l1 l2:list A):Prop :=
              forall x:A,In x l1 -> In x l2.

Fixpoint inbool (x:A) (l:list A) :bool :=
           match l with
           | nil => false
           | x'::l' => match (var_dec x' x) with
                           | left _ => true
                           | right _ => inbool x l'
                           end
           end.

Fixpoint diff(l1 l2:list A):nat :=
  match l2 with
  | nil => 0
  | x::l' => if inbool x l1 then diff l1 l' else S (diff (x::l1) l')
  end.

例如。差异 [] {1,2} = 2; 差异 [] {1,2,2} = 2。

Lemma diff_le_length_le1:
  forall a l, diff (a::nil) l <= diff nil l.


Lemma include_diff:forall l1 l2,included l1 l2 -> diff nil l1 <= diff nil l2.

强大的鸽子洞原理。

Theorem pigeon_hole_princible_sf:
            forall r:nat,forall h p,
             r>0->
             included p h -> length p > length h*(r-1) -> exists x : A , count x p >r-1.

如何证明引理？

Answer 1

我已经证明了第一个引理的概括。你可以在这里找到它。

最困难的部分是简化左侧的对象diff。我需要证明以下几点：

inbool a l1 = false -> inbool a l2 = false ->    diff (a :: l2) l1  = diff l2 l1
inbool a l1 = false -> inbool a l2 = true  ->    diff (a :: l2) l1  = diff l2 l1
inbool a l1 = true  -> inbool a l2 = false -> S (diff (a :: l2) l1) = diff l2 l1
inbool a l1 = true  -> inbool a l2 = true  ->    diff (a :: l2) l1  = diff l2 l1

证明这个其他算法的事情可能会更容易diff。

Fixpoint diff (l1 l2 : list A) : nat :=
  match l2 with
  | nil => O
  | a :: l3 =>
    if inbool a l1
    then diff l1 l3
    else if inbool a l3
      then diff l1 l3
      else S (diff l1 l3)
  end.