The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

There is another alternative.  The type indexes can be omitted in favor 
of extra equality fields.  Doing this enables the use of basic matches 
in the refine, as in the following rewriting of your example.  No convoy 
patterns are needed.  I don't know why this technique isn't mentioned 
more frequently.


Set Implicit Arguments.

Section Sequence.

Variable E: Set.

Inductive Sequence(n : nat) : Set :=
  | SequenceLeaf: E -> E -> n=0 -> Sequence n
  | SequenceNode: forall m, Sequence m -> Sequence m -> n = S m -> 
Sequence n.

Inductive List(n : nat) : Set :=
  | ListLeaf: E -> n=0 -> List n
  | ListNode: forall m, E -> List m -> n = S m -> List n.

End Sequence.

Inductive Digit :=
  | D0
  | D1.

Fixpoint get E n (t: Sequence E n) (ds: List Digit n): E.
Proof.
refine(
  match t with
  | SequenceLeaf e0 e1 e =>
      match ds with
      | ListLeaf D0 _ => e0
      | ListLeaf D1 _ => e1
      | @ListNode _ _ y _ _ e2 => _
      end
  | @SequenceNode _ _ x s0 s1 _ =>
      match ds with
      | ListLeaf _ e0 => _
      | @ListNode _ _ y d ds' _ =>
          match d with
          | D0 => get E x s0 _
          | D1 => get E x s1 _
          end
      end
  end
).
all:congruence.
Defined.

-- Jonathan