主页 / coding / 问题 / 78538115
Accepted
FH35
Asked: 2024-05-27 16:59:52 +0800 CST

展开策略中 Delta 减少后的 Beta 减少

  • 772

根据 coq 手册，展开策略对定义执行 delta 缩减，然后进行其他几个缩减，包括 beta 缩减。

似乎有时，要在展开中的 delta 缩减之后触发 beta 缩减，您需要首先解构一个参数。

例如，在下面的引理“ unfold_lemma ”中，第一个“ unfold myFunction ”（在代码中注释掉）似乎不会触发 beta-reduction，而 beta-reduction 是在参数 t 销毁后执行的。

显然，我对贝塔缩减有一些不理解的地方。有人可以帮我澄清这一点吗？

Inductive tree : Type :=
| tree_cons : list tree -> tree.

Fixpoint andAll (ls: list bool) : bool :=
    match ls with
     | nil => true
     | cons h t => andb h (andAll t)
    end.

Definition isLeaf (t: tree) : bool :=
      match t with
      | tree_cons l => match l with
                    | nil => true
                    | x::rest => false
                  end
      end.
    
Definition isSpecial (t: tree) : bool :=
      match t with
        | tree_cons l => match l with
                      | nil => false
                      | x::rest => andAll (map isLeaf l)
                    end
      end.
    
Section flat_map_index.

      Variables A B : Type.
      Variable f    : nat -> A -> list B.
    
      Fixpoint flat_map_index (n:nat) (l:list A) : list B :=
          match l with
            | nil => nil
            | cons x t => (f n x)++(flat_map_index (S n) t)
          end.
      
End flat_map_index.
    
Fixpoint myFunction (l:list nat) (index:nat) (t: tree) : list (list nat) :=
    let l' := (l++[index]) in
    if (isSpecial t) then
         match l' with
          | [] => []
          | xx::rest => [rest]
        end
    else 
      match t with
        | tree_cons subtrees => flat_map_index (myFunction l') O subtrees
      end.

Lemma unfold_lemma: forall a,
      In [0] (myFunction [0] 0 a) -> isSpecial a = true. 
Proof.
  intro t.
  (* unfold myFunction. *)
  destruct t as [subtrees].
  unfold myFunction.
  fold myFunction.
  destruct (isSpecial (tree_cons subtrees)) eqn:HCase.
  + easy.
  + ...
coq

1 个回答

  1. Best Answer

    Beta 缩减将参数替换为 lambda 抽象。Lambda 抽象不能是递归的。myFunction，作为Fixpoint，delta 归约为一个fix表达式，它与 lambda 抽象 ( fun) 不同。fix表达式的计算使用 Coq 所谓的iota-reduction，而不是 beta-reduction 。仅当固定点的递减参数以构造函数为首时，iota-reduction 才会减少固定点的应用。

    iota- 和 beta-reduction 之间的区别确保了强大的标准化：如果通过普通 beta-reduction 评估固定点，那么当递减参数不是构造函数时它们可以扩展，那么您可以永远在其内部扩展固定点。该系统仍然具有弱标准化：对于任何项，总是存在以某个值终止的归约序列。每个归约序列都以一个值终止的强归一化特性很快就会被点燃。

    一些代码演示了上述内容。

    Definition plus_two n := S (S n).
Print plus_two. (* plus_two = fun n : nat => S (S n) *)
(* plus_two delta-reduces to a lambda abstraction written with fun. *)
Goal plus_two 2 = 4.
  cbv delta[plus_two]. (* (plus_two 2 = 4) delta-converts to ((fun n : nat => S (S n)) 2 = 4) *)
  Fail (progress cbv iota). (* iota-reduction does not apply here (cbv iota does nothing) *)
  cbv beta. (* but beta-reduction does produce 4 = 4 *)
  reflexivity.
Qed.
Goal forall n, plus_two n = S (S n).
  intros n.
  cbv delta.
  cbv beta. (* beta is allowed when the argument is a variable *)
  reflexivity.
Qed.

Fixpoint quux_two n := match n with | O => 2 | S n => S (quux_two n) end.
Print quux_two. (* quux_two = fix quux_two (n : nat) : nat := ... *)
(* Coq defines quux_two with a fix expression.
   Note how a fix expression names itself so it can be used in its own body.
   It is NOT a lambda abstraction! *)
Goal quux_two 2 = 4.
  cbv delta. (* now the goal contains an application of a fix expression *)
  Fail (progress cbv beta). (* beta reduction does nothing because there is no lambda abstraction *)
  cbv iota. (* iota reduction does work and unfolds one turn of the fixpoint, exposing a lambda. *)
  cbv beta.
  cbv iota. (* iota also handles match; this line actually does 2 iotas *)
  cbv beta.
  cbv iota. (* two iotas again *)
  cbv beta.
  cbv iota. (* only one iota (for the match) this time *)
  reflexivity.
Qed.
Goal forall n, quux_two n = S (S n).
  intros n.
  cbv delta.
  Fail (progress cbv beta iota).
  (* beta fails because there is no lambda.
     iota fails because the decreasing argument of the fix is not constructor-headed.
     the goal is actually in normal form; no reductions can apply.
     if you *could* expand quux_two inside itself... that would be bad, since there would be an infinite sequence of reductions.
     must proceed by some kind of case split on n, here induction. *)
  induction n as [ | n rec]. (* induction appears to do some simplifying  *)
  - reflexivity.
  - f_equal.
    exact rec.
Qed.

    在您的代码中， 的递减参数myFunction是第三个参数t : tree。因此，仅当以 为首myFunction l index t时才会减少（即，在 Delta 减少后仅进行 iota 减少）。ttree_cons

    请注意，您始终可以显式证明表达式fix等于其展开式。你只是无法让 Coq 在转换过程中自动使用这样的等式。

    Theorem quux_two_eqn (n : nat)
: quux_two n = match n with | O => 2 | S n => S (quux_two n) end.
Proof.
  destruct n; reflexivity.
Qed.

    如果您认为这有帮助，您可以编写这样的引理myFunction并使用它，而不是依赖于转换。我还听说 Coq 的方程插件允许自动生成这样的引理，尽管我从未使用过它。

    （根据文档，unfold应用指定的 delta 缩减，然后应用所有 beta-、iota- 和 zeta-（简化lets）缩减。）

    • 1

相关问题