Stream: Coq users

Topic: Index Map proof

Malad Neymar (Apr 14 2021 at 15:49):

Hello guys! I'm very exciting learning COQ and just found this group. But i'm really having trouble with this specific exercise

Theorem index_map : forall {X Y:Set} (n:nat) (f:X->Y) (l:list X) (x:X),
index n l = Some x -> Some (f x) = index n (map f l).
Proof.
intros. generalize dependent n. induction l.

- simpl. intros. apply H. reflexivity.
- simpl. rewrite <- IHl. reflexivity.
Qed.

I'm using theses Fixpoints
Fixpoint index {X : Set} (n : nat) (l : list X) : option X :=
match l with
| [] => None
| h :: t => if n =? 0 then Some h else index (pred n) t
end.

Fixpoint map {X Y: Type} (f:X->Y) (l:list X) : (list Y) :=
match l with
| [] => []
| h :: t => (f h) :: (map f t)
end.

If someone can introduce me, thank you in advance!

Li-yao (Apr 14 2021 at 18:15):

Where are you getting stuck? Is there a particular goal you don't know how to solve?

Last updated: Oct 13 2024 at 01:02 UTC