I'm trying to do something in Coq similar to this liquid Haskell trick, which defines a partial function but proves it's actually total:
{-@ head :: {xs:[a] | len xs > 0} -> a @-}
head (x:xs) = x
Here is my first attempt, but Coq doesn't like it ("Casts are not supported in this pattern."):
Definition safeHead {A : Type} (xs : list A) (nonempty : xs <> nil) : A.
Proof.
refine (fun {A : type} (xs : list A) (pf : xs <> nil) =>
match xs with
| x : xs => x
| nil => _
end).
(* Some tactic here to prove the hole from nonempty *)
Defined.
I also tried adapting option 1 from this blog post, but that fails with the same error:
Definition safeHead {A : Type} (xs : list A) (not_nil : xs <> nil) : A
match xs return _ with
| x : xs => fun _ => x
| nil => fun is_nil => False_rect _ (not_nil is_nil)
end eq_refl.
Is there a way to get this to work in coq? I'd also love to understand the error message; what is the 'cast' and in which pattern is it failing?
As @kyo dralliam pointed out, you should use :: and not : for the cons operation of lists.
The main problem with your definition is that you lose the information that xs is not empty when you match on it. To keep that information you must be explicit about it. Like so:
From Coq Require Import Utf8 List.
Import ListNotations.
Definition safeHead {A : Type} (xs : list A) (nonempty : xs ≠ []) : A :=
match xs as l return l ≠ [] → A with
| [] => ltac:(contradiction)
| x :: xs => λ _, x
end nonempty.
Using the return information of the match I say that I construct a proof of l ≠ [] → A where l is a local name I give to xs using the as clause.
This means that in the case [] we have to inhabit [] ≠ [] → A and thus I conclude using the contradiction tactic, using tactics in terms.
In the cons case x :: xs we don't really care about the non-empty assumption so I ignore the argument and return the head x as we wanted.
Finally the whole match expression now has type xs ≠ [] → A so to get A we must give it the nonempty proof.