I have the following question, look in the code.
(* Suppose we have type A *)
Variable A: Type.
(* Also we have a function that returns the type (option A) *)
Definition f_opt x: option A := ...
(* Then, I can prove that this function always returns something: *)
Theorem always_some: forall x, exists y, f_opt x = Some y.
Admitted.
(* Or, equivalently: *)
Theorem always_not_none: forall x, f_opt x <> None.
Admitted.
Now I would like to get a version of f_opt
that always returns a value of type A
. Something like this:
Definition f x: A :=
match f_opt x with
| Some y => y
end.
But I get the following error:
Non exhaustive pattern-matching: no clause found for pattern
None
.
I understand that I need to do some kind of work with types, but I do not understand what exactly i should do.
In Coq's underlying theory, every pattern matching must be exhaustive -- that is, it must explicitly consider all the constructors of the inductive type in question. This is why you are getting the error message you saw.
How do we get around this restriction? There are a few solutions. First, let's see how to convince Coq that the
None
branch can never occur. For this, we will use youralways_not_none
theorem:This code might look strange at first sight, but it almost performs the pattern match you want. To explain to Coq that the
None
case never arises, it combinesalways_not_none
with the fact thatf_opt x = None
on that branch to derive a contradiction. This is theH eq_refl
term on that branch. Then, thematch
on that contradiction suffices to convince Coq that the branch is spurious. A bit more formally, becauseFalse
, the contradictory proposition, is defined without any constructors, when we match on a term of typeFalse
, there are no branches to deal with, and the entire expression can return any type that we want -- in this case,A
.What is strange about this code is the type annotations on the match, and that it returns a function instead of something of type
A
directly. This is done because of how dependent pattern match works in Coq: whenever we want to make use of information that we obtain from being in a particular branch of a match (here, thatf_opt x
is equal toNone
in that branch), we must explicitly make the match return a function -- what Adam Chlipala calls the convoy pattern. This is done so that Coq knows where you plan to use that extra information and check that it is done correctly. Here, we use thatf_opt x
isNone
to feed the hypothesis needed byalways_not_none x
to derive a contradiction.Although this will solve your problem, I would generally advise you against doing it this way. For instance, if you know that your
A
type is inhabited by some elementa : A
, then you can simply makef
returna
on that branch. This has the benefit of avoiding mentioning proofs inside your functions, which often gets in the way when simplifying and rewriting terms.