I am very new to Coq, and hope my question is not too basic. I am simply wondering how I define dependent functions in Coq. For example, how could I define a function from Booleans that sends true to true and false to the natural number seven ? I assume one can use the usual (f x) notation to apply a dependent function f to an input x.
To define dependent functions in Coq, you refer back to the parameter when specifying the type. In your example, you take a Boolean, let's call it b, and your return type is match b with true => bool | false => nat end (or if b then bool else nat).
In code, that looks like the following:
Definition foo (b : bool)
: match b with true => bool | false => nat end
:= match b with true => true | false => 7 end.
Compute foo true. (* = true *)
Compute foo false. (* = 7 *)
There is a little bit of magic that goes on in figuring out the type of the match construct here, if you give more type annotations it looks like
Definition foo'
: forall b : bool, match b return Set with true => bool | false => nat end
:= fun b : bool =>
match b as b'
return match b' return Set with true => bool | false => nat end
with true => true | false => 7 end.
Here, since the match construct can have different types depending on the value of b (which can be an arbitrary term, not just a variable), we use the annotation as b' return ... to give b a new name, and then specify the type of the match depending on the value of b'.
However, particularly when matching on a variable, Coq can often figure out the return ... annotation on it's own.
You can find some documentation of the match construct here, in the reference manual