在 Coq 中精确控制转换

Question

我尝试在 Coq 中证明以下定理：

Theorem simple :
    forall (n b:nat) (input output: list nat) , short (n::b::input) true (n::output) = None 
             -> short (b::input) false output = None.

简写如下：

Fixpoint short (input: list nat) (starting : bool) (output: list nat) : option (list nat) :=
match input with
  | nil => match output with
                 | nil => Some nil
                 | y::r => None
           end
  | x::rest => match output with
                | nil => ...
                | y::r => if ( beq_nat x y ) then match (short rest false r) with
                                                   | None => if (starting) then match (short rest starting output) with
                                                                               | Some pp => Some (0 :: pp)
                                                                               | None => None
                                                                           end 
                                                            else None 
                                                   | Some pp => Some (x :: pp)
                                                   end
                        else ...
end.

如果我能控制开始的转换步骤，证明会很简单

short (n::b::input) true (n::output)

最后得到类似的东西：

match (short (b::input) false output) with
            | None => match (short rest starting output) with
                            | Some pp => Some (0 :: pp)
                            | None => None
                      end 
            | Some pp => Some (x :: pp)
end

我已经试过了：

Proof.
  intros.
  cbv delta in H.
  cbv fix in H.
  cbv beta in H.
  cbv match in H.
  rewrite Nat.eqb_refl in H.
...

但似乎重写如果做的不仅仅是重写并执行转换我无法再次折叠到所需的形式...

知道如何进行这种转换吗？

谢谢！！

Answer 1

cbn 策略看起来在这里做得不错：

Theorem simple :
    forall (n b:nat) (input output: list nat) , short (n::b::input) true (n::output) = None 
             -> short (b::input) false output = None.
Proof.
  intros.
  cbn in *.
  rewrite Nat.eqb_refl in H.
  match goal with | |- ?t = _ => set (x := t) in * end.
  destruct x.
  all: congruence.
Qed.

一般来说，我建议不要 cbv 除非你真的想得到一个布尔值。但是，如果你想“展开一点点”，cbn 或 simpl 通常表现得更好。

在 Coq 中精确控制转换

Precise control of conversion in Coq

coq