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
|
Goal forall A B C (p : forall (x : A) (y : B), C x y) (x : A) (y : B), True.
Proof.
intros A B C p x y.
match type of p with
| forall x y, @?F x y => pose F as C1
end.
match type of p with
| forall x y, @?F y x => pose F as C2
end.
assert (C1 x y) as ?.
assert (C2 y x) as ?.
Abort.
Goal forall A B C D (p : forall (x : A) (y : B) (z : C), D x y) (x : A) (y : B), True.
Proof.
intros A B C D p x y.
match type of p with
| forall x y z, @?F x y => pose F as C1
end.
assert (C1 x y) as ?.
Abort.
Goal forall A B C D (p : forall (z : C) (x : A) (y : B), D x y) (x : A) (y : B), True.
Proof.
intros A B C D p x y.
match type of p with
| forall z x y, @?F x y => pose F as C1
end.
assert (C1 x y) as ?.
Abort.
(** Those should fail *)
Goal forall A B C (p : forall (x : A) (y : B), C x y) (x : A) (y : B), True.
Proof.
intros A B C p x y.
Fail match type of p with
| forall x, @?F x y => pose F as C1
end.
Fail match type of p with
| forall x y, @?F x x y => pose F as C1
end.
Fail match type of p with
| forall x y, @?F x => pose F as C1
end.
Abort.
(** This one is badly typed *)
Goal forall A (B : A -> Type) (C : forall x, B x -> Type), (forall x y, C x y) -> True.
Proof.
intros A B C p.
Fail match type of p with
| forall x y, @?F y x => idtac
end.
Abort.
Goal forall A (B : A -> Type) (C : Type) (D : forall x, B x -> Type), (forall x (z : C) y, D x y) -> True.
Proof.
intros A B C D p.
match type of p with
| forall x z y, @?F x y => idtac
end.
Abort.
|
