0

我想定义一个参数化命题decidable，讨论其他参数化命题的可判定性。举一个常见的例子，even是一个参数化的命题，它接受 1 个类型的参数nat，它是可判定的。lt是一个带 2 个类型参数的参数化命题，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.

我认为它应该可以P \/ ~ P用作前提，因为 Coq 足够聪明，可以在给定先验前提的情况下d_0弄清楚这一点。它不是。P : PropX = Prop

所以现在我找不到任何方法来拼出整个丑陋的东西：如果我想说 someP : 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 多态性的初步了解，我可能忽略了一些巧妙的技巧。

有什么建议么？

4

1 回答 1

2 
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)))).
于 2014-08-23T23:57:01.420 回答