How to get the type of a subterm when you're building a match

Question

My general question is: is there an easy way to incrementally build up a definition in Coq when I'm not familiar with the type of what I'm working with?

Consider one definition of the natural numbers in Coq, from Coq.Narith.BinNat

Definition discr n : { p:positive | n = pos p } + { n = 0 }.

Now, to me it's a little confusing what this term looks like. Suppose I'm trying to extract this positive p from the definition. My first try failed:

Require Import Coq.Narith.BinNat.
Fail Definition NToPos (x : N) : positive :=
  match N.discr x with
  | inright HO   => 1 
  | inleft Hpos  => Hpos
  end.
(*
Error:
In environment
x : N
Hpos : {p : positive | x = N.pos p}
The term "Hpos" has type "{p : positive | x = N.pos p}"
while it is expected to have type "positive".
*)

Well... okay. Now I know my basic misunderstanding is with the notation {p : positive | x = N.pos p}, but where do I go from here?

My question is, is there a better way to understand a definition such as N.discr? What I think I want is the following:

Definition NToPos (x : N) : positive :=
  match N.discr x with
  | inright HO   => 1 
  | inleft Hpos  => (* Please tell me how to further destruct Hpos *)
  end.

Answer 1

In general, to decipher a notation, you can ask something like

Locate "{ x | p }".

In this case, this figures out what { p : positive | n = pos p } means (you replace the "replaceable" parts of the notation with (meta)variables). It gives

Notation "{ x  |  P }" := sig (fun x => P)

Now the name sig can be used to get more information.

Print sig.
(*
Inductive sig (A : Type) (P : A -> Prop) : Type :=
  exist : forall x : A,
          P x -> {x : A | P x}
Arguments exist [A]%type_scope _%function_scope
*)

Which tells you that you need to match Hpos against exist _ p Hpos (the Arguments say that A is implicit and that P is explicit, but P (as a parameter) is already fixed by the type of the scrutinee and must be ignored, and the remaining arguments, x : A and the P x, need to be named).

Alternatively,

Unset Printing Notations. (* In CoqIDE, you're told to set this from the view menu instead *)
Check N.discr.
(* Shows you that the notation stands for sig *)

And then continue as before.

Answer 2

I eventually figured this out by checking Print N.discr and observing:

N.discr = 
fun n : N =>
match n as n0 return ({p : positive | n0 = N.pos p} + {n0 = 0%N}) with
| 0%N => inright eq_refl
| N.pos p =>
    inleft (exist (fun p0 : positive => N.pos p = N.pos p0) p eq_refl)
end
     : forall n : N, {p : positive | n = N.pos p} + {n = 0%N}

and seeing that the case I want is exist (fun p0 : positive => N.pos p = N.pos p0) p eq_refl. Then, exist is the key function. From that I was able to correctly guess inleft (exists p Hpos) would work:

Definition NToPos (x : N) : positive :=
  match N.discr x with
  | inright HO            => 1 
  | inleft (exist p Hpos) => p
  end.