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 …

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

Using Coq

olaure01 May 7, 2020, 6:44pm 3

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

Topic		Replies	Views
How can I use destruct given the constraint I have for index range of a list? Using Coq	1	498	October 4, 2020
What I'm doing wrong? Smth not computing Using Coq	1	482	November 24, 2019
Overload list notation Using Coq notation	3	910	September 27, 2021
[Very basic] stack overflow and computability Using Coq	1	237	November 23, 2023
Defining and working with trivial finite sets like {x, y, z} easily Using Coq notation	6	644	July 8, 2021

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

Related Topics