The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi,

I was able to finish the definition of the function get by following the suggestion of Guillaume. As it may be useful to someone that, like me, is starting to use dependent types in Coq,  I am sending the full definition of the function get:

Fixpoint get E n (s: Sequence E n) (ds: List Digit n): E.

Proof.

  refine(

    match s in Sequence _ n1 return n = n1 -> E with

    | SequenceLeaf e0 e1 => 

        match ds in List _ n2 return n = n2 -> n = 0 -> E with

        | ListLeaf D0 => fun _ _ => e0

        | ListLeaf D1 => fun _ _ => e1

        | _ => _

        end

        eq_refl

    | SequenceNode n1 s0 s1 => 

        match ds in List _ n2 return n = n2 -> n = S n1 -> E with

        | ListNode n2 D0 ds' => fun _ _ => get E n1 s0 _

        | ListNode n2 D1 ds' => fun _ _ => get E n1 s1 _

        | _ => _

        end

        eq_refl

    end

    eq_refl

  ).

  {

    congruence.

  }

  {

    congruence.

  }

  {

    congruence.

  }

  {

    congruence.

  }

Defined.

Sincerely,

​Saulo