match: generalizing, motive, etc

Stream: new members

[Francisco Giordano]

Is there anywhere I could read about the more advanced features of Lean's match? In particular generalizingand motive. I'm also interested in manually proving that some cases are unreachable given hypotheses, I've found that I can do it using absurd but I don't know if that's how it's usually done.

[Francisco Giordano]

I've seen the term "motive" used around induction principles too, and I'm not sure how to interpret the general concept.

[Francisco Giordano]

Okay, after reviewing "The Type Theory of Lean" I think I get that the motive is just the type family for the result of the match expression. I'm guessing the motive of a match expression is usually inferred for normal programming, but may need to be spelled out for theorem proving.

[Kyle Miller]

The motive is to control how the type of the match expression should depend on the values of the objects being matched (so yeah, it's the type family you mentioned). Lean tries to compute a motive automatically, but if it gets it wrong you can override it. This might be necessary if you have really complicated dependent types.

The generalizing feature (which is on by default) is controlling whether to automatically include additional variables as discriminants if they depend on the discriminants being matched against. This is like a dual to the motive (generalizing is for variables in the context, and motive is for the expected type).

[Kyle Miller]

Francisco Giordano said:

I'm also interested in manually proving that some cases are unreachable given hypotheses, I've found that I can do it using absurd but I don't know if that's how it's usually done.

Yeah, absurd is common. If you're lazy, you can sometimes do by simp at h where h is your hypothesis, if that hypothesis simplifies to False.

[Kyle Miller]

If the hypothesis is an equality that's absurd, and it's an equality involving constructors, you can sometimes do by cases h

[Eric Wieser]

I thought generalizing was only sometimes on by default?

[Francisco Giordano]

I think that changed in Lean 4.0.0-m4. RELEASES.md says:

(generalizing := true) is the default behavior for match expressions even if the expected type is not a proposition

[Francisco Giordano]

Kyle Miller said:

whether to automatically include additional variables as discriminants if they depend on the discriminants being matched against

I'm not sure what this means. What are the discriminants?

Here's a situation that I don't fully understand yet. Would appreciate some pointers.

inductive Term where
  | var (id : String)
  | lam (id : String) (body : Term)
  | app (f : Term) (t : Term)

inductive IsValue : Term → Prop where
  | var : IsValue (Term.var _)
  | lam : IsValue (Term.lam _ _)

def typeOfValue (t : Term) (_ : IsValue t) :=
  match t with
  | Term.var _ => "var"
  | Term.lam _ _ => "lam"

This compiles fine, but when I add (generalizing := false) I get the following error:

application type mismatch
  ?m.753 (Term.var id✝) x✝
argument
  x✝
has type
  IsValue t : Prop
but is expected to have type
  IsValue (Term.var id✝) : Prop

[Eric Wieser]

Francisco Giordano said:

I think that changed in Lean 4.0.0-m4. RELEASES.md says:

(generalizing := true) is the default behavior for match expressions even if the expected type is not a proposition

I think I must have read an outdated docstring somewhere

[Kyle Miller]

@Francisco Giordano The syntax is match ...discriminants... with | ...patterns... => ... ...

[Kyle Miller]

Here's how to do when generalizing is false:

def typeOfValue (t : Term) (h : IsValue t) :=
  match (generalizing := false) t, h with
  | Term.var _, _ => "var"
  | Term.lam _ _, _ => "lam"

This is what generalizing := true does for you.

[Kyle Miller]

I think the way it works is that when you have multiple discriminants, each discriminant generalizes itself in the next, so in the first case for example the second pattern has type IsValue (Term.var _) rather than IsValue t

[Kyle Miller]

The reason you don't need to write the Term.app case is that the second pattern has type IsValue (Term.app _ _) and it's smart enough to see that there are no constructors that produce that, so it can handle that case automatically

[Kyle Miller]

I don't understand the application type mismatch error. It might be a bug.

[Francisco Giordano]

Leaving out the Term.app case without errors was exactly what I wanted in this example.

One final (tangential) thing about this function I'm having trouble with is that if I define {h : IsValue t} as an implicit, Lean is not able to synthesize it. It works well if I give it an auto-tactic: (h : IsValue t := by constructor). But this seems redundant, is this normal? Is there any way to customize implicit synthesis / elaboration?

[Francisco Giordano]

I think I understand now, that to synthesize implicit arguments Lean will only try to find a suitable value in the environment by unification without invoking any (other) tactics.

Thanks for the help!

[Kyle Miller]

Yes, I think (h : IsValue t := by constructor) is the way you'd do it. I wish you could do {h : IsValue t := by constructor} so that the only way to pass it explicitly is by using a keyword argument (like typeOfValue t (h := ...))