I defined it in such way: Definition eq_dec A := forall (x y: A), { x = y } + { x <> y }. Definition index_error A (dec: eq_dec A) (x: A) (L: list A): option nat. Proof. induction L. + exact None. + destruct (dec x a). - exact (Some 0). - exact (match IHL with Some n => Some (S n) | …

Hello, I would attack the problem as follows: For any list L : list A and any f : A -> B, show that map f L = map (fun n => f (nth n L d)) (seq 0 (length L)) For any L : list A and any f g : A -> B, show that (forall x, In x L -> f x = g x) -> map f L = map g L. Let f i = index dec d i …

Concerning the original question about index, it looks indeed natural in a context of lists on types with decidable equality. As first key statements, I would start with your argument of being an inverse for nth: index (nth ...) = ... and nth (index ...) = .... By the way, I would recommend to kee…

I proved both Theorem index_nth_id A (dec: eq_dec A) (L: list A) d d' (H: NoDup L) n (H0: n < length L): index dec (nth n L d') L d = n. and Theorem nth_index_id A (dec: eq_dec A) (L: list A) d d' x (H: In x L): nth (index dec x L d) L d' = x. And few other theorems at https://github.com/Lessnes…

Idea to add "index" function to Standard Library (or maybe not)

Using Rocq

olaure01 May 7, 2020, 6:44pm 3

Note that @nojb point 1 here moves us back to @nojb point 2 there.

Topic		Replies	Views
Yet another simple theorem Using Rocq	8	1224	May 4, 2020
How to express a list of any type X? Using Rocq	2	604	March 28, 2021
How to approach this (seemingly) simple theorem? Using Rocq	7	855	April 17, 2020
Another simple theorem Using Rocq	4	606	April 19, 2020
What I'm doing wrong? Smth not computing Using Rocq	1	537	November 24, 2019

Idea to add "index" function to Standard Library (or maybe not)

Related topics