英文:
Is there a way for Coq to recall it already proved a property for the same element in the same proof?
问题
在Coq中，我有一个关于元素的归纳性质，这些元素在同一个证明中可能出现多次。我想知道Coq是否可以记住已经证明过该属性的元素。另外，我想知道如何自动化简单的证明，就像我示例中的那个：
Require Import List.
Require Import List Notations.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Inductive Figure : Type :=
| P : Figure
| L : Figure -> Figure -> Figure
| C : list Figure -> Figure.
Inductive good : Figure -> Prop :=
| gP : good P
| gL : good (L P P)
| gC (ff: list Figure) (H1: goodL ff): good (C ff)
with goodL : list Figure -> Prop :=
| g0 : goodL nil
| g' (f: Figure) (ff: list Figure) (H1: good f) (H2: goodL ff) : goodL (f::ff).
Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. apply g'. apply gP. apply g'. apply gL.
apply g'. apply gC. apply g'. apply gP. apply g'. apply gL. apply g0. apply g0.
正如你在示例中所看到的，good P 和 good (L P P) 的证明出现了两次。在实际情况下，这可能会在同一个证明中发生数十次。断言中间引理的话可能帮助不大，因为要应用的规则非常直接。只是我可能有许多具有相同元素的子级别列表，我希望Coq能够记住我们已经证明过它们。另一个选择是让Coq做大部分工作，因为这看起来非常容易自动化，但我只是一个初学者。谢谢。
英文:
In Coq, I have an inductive property on elements which may appear many times in the same proof. I would like to know if it is possible for Coq to memorize elements for which the property has already been proven. Also I would like to know how it is possible to automatize simple proofs such as the one in my minimal working example:
Require Import List.
Require Import List Notations.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Inductive Figure : Type :=
| P : Figure
| L : Figure -> Figure -> Figure
| C : list Figure -> Figure.
Inductive good : Figure -> Prop :=
|gP : good P
|gL : good (L P P)
|gC (ff: list Figure) (H1: goodL ff): good (C ff)
with goodL : list Figure -> Prop :=
|g0 : goodL nil
|g' (f: Figure) (ff: list Figure) (H1: good f) (H2: goodL ff) : goodL (f::ff).
Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. apply g'. apply gP. apply g'. apply gL.
apply g'. apply gC. apply g'. apply gP. apply g'. apply gL. apply g0. apply g0.
As you can see in the example, the proof for good P and good (L P P) appear twice. In the real case, this could happen dozens of times in the same proof. Asserting intermediate lemmas would be of little help as the rules to apply are quite direct. It is just that I may have many sub-levels of lists with the same elements and I would like Coq to recall that we already proved them. Another option is to have Coq to most of work, as this looks like pretty straightforward to automatize, but I am only a beginner. Thank you.
答案1
得分: 3
如果你只有一堆 apply，通常可以使用 auto 进行重构，你可以通过 using 显式传递相关引理，或者通过 Hint 数据库隐式传递：
auto 10 using g', g0, gP, gL, gC.
或者，因为这些都是构造函数，
repeat constructor.
只有在该策略明显变慢时，重复的工作才会成为问题，此时你可以将工作提取为中间引理，并将它们添加到 auto using ... 或者最终采用的任何自动化脚本中。
英文:
If you just have a bunch of apply, you can usually refactor it using auto, to which you can pass the relevant lemmas explicitly with using (or implicitly via Hint databases):
auto 10 using g', g0, gP, gL, gC.
or, since those are all constructors,
repeat constructor.
Duplicate work only becomes a problem when it makes the tactic noticeably slow, at which point you can extract the work as intermediate lemmas and add them to auto using ... or whatever automation script you end up with.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论