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，得到一个Type，我可以证明引理：

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

然而，对于 TPrecision 的“正确”定义，使用 Prop，策略“依赖归纳”不起作用，出现以下错误：

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

如何提供这个缺失的实例？（或者如何以另一种方式证明引理？）如果我只使用“归纳法”而不是“依赖归纳法”，则该策略不会进行类型检查。我也尝试用 JMeq 代替常规相等来说明引理，但它也没有用。

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.

Coq：尝试使用依赖归纳法

Coq: trying to use dependent induction

coq

dependent-type