Injective Constructor As Parameter

Stream: new members

[Zach]

Hello! I'm just learning Lean 4 and I'm curious if it can solve a problem that I never found a way to address when I experimented with Rocq a while ago. I have a theorem I would like to generalize among a certain set of inductive type constructors, but the theorem relies upon knowing that my parameter is one of the constructors of the type (and not just any function producing that type). Here's a MWE in which I show a simple theorem about a small step function over a tiny arithmetic language:

inductive Expr : Type where
  | eerr : Expr
  | enat : Nat → Expr
  | eplus : Expr → Expr → Expr
  | etimes : Expr → Expr → Expr

def step (e : Expr) : Option Expr :=
  match e with
  | .eerr => none
  | .enat _ => none
  | .eplus (.enat n1) (.enat n2) => Expr.enat (n1 + n2)
  | .eplus (.enat n1) e2 => Option.map (.eplus (.enat n1)) (step e2)
  | .eplus e1 e2 => Option.map (fun e1' => .eplus e1' e2) (step e1)
  | .etimes (.enat n1) (.enat n2) => Expr.enat (n1 * n2)
  | .etimes (.enat n1) e2 => Option.map (.etimes (.enat n1)) (step e2)
  | .etimes e1 e2 => Option.map (fun e1' => .etimes e1' e2) (step e1)

theorem step_eplus_left_context :
  ∀ (e1 e1' e2 : Expr),
  (step e1 = some e1') → step (.eplus e1 e2) = some (.eplus e1' e2) := by
  intro e1 e1' e2 Hstep
  cases e1
  . unfold step at Hstep
    contradiction
  . unfold step at Hstep
    contradiction
  . unfold step
    unfold Option.map
    rewrite [ Hstep ]
    simp
  . unfold step
    unfold Option.map
    rewrite [ Hstep ]
    simp

Here, I would like to generalize step_eplus_left_context so I don't have to rewrite the exact same text again for step_etimes_left_context, but I don't know if it's possible for me to introduce a parameter which is known to be one of the constructors of Expr. I could address this by copying and pasting the above theorem and changing the constructor names in the type signature, but that feels silly.

If that's truly what's necessary, I wouldn't be above metaprogramming as a solution. But while Lean 4 has metaprogramming facilities, they don't seem to be geared toward this sort of template-based code stamping.

Any suggestions are welcome! Thanks for reading. :)

[Kyle Miller]

Functional induction principles at least help make the proofs be one-liners:

