Zulip Chat Archive

Stream: new members

Topic: cases with dependent types


Justin Pearson (Oct 26 2021 at 10:59):

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 (Oct 26 2021 at 11:08):

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

Last updated: Dec 20 2023 at 11:08 UTC