aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/somatching.v
blob: 5ed833ecc3b5a781407edb7b766a1bb2538f87e7 (plain)
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.