theorem step_eplus_left_context (e1 e1' e2 : Expr) (hStep : step e1 = some e1') :
    step (.eplus e1 e2) = some (.eplus e1' e2) := by
  fun_induction step e1 <;> simp_all [step]

[Kyle Miller]

It's not so bad proving these and even going on to create an inductive prop version of step and showing step e = some e' ↔ Step e e':

inductive Expr : Type where
  | eerr : Expr
  | enat : Nat → Expr
  | eplus : Expr → Expr → Expr
  | etimes : Expr → Expr → Expr

def step (e : Expr) : Option Expr :=
  match e with
  | .eerr => none
  | .enat _ => none
  | .eplus (.enat n1) (.enat n2) => Expr.enat (n1 + n2)
  | .eplus (.enat n1) e2 => Option.map (.eplus (.enat n1)) (step e2)
  | .eplus e1 e2 => Option.map (fun e1' => .eplus e1' e2) (step e1)
  | .etimes (.enat n1) (.enat n2) => Expr.enat (n1 * n2)
  | .etimes (.enat n1) e2 => Option.map (.etimes (.enat n1)) (step e2)
  | .etimes e1 e2 => Option.map (fun e1' => .etimes e1' e2) (step e1)

@[simp]
theorem step_eplus_left (e1 e1' e2 : Expr) (hStep : step e1 = some e1') :
    step (.eplus e1 e2) = some (.eplus e1' e2) := by
  fun_induction step e1 <;> simp_all [step]

@[simp]
theorem step_eplus_right (n1 : Nat) (e2 e2' : Expr) (hStep : step e2 = some e2') :
    step (.eplus (.enat n1) e2) = some (.eplus (.enat n1) e2') := by
  fun_induction step e2 <;> simp_all [step]

@[simp]
theorem step_etimes_left (e1 e1' e2 : Expr) (hStep : step e1 = some e1') :
    step (.etimes e1 e2) = some (.etimes e1' e2) := by
  fun_induction step e1 <;> simp_all [step]

@[simp]
theorem step_etimes_right (n1 : Nat) (e2 e2' : Expr) (hStep : step e2 = some e2') :
    step (.etimes (.enat n1) e2) = some (.etimes (.enat n1) e2') := by
  fun_induction step e2 <;> simp_all [step]

inductive Step : Expr → Expr → Prop
  | plus_enat (n1 n2 : Nat) :
    Step (.eplus (.enat n1) (.enat n2)) (.enat (n1 + n2))
  | plus_enat_congr_right (n1 : Nat) {e2 e2' : Expr} (he : Step e2 e2') :
    Step (.eplus (.enat n1) e2) (.eplus (.enat n1) e2')
  | plus_congr_left {e1 e1' e2 : Expr} (he : Step e1 e1') :
    Step (.eplus e1 e2) (.eplus e1' e2)
  | times_enat (n1 n2 : Nat) :
    Step (.etimes (.enat n1) (.enat n2)) (.enat (n1 * n2))
  | times_enat_congr_right (n1 : Nat) {e2 e2' : Expr} (he : Step e2 e2') :
    Step (.etimes (.enat n1) e2) (.etimes (.enat n1) e2')
  | times_congr_left {e1 e1' e2 : Expr} (he : Step e1 e1') :
    Step (.etimes e1 e2) (.etimes e1' e2)

theorem step_eq_some_iff {e e' : Expr} :
    step e = some e' ↔ Step e e' := by
  constructor
  · fun_induction step e generalizing e'
    all_goals simp <;> intros <;> subst_vars <;> constructor <;> (try solve_by_elim)
  · intro h
    induction h <;> simp [*, step]

[Zach]

Thanks! I clearly need to go learn about functional induction. :) I'm inferring from your post, though, that there isn't really a way to put a constructor for a particular data type into a variable in a way that would allow me to generalize these theorems. This isn't surprising — I think I encountered the same issue in Rocq — but it's good to know.

I appreciate the help! :)

ETA: There's a lot of good stuff here for a novice like me to learn from. As much as reading the manual has helped, examples like this are delightfully useful. Thanks again! :)

[Kyle Miller]

Zach said:

they don't seem to be geared toward this sort of template-based code stamping.

Why not? Lean 4 has a macro facility that operates on syntax.

import Lean

inductive Expr : Type where
  | eerr : Expr
  | enat : Nat → Expr
  | eplus : Expr → Expr → Expr
  | etimes : Expr → Expr → Expr

def step (e : Expr) : Option Expr :=
  match e with
  | .eerr => none
  | .enat _ => none
  | .eplus (.enat n1) (.enat n2) => Expr.enat (n1 + n2)
  | .eplus (.enat n1) e2 => Option.map (.eplus (.enat n1)) (step e2)
  | .eplus e1 e2 => Option.map (fun e1' => .eplus e1' e2) (step e1)
  | .etimes (.enat n1) (.enat n2) => Expr.enat (n1 * n2)
  | .etimes (.enat n1) e2 => Option.map (.etimes (.enat n1)) (step e2)
  | .etimes e1 e2 => Option.map (fun e1' => .etimes e1' e2) (step e1)

open Lean in
macro "theorem_step " declName:ident es:ident* " => " t:term : command => do
  let mut binders : TSyntaxArray ``Parser.Term.bracketedBinder := #[]
  let mut es' : TSyntaxArray `ident := #[]
  let mut t' : Syntax := t
  for e in es do
    let e' := mkIdentFrom e (← Macro.addMacroScope (e.getId.appendIndexAfter 1))
    es' := es'.push e'
    -- using `_root_.Expr` since otherwise it is ambiguous, as there's also `Lean.Expr`.
    binders := binders.push <| ← `(bracketedBinder| ($e $e' : _root_.Expr))
    binders := binders.push <| ← `(bracketedBinder| (_ : step $e = some $e'))
    t' := t'.rewriteBottomUp fun s => if s == e then e' else s
  `(
    set_option autoImplicit true in
    theorem $declName $binders* : step $t = some $(⟨t'⟩):term := by
      fun_induction step <;> simp_all [step]
  )

theorem_step step_eplus_left e1 => .eplus e1 e2
#check step_eplus_left
-- step_eplus_left {e2 : Expr} (e1 e1_1✝ : Expr) :
--   step e1 = some e1_1✝ → step (e1.eplus e2) = some (e1_1✝.eplus e2)

theorem_step step_eplus_right e2 => .eplus (.enat n1) e2
#check step_eplus_right
-- step_eplus_right {n1 : Nat} (e2 e2_1✝ : Expr) :
--   step e2 = some e2_1✝ → step ((Expr.enat n1).eplus e2) = some ((Expr.enat n1).eplus e2_1✝)

[Kyle Miller]

I'm not sure I'd recommend macros to save writing a few lemmas though. It's easier to maintain some concrete lemmas than to try to get a macro to work in some new unforeseen cases.

[Zach]

I'm not sure I'd recommend macros to save writing a few lemmas though. It's easier to maintain some concrete lemmas than to try to get a macro to work in some new unforeseen cases.

I agree entirely. I was imagining something with much simpler quasiquoting and antiquoting like

macro step_theorem_left txt :=
  let cname = "." + txt in
  let tname = "step_" + txt + "_left_context" in
  [|
  theorem {|tname|} :
    ∀ (e1 e1' e2 : Expr),
    (step e1 = some e1') → step ({|cname|} e1 e2) = some ({|cname|} e1' e2) := by
    intro e1 e1' e2 Hstep
    cases e1
    . unfold step at Hstep
      contradiction
    . unfold step at Hstep
      contradiction
    . unfold step
      unfold Option.map
      rewrite [ Hstep ]
      simp
    . unfold step
      unfold Option.map
      rewrite [ Hstep ]
      simp
  |]

{| step_theorem_left "eplus" |}
{| step_theorem_left "eminus" |}
...

I can see how the actual Lean macro framework supports variable hygiene and other nice features for sophisticated cases. In the case I have above, I'm basically asking for something to do string substitution for me. But better yet is to be able to write the proofs as tersely as you have so I don't feel the need. :)

[Kyle Miller]

You should take a careful look at the code I wrote — it's just doing quasiquoting and antiquoting. I've just got some extra stuff to make some of the construction dynamic, but it's all pretty much quasiquotation. The only non-quasiquotation part is when I construct t' (the RHS of the theorem).

[Kyle Miller]

With Macro.addMacroScope you should just think "gensym"

[Zach]

You should take a careful look at the code I wrote

Will do! I appreciate your pointing this out; it took me the extra look to follow what was going on here. :) Thanks again for all the help!