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通常会更好地表现。