对具有非统一类型参数的数据类型的归纳会产生不良类型的项

我正在努力使Coq中的Free Selective Applicative Functors正式化，但是我在通过归纳法对具有非均匀类型参数的归纳数据类型进行挣扎。

让我简要介绍一下我正在处理的数据类型。在Haskell中，我们将自由选择函子编码为GADT：

data Select f a where
    Pure   :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

关键是b第二个数据构造函数中的存在类型变量。

我们可以将此定义转换为Coq：

Inductive Select (F : Type -> Type) (A : Set) : Set :=
    Pure   : A -> Select F A
  | MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A.

作为附带说明，我使用-impredicative-set选项对其进行编码。

Coq对此数据类型生成以下归纳原理：

Select_ind :
  forall (F : Type -> Type) (P : forall A : Set, Select F A -> Prop),
  (forall (A : Set) (a : A), P A (Pure a)) ->
  (forall (A B : Set) (s : Select F (B + A)), P (B + A)%type s ->
     forall f0 : F (B -> A), P A (MkSelect s f0)) ->
  forall (A : Set) (s : Select F A), P A s

在这里，有趣的是谓词P : forall A : Set, Select F A -> Prop，该谓词不仅在表达式中参数化，而且在表达式类型参数中也参数化。据我了解，归纳原理具有这种特殊形式，这是因为MkSelecttype 的构造函数的第一个参数Select F (B + A)。

现在，我想证明类似的第三条适用于已定义数据类型的陈述：

Theorem Select_Applicative_law3
        `{FunctorLaws F} :
  forall (A B : Set) (u : Select F (A -> B)) (y : A),
  u <*> pure y = pure (fun f => f y) <*> u.

其中涉及type的值Select F (A -> B)，即包含函数的表达式。但是，调用induction此类变量会产生错误类型的术语。考虑一个过分简化的等式示例，该示例可以用证明reflexivity，但不能使用证明induction：

Lemma Select_induction_fail `{Functor F} :
  forall (A B : Set) (a : A) (x : Select F (A -> B)),
    Select_map (fun f => f a) x = Select_map (fun f => f a) x.
Proof.
  induction x.

Coq抱怨该错误：

Error: Abstracting over the terms "P" and "x" leads to a term
fun (P0 : Set) (x0 : Select F P0) =>
  Select_map (fun f : P0 => f a) x0 = Select_map (fun f : P0 => f a) x0
which is ill-typed.
Reason is: Illegal application (Non-functional construction):
The expression "f" of type "P0" cannot be applied to the term
 "a" : "A"

在这里，Coq无法构造在类型变量上抽象的谓词，因为语句中的反向函数应用程序类型错误。

我的问题是，如何在数据类型上使用归纳法？我看不到如何以这种方式修改归纳原理的方法，这样谓词就不会抽象该类型。我尝试使用dependent induction，但是它一直在产生归纳假设，(A -> B -> C) = (X + (A -> B -> C))该假设受等同于我认为无法实例化的等式约束。

请在GitHub上查看完整示例：https : //github.com/tuura/selective-theory-coq/blob/impredicative-set/src/Control/Selective/RigidImpredSetMinimal.v

更新： 根据要点的讨论，我试图通过对表达深度的归纳来进行证明。不幸的是，由于我在定理中得出的归纳假设Select_Applicative_law3似乎无法使用，因此这条道路并不是很富有成效。我将暂时解决此问题，稍后再试。

丽瑶，非常感谢您帮助我增进理解！