主页 / user-5700198

FH35's questions

Martin Hope
FH35
Asked: 2024-05-27 16:59:52 +0800 CST
  • 5

根据 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