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 = []
Definition of weak specification:
To define these functions with a weak specification and then add companion lemmas. For instance, we define a function f : A->B and we prove a statement of the form ∀ x:A, Rx (fx), where R is a relation coding the intended input/output behaviour of the function.
Definition of strong specification:
To give a strong specification of the function: the type of this function directly states that the input is a value x of type A and that the output is the combination of a value v of type B and a proof that v satisfies Rxv. This kind of specification usually relies on dependent types.
EDIT: I heard back from my teacher and apparently I have to do something similar to this, but for the replicate case:
"For example, if we want to extract a function that computes the length of a list from its specification, we can define a relation RelLength which establishes a relation between the expected input and output and then prove it. Like this:
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.
The function used to prove must use the list “recursor” directly (that’s why fixpoint won’t show up - it’s hidden in list_rect).
So you don’t need to write the function itself, only the relation, because the function will be defined by the proof."
Knowing this, how can I apply it to the replicate function case?
A possible specification would look like this :
I did the zero case, leaving you the successor case. Its conclusion should be something like
RelReplicate A a (S n) (a :: l)
. As in your example, you can then try and prove something likewhich should be easy by induction on
n
. If you want to check that your functionreplicate_corr
corresponds to what you had in mind, you can try it on a few examples, withwhich evaluates the first argument (the one corresponding to the "real function" and not the proof) of
rep_corr
. To be able to do that, you should end yourTheorem
withDefined
rather thanQed
so that Coq can evaluate it.