1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
Require Import Utf8 Relation_Definitions.
Class Equiv A := equiv: relation A.
Hint Mode Equiv ! : typeclass_instances.
Class Lookup (K A M : Type) := lookup: K → M → option A.
Hint Mode Lookup ! - - : typeclass_instances.
Hint Mode Lookup - - ! : typeclass_instances.
Parameter list_equiv : ∀ A, Equiv A → Equiv (list A).
Parameter option_equiv : ∀ A, Equiv A → Equiv (option A).
Parameter list_lookup : ∀ A, Lookup nat A (list A).
Existing Instance list_equiv.
Existing Instance option_equiv.
Existing Instance list_lookup.
Set Typeclasses Debug.
(* fails *)
Lemma list_equiv_lookup {A} `{Equiv A} (l k : list A) :
equiv l k ↔ ∀ i, equiv (lookup i l) (lookup i k).
Admitted.
(*
?Equiv : "Equiv (option ?A)"
?Lookup : "Lookup ?K ?A (list A)"
?Lookup0 : "Lookup ?K ?A (list A)"
*)
|
