Reusing knowledge from a pattern match

Stream: lean4

[Rob Simmons]

Would be happy for guidance on whether this belongs here, in #new members, or elsewhere. It definitely seems like a newbie question coming from over-indexing on Agda experience. Here's what I'm trying:

inductive IN {α: Type} (x : α) : List α -> Type where
  | z {l : List α} : IN x (x :: l)
  | s {y : α} {l : List α} : IN x l -> IN x (y :: l)

inductive OR (A: Type) (B: Type) : Type where
 | inl : A -> OR A B
 | inr : B -> OR A B

inductive EQ {A: Type} : A -> A -> Type where
 | refl {x} : EQ x x

def listeither {α} {x: α} {y: α} {l: List α} (l': List α)
  (p : IN x (l' ++ y :: l))
  : OR (EQ x y) (IN x (l' ++ l)) :=
  match l' with
  | [] => sorry
  | w :: l'' => sorry

In the first pattern match case, my subgoals are

α : Type
x y : α
l l' : List α
p : IN x (l' ++ y :: l)
⊢ OR (EQ x y) (IN x ([] ++ l))

and I'd like the premise p to get rewritten with the knowledge that l' is [] (and therefore (l' ++ y :: l) is (y :: l). (I'm assuming that List.append is defined by induction on the first list.)

[Daniel Selsam]

@Rob Simmons You need to pass (generalizing := true) to the match:

def listeither {α} {x: α} {y: α} {l: List α} (l': List α)
  (p : IN x (l' ++ y :: l))
  : OR (EQ x y) (IN x (l' ++ l)) :=
  match (generalizing := true) l' with
  | [] => sorry
  | w :: l'' => sorry

The first goal is now:

α : Type
x y : α
l l' : List α
p✝ : IN x (l' ++ y :: l)
p : IN x ([] ++ y :: l)
⊢ OR (EQ x y) (IN x ([] ++ l))

Note: generalizing defaults to true when the return type is a Prop. So in your case, you could also just make OR a Prop instead.

[Rob Simmons]

Aah okay that helps... how does one then go about telling Lean to hit ([] ++ l) with some normalization to learn that it's just l?

[Daniel Selsam]

by simp at p

[Rob Simmons]

Hmm, it seems like it's being forgetful.

def listeither {α} {x: α} {y: α} {l: List α} (l': List α)
  (p : IN x (l' ++ y :: l))
  : OR (EQ x y) (IN x (l' ++ l)) :=
  match (generalizing := true) l' with
  | [] => by
    simp at p
    simp
    admit
  | _ :: _ => by admit

goal is back to

α : Type
x y : α
l l' : List α
p : IN x (l' ++ y :: l)
⊢ OR (EQ x y) (IN x (l' ++ l))

like I never performed the pattern match.

[David Renshaw]

Why I try that my goals at the admits are:

α : Type
x y : α
l l' : List α
p : IN x (l' ++ y :: l)
p : IN x (y :: l)
⊢ OR (EQ x y) (IN x l)

and

α : Type
x y : α
l l' : List α
p : IN x (l' ++ y :: l)
x¹ : α
x : List α
p : IN x (x¹ :: x ++ y :: l)
⊢ OR (EQ x y) (IN x (x¹ :: x ++ l))

[Ryan Lahfa]

Is it even possible to prove this in Lean 4?

EQ x y is Type and not Prop, so excluded middle won't work, right? I tried a bit, but byCases / match-em was always failing?

[David Renshaw]

I managed to get it to work:

def listeither {α} {x: α} {y: α} {l: List α} (l': List α)
  (p : IN x (l' ++ y :: l))
  : OR (EQ x y) (IN x (l' ++ l)) :=
  match (generalizing := true) l' with
  | [] => match p with
          | IN.z => OR.inl EQ.refl
          | IN.s h => OR.inr h
  | w :: l'' => by rw [List.cons_append]
                   rw [List.cons_append] at p
                   match p with
                   | IN.z => exact OR.inr IN.z
                   | IN.s h3 => match listeither l'' h3 with
                                | OR.inl he => exact OR.inl he
                                | OR.inr hi => exact OR.inr $ IN.s hi

[Ryan Lahfa]

Right, matching over p makes sense.

[David Renshaw]

The rw [List.cons_append] at p seems to be necessary. Otherwise, matching on p fails.

[David Renshaw]

Ah! If we define our own append function, then we don't need the manual rewrites:

def append' {A: Type} : List A → List A → List A
| [], xs => xs
| h::tl, xs => h::(append' tl xs)

def listeither' {α} {x: α} {y: α} {l: List α} (l': List α)
  (p : IN x (append' l' (y :: l)))
  : OR (EQ x y) (IN x (append' l' l)) :=
  match (generalizing := true) l' with
  | [] => match p with
          | IN.z => OR.inl EQ.refl
          | IN.s h => OR.inr h
  | w :: l'' => match p with
                | IN.z => OR.inr IN.z
                | IN.s h3 => match listeither' l'' h3 with
                                | OR.inl he => OR.inl he
                                | OR.inr hi => OR.inr $ IN.s hi

[David Renshaw]

(This was Jason Reed's idea.)

[David Renshaw]

Apparently, the built-in append does not normalize quite as nicely as append' in this situation. https://github.com/leanprover/lean4/blob/51d26e1172adb6b30936424d806f72e5d07d8cdb/src/Init/Data/List/Basic.lean#L27

[Kevin Buzzard]

Indeed in mathlib4 https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/Basic.lean we define a second append

[Kevin Buzzard]

My understanding is that a lot of the definitions in Lean 4 are optimised for computing and of course this is a really good idea. Lean 4 has already shown that it can compete with the best of them when it comes to formalising mathematics but it's an interesting question to see if it can compete with other functional programming languages for speed, and this means that one has to take things like tail recursion etc into account and give definitions optimised for speed. Then the trick is to make other definitions optimised for proofs, show that they're equivalent to the speedy definitions, and then you have access to the best of both worlds as long as you can transfer proofs along isomorphisms, which can be done with tactics

[Mario Carneiro]

I think that the mathlib definitions of length' and append' should be the official ones, and the tail recursive implementation currently in lean 4 core should be the compiler-facing definition swapped out via implementedBy

[Mario Carneiro]

implementedBy really allows us to solve this issue of having something good for reasoning and also good for execution once and for all

[Mario Carneiro]

It currently has the limitation that it doesn't require or accept a proof of equality of the two functions, which can help to improve confidence in the correctness of the implementation swapping, but I think implementedBy is worth it even without that

[Mario Carneiro]

it's something we can clean up in mathlib anyway, once we get custom attributes