2

我为正在验证此表单的编译器定义了几种归纳类型

Inductive types := Int | Char | Symbol | Bool.
Inductive val : types -> Type := 
| T : val Bool
| F : val Bool
| Num : nat -> val Int
...

Inductive exp : types -> Type :=
   | If : forall {t}, val Bool -> exp t -> exp t -> exp t
   etc...

现在这很好并且简化了许多事情，直到我尝试证明一些定理，例如

Theorem example : forall t test (b1 b2 : exp t),
    eval (If test b1 b2) = eval b1
    \/ eval (If test b1 b2) = eval b2.

现在我想进行简单的案例分析，destruct test因为只有 2 个案例，T并F考虑。但是如果我尝试这样做，我会收到一个错误，通知我该destruct策略会生成错误类型的术语。它确实如此。

是否有任何类似的策略destruct可以让我对输入正确的术语进行案例分析并自动发送那些输入错误的术语？我怀疑这是不可能的，在这种情况下，处理此类证明的正确方法是什么？

4

1 回答 1

2

由于您不提供代码，因此我不会尝试确保它有效，但它的要点是进行依赖反转，传递应该使用的类型：

dependent inversion test with (
  fun t v =>
  match t as _t return val _t -> Prop with
  | Bool => fun v => eval (If v b1 b2) = eval b1 \/ eval (If v b1 b2) = eval b2
  | _    => fun v => False
  end v
).

这基本上等同于编写您自己的依赖模式匹配，这样with子句中的内容就是您的返回注释。

这有点等价于这样做：

refine (
  match test as _test in val _t return
    match _t as __t return val __t -> Prop with
    | Bool => fun test => eval (If test b1 b2) = eval b1 \/ eval (If test b1 b2) = eval b2
    | _    => fun _    => _t = Bool -> False
    end _test
  with
  | T => _
  | F => _
  | _ => _
  end
); try discriminate.
于 2013-06-14T04:09:19.393 回答