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 :
Inductive RelReplicate (A : Type) (a : A) : nat -> (list A) -> Prop :=
| rep0 : RelReplicate A a 0 nil
| repS : …
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 like
Theorem replicate_corr : forall (A:Type) (a : A) (n : nat), {l | ReplicateRel A a n l}.
which should be easy by induction on n.
If you want to check that your function replicate_corr corresponds to what you had in mind, you can try it on a few examples, with
Eval compute in (proj1_sig (rep_corr nat 0 3)).
which 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 your Theorem with Defined rather than Qed so that Coq can evaluate it.