How to arrange elements in the list

Question

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.

Answer 1

I am adding a new answer because the comments on the previous answer make it possible to clarify the initial intent.

In the initial question, the author wishes to show that g_value (length l) l always returns the greatest element of l or 0 if l is empty. However, in the statement that is proposed in the initial question, or in the statement proposed later in the comments, there is no constraint on n.

So you should simply write the following two lemmas:

Lemma value_in_input s l : l = nil \/ In (g_value s l) l.

Lemma value_greater s l n : In n (firstn s l) -> n <= g_value s l.

I had time to check that both statements are provable.

The function firstn is provided in the Coq standard library, and it is recursive on its two inputs. An analysis of g_value (and the feedback message from Coq) tells us that g_value is recursive on its first argument, this suggests that value_greater should be proved by induction on n.

Here is an example of how this proof can be done:

Lemma value_greater s l n : In n (firstn s l) -> n <= g_value s l.
Proof.
revert l n; induction s as [ | s IH].
  destruct l as [ | n1 l]; contradiction.
destruct l as [ | n1 [ | n2 l]]; try contradiction.
  simpl; intros n [nn1 | abs].
    now rewrite nn1; auto with arith.
  destruct s; simpl in abs; contradiction.
intros n inn.
simpl.
destruct (n1 <=? n2) eqn:cmp.
  simpl in inn.
  destruct inn as [n1_is_n | inn'].
    apply le_trans with n2.
      rewrite <- Nat.leb_le.
      rewrite <- n1_is_n.
      exact cmp.
    destruct s as [ | s'].
      simpl.
      destruct l.
        apply le_n.
      now apply le_n.
    apply IH.
    simpl.
    now auto.
  apply IH. 
  exact inn'.
assert (n1le : n1 <= g_value s (n1 :: l)).
  destruct s as [ | s'].
     simpl.
   destruct l.
      apply le_n.
    apply le_n.
  apply IH.
  simpl.
  now auto.
simpl in inn.
destruct inn as [n1_is_n | other].
  rewrite <- n1_is_n.
  assumption.
destruct s as [ | s'].    
  simpl in other.
  now destruct other.
simpl in other.
destruct other as [n2_is_n | other'].
  rewrite <- n2_is_n.
  apply le_trans with n1.
    apply Nat.lt_le_incl.
    rewrite <- Nat.leb_gt.
    exact cmp.
  exact n1le.
apply IH.
simpl.
right.
exact other'.
Qed.

This proof is long and complicated, but it feels to me that you have some responsibility for that, because the code of g_value and change are overly complicated for the purpose at hand.

Your attempt for a proof of induction goes in the wrong direction because, you let s be fixed during the induction proof, but in recursive calls to g_value and firstn, s decreases. If s is fixed, the induction hypotheses cannot be used to reason about the recursive calls.

Answer 2

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.