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!

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

Last updated: Oct 03 2023 at 02:34 UTC