blob: a759674115609f6c398282a50ea43e472ec18c4c (
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
|
(* Check the behaviour of Discriminate *)
(* Check that Discriminate tries Intro until *)
Lemma l1 : 0 = 1 -> False.
discriminate 1.
Qed.
Lemma l2 : forall H : 0 = 1, H = H.
discriminate H.
Qed.
(* Check the variants of discriminate *)
Goal O = S O -> True.
discriminate 1.
Undo.
intros.
discriminate H.
Undo.
Ltac g x := discriminate x.
g H.
Abort.
Goal (forall x y : nat, x = y -> x = S y) -> True.
intros.
try discriminate (H O) || exact I.
Qed.
Goal (forall x y : nat, x = y -> x = S y) -> True.
intros.
ediscriminate (H O).
instantiate (1:=O).
Abort.
(* Check discriminate on identity *)
Goal ~ identity 0 1.
discriminate.
Qed.
|
