Home |
Source |
This group of tactics is very frequently used in the middles of proofs. Rewriting in all of its forms is an efficient way to bring together previously-independent parts of a goal.
rewrite takes an equivalence proof as input, like t1 = t2, and replaces all occurances of t1 with t2. Replacement of t2 with t1 can be achieved with the variant rewrite <- (rewrite backwards). Multiple rewrites can be chained with one tactic via a list of comma-separated equivalence proofs. Each of the equivalence proofs in the chain may be rewritten backwards. rewrite will fail if there are no t1’s (in this example) to replace.
(* Replace t1 with t2 in the goal *)
rewrite t1_eq_t2.
(* Rewrite in an assumption *)
rewrite Eq in H.
(* Rewrite in the goal and all assumptions *)
rewrite HEq in *.
(* Rewrite multiple values *)
rewrite t1_eq_t2, <- x_eq_y, ht_eq_ht.Before
x, y: nat
H: x = y
-------------------------
x + y = y + yrewrite H.After
x, y: nat
H: x = y
-------------------------
y + y = y + yAlternatively,
rewrite <- H.x, y: nat
H: x = y
-------------------------
x + x = x + xrename changes the name of an introduced variable or assumption.
(* Simple example *)
rename x into y.Before
n: nat
-------------------------
1/1
n = nrename n into x.After
x: nat
-------------------------
1/1
x = xremember gives a name to complex terms. Specifically, remember t (where t has type T) introduces an assumption that there exists a member of type T, gives it a name such as t0, and provides another assumption that t = t0.
(* Simple usage *)
remember (5 + x).
(* Provide a name for the remembered term *)
remember ("hello world") as s.Before
x, y: nat
H: x + y = x
-------------------------
1/1
y = 0remember (x + y) as sum.After
x, y, sum: nat
Heqsum: sum = x + y
H: sum = x
-------------------------
1/1
y = 0