如何在不同的指数下寻找价值

Question

我定义了一个函数，从自然数列表中找到最大的值，并将这个值移动到列表的头部位置。我确定，列表中的所有元素都小于或等于头部位置的值，然后我定义了index_value函数，用于查找列表中任意索引的值。然后，我定义了index_value函数，以找到列表中任何索引的值。为了澄清[4,7,11,9,11]列表成为[11,7,9,11]。请指导我。

 ` Require Import Coq.Arith.PeanoNat.
   Require Import Lia.
   Fixpoint index_value (index: nat) (l: list nat) : nat :=
   match l with
         | nil => 0
         | cons h t => match (Nat.eqb index 0) with
         | true => h
         | false => index_value (index - 1) t
        end
          end.

Theorem head_value : forall ( n':nat) (l:list nat),
 (index_value 0 l)<= n'.
 Proof.
 Admitted.
 Theorem index_value1:forall (n s2:nat) (l:list nat),
 index_value  (S s2) (n :: l) <=
  index_value  0 (n :: l) \/
 index_value  (S s2) (n :: l) > 0.
 Proof.
  intros. simpl in *. left . induction s2. simpl. 
   appply head_value . simpl in *.  auto with arith.`

Answer 1

我认为你的说法不完全是你认为的意思。 第一条是矛盾的，第二条是琐碎的：你不需要定义的 index_value 完全没有。

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

Import ListNotations.

Fixpoint index_value (index: nat) (l: list nat) : nat :=
  match l with
  | nil => 0
  | cons h t => match (Nat.eqb index 0) with
                | true => h
                | false => index_value (index - 1) t
                end
  end.

Theorem not_head_value :
  ~ forall ( n':nat) (l:list nat),
                             (index_value 0 l)<= n'.
Proof.
  intros contra.
  specialize (contra 0 (1 :: nil)).
  simpl in *. lia.
Qed.

Theorem index_value1:forall (n s2:nat) (l:list nat),
    index_value  (S s2) (n :: l) <=
    index_value  0 (n :: l) \/
    index_value  (S s2) (n :: l) > 0.
Proof. intros n s2 l. lia. Qed.