如何排列列表中的元素 [英] How to arrange elements in the list

问题描述

我正在按列表中的特定顺序排列自然数。我定义的函数在列表中找到最大的元素（n0）。现在，我想证明列表中的所有元素都小于或等于n0。我在证明引理方面有问题。我想证明以下引理

I am arranging natural numbers in a specific order in the list. My defined function finds the greatest element(n0) in the list. Now I want to prove that all the elements in the list,are less or equal, to n0. I have a problem in proving a lemma. I want to prove the following lemma

Theorem values_les_than_n :forall(n0 n1:nat) ( l:list nat),    
        (g_value (length (n1 :: l))    
        (change n0 (n1 :: l)) <=? n0) = true
   
     Definition change (n: nat) (l: list nat) : list nat :=  
       match l with  
       | nil => l  
       | h::tl => if n <=? h then l else n::tl  end.
        Fixpoint g_value (elements: nat) (l: list nat) : nat :=       
        match l with       
         | nil => 0       
         | [n] => n       
         | h :: l => match elements with       
         | O => h       
         | S elements' => g_value elements' (change h l)
          end     
         end.
Lemma ni_con:forall(x:A)(l:list A),[]<>x::l.
Proof.
simpl.  discriminate. 
Qed.
Definition listvalue (n:nat)(l : list nat) : In (g_value n l) l -> nat.
intros.
apply : g_value (n l).
Defined.

Lemma value_in_input s l : 
  l = nil \/ In (g_value s l) l.
Proof.
intros.
left. 
assert(forall(x:A)(l:list A),[]<>x::l).
{ apply ni_con. }
simpl. auto . discriminate. 
right. unfold g_value. 
Admitted.

 Fixpoint In (a:nat) (l:list nat) : Prop :=
  match l with
  | nil => False
  | b :: m => b = a \/ In a m
  end.

   Fixpoint firstn {A} (x : nat) (ls : list A) : list A := 
    match x with
       |S n' => match ls with
             |h :: t => h::firstn n' t
             |[] => []
            end
      |0 => []
      end.

       Lemma value_greater s l n : In n (firstn s l) -> n <= g_value s l.
       Proof.
        induction 1. intros k H'.
      now exfalso; apply in_nil in H'. 
       Admitted.

推荐答案

该定理不能成立： n 完全独立于 n0 ， n1 或服务器。 g_value 表达式（在定理语句中）返回的值只能在 n0 n1 和服务器，不难确定值是否相同。这是一个示例：如果您能够证明该定理，就会出现矛盾。

This theorem cannot be true: n is completely independent from n0, n1, or servers. The value returned by the g_value expression (in your theorem statement) can only be taken among n0 n1 and servers, it is not hard to make sure the values are not the same. Here is an example: if you were able to prove the theorem, there would be a contradiction.

Require Import List Arith.

Import ListNotations.

Definition Servers := list nat.

Definition change (n: nat) (l: list nat) : list nat :=  
   match l with  
   | nil => l  
   | h::tl => if n <=? h then l else n::tl  end.

Fixpoint g_value (elements: nat) (l: list nat) : nat :=       
    match l with       
     | nil => 0       
     | [n] => n       
     | h :: l => match elements with       
     | O => h       
     | S elements' => g_value elements' (change h l)
      end     
     end.

Theorem values_les_than_n :forall(n n0 n1:nat) ( servers:Servers),    
    (g_value (length (n1 :: servers))    
    (change n0 (n1 :: servers)) <=? n) = true.
Admitted.

Lemma contradict_it : False.
  assert (tmp := values_les_than_n 0 1 1 nil).   
  discriminate tmp.
Qed.

在尝试证明之前，您应该经常测试功能。

You should often test your functions before attempting proofs.

这篇关于如何排列列表中的元素的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！