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
|
Definition prod_map {A A' B B'} (f : A -> A') (g : B -> B')
(p : A * B) : A' * B'
:= (f (fst p), g (snd p)).
Arguments prod_map {_ _ _ _} _ _ !_ /.
Lemma test1 {A A' B B'} (f : A -> A') (g : B -> B') x y :
prod_map f g (x,y) = (f x, g y).
Proof.
Succeed progress simpl; match goal with |- ?x = ?x => idtac end. (* LHS becomes (f x, g y) *)
Succeed progress cbn; match goal with |- ?x = ?x => idtac end. (* LHS is not simplified *)
Admitted.
Axiom n : nat.
Arguments Nat.add _ !_.
Goal n + S n = 0.
Fail progress cbn.
Abort.
Goal S n + S n = 0.
progress cbn.
match goal with |- S (n + S n) = 0 => idtac end.
Abort.
Goal S n + n = 0.
Fail progress cbn.
Abort.
|
