blob: 130d9f9abfd923a572bd93fab424947ca80fa169 (
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
|
Goal ((forall (t : Type) (x y : t),
True ->
x = y)) -> False.
Proof.
intro HG.
let P := lazymatch goal with
| [ H : forall t x y, True -> @?P t x y
|- _ ]
=> P
end in
pose (f := P).
unify f (fun (t : Type) (x y : t) => x = y).
Abort.
Goal True.
Proof.
let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with
| fun _ y _ => @?C y => C
end in
pose (f := c).
unify f (fun n : nat => n).
Abort.
Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
Proof.
intro.
let P := lazymatch goal with
| [ H : forall y, @?P y -> @?P y \/ _ |- _ ]
=> P
end in
pose (f := P).
unify f (fun x : nat => x = x).
Abort.
Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
Proof.
intro.
lazymatch goal with
| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ]
=> idtac
end.
Abort.
Axiom eq : forall {T} (_ : T), Prop.
Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop.
Proof.
intro.
let P := lazymatch goal with
| [ H : forall t _ x, @?P t x |- _ ]
=> P
end in
pose (f := P).
Abort.
|
