Partial function in Coq / underdefined?

Question

I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages used in that text.

For context I have finished writing the compiler, and am now in the verification stage, however I had to make a significant difference to Concrete Semantics in the definition of machine instruction execution. This difference seemed necessary in Agda, but now is making the verification stage incredibly complex.

In trying to do the simpler version of instruction execution given in Concrete Semantics, I've come across this line, which may explain why I am having trouble directly translating this into Agda:

Also useful are the head of a list, its first element, and the tail, the rest of the list:

fun hd :: 'a list ⇒ 'a
hd (x # xs) = x

Note that since HOL is a logic of total functions, hd [] is defined, but we do not know what the result is. That is, hd [] is not undefined but underdefined.

What is does it mean for hd [] to be underdefined? Is this the equivalent of having an incomplete pattern in Agda?

The assembly instruction execution function relies heavily on hd. In my implementation of it in Agda I gave indices to multiple types to allow me to build proofs that the stack always has the minimum number of elements, in order to avoid the incomplete pattern matching problem. Now that I am trying to verify the compiler the proofs are magnitudes more complex than the proofs in Concrete Semantics, since I have to work with these indices.

Am I missing something or are the proofs in Concrete Semantics incomplete with hd [] not being defined?

Legionnaire

This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/… – Scutcheon

Answer 1

hd [] in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd [] = hd [] because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd [].

Am I missing something or are the proofs in Concrete Semantics incomplete with hd [] not being defined?

They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.

Semipro