Strong specification of haskell's Replicate function

Using Coq
1

Hi! I’m having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it creates a list of length n, with all elements equal to x) using the strong specification way, how would I be able to do that? Apparently I have to write an Inductive “version” of the function but how?

Definition in Haskell:

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

Thank you!

2

The “weak” version has the same definition and type as in Haskell. You then (separately) prove two lemmas: length (replicate n x) = n and x' \in (replicate n x) -> x' = x.

The “strong” version packages the lemmas with the return value, so the new function has type forall (n: nat) (x: A), { l: list A | length l = n /\ forall x', x' \in l -> x' = x }.

1 Like