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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(* Interaction between coercions and casts *)
(* Example provided by Eduardo Gimenez *)
Parameter Z S : Set.
Parameter f : S -> Z.
Coercion f : S >-> Z.
Parameter g : Z -> Z.
Check (fun s => g (s:S)).
(* Check uniform inheritance condition *)
Parameter h : nat -> nat -> Prop.
Parameter i : forall n m : nat, h n m -> nat.
Coercion i : h >-> nat.
(* Check coercion to funclass when the source occurs in the target *)
Parameter C : nat -> nat -> nat.
Coercion C : nat >-> Funclass.
(* Remark: in the following example, it cannot be decided whether C is
from nat to Funclass or from A to nat. An explicit Coercion command is
expected
Parameter A : nat -> Prop.
Parameter C:> forall n:nat, A n -> nat.
*)
(* Check coercion between products based on eta-expansion *)
(* (there was a de Bruijn bug until rev 9254) *)
Section P.
Variable E : Set.
Variables C D : E -> Prop.
Variable G :> forall x, C x -> D x.
Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y).
End P.
(* Check that class arguments are computed the same when looking for a
coercion and when applying it (class_args_of) (failed until rev 9255) *)
Section Q.
Variable bool : Set.
Variables C D : bool -> Prop.
Variable G :> forall x, C x -> D x.
Variable f : nat -> bool.
Definition For_all (P : nat -> Prop) := forall x, P x.
Check fun (H : For_all (fun x => C (f x))) => H : forall x, D (f x).
Check fun (H : For_all (fun x => C (f x))) x => H x : D (f x).
Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
End Q.
(* Combining class lookup and path lookup so that if a lookup fails, another
descent in the class can be found (see wish #1934) *)
Record Setoid : Type :=
{ car :> Type }.
Record Morphism (X Y:Setoid) : Type :=
{evalMorphism :> X -> Y}.
Definition extSetoid (X Y:Setoid) : Setoid.
constructor.
exact (Morphism X Y).
Defined.
Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
(* Check that coercions are made visible only when modules are imported *)
Module A.
Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B.
Fail Check S true.
End A.
Import A.
Fail Check S true.
(* Tests after the inheritance condition constraint is relaxed *)
Inductive list (A : Type) : Type :=
nil : list A | cons : A -> list A -> list A.
Inductive vect (A : Type) : nat -> Type :=
vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n).
Fixpoint size A (l : list A) : nat := match l with nil _ => 0 | cons _ _ tl => 1+size _ tl end.
Section test_non_unif_but_complete.
Fixpoint l2v A (l : list A) : vect A (size A l) :=
match l as l return vect A (size A l) with
| nil _ => vnil A
| cons _ x xs => vcons A (size A xs) x (l2v A xs)
end.
Local Coercion l2v : list >-> vect.
Check (fun l : list nat => (l : vect _ _)).
End test_non_unif_but_complete.
Section what_we_could_do.
Variables T1 T2 : Type.
Variable c12 : T1 -> T2.
Class coercion (A B : Type) : Type := cast : A -> B.
Instance atom : coercion T1 T2 := c12.
Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) :=
fun x => (c1 (fst x), c2 (snd x)).
Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) :=
match l as l return vect B (size A l) with
| nil _ => vnil B
| cons _ x xs => vcons _ _ (c x) (l2v2 xs) end.
Local Coercion l2v2 : list >-> vect.
(* This shows that there is still something to do to take full profit
of coercions *)
Fail Check (fun l : list (T1 * T1) => (l : vect _ _)).
Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)).
Section what_we_could_do.
|
