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
|
From stdpp Require Import tactics strings.
Unset Mangle Names.
Check "eunify_test".
Lemma eunify_test : ∀ x y, 0 < S x + y.
Proof.
intros x y.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
match goal with
| |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
end.
lia.
Qed.
Check "eunify_test_evars".
Lemma eunify_test_evars : ∃ x y, 0 < S x + y.
Proof.
eexists _, _.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds even if the goal contains evars *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
(* Let's try to use [eunify] to instantiate the first evar *)
match goal with
| |- 0 < ?x => eunify x (1 + _)
end.
(* And the other evar *)
match goal with
| |- 0 < ?x => eunify x 2
end.
lia.
Qed.
|
