Coq：如何證明列表中的差異元素的大小小於列表的長度

Question

我想用下面的引理來證明pigeon_hole的強壯原理。

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. 

例如。 diff [] {1,2} = 2; DIFF [] {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. 

強形式鴿子洞princible。

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

我已經證明了第一個引理的泛化。你可以找到它here。

最困難的部分是簡化對象從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.