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
|
(* as it is dynamically inferred by simpl *)
Arguments minus !n / m.
Lemma foo x y : S (S x) - S y = 0.
simpl.
match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end.
Abort.
(* we avoid exposing a match *)
Arguments minus n m : simpl nomatch.
Lemma foo x : minus 0 x = 0.
simpl.
match goal with |- (0 = 0) => idtac end.
Abort.
Lemma foo x y : S (S x) - S y = 0.
simpl.
match goal with |- (S x - y = 0) => idtac end.
Abort.
Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
simpl.
match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
Abort.
(* we unfold as soon as we have 1 args, but we avoid exposing a match *)
Arguments minus n / m : simpl nomatch.
Lemma foo : minus 0 = fun x => 0.
simpl.
match goal with |- minus 0 = _ => idtac end.
Abort.
(* This does not work as one may expect. The point is that simpl is implemented
as "strong (whd_simpl_state)" and after unfolding minus you have
(fun m => match 0 => 0 | S n => ...) that is already in whd and exposes
a match, that of course "strong" would reduce away but at that stage
we don't know, and reducing by hand under the lambda is against whd *)
(* extra tuning for the usual heuristic *)
Arguments minus !n / m : simpl nomatch.
Lemma foo x y : S (S x) - S y = 0.
simpl.
match goal with |- (S x - y = 0) => idtac end.
Abort.
Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
simpl.
match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
Abort.
(* full control *)
Arguments minus !n !m /.
Lemma foo x y : S (S x) - S y = 0.
simpl.
match goal with |- (S x - y = 0) => idtac end.
Abort.
Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
simpl.
match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
Abort.
(* omitting /, that being immediately after the last ! is irrelevant *)
Arguments minus !n !m.
Lemma foo x y : S (S x) - S y = 0.
simpl.
match goal with |- (S x - y = 0) => idtac end.
Abort.
Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
simpl.
match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
Abort.
Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) :=
fun x => (f (fst x), g (snd x)).
Delimit Scope foo_scope with F.
Notation "@@" := nat (only parsing) : foo_scope.
Notation "@@" := (fun x => x) (only parsing).
Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x.
Abort.
Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
(* fcomp is unfolded if applied to 6 args *)
Arguments fcomp {A B C}%type f g x /.
Notation "f \o g" := (fcomp f g) (at level 50).
Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x).
simpl.
match goal with |- (pf (f \o g) h x = _) => idtac end.
case x; intros x1 x2.
simpl.
match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end.
unfold pf; simpl.
match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
Abort.
Definition volatile := fun x : nat => x.
Arguments volatile / _.
Lemma foo : volatile = volatile.
simpl.
match goal with |- (fun _ => _) = _ => idtac end.
Abort.
Set Implicit Arguments.
Section S1.
Variable T1 : Type.
Section S2.
Variable T2 : Type.
Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
match n, m with
| 0,_ => 0
| S _, 0 => n
| S n', S m' => f x y n' v m' end.
Global Arguments f x y !n !v !m.
Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m).
simpl.
match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
Abort.
End S2.
Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m).
simpl.
match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
Abort.
End S1.
Arguments f : clear implicits and scopes.
|
