Coq Trivia: Dependent Pattern-Matching and Inversion

I found some more time to study Coq. One place where I stumble very frequently is case analysis of value-indexed inductive types. There are often cases that lead to contradiction. Other cases intuitively imply some variables to be equal. Vanilla match constructs gives you no help, leaving you stranded. In proof mode, inversion tactic helps a lot. However, generated proofs are huge and hard to navigate. Another option is to use dependent pattern matching directly (which is what inversion generates for you).

I was eager to figure this out because there are times when proof mode is too confusing for me as a beginner or I seem to lack control defining precisely what I want. In particular, if you do code extraction, you do not want to use inversion-generated convoluted code. But up until today I had little success. Here is the first, and very modest, success story: retrieving the head of a non-empty length-indexed list, and discharging the Nil case with dependent pattern-matching:

	(* Consider lists indexed by length. *)
	Inductive List (t : Type) : nat -> Type :=
	| Nil : List t 0
	| Cons : forall n, t -> List t n -> List t (S n).
	(* Every non-empty list has a head element. *)
	Definition Head : forall t n, List t (S n) -> t.
	intros t n list. inversion list. assumption. Defined.
	(* In the proof, "inversion" tactic saved the day, eliminating the
	"Nil" case. However, the body of the proof term is not very
	pretty. Consider: *)
	Print Head.
	(*
	Head =
	fun (t : Type) (n : nat) (list : List t (S n)) =>
	let X :=
	match list in (List _ n0) return (n0 = S n -> t) with
	| Nil =>
	fun H : 0 = S n =>
	let H0 :=
	eq_ind 0 (fun e : nat => match e with
	| 0 => True
	| S _ => False
	end) I (S n) H in
	False_rect t H0
	| Cons n0 X X0 =>
	fun H : S n0 = S n =>
	let H0 :=
	let H0 :=
	f_equal (fun e : nat => match e with
	| 0 => n0
	| S n1 => n1
	end) H in
	eq_rect n (fun n1 : nat => t -> List t n1 -> t)
	(fun (X1 : t) (_ : List t n) => X1) n0 (eq_sym H0) in
	H0 X X0
	end in
	X (eq_refl (S n))
	: forall (t : Type) (n : nat), List t (S n) -> t
	*)
	(* Whoah, what a proof! Can we do better manually? Yes, if we find a
	way to discharge the "Nil" case. Dependent pattern-matching to the
	rescue: *)
	Definition HeadManual t n (list: List t (S n)) : t :=
	match list in List _ k return match k with
	| O => unit
	| S _ => t
	end with
	| Nil => tt
	| Cons _ x _ => x
	end.
	(* This worked out because "O" case never matches, that is, we
	exploited the contradiction and were allowed to return unit. The
	automated proof was more explicit about it, deriving an arbitrary
	value from "0 = S n" which implies "False". This example is very
	simple and in a sense we were lucky here. For more involved worked
	examples see this CPDT chapter:
	http://adam.chlipala.net/cpdt/html/DataStruct.html *)

view raw ManualInversion.v hosted with ❤ by GitHub