The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Sun, 15 May 2011 09:43:04 -0400
Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> I just want to make sure you're aware that all of these definitions 
> (including the one you're struggling with) also appear in "Certified 
> Programming with Dependent Types."

I believe I'm making some progress, but I'm having trouble adapting
one of the techniques shown in the subset types chapter. The contrived
example I'm working with (in order to better understand how to use
proof terms to satisfy impossible pattern matches):

Require Coq.Arith.Lt.
Require Coq.Arith.Gt.

Inductive finite : nat -> Set :=
  | FO : forall (b : nat), finite (S b)
  | FS : forall (b : nat), finite b -> finite (S b).

Implicit Arguments FO [b].
Implicit Arguments FS [b].

Fixpoint finite_nat {b : nat} (f : finite b) : nat :=
  match f with
    | FO _    => 0
    | FS _ f' => S (finite_nat f')
  end.

Theorem lt_finite_nat_fb_b : forall (b : nat) (f : finite b),
  finite_nat f < b.
Proof.
  induction f.
  simpl.
  apply Lt.lt_0_Sn.

  simpl.
  apply Lt.lt_n_S.
  apply IHf.
Defined.

Inductive contrived (A : Set) :=
  | C : A -> A -> A -> A -> contrived A.

Now, a function that takes a value of type finite 4 and returns the
corresponding field from a value of type contrived A:

Definition get {A : Set} (f : finite 4) (c : contrived A) : A :=
  match c with
    | C n0 n1 n2 n3 =>
      match (finite_nat f) with
        | 0               => n0
        | 1               => n1
        | 2               => n2
        | 3               => n3
        | n               => ??
      end
  end.

I understand the correct thing to do is to use a proof of False
to create a value of any type in order to satisfy the type
checker (I realize I could also just return any one of the other
fields, but I'd rather not!). I've tried variations of the above,
such as:

Lemma lt_SSSSn_4_absurd : forall n, S (S (S (S n))) < 4 -> False.
Proof.
  intro n.
  apply Gt.gt_not_le.
  induction n.
  auto.
  auto.
Defined.

Definition get {A : Set} (f : finite 4) (c : contrived A) : A :=
  match c with
    | C n0 n1 n2 n3 =>
      match (finite_nat f) with
        | 0               => n0
        | 1               => n1
        | 2               => n2
        | 3               => n3
        | S (S (S (S n))) => ??
      end
  end.

... but even in that case, I don't know how to *use* the actual
proof.