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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
Let test_stack_unification_interaction_with_delta A
: (if negb _ then true else false) = if orb false (negb A) then true else false
:= eq_refl.
(* Test patterns unification *)
Lemma l1 : (forall P, (exists x:nat, P x) -> False)
-> forall P, (exists x:nat, P x /\ P x) -> False.
Proof.
intros; apply (H _ H0).
Qed.
Lemma l2 : forall A:Set, forall Q:A->Set,
(forall (P: forall x:A, Q x -> Prop),
(exists x:A, exists y:Q x, P x y) -> False)
-> forall (P: forall x:A, Q x -> Prop),
(exists x:A, exists y:Q x, P x y /\ P x y) -> False.
Proof.
intros; apply (H _ H0).
Qed.
Lemma l3 : (forall P, ~(exists x:nat, P x))
-> forall P:nat->Prop, ~(exists x:nat, P x -> P x).
Proof.
intros; apply H.
Qed.
(* Feature introduced June 2011 *)
Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
Proof.
intros x P H; apply H.
Qed.
(* Example submitted for Zenon *)
Axiom zenon_noteq : forall T : Type, forall t : T, ((t <> t) -> False).
Axiom zenon_notall : forall T : Type, forall P : T -> Prop,
(forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
(* Must infer "P := fun x => x=x" in zenon_notall *)
Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
(fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)).
(* Core of an example submitted by Ralph Matthes (BZ#849)
It used to fail because of the K-variable x in the type of "sum_rec ..."
which was not in the scope of the evar ?B. Solved by a head
beta-reduction of the type "(fun _ : unit + unit => L unit) x" of
"sum_rec ...". Shall we used more reduction when solving evars (in
real_clean)?? Is there a risk of starting too long reductions?
Note that the example originally came from a non re-typable
pretty-printed term (the checked term is actually re-printed the
same form it is checked).
*)
Set Implicit Arguments.
Inductive L (A:Set) : Set := c : A -> L A.
Parameter f: forall (A:Set)(B:Set), (A->B) -> L A -> L B.
Parameter t: L (unit + unit).
Check (f (fun x : unit + unit =>
sum_rec (fun _ : unit + unit => L unit)
(fun y => c y) (fun y => c y) x) t).
(* Test patterns unification in apply *)
Require Import Arith.
Parameter x y : nat.
Parameter G:x=y->x=y->Prop.
Parameter K:x<>y->x<>y->Prop.
Lemma l4 : (forall f:x=y->Prop, forall g:x<>y->Prop,
match eq_nat_dec x y with left a => f a | right a => g a end)
-> match eq_nat_dec x y with left a => G a a | right a => K a a end.
Proof.
intros.
apply H.
Qed.
(* Test unification modulo eta-expansion (if possible) *)
(* In this example, two instances for ?P (argument of hypothesis H) can be
inferred (one is by unifying the type [Q true] and [?P true] of the
goal and type of [H]; the other is by unifying the argument of [f]);
we need to unify both instances up to allowed eta-expansions of the
instances (eta is allowed if the meta was applied to arguments)
This used to fail before revision 9389 in trunk
*)
Lemma l5 :
forall f : (forall P, P true), (forall P, f P = f P) ->
forall Q, f (fun x => Q x) = f (fun x => Q x).
Proof.
intros.
apply H.
Qed.
(* Feature deactivated in commit 14189 (see commit log)
(* Test instantiation of evars by unification *)
Goal (forall x, 0 + x = 0 -> True) -> True.
intros; eapply H.
rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
Abort.
*)
(* Check handling of identity equation between evars *)
(* The example failed to pass until revision 10623 *)
Lemma l6 :
(forall y, (forall x, (forall z, y = 0 -> y + z = 0) -> y + x = 0) -> True)
-> True.
intros.
eapply H.
intros.
apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *)
reflexivity.
Qed.
(* Check treatment of metas erased by K-redexes at the time of turning
them to evas *)
Inductive nonemptyT (t : Type) : Prop := nonemptyT_intro : t -> nonemptyT t.
Goal True.
try case nonemptyT_intro. (* check that it fails w/o anomaly *)
Abort.
(* Test handling of return type and when it is decided to make the
predicate dependent or not - see "bug" BZ#1851 *)
Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True).
intros.
exists (fun n => match n with O => a | S n' => f' n' end).
constructor.
Qed.
(* Check use of types in unification (see Andrej Bauer's mail on
coq-club, June 1 2009; it did not work in 8.2, probably started to
work after Sozeau improved support for the use of types in unification) *)
Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
Proof.
intros.
rewrite H with (f:=f0).
Abort.
(* Three tests provided by Dan Grayson as part of a custom patch he
made for a more powerful "destruct" for handling Voevodsky's
Univalent Foundations. The test checks if second-order matching in
tactic unification is able to guess by itself on which dependent
terms to abstract so that the elimination predicate is well-typed *)
Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) :
identity (fxe x) (fxe x).
Proof. destruct (fxe x). apply identity_refl. Defined.
(* a harder example *)
Definition UU := Type .
Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0.
Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1.
Proof. intros t. exact t. Defined.
Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k).
Proof.
destruct k.
apply idpath.
Defined.
(* an example with two constructors *)
Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU :=
| newfoo1 : foo' x0 x0
| newfoo2 : foo' x0 x0 .
Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} :
foo' x0 x1 -> foo' x0 x1.
Proof. intros t. exact t. Defined.
Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k).
Proof.
destruct k.
apply idpath.
apply idpath.
Defined.
(* An example where it is necessary to evar-normalize the instance of
an evar to evaluate if it is a pattern *)
Check
let a := ?[P] in
fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
x (p:x=0) =>
H ?[y] a p : x = 0.
(* We have to solve "?P ?y[x] == x = 0" knowing from
"p : (x=0) == (?y[x] = 0)" that "?y := x" *)
|
