Coq：尝试使用依赖归纳。

Question

我有以下有关类型精度的定义：

Require Import Coq.Program.Equality.

Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.

Reserved Infix "<|" (at level 80).

(* Inductive TPrecision : type -> type -> Prop := *)
Inductive TPrecision : type -> type -> Type :=   (* see below *)
| PRInt : TInt <| TInt
| PRFun : forall t1 t2 t1' t2',
    t1 <| t2 -> t1' <| t2' -> TFun t1 t1' <| TFun t2 t2'
| PRStar : forall t, t <| TStar

  where "x '<|' y" := (TPrecision x y).

我希望证明 "x <| y" 的证明是唯一的:

Lemma TP_unique: forall t1 t2 (P1 P2 : t1 <| t2), P1 = P2.

利用之前定义的 TPrecision 来定义一个类型，我可以证明以下引理：

Proof.
  intros.
  dependent induction P1; dependent destruction P2; trivial.
  f_equal; auto.
Qed.

然而，使用Prop中TPrecision的“正确”定义后，使用“dependent induction”策略将无法工作，并给出以下错误：

Cannot infer this placeholder of type
"DependentEliminationPackage (t1 <| t2)" (no type class instance found) in
environment:
t1, t2 : type
P1 : t1 <| t2

如何提供这个缺失的实例？（或者另一种证明引理的方式是什么？）如果我只使用“归纳法”，而不是“依赖归纳法”，该策略无法通过类型检查。 我还尝试用JMeq而不是常规等式来陈述引理，但也无法成功。

- Roberto Ierusalimschy

---

即使这不是一个合适的解决方案，你仍然可以通过定义形式为 Lemma inv_star t (p: TPrecision t TStar)：p = PRStar t. 的反演引理来避开困难，并按类型归纳而不是按精度证明进行。 - kyo dralliam

Answer 1

问题在于，Coq默认情况下不会为命题生成依赖归纳原理。我们可以通过覆盖此默认设置来解决此问题：

Require Import Coq.Program.Equality.

Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.

Reserved Infix "<|" (at level 80).

(* Ensure Coq does not generate TPrecision_ind when processing this definition *)
Unset Elimination Schemes.
Inductive TPrecision : type -> type -> Prop :=   (* see below *)
| PRInt : TInt <| TInt
| PRFun : forall t1 t2 t1' t2',
    t1 <| t2 -> t1' <| t2' -> TFun t1 t1' <| TFun t2 t2'
| PRStar : forall t, t <| TStar

  where "x '<|' y" := (TPrecision x y).
(* Re-enable automatic generation *)
Set Elimination Schemes.

(* Compare the following induction principle with the one generated by Coq by
default. *)
Scheme TPrecision_ind := Induction for TPrecision Sort Prop.

Lemma TP_unique: forall t1 t2 (P1 P2 : t1 <| t2), P1 = P2.
Proof.
  intros.
  dependent induction P1; dependent destruction P2; trivial.
  f_equal; auto.
Qed.

- Arthur Azevedo De Amorim