Pattern matching and proofs involving equality

Stream: new members

[Kuba]

Hi,

Following advice from chapter 7 of TPIL, I am trying to develop the concept of partial function (function that is defined only for some elements of a given type) composition. Here is what I have got:

def compose_part.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (outer : β → Option γ) (inner : α → Option β) : α → Option γ
    :=
    fun (x : α) => match inner x with
    |   none => none
    |   some b => outer b

Next, I wanted to prove some properties of this definition. As a warm up, I decided to show that if for a given argument, the inner function evaluates to none, then so does the composition. I wanted to write this proof without using tactics or the triangle ▸ macro, in order to better understand how the proofs involving equality actually work. Here is what I was able to come up with:

theorem theorem1.{u,v,w} {α : Type u} {β : Type v} {γ : Type w} :
    ∀ (f : β → Option γ) (g : α → Option β),
    ∀ (x : α), g x = none → compose_part f g x = none
    :=
    λ f g => λ x => λ h => calc
        compose_part f g x =
            (match g x with
            |   none => none
            |   some b => f b)
            := rfl
        _ = none := Eq.rec (Eq.refl
            (match none with
            |   none => none
            |   some b => f b)) (Eq.symm h)

Whilst this seems to be correct, repeatedly writing down those pattern matching expressions seems a bit awkward. Is there a nicer way of writing this proof, without resorting to the means I mentioned above? Is there a general method of proving things about functions defined using pattern matching? Is there a nice way of combining pattern matching and calculational proofs?

Any other suggestions about how to make this definition and/or proof nicer are also very welcome.

Update:
In order to understand a bit better how equality works in lean, I tried to supply the motive for the Equality type recursor by hand, instead of relying on the elaborator. The following is my attempt:

theorem theorem1.{u,v,w} {α : Type u} {β : Type v} {γ : Type w} :
    ∀ (f : β → Option γ) (g : α → Option β),
    ∀ (x : α), g x = none → compose_part f g x = none
    :=
    λ f g => λ x => λ hyp => calc
        compose_part f g x = (match g x with | none => none | some b => f b)
            := rfl
        _ = (match none with | none => none | some b => f b)
            := Eq.rec
                (motive := λ a => λ _ =>
                    ((match g x with | none => none | some b => f b) =
                        match a with | none => none | some b => f b))
                (Eq.refl (match g x with | none => none | some b => f b))
                hyp
        _ = none := rfl

It fails, with the following error:

application type mismatch
  @Eq.rec (Option β) (g x)
    (fun a x_1 =>
      (match g x with
        | none => none
        | some b => f b) =
        match a, x_1 with
        | none, x => none
        | some b, x => f b)
    (Eq.refl
      (match g x with
      | none => none
      | some b => f b))
argument
  Eq.refl
    (match g x with
    | none => none
    | some b => f b)
has type
  (match g x with
    | none => none
    | some b => f b) =
    match g x with
    | none => none
    | some b => f b : Prop
but is expected to have type
  (match g x with
    | none => none
    | some b => f b) =
    match g x, (_ : g x = g x) with
    | none, x => none
    | some b, x => f b : Prop

This makes no sense to me. Why is lean inserting x_1 into one of the match expressions? What am I missing here?

[Kevin Buzzard]

The nicer way of writing the proof is to use tactics, precisely because the intuitively clear concept of "replace this subterm of a term with this equal term" gets totally drowned in type theory when you write it as "apply the recursor for equality to this specific motive". The debugging hell that you're going through trying to explicitly use the recursor is exactly what should be telling you to use the rw tactic. Compare with this:

def compose_part {α : Type _} {β : Type _} {γ : Type _}
    (outer : β → Option γ) (inner : α → Option β) (a : α) : Option γ :=
  match inner a with
  | none => none
  | some b => outer b

theorem theorem1 (f : β → Option γ) (g : α → Option β) (x : α) (h : g x = none) :
    compose_part f g x = none := by
  simp [compose_part, h]

The simplifier just does all the rewrites for you and deals with all the recursor stuff. I appreciate that you have a question above, but the point of tactics is exactly so that humans don't have to bother with that kind of question.

[Kevin Buzzard]

You can see the proof which the tactic generated under the hood with #print theorem1.

[Kuba]

Yeah, I definitely would not want to do it the hard way every time, but I am still determined to try a few examples by hand. One of the reasons I picked up lean is that I want to learn a bit more about theorem proving itself. Also, I guess I can't stop myself from taking things apart to see how they work.

Anyway, I followed your advice about printing the auto-generated proof. After some digging and then more digging, I realised that for the sort of low level, manual work that I am trying to do, I might want to alter my definition of compose_part. Here it is:

def compose_part.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (outer : β → Option γ) (inner : α → Option β) (x : α) : Option γ
    :=
    Option.rec none (λ y => outer y) (inner x)

To my dismay, I get the following message:

code generator does not support recursor 'Option.rec' yet,
consider using 'match ... with' and/or structural recursion

How is this possible? Recursors seem to be quite fundamental objects, so it seems weird one would not be supported. Also, aren't match expressions supposed to be compiled to recursors? Am I making a mistake here? Is it possible this is a bug in some part of lean (probably not)?

[Alex J. Best]

Do you actually want executable code for your purposes? If not you can simply use noncomputable def here as a workaround for now.

[Kuba]

I am not sure what computability has to do with my problem. I am not familiar with noncomputable def. Can you elaborate (pun unintended)?

[Alex J. Best]

By default lean tries to produce executable code for all definitions so that for appropriate arguments functions can be actually run and the output evaluated. The error you are seeing is that the code generator, which is the system that produces the executable code for this, doesn't support what you are doing (yet). So if you never want to actually evaluate your functions as if it were a program (rather you just want to prove things about them) then telling lean you don't want to produce code for them then there is no longer an issue

