Coq：当只有一种情况时，对 Set 的 Prop 执行反转

Question

假设我有一些编程语言，有一个 "has type" 关系和一个 "small step" 关系。

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 对排序值 Prop 执行案例分析，我们不能这样做，因为它在提取的代码中被删除了。

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

理想情况下，我可以应用一堆如下所示的引理：

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

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

我查看了 Derive Inversion，但它似乎并没有满足我在这里的需求，虽然我可能没有正确理解它。

有没有办法做这种 "case analysis where there's only one case?" 或者得到 Prop 证明隐含的等式，这样我就只能在我提取的解释器中写出可能的情况？可以使用 Ltac 或派生机制自动派生这些引理吗？

Answer 1

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

Answer 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.

你主要的证明objectiveprogress_interp大概可以进行通过对 tm 的结构进行归纳。这相当于将您的解释器直接编写为 gallina 递归函数。

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

Coq：当只有一种情况时，对 Set 的 Prop 执行反转

Coq: performing inversion on Prop for Set when there is only one case

coq

dependent-type

coq-tactic

ltac