为什么构造函数在这里要花这么长时间？ [英] Why does constructor take such a long time here?

问题描述

考虑以下代码：

Inductive Even : nat -> Prop :=
| EO : Even O
| ESS : forall n, Even n -> Even (S (S n)).

Fixpoint is_even_prop (n : nat) : Prop :=
  match n with
  | O => True
  | S O => False
  | S (S n) => is_even_prop n
  end.

Theorem is_even_prop_correct : forall n, is_even_prop n -> Even n.
Admitted.

Example Even_5000 : Even 5000.
Proof.
  apply is_even_prop_correct.

  Time constructor. (* ~0.45 secs *)
  Undo.

  Time (constructor 1). (* ~0.25 secs *)
  Undo.

  (* The documentation for constructor says that "constructor 1"
     should be the same thing as doing this: *)
  Time (apply I). (* ~0 secs *)
  Undo.

  (* Apparently, if there's only one applicable constructor,
     reflexivity falls back on constructor and consequently
     takes as much time as that tactic: *)
  Time reflexivity. (* Around ~0.45 secs also *)
  Undo.

  (* If we manually reduce before calling constructor things are
     faster, if we use the right reduction strategy: *)
  Time (cbv; constructor). (* ~0 secs *)
  Undo.

  Time (cbn; constructor). (* ~0.5 secs *)
Qed.

Theorem is_even_prop_correct_fast : forall n, is_even_prop n = True -> Even n.
Admitted.

Example Even_5000_fast : Even 5000.
Proof.
  apply is_even_prop_correct_fast.

  (* Everything here is essentially 0 secs: *)
  Time constructor.
  Undo.
  Time reflexivity.
  Undo.
  Time (apply eq_refl). Qed.

我只是想看看您是否可以在 Prop 而不是 Set 并偶然发现了这一点。我的问题不是如何正确进行反射，我只想知道为什么 constructor 在第一种情况下比第二种情况这么慢？ （也许与构造函数有关系，可以立即看到（不作任何减少）构造函数必须为 eq_refl 在第二种情况下呢？但是事后它仍然必须减少...）

I just wanted to see if you could do reflection in Prop rather than Set and stumbled upon this. My question is not how to do the reflection properly, I just want to know why constructor is so slow in the first case compared to the second case. (Maybe it has something to do with that constructor can immediately see (without any reductions) that the constructor must be eq_refl in the second case? But it must still reduce afterwards...)

此外，在试图弄清楚构造函数正在执行此操作时，我注意到文档未说明该策略将使用哪种减少策略。这种疏忽是故意的吗，其想法是，如果您特别想要一种减少策略，则应该明确地说出您想要哪种减少策略（否则该实现可以自由选择）？

Also, while trying to figure out what constructor is doing I noticed that the documentation does not say which reduction strategy will be used by the tactic. Is this omission intentional, and the idea is that you should explicitly say which reduction strategy you want if you want one in particular (otherwise the implementation is free to pick any)?

推荐答案

简短的回答：它花费时间试图弄清您的目标是哪个归纳家庭的一部分（对于构造函数），使用 hnf 。

Short answer: It spends its time trying to figure out what inductive family your goal is a part of (twice, in the case of constructor), using hnf.

更长的答案：做一些源头潜水，看起来像< a href = https://github.com/coq/coq/blob/V8.7+beta1/plugins/ltac/coretactics.ml4#L118 rel = nofollow noreferrer> 构造函数调用 Tactics.any_constructor ，而 构造函数1 调用 Tactics.constructor_tac 。 战术。 any_constructor 依次调用 Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind 确定归纳类型以计算构造函数，然后调用 Tactics.constructor_tac 依次在每个可能的构造函数上。对于 True ，由于有一个构造函数，因此暗示构造函数的时间大约是<$的两倍。 c $ c>构造函数1 ;我猜测时间因此花费在 reduce_to_quantified_ind 中。 Tacred.reduce_to_quantified_ind 依次调用 reduce_to_ind_gen ，依次称为 hnf_constr 。而且，确实， Time hnf 和 Time构造函数1 看起来差不多。此外，时间构造函数在手动 hnf 之后是即时的。我不确定 hnf 在内部使用什么策略。文档遗漏几乎肯定不是故意的（至少，无论当前策略是什么，我都认为应该在脚注中显示，所以随时报告错误），但是我不清楚<$ c使用的减少策略$ c>构造函数，以确定您的目标属于哪个归纳族应该成为构造函数规范的一部分。

Longer answer: Doing a bit of source-diving, it looks like constructor calls Tactics.any_constructor, while constructor 1 calls Tactics.constructor_tac. Tactics.any_constructor in turn calls Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind to determine the inductive type to count the constructors, and then calls Tactics.constructor_tac on each possible constructor in turn. For True, since there is one constructor, it's suggestive that the time for constructor is about double the time for constructor 1; I'm guessing that the time is therefore spent in reduce_to_quantified_ind. Tacred.reduce_to_quantified_ind, in turn, calls reduce_to_ind_gen, which, in turn calls hnf_constr. And, indeed, it looks like Time hnf and Time constructor 1 are about the same. Furthermore, Time constructor is instant after a manual hnf. I'm not sure what strategy hnf uses internally. The documentation omission is almost certainly not deliberate (at least, whatever the current strategy is should appear in a footnote, I think, so feel free to report a bug), but it's not clear to me that the reduction strategy used by constructor in determining what inductive family your goal is a part of should be part of the specification of constructor.

这篇关于为什么构造函数在这里要花这么长时间？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！