## Stream: new members

### Topic: lack of information in match

#### Gun Pinyo (Jul 15 2019 at 16:32):

Hi everyone, I have a problem with match expression. Given the following code

def foo (α : Type) (n : ℕ) (i : fin n) : α :=
match n with
| nat.zero    := {! 1 !}
| nat.succ n' := {! 2 !}
end

To complete the first goal, I should be able to put fin.elim0 i
since i : fin 0 and has no element.

However, the problem is that Lean tells me that i : fin n. That's
fine since n = 0 anyway but how can get such evidence that n = 0 from match?

#### Kevin Buzzard (Jul 15 2019 at 16:37):

This should be in a FAQ; it comes up every couple of months. There's some clever trick to get round it which sometimes I remember but right now I don't.

#### Bryan Gin-ge Chen (Jul 15 2019 at 16:38):

For this example, you can use pattern-matching more directly like this:

def foo' (α : Type) :  n, fin n  α
| 0 f := f.elim0
| (n+1) f := {! 2 !}

#### Bryan Gin-ge Chen (Jul 15 2019 at 16:39):

I guess this works in match:

def foo (α : Type) (n : ) (i : fin n) : α :=
match n, i with
| nat.zero, i   := i.elim0
| nat.succ n', i := {! 2 !}
end

#### Andrew Ashworth (Jul 15 2019 at 16:40):

in Lean you must explicitly list i as a parameter in match, since it participates in the function

#### Gun Pinyo (Jul 15 2019 at 16:41):

ah, thank you, everyone.

#### Keeley Hoek (Jul 16 2019 at 04:30):

woah, what is this "a comma is allowed in match" syntax? Does a comma make a term of prod without the outer parentheses, or is that hardcoded?

#### Mario Carneiro (Jul 16 2019 at 04:37):

No, match is more like a multiple lambda + application. It supports multiple args same as def, they aren't tupled

#### Keeley Hoek (Jul 16 2019 at 04:51):

why does the syntax for an "inline match" used to make a definition not require the use of commas, then?

#### Marc Huisinga (Jul 16 2019 at 08:45):

i assume the syntax for definitions is that way to be consistent with everything else (where space is usually the delimiter of choice when possible).
for the match syntax, you need some delimiter between the arguments to the match to distinguish it from function application, and the syntax for the cases is then chosen to be consistent with the delimiter for the parameters.

#### Gun Pinyo (Jul 17 2019 at 09:59):

Hi, I have another question to ask. This is the original motivation why I open this topic in the first place. I just manage to simplify from my original code.

def foo1 (α : unit  Type*) (x : unit) (y : α x) : y = y :=
match x with
| unit.star := rfl
end

def foo2 (α : unit  Type*) (x : unit) (y : α x) : y = y :=
match x, y with
| unit.star, y := rfl
end

foo1 should be able to finish with rfl alone but my original code requires me to use match (so be it). The match expression is trivial yet lean complain that

"invalid match/convoy expression, user did not provide type for the expression, lean tried to infer one using expected type information, but result is not type correct nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)"

So after seeing a trace from 'set_option trace.check true' I see that the problem comes from yso I fix it in foo2. However, it doesn't make any sense why I must pattern matching in y as it is not used in rfl at all. Anyone, please explain to me, please?

#### Gun Pinyo (Jul 17 2019 at 10:15):

Another thing that I notice is that, the old y in foo2 outside match doesn't go away, I know this from the context of an error message when rfl is replaced by _, there are two y in the context. Well, this makes sense if match is just a syntactic sugar of the original pattern matching function.

My concern is that, should I really use the same name for both y? I don't want to use the different name since it pollutes the context, but if I use the same name, I might run into another cryptic error message where I have another variable that depends on the original y and I think that the variable depends on the new y. Moreover, I don't have evidence that the old and new y are equal (the same problem of my very first question).

I try to think that is there a way not to introduce a new y? I try to use an inaccessible term by changing the inner y to be .(y)but I have an error message saying that "ill-formed match/equation expression". Doesn't an inaccessible term work in match expression?

#### Jesse Michael Han (Jul 17 2019 at 18:36):

Lean accepts rfl as a proof term for foo1 (for me).

You can replace the y in the match-expression in foo2 with placeholder (_) to indicate that it doesn't really matter.

There's a tactic for clearing away assumptions whose names begin with underscores.

#### Kevin Buzzard (Jul 17 2019 at 18:38):

I guess the issue isn't proving foo1, it's why the match doesn't work. One could imagine a more complex situation where you need the case split

#### Mario Carneiro (Jul 17 2019 at 18:39):

You can't match x in the first place there

Why not?

#### Kevin Buzzard (Jul 17 2019 at 18:40):

def foo1 (α : unit  Type*) (x : unit) (y : α x) : y = y :=
match (x : unit) with
| unit.star := (rfl : y = y)
end

/-
invalid match/convoy expression, user did not provide type for the expression, lean tried to infer one using expected type information, but result is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
-/

#### Kevin Buzzard (Jul 17 2019 at 18:40):

dammit Lean I provided types for all the expressions

#### Mario Carneiro (Jul 17 2019 at 18:41):

Think about this from first principles. The recursor says that if you want to prove forall x : unit, C x it suffices to prove it for C star. match is reverting x, then applying the recursor, but it's not possible to revert only x because y depends on x

#### Kevin Buzzard (Jul 17 2019 at 18:42):

def foo1 (α : unit  Type*) (x : unit) (y : α x) : y = y :=
begin
cases x,
refl,
end

I matched!

#### Mario Carneiro (Jul 17 2019 at 18:42):

when lean says "user did not provide type for the expression" it means you didn't write match x : forall x : unit, y = y with ...

#### Kevin Buzzard (Jul 17 2019 at 18:42):

Aah, I see your point now Mario. So match reverts only the stuff being matched, and then attempts to apply the recursor.

#### Mario Carneiro (Jul 17 2019 at 18:43):

cases will automatically revert and re-intro all dependent hypotheses like y here, so it has the same effect as putting y in the match and also in the pattern

#### Mario Carneiro (Jul 17 2019 at 18:44):

It also removes the outer y if it can so you don't get confused

#### Kevin Buzzard (Jul 17 2019 at 18:44):

def foo1 (α : unit  Type*) (x : unit) (y : α x) : y = y :=
begin
revert x,
refine punit.rec _,
-- refl will not work here
intros, refl
end

#### Kevin Buzzard (Jul 17 2019 at 18:46):

@Gun Pinyo the moral is that you shouldn't be matching terms when other terms depend on them. You have to match all the terms depending on them too.

#### Mario Carneiro (Jul 17 2019 at 18:47):

If the type of a variable has to change, then it can't be the same variable

#### Mario Carneiro (Jul 17 2019 at 18:47):

the old y had type A x, the new one has type A star

#### Gun Pinyo (Jul 18 2019 at 11:01):

@Mario Carneiro @Kevin Buzzard Thank you for your explanation.

It seems to me that the tactic approach is much cleaner and easier to use than term-proving approach (at least for my questions). Up until now, I try to use the term-proving approach as much as possible to aid readability but now I need to change my mind.

Last updated: Dec 20 2023 at 11:08 UTC