Положение элементов в списке

Question

Я использую функцию индекса, чтобы найти значение элемента в любом месте списка nat. Плз, помогите мне в доказательстве второй части леммы, которая проиллюстрирована ниже

 Fixpoint index(n: nat) (m: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h tl => match (eqb n m) with
| true => h
| false => index (succ n) m tl
 end
  end.
  Theorem a_ref:forall (a:nat),
    a <= a.
 Proof.
    intros. eauto.
  Qed.
Theorem n_leq_0 :forall (n:nat),
  n <= 0.
  Proof.
  intros. induction n.
+ simpl. apply a_ref.
+ Admitted.
Theorem n_le_index:forall (n:nat) (l:list nat),
 n <= index (succ (succ 0)) 0 l.
Proof.
intros. induction l as [| l'].
+ simpl. apply n_leq_0.
+ simpl in *.  inversion IHl.  
rewrite <- H.

Answer 1

Теорема, которую вы хотите, не может быть доказана:

Fixpoint index(n: nat) (m: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h tl => match (Nat.eqb n m) with
| true => h
| false => index (Nat.succ n) m tl
 end
  end.

Theorem n_le_index:forall (n:nat) (l:list nat),
 n <= index (Nat.succ (Nat.succ 0)) 0 l.
Admitted.

Require Import Omega.

Goal False.
pose proof (n_le_index 10 nil).
simpl in H.
omega.
Qed.