1

假设我有一些编程语言，具有“有类型”关系和“小步”关系。

Inductive type : Set :=
| Nat : type
| Bool : type.

Inductive tm : Set :=
| num : nat -> tm
| plus : tm -> tm -> tm
| lt : tm -> tm -> tm
| ifthen : tm -> tm -> tm -> tm.

Inductive hasType : tm -> type -> Prop :=
| hasTypeNum :
    forall n, hasType (num n) Nat
| hasTypePlus:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (plus tm1 tm2) Nat
| hasTypeLt:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (lt tm1 tm2) Bool
| hasTypeIfThen:
    forall tm1 tm2 tm3,
      hasType tm1 Bool ->
      hasType tm2 Nat ->
      hasType tm3 Nat ->
      hasType (ifthen tm1 tm2 tm3) Nat.

Inductive SmallStep : tm -> tm -> Prop :=
  ...

Definition is_value (t : tm) := ...

这里的关键细节是，对于每个术语变体，只有一个可能匹配的 HasType 变体。

假设我想证明一个进度引理，但我也希望能够从中提取一个解释器。

Lemma progress_interp: 
  forall tm t, 
  hasType tm t -> 
  (is_value tm = false) -> 
  {tm2 | SmallStep tm tm2}.
intro; induction tm0; intros; inversion H.

这给出了错误Inversion would require case analysis on sort Set which is not allowed for inductive definition hasType.

我理解它为什么这样做：inversion对 sort 的值执行案例分析Prop，我们不能这样做，因为它在提取的代码中被删除了。

但是，由于术语变体和类型派生规则之间存在一一对应的关系，我们实际上不必在运行时执行任何分析。

理想情况下，我可以应用一堆看起来像这样的引理：

plusInv: forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).

每个案例都有一个这样的引理（或者是这些案例的结合的单个引理）。

我看过Derive Inversion但它似乎没有做我在这里寻找的东西，尽管我可能没有正确理解它。

有没有办法进行这种“只有一个案例的案例分析”？或者为了得到Prop证明所隐含的等式，这样我就只能在我提取的解释器中写出可能的情况？可以使用 Ltac 或 Deriving 机制自动导出这些引理吗？

4

2 回答 2

2

引理plus_inv可以通过对类型tm的案例分析而不是对类型的案例分析来获得hasType。

Lemma plus_inv : forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).
Proof.
intros e; case e; try (intros; discriminate).
intros e1 e2 t h; inversion h; intros e5 e6 heq; inversion heq; subst; auto.
Qed.

您的主要目标的证明progress_interp可能也可以通过对结构的归纳来执行tm。这相当于直接将您的解释器编写为 Gallina 递归函数。

你的问题有第二部分：这可以自动化吗？答案是肯定的，大概。我建议为此使用template-coq包或elpi包。这两个包都可以作为 opam 包使用。

于 2018-08-28T06:29:31.157 回答
1

我认为eexists可以解决问题：存在变量应该在 sigma 类型的证明过程中的某个时间点填写（您可以inversion在hasType假设上自由使用）。

于 2018-08-27T19:26:38.663 回答