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

Question

我正在努力使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似乎无法使用，因此这条道路并不是很富有成效。我将暂时解决此问题，稍后再试。

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

Answer 1

归纳证明是由递归定义激发的。因此，要了解归纳法应用于什么，请查找Fixpoints。

您Fixpoint最有可能处理由单一类型变量索引的术语Select F A，这正是您想要使用归纳的地方，而不是在目标的顶层。

Fixpoint按函数类型索引的 on 术语是A -> B无用的，因为任何Select术语的子术语都没有按函数类型索引。出于同样的原因，induction在这种情况下是没有用的。

在这里，我认为强类型规则实际上迫使您在尝试在 Coq 中做任何事情之前先在纸上解决所有问题（在我看来这是一件好事）。尝试在纸上进行证明，甚至不用担心类型；明确写下您想要通过归纳法证明的谓词。这是一个模板，可以了解我的意思：

通过归纳u，我们将证明

 u <*> pure x = pure (fun f => f x) <*> u

    (* Dummy induction predicate for the sake of example. *)
    (* Find the right one. *)
    (* It may use quantifiers... *)

1. 基本情况（设置u = Pure f）。证明：

   Pure f <*> pure x = pure (fun f => f x) <*> Pure f
   

2. 归纳步骤（设置u = MkSelect v h）。证明：

   MkSelect v h <*> pure x = pure (fun f => f x) <*> MkSelect v h
   

   v假设子项（集合）的归纳假设u = v：

   v <*> pure x = pure (fun f => f x) <*> v
   

请特别注意，最后一个方程的类型错误，但您仍然可以使用它来进行方程推理。无论如何，在简化目标后很可能无法应用该假设。

如果您确实需要使用 Coq 进行一些探索，有一个技巧，即删除有问题的类型参数（以及依赖于它的所有术语）。根据您对 Coq 的熟悉程度，这个技巧可能会比任何东西都更令人困惑。所以要小心。

这些术语仍将具有相同的递归结构。请记住，证明也应该遵循相同的结构，因为重点是之后在顶部添加更多类型，因此如果可以的话，您应该避免依赖于缺少类型的快捷方式。

(* Replace all A and B by unit. *)
Inductive Select_ (F : unit -> Type) : Set :=
| Pure_ : unit -> Select_ F
| MkSelect_ : Select_ F -> F tt -> Select_ F
.

Arguments Pure_ {F}.
Arguments MkSelect_ {F}.

(* Example translating Select_map. The Functor f constraint gets replaced with a dummy function argument. *)
                                        (*      forall A B, (A -> B) -> (F A -> F B) *)
Fixpoint Select_map_ {F : unit -> Type} (fmap : forall t,   unit     -> (F t -> F t)) (f : unit -> unit) (v : Select_ F) : Select_ F :=
  match v with
  | Pure_ a => Pure_ (f a)
  | MkSelect_ w h => MkSelect_ (Select_map_ fmap f w) (fmap _ tt h)
  end.

这样，您可以尝试证明函子定律的精简版本，例如：

Select_map_ fmap f (Select_map_ fmap g v) = Select_map_ fmap (fun x => f (g x)) v

(* Original theorem:

Select_map f (Select_map g v) = Select_map (fun x => f (g x)) v

*)

关键是删除参数可以避免相关的键入问题，因此您可以尝试天真地使用归纳法来查看事情（不）如何进行。