lambda_ite

Stream: Is there code for X?

[Joachim Breitner]

We have theorems like docs#apply_ite and docs#ite_apply. Are we missing something for pushing a lambda inside the branches of an ite? I.e. to do the following rewrite without using split?

example (c : Bool) (t e : Nat → Prop):
   (fun x => ite c (t x) (e x)) = (ite c (fun x => t x) (fun x => e x)) := by
  split <;> simp

Or does that somehow follow from the existing ite lemmas?

Can we maybe even write a single apply_ite-like lemma that can push an arbitrary context inside the branches, even if it binds one or more variables (assuming these variables do not appear in the condition)?

(Somehow I feel like I have a knot in my head)

[Martin Dvořák]

I am not aware of any existing lemma that does that.
BTW, a small refactoring:

example (c : Bool) (t e : Nat → Prop):
   (fun x => ite c (t x) (e x)) = ite c t e := by
  split <;> rfl

[Yaël Dillies]

Joachim Breitner said:

Can we maybe even write a single apply_ite-like lemma that can push an arbitrary context inside the branches, even if it binds one or more variables (assuming these variables do not appear in the condition)?

I've been wanting a pair norm_ite/push_ite of tactics for a while now

[Joachim Breitner]

These tactics may come out of https://github.com/leanprover/lean4/pull/5923 (for these purposes I’d argue it makes sense to treat ite like a match statement.

[Joachim Breitner]

Ok, I can answer my own question: The rewrite that I wanted does follow from ite_apply:

example (c : Prop) [Decidable c] (t e : Nat → Prop):
   (fun x => ite c (t x) (e x)) = (ite c (fun x => t x) (fun x => e x)) :=
  funext (fun x => (ite_apply c t e x).symm)

(A more detailed proof would do the appropriate eta-expansion and contraction, but lean does figure that out.)

---

In fact, the apply_ite theorem is sufficient to infer the other ones:

import Mathlib

universe u v
variable {α : Sort u} {β : Sort v}

axiom m : (t e : α) → α
axiom apply_m (f : α → β) (t e : α) : f (m t e) = m (f t) (f e)

theorem m_apply (t e : α → β) (x : α) : (m t e) x = m (t x) (e x) :=
  apply_m (f := (· x)) t e

theorem lam_f (t e : α → β) : (fun x => m (t x) (e x)) = m t e :=
  funext (fun x => (m_apply t e x).symm)

This means that every operation (ite, match-statements) that admit an apply_foo lemma can be lifted out of (at least non-dependent) contexts with a suitable tactic. I guess this is a pretty good characterization of a “tail-position”, e.g. when recognizing tail-recursive functions (e.g. for lean4#3119).

[Joachim Breitner]

And more interesting lemmas follow just from apply_m:

theorem m_self (e : α) : m e e = e :=
  (apply_m (fun _ => e) () ()).symm

theorem m_split (P : α → Prop) (t e : α) (ht : P t) (he : P e) : P (m t e) := by
  rw [apply_m (f := (P ·))]
  rw [eq_true ht]
  rw [eq_true he]
  rw [m_const]
  trivial

theorem apply_m₂ (t1 e1 : α) (t2 e2 : β) (f : α → β → γ) :
    f (m t1 e1) (m t2 e2) = m (f t1 t2) (f e1 e2) :=
  calc f (m t1 e1) (m t2 e2)
    _ = f (m (PProd.fst ⟨t1,t2⟩) (PProd.fst ⟨e1,e2⟩)) (m (PProd.snd ⟨t1,t2⟩) (PProd.snd ⟨e1,e2⟩)) := rfl
    _ = f (PProd.fst (m ⟨t1,t2⟩ ⟨e1,e2⟩)) (m (PProd.snd ⟨t1,t2⟩) (PProd.snd ⟨e1,e2⟩)) := by rw [← apply_m (f := PProd.fst)]
    _ = f (PProd.fst (m ⟨t1,t2⟩ ⟨e1,e2⟩)) (PProd.snd (m ⟨t1,t2⟩ ⟨e1,e2⟩)) := by rw [← apply_m (f := PProd.snd)]
    _ = m (f t1 t2) (f e1 e2) := apply_m (fun (x : PProd α β) => f x.1 x.2) _ _

[Joachim Breitner]

Especially the last one I wasn’t sure if it was derivable, and find it particularly interesting: This means that if you have multiple instances of the same “match” expressions (that is, same target, but diffferent arms, different motives) in the goal, you can lift them out together and end up having only a single match expression.

[Joachim Breitner]

Oh, even this can be proven purely from apply_m:

theorem m_m (e1 e2 e3 : α) : m (m e1 e2) e3 = m e1 e3 :=
  calc m (m e1 e2) e3
    _ = (fun x => m x e3) (m e1 e2) := rfl
    _ = (fun a b => a b) (fun x => m x e3) (m e1 e2) := rfl
    _ = (fun a b => a b) (m (fun x => x) (fun x => e3)) (m e1 e2) := by rw [lam_m]
    _ = m ((fun a b => a b) (fun x => x) e1) ((fun a b => a b) (fun x => e3) e2) := apply₂_m (fun x => x) (fun x => e3) e1 e2 (fun a b => a b)
    _ = m e1 e3 := rfl

[Daniel Weber]

You can prove

theorem m_val (a b : α) : m a b = if m true false then a else b := by
  simpa using (apply_m (fun x ↦ if x then a else b) true false).symm

i.e. m is either constant left or constant right, so I'd expect this

[Joachim Breitner]

Heh, good point. But I hope all of this generalizes to more complex match statements, with multiple alternatives, bound variables in the alternative etc.

In (maybe) other words: Is apply_m sufficient to prove all the things that in other settings you’d get from parametricity?

[Joachim Breitner]

Right now I’m puzzling about this: From

axiom apply_m (f : α → β) (t e : α) : f (m t e) = m (f t) (f e)

I can derive

theorem apply_m' (f : (α → α → α) → β) : f m = m (f (fun t e => t)) (f (fun t e => e)) := by
  change f (fun t e => m t e) = m (f (fun t e => t)) (f (fun t e => e))
  conv => lhs; arg 1; ext t; apply lam_m
  conv => lhs; arg 1; apply lam_m
  apply apply_m f

but can I also do

theorem apply_m'' (f : (∀ {α}, α → α → α) → β) : f m = m (f (fun t e => t)) (f (fun t e => e)) := by
  sorry

(note the changed argument of f), or should that be the “more basic” axiom for a “match-like function”?

[Joachim Breitner]

Hmm, but even if I had that, I had hoped I could prove theorems like

theorem m_strong_split (P : α → Prop) {t e : α} :
    (ht : (∀ (α : Sort u) (t e : α), m t e = t) → P t) →
    (he : (∀ (α : Sort u) (t e : α), m t e = e) → P e) →
    P (m t e) := by

theorem m_congr (t1 t2 e1 e2 : α)
      (ht : (∀ (α : Sort u) (t e : α), m t e = t) → t1 = t2)
      (he : (∀ (α : Sort u) (t e : α), m t e = e) → e1 = e2) :
      m t1 e1 = m t2 e2 := by

and I almost can, but then the universes get in the way.