Coq：自动重复重写
Coq: automate repeated rewriting
Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof.
intros f n H. repeat rewrite H. reflexivity.
Qed.
进一步自动化的好方法是什么？特别是，我不想在任何地方提及假设的名称。
如果可以通过一些重写序列来解决目标，那么 congruence 策略就可以解决。
The tactic congruence, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols. It also include the constructor theory (see 8.5.7 and 8.5.6). If the goal is a non-quantified equality, congruence tries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
congruence is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for congruence to match against it.
以上基本上是说congruence可以用rewrite和discriminate战术解决你的目标。但有时 congruence 无法帮助您，因为它不会为您展开定义 - 在这种情况下，您将不得不帮助它。
Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof. congruence. Qed.
Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof.
intros f n H. repeat rewrite H. reflexivity.
Qed.
进一步自动化的好方法是什么？特别是，我不想在任何地方提及假设的名称。
如果可以通过一些重写序列来解决目标，那么 congruence 策略就可以解决。
The tactic
congruence, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols. It also include the constructor theory (see 8.5.7 and 8.5.6). If the goal is a non-quantified equality,congruencetries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality from those in the context. Alternatively,congruencetries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
congruenceis also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order forcongruenceto match against it.
以上基本上是说congruence可以用rewrite和discriminate战术解决你的目标。但有时 congruence 无法帮助您，因为它不会为您展开定义 - 在这种情况下，您将不得不帮助它。
Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof. congruence. Qed.