0

次の見出語を使用して、強力な形式の鳩の巣原理を証明したいと思います。

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.

力強いフォルムの鳩穴がプリンシパル。

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.

見出語を証明する方法は？

4

1 に答える 1

0

最初の補題の一般化を証明しました。ここで見つけることができます。

最も困難な部分は、 の左側からオブジェクトを単純化することでした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.
于 2013-02-04T20:52:45.893 に答える