Coq:haskell 的 Replicate 函数的强规范
Coq: Strong specification of haskell's Replicate function
我在理解 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 是编码函数预期 input/output 行为的关系。
strong规范的定义:
给函数一个强规范:这个函数的类型直接声明输入是一个类型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 中)。
所以你不需要写函数本身,只需要写关系,因为函数将由证明定义。
了解了这一点,如何将其应用到复制函数案例中?
只是为了好玩,这是 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
可能的规范如下所示:
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
的第一个参数(对应于“实函数”而不是证明的参数)。为了能够做到这一点,你应该以 Defined
而不是 Qed
结束你的 Theorem
以便 Coq 可以评估它。
我在理解 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 是编码函数预期 input/output 行为的关系。
strong规范的定义:
给函数一个强规范:这个函数的类型直接声明输入是一个类型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 中)。
所以你不需要写函数本身,只需要写关系,因为函数将由证明定义。
了解了这一点,如何将其应用到复制函数案例中?
只是为了好玩,这是 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
可能的规范如下所示:
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
的第一个参数(对应于“实函数”而不是证明的参数)。为了能够做到这一点,你应该以 Defined
而不是 Qed
结束你的 Theorem
以便 Coq 可以评估它。