lack of information in `match`

Stream: new members

[Gun Pinyo]

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]

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]

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]

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]

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

[Gun Pinyo]

ah, thank you, everyone.

[Keeley Hoek]

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]

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

[Keeley Hoek]

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

[Keeley Hoek]

instead we have to do that weird bracket business

[Marc Huisinga]

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]

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]

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]

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]

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]

You can't match x in the first place there

[Kevin Buzzard]

Why not?

[Kevin Buzzard]

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]

dammit Lean I provided types for all the expressions

[Mario Carneiro]

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]

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

I matched!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

@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]

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

[Mario Carneiro]

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

[Gun Pinyo]

@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.