dependent pattern matching issue

Stream: new members

[Emmanuel Beffara]

Hello,

I am currently learning Lean, after practicing a bit of Coq in the past. For this, I alternate between following tutorials and trying to transpose some code of mine from Coq (mostly related to programming language semantics) to get a feel of the differences.

I am struggling to understand an issue with dependent pattern matching in Lean3. I tried to minimize the example by removing as much as I could from the original code, and I get the following, which of course makes little sense in itself but exhibits my issue:

universes u

inductive thing : Type u → Type (u + 1)
| nil (α) : thing α

def extend : ℕ → Type u → Type u
| 0 α := α
| _ α := α

def grow (n) {α} (_ : thing α) : option (thing (extend n α)) := none

def truncate (n : ℕ) {α} (t : thing α) : option (thing α) :=
match grow n t with
| (some (thing.nil _)) := none
| _ := none
end

I get the error dependent pattern matching result is not a constructor application but I don't get why, because everything in the definition of truncate has an expected type that starts with a constructor. I tried to use set_option trace.eqn_compiler.elim_match true as the message suggests but it doesn't help me understand. If I translate this into Coq, it works fine, so my guess is that this is not a deep theoretical issue but rather has something to do with the form of my definition.

Further exploration shows that:

• if I replace some (thing.nil _) with some _, then it works fine
• if I remove the first case of extend so that no matching is needed there, then it works fine too
• I can also define the function in tactic mode with cases and exact, or with calls to cases_on with explicit motives

So what would be the proper way to proceed? Maybe I need to add some type annotations somewhere?

[Kyle Miller]

I tested it out in Lean 4, and it works fine there:

universe u

inductive thing : Type u → Type (u + 1)
| nil (α) : thing α

@[matchPattern]
def thing.nil' (α : Type u) : thing α := thing.nil

def extend : Nat → Type u → Type u
| 0, α => α
| _, α => α

def grow (n) {α} (_ : thing α) : Option (thing (extend n α)) := none

def truncate (n : Nat) {α} (t : thing α) : Option (thing α) :=
match grow n t with
| (some (thing.nil' _)) => none
| _ => none

(I just needed to define a synonym for the constructor since for some reason α is now forced to be implicit. Not sure if that's intended.)

[Emmanuel Beffara]

Ok, good to know. I still fail to see how I should do this properly in Lean 3, though.

As for the choice of versions, at first I thought that learning directly with Lean 4 would be natural, since it does appear first in the documentation page and it already works, but most existing libraries and learning material is for Lean 3 and mathlib 4 is still experimental, so Lean 4 does not seem ready for development of stable things.

[Kyle Miller]

Sorry, I forgot to mention that I only tested it in Lean 4 to see whether it's something might expect to work or not. It would be nice to see why it's not working in Lean 3.

[Kyle Miller]

It seems that in Lean 3 a workaround is to use the cases tactic, which isn't the best, but at least it points to this being possible.

import tactic

universes u

inductive thing : Type u → Type (u + 1)
| nil (α) : thing α

def extend : ℕ → Type u → Type u
| 0 α := α
| _ α := α

def grow (n) {α} (_ : thing α) : option (thing (extend n α)) := none

def truncate (n : ℕ) {α} (t : thing α) : option (thing α) :=
begin
  generalize h : grow n t = x, -- create a local variable `x` that is equal to `grow n t` via `h`
  cases x,
  case option.none
  { exact none },
  case option.some
  { cases x,
    /- h : grow n t = some (thing.nil (extend n α)) -/
    exact none },
end

[Kyle Miller]

It seems that extend is somehow causing the "dependent pattern matching result is not a constructor application" error. If you comment out the 0 case for it, then the error goes away.

def extend : ℕ → Type u → Type u
--| 0 α := α
| _ α := α

[Kyle Miller]

Or if you change n to n+1 in truncate the error goes away.

def truncate (n : ℕ) {α} (t : thing α) : option (thing α) :=
match grow (n+1) t with
| (some (thing.nil _)) := none
| _ := none
end

[Kyle Miller]

This makes me think that it's trying to see what extend n α is definitionally equal to -- both of these modifications are things that let it reduce extend.

[Kyle Miller]

@Emmanuel Beffara Oh, maybe it has something to do with exhaustiveness checking and your use of _ as a catch-all pattern. All you need to do is use none instead:

def truncate (n : ℕ) {α} (t : thing α) : option (thing α) :=
match grow n t with
| (some (thing.nil _)) := none
| none := none
end

[Emmanuel Beffara]

Interesting ! Thanks for the last solution. So maybe it has to do with the shape of the code produced by the equation compiler.

This trick does solve the issue in my original code, although I have to manually split the catch-all _ into enough sub-cases so that all cases are explicitly disjoint, which makes 5 cases because the pattern and the types are more complicated. not completely satisfying, but it does the job…