如何在coq中定义自定义归纳原理？

Question

这是对我问的上一个question的一种跟进，但是现在我只是在尝试实现自己对等式类型的归纳原理，我不确定如果没有某种模式，该如何做匹配。我避免在以下定义中使用归纳策略，因为这显然会导致一种鸡与蛋的难题。是否有任何可能的方法可以通过一些基本策略except指示以及通过香草的定义J2：= ...？

(* define a similair induction principle from this agda code*)
J2 : {A : Set} → (D : (x y : A) → (I A x y) →  Set)
  →  (d : (a : A) → (D a a r )) → (x y : A) → (p : I A x y) → D x y p
J2 D d x .x r = d x

Theorem J2 {A} :
  forall (D : forall (x y : A), Id A x y -> Prop), 
  forall (d : forall (a : A), (D a a (refl A a))),
  forall (x y : A) (p : Id A x y), D x y p.
Proof.
  intros.
  inversion p.
  subst.
  apply D y.

这将产生以下错误，我不确定如何指示p必须是没有归纳策略的反射。

1 subgoal (ID 34)

  A : Type
  D : forall x y : A, Id A x y -> Prop
  d : forall a : A, D a a (refl A a)
  y : A
  p : Id A y y
  ============================
  D y y p

会产生以下错误。

Error:
In environment
A : Type
D : forall x y : A, Id A x y -> Prop
d : forall a : A, D a a (refl A a)
y : A
p : Id A y y
Unable to unify "D y y (refl A y)" with "D y y p".

最后，当我尝试编写apply d in y时，出现了一个伴随的错误，出现以下错误。

Error:
Unable to apply lemma of type "forall a : A, D a a (refl A a)"
on hypothesis of type "A".

为什么类型检查器不满意？

Answer 1

代替inversion p，请使用destruct p，它可以直接进行模式匹配。

inversion仅用于假设目标中未使用证明条件的假设。目标中使用p。