关于Coq中其他未知参数化命题的参数化

Question

我想定义一个参数化命题decidable，它讨论其他参数化命题的可判定性。作为一个常见的例子，even是一个参数化命题，它采用nat类型的一个参数，并且是可判定的。lt是一个参数化命题，它采用nat型的两个参数，并且它也是可判定的。我希望decidable是这样的，decidable even和decidable lt都是可证明的命题。

定义decidable的主要困难是指定它的类型。它必须接受A -> B -> C -> ... Z -> Prop类型的任何参数化命题，其中A.Z是类型，它们的总数是任意的。

这是我的第一次尝试：

Inductive decidable { X : Type } ( P : X ) : Prop :=
| d_0 : X = Prop -> P \/ ~ P -> decidable X P   
| d_1 : forall ( Y Z : Type ), ( X = Y -> Z ) 
  -> ( forall ( y : Y ), decidable Z ( P y ) )
  -> decidable X P.

我认为在d_0中使用d_0作为一个前提应该是可以的，因为Coq将足够聪明地计算出P : Prop，考虑到前面的前提X = Prop。事实并非如此。

所以现在我找不到任何方法来拼写出所有丑陋的东西:如果我想说某些P : A -> B -> C -> ... Z -> Prop是可判定的，那么它必须是forall ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z \/ ~ P a b c ... z。呃。

但也许我遗漏了什么。也许，由于我对Coq多态性的基本知识，我忽略了一些巧妙的技巧。

有什么建议吗？

Answer 1

Require Import Coq.Arith.Even.

您将需要一个异构的类型列表。它只包含类型，但类型可能来自不同的宇宙。

Inductive list : Type :=
  | nil : list
  | cons : Type -> list -> list.

此函数接受集合列表，并返回与这些集合不同的谓词的类型。我不知道如何泛化这个函数以接受任何类型的列表(Prop，Type 1，Type 2，.)。

Fixpoint predicate (l1 : list) : Type :=
  match l1 with
  | nil => Prop
  | cons t1 l2 => t1 -> predicate l2
  end.

Eval simpl in predicate (cons bool nil).
Eval simpl in predicate (cons bool (cons nat nil)).

该函数接受一个集合列表和一个在这些集合上不同的谓词，并断言谓词是可判定的。

Fixpoint decidable (l1 : list) : predicate l1 -> Prop :=
  match l1 with
  | nil => fun p1 => p1 \/ ~ p1
  | cons t1 l2 => fun p1 => forall x1, decidable l2 (p1 x1)
  end.

Eval simpl in decidable (cons nat nil) even.
Eval simpl in decidable (cons nat (cons nat nil)) le.
Eval simpl in decidable (cons nat (cons Prop (cons Set (cons Type nil)))).