是否有一些策略来证明这个显然容易的目标？

Question

我有以下目标：

1个子目标

______________________________________(1/1)

（if（a =？a）％string || false然后#a :: nil else nil）= nil

因为很明显a = a，我想知道为什么战术“简化”不起作用。

Answer 1

Print "=?".

String.eqb = 
fix eqb (s1 s2 : string) {struct s1} : bool :=
  match s1 with
  | "" => match s2 with
          | "" => true
          | String _ _ => false
          end
  | String c1 s1' =>
      match s2 with
      | "" => false
      | String c2 s2' => if Ascii.eqb c1 c2 then eqb s1' s2' else false
      end
  end
     : string -> string -> bool

String.eqb被定义为fix，这意味着如果Coq无法看到该参数的头部符号（构造函数），Coq将不会减少它对参数的应用。在这种情况下，simpl战术不能适用String.eqb a a，因为a是一个变量，我们对它的“形状”一无所知 - 因此你什么也看不见。

顺便说一句，||，即orb函数是由它的第一个参数上的模式匹配定义的，因此simpl不能将(a =? a)%string || false减少到(a =? a)%string。

这里的一个出路是用String.eqb_refl引理重写，在使用这个引理后很明显，除非你在上下文中有矛盾，否则目标是不可证明的，在这种情况下你不需要String.eqb_refl。