[Eric Wieser]

Kuba said:

Is it possible this is a bug in some part of lean (probably not)?

lean4#2049

[Kuba]

Hmm, I see. I think I would like to be able to actually run this function.

I should probably mention that I do not get this message if I use casesOn:

def compose_part.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (outer : β → Option γ) (inner : α → Option β) (x : α) : Option γ
    :=
    Option.casesOn (inner x) none (λ y => outer y)

But if you print what casesOn actually is:

#print Option.casesOn

@[reducible] protected def Option.casesOn.{u_1, u} : {α : Type u} →
  {motive : Option α → Sort u_1} → (t : Option α) → motive none → ((val : α) → motive (some val)) → motive t :=
fun {α} {motive} t none some => Option.rec none (fun val => some val) t

It is a 'wrapper' around Option.rec

I will see if I can actually evaluate an expression with compose_part thus defined.

[Kuba]

If I use casesOn instead of rec it seems to work fine:

def compose_part.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (outer : β → Option γ) (inner : α → Option β) (x : α) : Option γ
    :=
    Option.casesOn (inner x) none (λ y => outer y)

def f (n : Nat) : Option Nat :=
    match n with
    |   0 => none
    |   _ => some (2*n)

def g (n : Nat) : Option Nat :=
    match n with
    |   1 => none
    |   _ => some (n+1)

#eval compose_part f g 0 -- some 2
#eval compose_part f g 1 -- none

This seems weird given that casesOn is itself defined using rec.

[Kuba]

Eric Wieser said:

Kuba said:

Is it possible this is a bug in some part of lean (probably not)?

lean4#2049

Does this mean that the code generator has to be modified every time a new inductive type is defined in order for it to support its corresponding recursor?

[Kyle Miller]

No, thankfully not. The code generator is able to see that there's a match and compile it, rather than going through recursors.

There are some reasons not to expand everything out to recursors and then compile those. One reason I know of is that since Lean has strict evaluation semantics, there are things that can evaluate you didn't expect to evaluate. However, there are plans to get the code generator to know how to compile recursors. It's just not been a priority, as I understand.

[Kuba]

Kyle Miller said:

No, thankfully not. The code generator is able to see that there's a match and compile it, rather than going through recursors.

There are some reasons not to expand everything out to recursors and then compile those. One reason I know of is that since Lean has strict evaluation semantics, there are things that can evaluate you didn't expect to evaluate. However, there are plans to get the code generator to know how to compile recursors. It's just not been a priority, as I understand.

Does this mean that pattern matching expressions are compiled directly to executable code, without going through recursors? Does casesOn use pattern matching under the hood and that is why it works where rec fails?

[Kuba]

It looks like sticking with the definition of compose_part that uses pattern matching might be a better option then.
But this brings me back to the question of how to prove my little toy theorem, without using tactics. Is there a general way of writing term style theorem proofs that involve functions defined using pattern matching?

[Kyle Miller]

I'm not sure why casesOn compiles, but I'd guess there's special support for it.

[Kyle Miller]

Here:

theorem theorem1 (f : β → Option γ) (g : α → Option β) (x : α) (h : g x = none) :
    compose_part f g x = none :=
  show (match g x with | none => none | some b => f b) = none from
    h ▸ rfl

[Kyle Miller]

I'm not sure if there's a good way to unfold the definition of compose_part without tactics.

[Kyle Miller]

But the idea is that once you rewrite g x = none the equality is true by definition of match.

[Mario Carneiro]

in term mode you can unfold things by using show and asserting the unfolded expression

[Mario Carneiro]

Kyle Miller said:

I'm not sure why casesOn compiles, but I'd guess there's special support for it.

Yes

[Mario Carneiro]

The same support could in principle exist for rec, it just hasn't been done yet

[Kyle Miller]

Mario Carneiro said:

in term mode you can unfold things by using show and asserting the unfolded expression

Right, that's what I did, but you can't use any placeholder tricks to avoid stating the whole definition

[Mario Carneiro]

theorem theorem1 (f : β → Option γ) (g : α → Option β) (x : α) (h : g x = none) :
    compose_part f g x = none :=
  show (g x).casesOn _ _ = none from h ▸ rfl

[Mario Carneiro]

theorem theorem1 (f : β → Option γ) (g : α → Option β) (x : α) (h : g x = none) :
    compose_part f g x = none :=
  congrArg (Option.casesOn · ..) h

[Kuba]

Mario Carneiro said:

theorem theorem1 (f : β → Option γ) (g : α → Option β) (x : α) (h : g x = none) :
    compose_part f g x = none :=
  show (g x).casesOn _ _ = none from h ▸ rfl

Hmm, I tried this, the exact code being:

def compose_part.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (outer : β → Option γ) (inner : α → Option β) (x : α) : Option γ
    :=
    match inner x with
    |   none => none
    |   some y => outer y

theorem theorem1.{u,v,w} {α : Type u} {β : Type v} {γ : Type w}
    (f : β → Option γ) (g : α → Option β) (x : α)
    (h : g x = none) : compose_part f g x = none
    :=
    show (g x).casesOn _ _ = none from h ▸ rfl

But I get the following message:

type mismatch
  h ▸ rfl
has type
  Option.casesOn (g x) (?m.3242 f g x h) (?m.3243 f g x h) =
    Option.casesOn (g x) (?m.3242 f g x h) (?m.3243 f g x h) : Prop
but is expected to have type
  Option.casesOn (g x) (?m.3242 f g x h) (?m.3243 f g x h) = none : Prop