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
|
(* Test apply in *)
Goal (forall x y, x = S y -> y=y) -> 2 = 4 -> 3=3.
intros H H0.
apply H in H0.
assumption.
Qed.
Require Import ZArith.
Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z.
intros; apply Znot_le_gt, Zgt_lt in H.
apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
Qed.
(* Check if it unfolds when there are not enough premises *)
Goal forall n, n = S n -> False.
intros.
apply n_Sn in H.
assumption.
Qed.
(* Check naming in with bindings; printing used to be inconsistent before *)
(* revision 9450 *)
Notation S':=S (only parsing).
Goal (forall S, S = S' S) -> (forall S, S = S' S).
intros.
apply H with (S0 := S).
Qed.
(* Check inference of implicit arguments in bindings *)
Goal exists y : nat -> Type, y 0 = y 0.
exists (fun x => True).
trivial.
Qed.
(* Check universe handling in typed unificationn *)
Definition E := Type.
Goal exists y : E, y = y.
exists Prop.
trivial.
Qed.
Variable Eq : Prop = (Prop -> Prop) :> E.
Goal Prop.
rewrite Eq.
Abort.
(* Check insertion of coercions in bindings *)
Coercion eq_true : bool >-> Sortclass.
Goal exists A:Prop, A = A.
exists true.
trivial.
Qed.
(* Check use of unification of bindings types in specialize *)
Variable P : nat -> Prop.
Variable L : forall (l : nat), P l -> P l.
Goal P 0 -> True.
intros.
specialize L with (1:=H).
Abort.
Reset P.
(* Two examples that show that hnf_constr is used when unifying types
of bindings (a simplification of a script from Field_Theory) *)
Require Import List.
Open Scope list_scope.
Fixpoint P (l : list nat) : Prop :=
match l with
| nil => True
| e1 :: nil => e1 = e1
| e1 :: l1 => e1 = e1 /\ P l1
end.
Variable L : forall n l, P (n::l) -> P l.
Goal forall (x:nat) l, P (x::l) -> P l.
intros.
apply L with (1:=H).
Qed.
Goal forall (x:nat) l, match l with nil => x=x | _::_ => x=x /\ P l end -> P l.
intros.
apply L with (1:=H).
Qed.
(* The following call to auto fails if the type of the clause
associated to the H is not beta-reduced [but apply H works]
(a simplification of a script from FSetAVL) *)
Definition apply (f:nat->Prop) := forall x, f x.
Goal apply (fun n => n=0) -> 1=0.
intro H.
auto.
Qed.
(* The following fails if the coercion Zpos is not introduced around p
before trying a subterm that matches the left-hand-side of the equality
(a simplication of an example taken from Nijmegen/QArith) *)
Require Import ZArith.
Coercion Zpos : positive >-> Z.
Variable f : Z -> Z -> Z.
Variable g : forall q1 q2 p : Z, f (f q1 p) (f q2 p) = Z0.
Goal forall p q1 q2, f (f q1 (Zpos p)) (f q2 (Zpos p)) = Z0.
intros; rewrite g with (p:=p).
reflexivity.
Qed.
|
