The Coq mailing list

["Kouskoulas, Yanni A." <Yanni.Kouskoulas AT jhuapl.edu>]

Greetings,

My apologies if this question has already been answered, but I looked through 
the archives and did not see it before.

I find that when using refine, the context that I have access to lacks 
assumptions that I think should be available. Consider the following somewhat 
contrived example:

Section foo.
Variable lprop : list nat -> Prop.

Theorem bar (i : list nat) : nat -> lprop i -> nat.
refine((fix f (i : list nat) (p : nat) (prf : lprop i) {struct p} : nat  :=
  match p with 
    | S (S (S (S q))) =>
      match i with
        | nil => 1
        | h :: tl => (f tl q _)
      end
    | _ => 0
  end)).

The refine tactic puts me in a proof environment that asks me to prove "lprop 
tl", which is correct, but it will not include information in the context 
about how tl relates to lst, i.e., lst = h :: tl. This is information that 
seems derivable from the match construct.

To address this problem when I encounter it, I end up making my hole bigger,

Theorem bar (i : list nat) : nat -> lprop i -> nat.
refine((fix f (i : list nat) (p : nat) (prf : lprop i) {struct p} : nat  :=
  match p with 
    | S (S (S (S q))) => _
    | _ => 0
  end)).

and then using tactics to reconstruct the match that I took out. Is there a 
better way to use refine so that it gives me more detailed context? Widening 
holes like this seems like extra work to me.

-Yanni