时间戳

首页 > 解决方案 > 自然数列表中的最大值

coq - 自然数列表中的最大值

问题描述

我已经定义了一个函数，它在自然数列表中找到最大值，并且列表的头部保存这个值。我想证明列表中的所有元素都小于或等于列表开头的自然数。我在证明引理时遇到问题。我写了两个引理，我想知道，这将有助于解决问题。感谢您的帮助和支持。

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.

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

 Fixpoint largest_value (numbers: nat) (l: list nat) {struct numbers}: nat:= 
 match l with
 | nil => 0
 | cons b nil => b 
 | cons h l => match numbers with
 | O => h
 | S numbers' => largest_value numbers' (change_variable h l)
  end
  end.

Theorem all_values_less :forall (n c :nat)(l:list nat),
(largest_value (length (c :: l))
 (change_variable n (c :: l)) <= n). 

    First in this way,
       Inductive changing : l -> Prop :=
        | change_nil : changing nil
        | change_1 n : changing (cons n nil)
        | change_head n h l :
         n <= h ->
        changing (cons h l) ->
      changing (cons n l).

  Lemma head_is_gt l a:
   changing  l -> forall n, In n l -> n <= hd a l.
      Proof.
      induction 1. intros k H'.
      now exfalso; apply in_nil in H'. 
      Admitted.
    
    Secondly ,
    Definition head_is_greater (l: list nat): nil <> l -> nat.
    intros.
    destruct l.
    destruct (H (@erefl (list nat) nil)).
     apply : (largest_value s l).
    
     Defined. 
     Theorem values_les_n : forall l (H : [] <> l) n, In n l -> n <= 
      head_is_greater H.

标签： coq

解决方案

不幸的是，这个定理不成立。这是一个反例：

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Lia.
Import ListNotations.

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

 Fixpoint largest_value (numbers: nat) (l: list nat) {struct numbers}: nat:=
 match l with
 | nil => 0
 | cons b nil => b
 | cons h l => match numbers with
 | O => h
 | S numbers' => largest_value numbers' (change_variable h l)
  end
  end.

Hypothesis all_values_less :forall (n c :nat)(l:list nat),
(largest_value (length (c :: l))
 (change_variable n (c :: l)) <= n).

Theorem contra : False.
Proof.
pose proof (all_values_less 0 1 []).
simpl in *. lia.
Qed.

您可能需要在您的陈述中添加更多假设以排除此类情况。

推荐阅读