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 to express a list of any type X? Using Coq	2	583	March 28, 2021
Proving obvious logic Using Coq	3	146	June 21, 2024
How can I use destruct given the constraint I have for index range of a list? Using Coq	1	558	October 4, 2020
What I'm doing wrong? Smth not computing Using Coq	1	522	November 24, 2019
Issue with syntax in tr_rev_correct Using Coq notation , software-foundations	2	49	June 27, 2024

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

Related topics