5

我在理解 Coq 中强规范和弱规范之间的区别时遇到了一些麻烦。例如，如果我想使用强规范方式编写复制函数（给定一个数字 n 和一个值 x，它会创建一个长度为 n 的列表，所有元素都等于 x），我将如何做到这一点? 显然我必须编写函数的归纳“版本”，但如何？

Haskell 中的定义：

myReplicate :: Int -> a -> [a]
myReplicate 0 _ = []
myReplicate n x | n > 0 = x:myReplicate (n-1) x
                | otherwise = []

弱规范的定义：

用弱规范定义这些函数，然后添加伴随引理。例如，我们定义了一个函数 f : A->B 并证明了一个形式为 ∀ x:A, Rx ( fx ) 的语句，其中 R 是编码函数预期输入/输出行为的关系。

强规范的定义：

给出函数的强说明：这个函数的类型直接说明输入是类型 A 的值 x，输出是类型 B 的值 v 和 v 满足Rxv的证明的组合。这种规范通常依赖于依赖类型。

编辑：我收到了老师的回复，显然我必须做类似的事情，但对于复制案例：

“例如，如果我们想从它的规范中提取一个计算列表长度的函数，我们可以定义一个关系 RelLength 来建立预期输入和输出之间的关系，然后证明它。像这样：

Inductive RelLength (A:Type) : nat -> list A -> Prop :=
| len_nil : RelLength  0 nil
| len_cons : forall l x n, RelLength n l -> RelLength (S n) (x::l) .


Theorem len_corr : forall (A:Type) (l:list A),  {n | RelLength n l}.
Proof.
 …
Qed.

Recursive Extraction len_corr.

用于证明的函数必须直接使用列表“recursor”（这就是fixpoint 不会显示的原因——它隐藏在list_rect 中）。

所以你不需要编写函数本身，只需要编写关系，因为函数将由证明定义。”

知道了这一点，我如何将其应用于复制功能案例？

4

2 回答 2

2

只是为了好玩，这就是 Haskell 中的样子，所有依赖的东西都更烦人。这段代码使用了一些非常新的 GHC 特性，主要是为了使类型更加明确，但可以很容易地修改它以使用旧的 GHC 版本。

{-# language GADTs, TypeFamilies, PolyKinds, DataKinds, ScopedTypeVariables,
  TypeOperators, TypeApplications, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}

module RelRepl where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))

-- | Singletons (borrowed from the `singletons` package).
type Sing :: forall (k :: Type). k -> Type
type family Sing
type instance Sing @Nat = SNat
type instance Sing @[a] = SList @a
-- The version of Sing in the singletons package has many more instances;
-- in any case, more can be added anywhere as needed.

-- Natural numbers, used at the type level
data Nat = Z | S Nat

-- Singleton representations of natural numbers, used
-- at the term level.
data SNat :: Nat -> Type where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

-- Singleton lists
data SList :: forall (a :: Type). [a] -> Type where
  SNil :: SList '[]
  SCons :: Sing a -> SList as -> SList (a ': as)

-- The relation representing the `replicate` function.
data RelRepl :: forall (a :: Type). Nat -> a -> [a] -> Type where
  Repl_Z :: forall x. RelRepl 'Z x '[]
  Repl_S :: forall n x l. RelRepl n x l -> RelRepl ('S n) x (x ': l)

-- Dependent pairs, because those aren't natively supported.
data DPair :: forall (a :: Type). (a -> Type) -> Type where
  MkDPair :: forall {a :: Type} (x :: a) (p :: a -> Type).
               Sing x -> p x -> DPair @a p

-- Proof that every natural number and value produce a list
-- satisfying the relation.
repl_corr :: forall {a :: Type} (n :: Nat) (x :: a).
  SNat n -> Sing x -> DPair @[a] (RelRepl n x)
repl_corr SZ _x = MkDPair SNil Repl_Z
repl_corr (SS n) x
  | MkDPair l pf <- repl_corr n x
  = MkDPair (SCons x l) (Repl_S pf)

-- Here's a proof that the relation indeed specifies
-- a *unique* function.
replUnique :: forall {a :: Type} (n :: Nat) (x :: a) (xs :: [a]) (ys :: [a]).
  RelRepl n x xs -> RelRepl n x ys -> xs :~: ys
replUnique Repl_Z Repl_Z = Refl
replUnique (Repl_S pf1) (Repl_S pf2)
  | Refl <- replUnique pf1 pf2
  = Refl
于 2021-05-24T03:40:26.783 回答
1

可能的规范如下所示：

Inductive RelReplicate (A : Type) (a : A) : nat -> (list A) -> Prop :=
  | rep0 : RelReplicate A a 0 nil
  | repS : …

我做了零案例，留下你的后继案例。它的结论应该是这样的RelReplicate A a (S n) (a :: l)。就像在你的例子中一样，你可以尝试证明类似的东西

Theorem replicate_corr : forall (A:Type) (a : A) (n : nat), {l | ReplicateRel A a n l}.

通过归纳应该很容易n。如果您想检查您的功能是否replicate_corr与您的想法相符，您可以在几个示例中进行尝试，使用

Eval compute in (proj1_sig (rep_corr nat 0 3)).

它评估rep_corr. 为了能够做到这一点，你应该结束你Theorem的Defined而不是Qed让 Coq 可以评估它。

于 2021-05-25T08:40:08.617 回答