blob: 35ba94fb675a16087faa82e3f0dbbafeed6a756b (
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
65
66
67
68
69
70
71
|
(* Thinning introduction hypothesis must be done after all introductions *)
(* Submitted by Guillaume Melquiond (bug #1000) *)
Goal forall A, A -> True.
intros _ _.
Abort.
(* This did not work until March 2013, because of underlying "red" *)
Goal (fun x => True -> True) 0.
intro H.
Abort.
(* This should still work, with "intro" calling "hnf" *)
Goal (fun f => True -> f 0 = f 0) (fun x => x).
intro H.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.
(* Somewhat related: This did not work until March 2013 *)
Goal (fun f => f 0 = f 0) (fun x => x).
hnf.
match goal with [ |- 0 = 0 ] => reflexivity end.
Abort.
(* Fixing behavior of "*" and "**" in branches, so that they do not
introduce more than what the branch expects them to introduce at most *)
Goal forall n p, n + p = 0.
intros [|*]; intro p.
Abort.
(* Check non-interference of "_" with name generation *)
Goal True -> True -> True.
intros _ ?.
exact H.
Qed.
(* A short test about introduction pattern pat/c *)
Goal (True -> 0=0) -> True /\ False -> 0=0.
intros H (H1/H,_).
exact H1.
Qed.
(* A test about bugs in 8.5beta2 *)
Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
intros H H0 H1.
destruct H0 as (a/H,_).
(* Check that H0 is removed (was bugged in 8.5beta2) *)
Fail clear H0.
(* Check position of newly created hypotheses when using pat/c (was
left at top in 8.5beta2) *)
match goal with H:_ |- _ => clear H end. (* clear H1:False *)
match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
Qed.
Goal (True -> 0=0) -> True -> 0=0.
intros H H1/H.
exact H1.
Qed.
Goal forall n, n = S n -> 0=0.
intros n H/n_Sn.
destruct H.
Qed.
(* Another check about generated names and cleared hypotheses with
pat/c patterns *)
Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
intros H (H1,?)/H.
change (1=1) in H0.
exact H1.
Qed.
|
