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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
(* 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 _ _)).
End what_we_could_do.
(** Unit test for Prop as source class *)
Module TestPropAsSourceCoercion.
Parameter heap : Prop.
Parameter heap_empty : heap.
Definition hprop := heap -> Prop.
Coercion hpure (P:Prop) : hprop := fun h => h = heap_empty /\ P.
Parameter heap_single : nat -> nat -> hprop.
Parameter hstar : hprop -> hprop -> hprop.
Notation "H1 \* H2" := (hstar H1 H2) (at level 69).
Definition test := heap_single 4 5 \* (5 <> 4) \* heap_single 2 4 \* (True).
(* Print test. -- reveals [hpure] coercions *)
End TestPropAsSourceCoercion.
(** Unit test for Type as source class *)
Module TestTypeAsSourceCoercion.
Require Import Coq.Setoids.Setoid.
Record setoid := { A : Type ; R : relation A ; eqv : Equivalence R }.
Definition default_setoid (T : Type) : setoid
:= {| A := T ; R := eq ; eqv := _ |}.
Coercion default_setoid : Sortclass >-> setoid.
Definition foo := Type : setoid.
Inductive type := U | Nat.
Inductive term : type -> Type :=
| ty (_ : Type) : term U
| nv (_ : nat) : term Nat.
Coercion ty : Sortclass >-> term.
Definition ty1 := Type : term _.
Definition ty2 := Prop : term _.
Definition ty3 := Set : term _.
Definition ty4 := (Type : Type) : term _.
End TestTypeAsSourceCoercion.
|
