cases with dependent types

Stream: new members

[Justin Pearson]

In the following code extract_n works, while extract_z does not.

inductive mysum : ℕ → Type
 | pn (n : ℕ)  :     (mysum 1)
 | pz (z : ℕ)  :     (mysum 2)

def extract_n (h : mysum 1) : ℕ :=
begin
  cases h with n ,
  exact n
end


def extract_z (h : mysum 2) : ℤ :=
begin
 cases h  with z ,
 exact z
end

When I say that it does not work, I mean that in extract_z you cannot use the with expression to name the terms, even though they get extracted.
Even stranger, if I swap the order of pn and pz in the definition of mysum then extract_z works and extract_n does not work.

I don't want to write the above functions, and I know that there are other ways to achieve the above, but I want to use cases in a proof with a depenedent type. My case is of course more complicated, I have a dependent type something : Blah → Prop, and I want to use cases in tactic to extract the information from a particular term of type (something (b : Blah)).

Is there a better way of doing this? Or what am I misunderstanding?

[Reid Barton]

You need to provide names even for the fields of constructors that cases will determine are impossible--I never understood exactly why.

inductive mysum : ℕ → Type
 | pn (n : ℕ)  :     (mysum 1)
 | pz (z : ℤ)  :     (mysum 2)

def extract_n (h : mysum 1) : ℕ :=
begin
  cases h with n _,
  exact n
end

def extract_z (h : mysum 2) : ℤ :=
begin
 cases h with _ z,
 exact z
end