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
|
Arguments plus : simpl never.
Lemma test1 P : P 3 -> P (1 + 2).
Proof.
intros p3.
simpl.
match goal with |- P (_ + _) => idtac "ok" end.
assumption.
Qed.
Definition plus' := plus.
Lemma test2 P : P 3 -> P (plus' 1 2).
Proof.
intros p3.
simpl.
match goal with |- P (plus' _ _) => idtac "ok" end.
assumption.
Qed.
Lemma test3 P : P 3 -> P (1 + 2).
Proof.
intros p3.
pose (plus'' := plus).
assert (P (plus'' 1 2)).
simpl.
match goal with |- P (plus'' _ _) => idtac "ok" end.
assumption.
assumption.
Qed.
Fixpoint rec_id (x : nat) := match x with O => O | S p => S (rec_id p) end.
Arguments rec_id : simpl never.
Lemma test4 P : P 3 -> P (rec_id 3).
Proof.
intros p3.
simpl.
match goal with |- P (rec_id _) => idtac "ok" end.
assumption.
Qed.
Arguments rec_id ! _ / .
Lemma test5 P : P 3 -> P (rec_id 3).
Proof.
intros p3.
simpl.
match goal with |- P 3 => idtac "ok" end.
assumption.
Qed.
|
