COQ:只有一种情况时,对道具进行反转。

假设我有一些编程语言,有“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 但它似乎没有做我在这里寻找的,虽然也许我没有正确理解它。

有没有办法做这种“只有一个案例的案例分析”?或者得到 支柱 证明,这样我就只能在提取的解释器中编写可能的案例?用LTAC或派生机制可以自动派生这些引理吗?