Match statement proposition inference

Stream: new members

[Jonathan Lacombe]

Is it possible to infer propositions from cases in match statements, when defining a function? In other words, how do I show that a case must be of a certain type because the other cases were covered.

I have a simple example below where I would expect to be able to use simp or assumption. I know I could just write out the other two cases but the real problem I am working on is a bit more complicated.

inductive Day where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday

def Weekday := { x: Day // (x ≠ Day.saturday ∧ x ≠ Day.sunday) }
def Weekend := { x: Day // (x = Day.saturday ∨ x = Day.sunday) }

def Day.next_weekend (d: Day): Weekend :=
  match d with
  | monday => Subtype.mk Day.saturday (by simp)
  | tuesday => Subtype.mk Day.saturday (by simp)
  | wednesday => Subtype.mk Day.saturday (by simp)
  | thursday => Subtype.mk Day.saturday (by simp)
  | friday => Subtype.mk Day.saturday (by simp)
  | d => Subtype.mk d (by assumption) -- neither this nor simp works here

[Kyle Miller]

match doesn't have that feature, but it's able to take into account hypotheses floating around. For example

def Day.next_weekend (d : Day) : Weekend :=
  if h : d = Day.saturday ∨ d = Day.sunday then
    Subtype.mk d h
  else
    match d with
    | monday => Subtype.mk Day.saturday (by simp)
    | tuesday => Subtype.mk Day.saturday (by simp)
    | wednesday => Subtype.mk Day.saturday (by simp)
    | thursday => Subtype.mk Day.saturday (by simp)
    | friday => Subtype.mk Day.saturday (by simp)

[Jonathan Lacombe]

Kyle Miller said:

match doesn't have that feature, but it's able to take into account hypotheses floating around. For example

def Day.next_weekend (d : Day) : Weekend :=
  if h : d = Day.saturday ∨ d = Day.sunday then
    Subtype.mk d h
  else
    match d with
    | monday => Subtype.mk Day.saturday (by simp)
    | tuesday => Subtype.mk Day.saturday (by simp)
    | wednesday => Subtype.mk Day.saturday (by simp)
    | thursday => Subtype.mk Day.saturday (by simp)
    | friday => Subtype.mk Day.saturday (by simp)

Thank you so much for this. I did have to add deriving DecidableEq to the inductive type definition, but it works perfectly. I wasn't even familiar with using a hypothesis like that in an if statement. I can actually do a lot more with this. :+1:

[Jonathan Lacombe]

Btw, is there a type of way to extract d = Day.saturday ∨ d = Day.sunday into it's own definition?

Doing this doesn't work:

def is_weekend (d: Day) := d = Day.saturday ∨ d = Day.sunday

The resulting definition has the signature: is_weekend (d : Day) : Prop, returning a Prop instead of the expected d = Day.saturday ∨ d = Day.sunday

[Kyle Miller]

What you have is correct, and it's supposed to return a Prop.

[Kyle Miller]

(Remember that every element of Prop is equal to either True or False)

[Kyle Miller]

inductive Day where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
  deriving DecidableEq

@[simp] abbrev isWeekend (d: Day) := d = Day.saturday ∨ d = Day.sunday

def Weekday := { x: Day // ¬ isWeekend x }
def Weekend := { x: Day // isWeekend x }

def Day.next_weekend (d : Day) : Weekend :=
  if h : isWeekend d then
    Subtype.mk d h
  else
    match d with
    | monday => Subtype.mk Day.saturday (by simp)
    | tuesday => Subtype.mk Day.saturday (by simp)
    | wednesday => Subtype.mk Day.saturday (by simp)
    | thursday => Subtype.mk Day.saturday (by simp)
    | friday => Subtype.mk Day.saturday (by simp)

[Kyle Miller]

abbrev makes it so the Decidable is able to be inferred automatically, and @[simp] makes it so that simp will unfold the definition automatically.

[Kyle Miller]

You can also derive a decidable instance by getting Lean to unfold the definition a bit, if you don't want it to be an abbrev.

@[simp] def isWeekend (d: Day) := d = Day.saturday ∨ d = Day.sunday
instance : DecidablePred isWeekend := fun _ => inferInstanceAs <| Decidable (_ ∨ _)

[Kyle Miller]

I think I saw that there's some sort of deriving syntax here that makes this cleaner, but I forgot how...

[Jonathan Lacombe]

Kyle Miller said:

You can also derive a decidable instance by getting Lean to unfold the definition a bit, if you don't want it to be an abbrev.

@[simp] def isWeekend (d: Day) := d = Day.saturday ∨ d = Day.sunday
instance : DecidablePred isWeekend := fun _ => inferInstanceAs <| Decidable (_ ∨ _)

That works perfectly. I don't really understand the DecidablePred syntax but the abbrev works just as well for me. I'll make sure to read up on the Decidable and unfolding, I don't really understand those terms. This really helps a lot. I feel like Lean has a bigger learning curve (compared to other programming languages) but everything I learn seems extremely useful. Thanks

[Kyle Miller]

DecidablePred p is an abbreviation for fun x => Decidable (p x), for convenience.

[Kyle Miller]

inferInstanceAs is a way to change how the expression is represented, and "unfolding" is referring to unfolding a definition (i.e., replacing it with the body of its definition). Here I'm triggering an unfolding of isWeekend using a trick where I know that the definition is "something or something"

[Kyle Miller]

More explicitly, but more to write,

instance : DecidablePred isWeekend :=
  fun d => inferInstanceAs <| Decidable (d = Day.saturday ∨ d = Day.sunday)

[Kyle Miller]

And Decidable is a way to make it so that a given Prop can be used in an if statement's condition. A Prop is just a logical specification of a truth value, but Decidable is a mechanism to synthesize a way to evaluate the truth value.

[Jonathan Lacombe]

Kyle Miller said:

And Decidable is a way to make it so that a given Prop can be used in an if statement's condition. A Prop is just a logical specification of a truth value, but Decidable is a mechanism to synthesize a way to evaluate the truth value.

Okay, I think I get it - Decidable is like computable, we can evaluate the body. And I am guessing the unfolding happens due to the definition of the DecidablePred, it sorts of inserts that isWeekend definition where the (_ ∨ _) is. This really helps a lot. I really appreciate this.

[Kyle Miller]

You can sort of think of Decidable as mechanically building a Bool expression for a Prop, for example replacing ∨ with &&, by searching through the database of Decidable instances to make these replacements.

This is all to make it so that as many propositions as possible "are" booleans. Of course, by incompleteness, there's no algorithm that can do this translation in general.

[Jonathan Lacombe]

Kyle Miller said:

You can sort of think of Decidable as mechanically building a Bool expression for a Prop, for example replacing ∨ with &&, by searching through the database of Decidable instances to make these replacements.

This is all to make it so that as many propositions as possible "are" booleans. Of course, by incompleteness, there's no algorithm that can do this translation in general.

I see. I should probably get familiar with using it since I'll mostly be using Lean in a programming context

[Jonathan Lacombe]

@Kyle Miller Regarding the example above, do you know how I might check for equality (or some other condition) over multiple argument values.

Adding an argument to one of the inductive cases breaks what I wanted to do. Is there a way I can create a proposition that I can check if a day is equal to any saturday (n: Nat). I tried ∃ x, d = Day.saturday x but then I got decidable synthesize errors again. I tried creating a DecidablePred but it didn't work out with the existential modifier.

The code below has a "metavariables in h" error

inductive Day where
  | monday (n: Nat)
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday (n: Nat)
  | sunday
  deriving DecidableEq

def Weekday := { x: Day // (x ≠ Day.saturday 6 ∧ x ≠ Day.sunday) }
def Weekend := { x: Day // (x = Day.saturday 6 ∨ x = Day.sunday) }

abbrev isWeekend (d: Day) := d = Day.saturday 6 ∨ d = Day.sunday

def Day.next_weekend (d : Day) : Weekend :=
  if h: d = Day.saturday _ ∨ d = Day.sunday then
    Subtype.mk (Day.saturday 6) (by simp)
  else
    match d with
    | monday _ => Subtype.mk (Day.saturday 6) (by simp)
    | tuesday => Subtype.mk (Day.saturday 6) (by simp)
    | wednesday => Subtype.mk (Day.saturday 6) (by simp)
    | thursday => Subtype.mk (Day.saturday 6) (by simp)
    | friday => Subtype.mk (Day.saturday 6) (by simp)

With this example, saturday is still a missing case

[Kyle Miller]

Instead of using =, you could use a matches expression, which is just syntax sugar for a match, but somehow it works cleanly here.

inductive Day where
  | monday (n: Nat)
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday (n: Nat)
  | sunday

def Weekday := { x: Day // (x ≠ Day.saturday 6 ∧ x ≠ Day.sunday) }
def Weekend := { x: Day // (x = Day.saturday 6 ∨ x = Day.sunday) }

def Day.next_weekend (d : Day) : Weekend :=
  if h : d matches .saturday _ | .sunday then
    Subtype.mk (Day.saturday 6) (by simp)
  else
    match d with
    | monday _ => Subtype.mk (Day.saturday 6) (by simp)
    | tuesday => Subtype.mk (Day.saturday 6) (by simp)
    | wednesday => Subtype.mk (Day.saturday 6) (by simp)
    | thursday => Subtype.mk (Day.saturday 6) (by simp)
    | friday => Subtype.mk (Day.saturday 6) (by simp)

(If you haven't seen .saturday syntax, it's using the expected type to see that it should be Day.saturday.)

[Kyle Miller]

Or there's wrapping that up as a predicate:

def isWeekend (d : Day) : Bool :=
  match d with
  | .saturday _ | .sunday => true
  | _ => false

def Day.next_weekend (d : Day) : Weekend :=
  if h : isWeekend d then
    Subtype.mk (Day.saturday 6) (by simp)
  else
    ... same as before ...

This is illustrating using Bool instead of Prop, which saves needing to create Decidable instances. There are reasons to prefer Prop when you're doing reasoning, but sometimes it's easier to use Bool directly (plus the match seems to be able to handle it).

[Jonathan Lacombe]

Kyle Miller said:

Or there's wrapping that up as a predicate:

def isWeekend (d : Day) : Bool :=
  match d with
  | .saturday _ | .sunday => true
  | _ => false

def Day.next_weekend (d : Day) : Weekend :=
  if h : isWeekend d then
    Subtype.mk (Day.saturday 6) (by simp)
  else
    ... same as before ...

This is illustrating using Bool instead of Prop, which saves needing to create Decidable instances. There are reasons to prefer Prop when you're doing reasoning, but sometimes it's easier to use Bool directly (plus the match seems to be able to handle it).

Thanks, I like the match syntax. This is actually really great, and I can still do stuff like abbrev isSaturday (d: Day) := d matches Day.saturday _ which is really cool.

[Kyle Miller]

Make sure to right click on matches and "go to definition" to see that it's just a macro too :-)

Here's a way to see how it expands:

def isWeekend (d : Day) : Bool :=
  d matches .saturday _ | .sunday
#print isWeekend
/-
def isWeekend : Day → Bool :=
fun d ↦
  match d with
  | Day.saturday n => true
  | Day.sunday => true
  | x => false
-/

[Jonathan Lacombe]

Kyle Miller said:

Make sure to right click on matches and "go to definition" to see that it's just a macro too :-)

Here's a way to see how it expands:

def isWeekend (d : Day) : Bool :=
  d matches .saturday _ | .sunday
#print isWeekend
/-
def isWeekend : Day → Bool :=
fun d ↦
  match d with
  | Day.saturday n => true
  | Day.sunday => true
  | x => false
-/

I actually did look at the macro but I didn't understand it, but I forgot you can use print to inspect the generated code

[Kyle Miller]

Macro syntax can be rather obscure, but I just think it's neat that it's something you could define yourself, without needing to wait for Lean to implement it.