CODEWITHSUNDEEP
coq
laiba naz
laiba naz

Reputation: 57

Position of elements in list

I am using index function to find the value of element at any location in the list nat. Plz guide me in proving the second part of the lemma, which is illustrated below 

 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.

Upvotes: 0

Views: 162

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

The theorem you want cannot be proved:

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.

Upvotes: 1

Related Questions