Stream: Coq users

Topic: Index Map proof

view this post on Zulip 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).
intros. generalize dependent n. induction l.

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

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

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

If someone can introduce me, thank you in advance!

view this post on Zulip 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: Jun 25 2024 at 15:02 UTC