Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Doubt about refine

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Doubt about refine


Chronological Thread 
  • From: Saulo Araujo <saulo2 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Doubt about refine
  • Date: Sun, 7 Feb 2016 00:22:28 -0300
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=saulo2 AT gmail.com; spf=Pass smtp.mailfrom=saulo2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f41.google.com
  • Ironport-phdr: 9a23:OLTtWxQeGoN9aFgEhtz+ZB9EI9psv+yvbD5Q0YIujvd0So/mwa64ZxCN2/xhgRfzUJnB7Loc0qyN4/+mAzBLu8/b+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVOVkD3mPnKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxyFBHgzCpDjgV4rztWOureNg3C7AFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==
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

Archive powered by MHonArc 2.6.18.

Top of Page