The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

Hi Saulo,

You are running up against the limitations of dependent pattern matching in Coq. It is indeed possible to recover the lost information, but Coq doesn't do it for you automatically. One way to find out how to do it is to do [Print get.] after defining get using tactics to see how Coq manages to do it. (Warning: the term may be ugly!) For more information on how to construct these things yourself, search for the "convoy pattern" in http://adam.chlipala.net/cpdt/html/Cpdt.MoreDep.html . Shameless plug: I also have a blog post about writing similar match statements at http://homes.cs.washington.edu/~jrw12/dep-destruct.html . I have used the techniques described there to produce a definition of your get function that doesn't use tactics; you can find it at https://gist.github.com/wilcoxjay/45ad7b486f4ecbf209d2 .

Hope this helps,

James

On Sat, Feb 6, 2016 at 7:22 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:

Hi,

I have the following types:

Set Implicit Arguments.

Section Sequence.

Variable E: Set.

Inductive Sequence: nat -> Set :=

  | SequenceLeaf: E -> E -> Sequence 0

  | SequenceNode: forall n, Sequence n -> Sequence n -> Sequence (S n).

Inductive List: nat -> Set :=

  | ListLeaf: E -> List 0

  | ListNode: forall n, E -> List n -> List (S n).

End Sequence.

Inductive Digit := 

  | D0

  | D1.

Now I am trying to define the function:

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

I am able to define it using tactics:

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

Proof.

  inversion t as [e0 e1 | x s0 s1].

  {

    destruct ds as [d | y d ds'].

    {

      destruct d.

      {

        apply e0.

      }

      {

        apply e1.

      }

    }

    {

      congruence.

    }

  }

  {

    destruct ds as [d | y d ds'].

    {

      congruence.

    }

    {

      inversion H.

      rewrite <- H1 in ds'.

      destruct d.

      {

        apply get with (n := x).

        apply s0.

        apply ds'.

      }

      {

        apply get with (n := x).

        apply s1.

        apply ds'.

      }

    }

  }

Defined.

Unfortunately, I am not being able to define the function using refine

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

Proof.

refine(

  match t with

  | SequenceLeaf e0 e1 =>

      match ds with

      | ListLeaf d =>

          match d with 

          | D0 => e0

          | D1 => e1

          end

      | ListNode y d ds' => _

      end

  | SequenceNode x s0 s1 =>

      match ds with 

      | ListLeaf d => _

      | ListNode y d ds' => 

          match d with 

          | D0 => get E x s0 _

          | D1 => get E x s1 _

          end

      end

  end

).

{

  congruence.

}

{

  (* ??? *)

}

Defined.

Looks like refine is discarding some information that the command 

inversion t as [e0 e1 | x t0 t1].

(in the tactics based definition of the function get) is preserving. Is there anything that I can do in order to refine preserve this information?

Any help will be gratefully appreciated,

Saulo