How to reduce a goal

Stream: general

[Giacomo Stevanato]

Hi, newcomer here. I have some experience with Agda, but Lean is pretty new to me. I'm exploring the language, and to start I tried formalizing some of the arguments I was studying recently, which among other things involve possibly infinite sequences. I tried the Stream'.Seq type, though I was not very satisfied, so I tried to write my own, also as a way to better understand how the language works.

I thus wrote this simplified Sequence type:

structure Sequence (α : Type) where
  get : Nat → Option α
  seq : ∀ n, get n = none → get (n + 1) = none

and I wanted to extend it with a Sequence.iterate function, similar to Stream'.iterate (which doesn't seem to exist for Stream'.Seq)

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  let rec get
  | 0 => some a
  | n + 1 => match (get n) with
    | some x => f x
    | none => none
  let seq n e := sorry;
  Sequence.mk get seq

I'm however stuck at proving seq. The goal is get (n + 1) = none but I would expect this to automatically reduce using the definition of get to something like:

(match (get n) with
  | some x => f x
  | none => none
  ) = none

Then I would rewrite using the equality e (of type get n = none) and after a final reduction I would expect a goal of type none = none, which should be trivially solvable with rfl.

However I cannot get the goal to perform the first reduction. None simp, unfold get, unfold_let, whnf or reduce` seem to reduce the goal.

(Also, bonus points if this is doable without tactics. They feel very much magic and at least initially I would like to understand how to do things manually, and let tactics do the work only after I've understood what that work is)

For comparison, this is what I would write in Agda:

open import Agda.Builtin.Equality
open import Agda.Builtin.Maybe
open import Agda.Builtin.Nat

record Sequence {a} (T : Set a) : Set a where
  field
    get : Nat → Maybe T
    seq : (n : Nat) → get n ≡ nothing → get (suc n) ≡ nothing

iterate : ∀ {a} {T : Set a} → T → (T → Maybe T) → Sequence T
iterate {_} {T} x f = record { get = get; seq = seq }
  where
  get : Nat → Maybe T
  get zero = just x
  get (suc n) with get n
  ... | nothing = nothing
  ... | just y  = f y
  seq : (n : Nat) → get n ≡ nothing → get (suc n) ≡ nothing
  seq n e rewrite e = refl

[Kim Morrison]

(It's super helpful when asking questions to post a #mwe, i.e. a single chunk of code that people can copy and paste, or open in the live sandbox.)

[Giacomo Stevanato]

The first two snippets together make up a mwe. In hindsight I should have put them in the same code block. For convenience I will repost them here together so they're simplier to copy-paste or open in the live sandbox. I've also added an import Mathlib, which seems to be needed to use some tactics like whnf and reduce.

import Mathlib

structure Sequence (α : Type) where
  get : Nat → Option α
  seq : ∀ n, get n = none → get (n + 1) = none

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  let rec get
  | 0 => some a
  | n + 1 => match (get n) with
    | some x => f x
    | none => none
  let seq n e := sorry;
  Sequence.mk get seq

[Kim Morrison]

I feel your pain. An intermediate definition solves the problem:

structure Sequence (α : Type) where
  get : Nat → Option α
  seq : ∀ n, get n = none → get (n + 1) = none

def Sequence.iterate_get (a : α) (f : α → Option α) : Nat → Option α
  | 0 => some a
  | n + 1 => match (iterate_get a f n) with
    | some x => f x
    | none => none

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk (iterate_get a f) (fun n h => by simp_all [iterate_get])

[Kim Morrison]

but I'm sad I can't find any way to unfold the let rec (or using a where clause...)

[Giacomo Stevanato]

I see. Is there an explanation somewhere of why this makes a difference?

[Kim Morrison]

If there is I am looking forward to reading it as well! :-)

[Giacomo Stevanato]

Now onto unraveling what simp_all is doing. Using set_option trace.Meta.Tactic.simp true I saw that it's using iterate_get.eq_def to reduce the call to iterate_get to its body. There doesn't seem to be a way to get the equivalent for a let rec binding or a where closure however, maybe that's why it didn't work? Using iterate_get.eq_def I also managed to write this without tactics:

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => Eq.trans
      (iterate_get.eq_def a f (n + 1))
      (Eq.substr (p := fun x => (match x with | some x => f x | none => none) = none) h rfl))

Actually, nevermind, iterate_get.eq_def doesn't seem to be necessary, as this work too, which is a bit confusing:

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => Eq.substr (p := fun x => (match x with | some x => f x | none => none) = none) h rfl)

Now, in Agda I would use dependent pattern matching instead of Eq.substr. Using dependent pattern matching with iterate_get.eq_def seems to work, as it reduces the goal (check the goal at the sorry):

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => match (generalizing := true) iterate_get a f (n + 1), iterate_get.eq_def a f (n + 1) with
      | _, rfl => sorry)

However further trying to use dependent pattern matching with h doesn't seem to work (check the goal at sorry, it's still the same as before; not even the lhs of h has been generalized)

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => match (generalizing := true) iterate_get a f (n + 1), iterate_get.eq_def a f (n + 1) with
      | _, rfl => match (generalizing := true) iterate_get a f n, h with
        | x, rfl => sorry)

Am I mistaking how match (generalizing := true) works?

(Edit: I should mention that all of these snippets are to be used in place of your definition of Sequence.iterate)

[Giacomo Stevanato]

Giacomo Stevanato said:

There doesn't seem to be a way to get the equivalent for a let rec binding or a where closure however, maybe that's why it didn't work?

Actually, looks like there is an equivalent, but it becomes defined only after the def is concluded (however I need it inside the def!)

[Giacomo Stevanato]

Giacomo Stevanato said:

However further trying to use dependent pattern matching with h doesn't seem to work (check the goal at sorry, it's still the same as before; not even the lhs of h has been generalized)

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => match (generalizing := true) iterate_get a f (n + 1), iterate_get.eq_def a f (n + 1) with
      | _, rfl => match (generalizing := true) iterate_get a f n, h with
        | x, rfl => sorry)

Am I mistaking how match (generalizing := true) works?

I found out there is a more specific iterate_get.eq_2 that also simplifies the match. This, combined with reversing the order of the matches, fixes the issue.

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk
    (iterate_get a f)
    (fun n h => match iterate_get a f n, h, iterate_get a f (n + 1), iterate_get.eq_2 a f n with
      | _, rfl, _, rfl => rfl)

It's not that visually pleasing, but I guess it's as simple as this can get.

[Giacomo Stevanato]

Update: I'm trying to prove some properties of this Sequence type, particular the relation between elements when created using the iterate function. It's mostly fine except one step where I need to simplify { get := x, seq := y }.get into just x. simp works but set_option trace.Meta.Tactic.simp true doesn't tell me what it's doing. I would expect this to be Sequence.get.eq_def, but that actually proves that s.get = s.1, which seems useless. Moreover I see I can prove { get := x, seq := y }.get (called Sequence.get.eq_def' in the MWE) by just using rfl (no tactics needed!), but I don't understand how to do this without an additional binding.

MWE:

structure Sequence (α : Type) where
  get : Nat → Option α
  seq : ∀ n, get n = none → get (n + 1) = none

def Sequence.iterate.get (a : α) (f : α → Option α)
  | 0 => some a
  | n + 1 => (iterate.get a f n).bind f

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α :=
  Sequence.mk (iterate.get a f) (fun _ h => by rw [iterate.get, h, Option.bind])

def Sequence.get.eq_def' {get seq} : { get, seq : Sequence α }.get = get := rfl

def Sequence.succ_iterate (a : α) (f : α → Option α)
  : (iterate a f).get (n + 1) = ((iterate a f).get n).bind f
  := by rw [iterate, Sequence.get.eq_def', Sequence.iterate.get]

[Kyle Miller]

Kim Morrison said:

but I'm sad I can't find any way to unfold the let rec (or using a where clause...)

Yeah, it'd be nice if this worked. My understanding is that let rec is a shorthand for creating a mutual block, setting up a mutual recursion, and in any recursion you can't unfold the definition(s) being defined. The where clause is a macro for a let rec by the way.

It would be nice if somehow there were a way to detect whether a definition in a let rec could be defined outside the mutual block, letting you unfold it.

[Kyle Miller]

@Giacomo Stevanato I'm not sure what your current question is. Are you wanting to avoid simp for some reason? This looks fine to me:

structure Sequence (α : Type) where
  get : Nat → Option α
  seq : ∀ n, get n = none → get (n + 1) = none

def Sequence.iterate.get (a : α) (f : α → Option α) : Nat → Option α
  | 0 => some a
  | n + 1 => (iterate.get a f n).bind f

def Sequence.iterate (a : α) (f : α → Option α) : Sequence α where
  get := iterate.get a f
  seq _ h := by simp [iterate.get, h]

def Sequence.succ_iterate (a : α) (f : α → Option α) :
    (iterate a f).get (n + 1) = ((iterate a f).get n).bind f := by
  simp [iterate, iterate.get]

[Kyle Miller]

It's mostly fine except one step where I need to simplify { get := x, seq := y }.get into just x. simp works but set_option trace.Meta.Tactic.simp true doesn't tell me what it's doing.

This { get, seq : Sequence α }.get = get reduction is built in to simp/dsimp. There are a number of basic reductions these tactics will do, and you can take a look at docs#Lean.Meta.Simp.Config to see most of them.

If you want to only do these reductions without any rewriting, you can do dsimp only.

[Kyle Miller]

For example here's configuring dsimp to only do projection reduction.

def Sequence.succ_iterate (a : α) (f : α → Option α) :
    (iterate a f).get (n + 1) = ((iterate a f).get n).bind f := by
  rw [iterate]
  dsimp (config := {Lean.Meta.Simp.neutralConfig with proj := true}) only
  rw [iterate.get]

It's not normal to configure dsimp in this way, so don't be alarmed by how complicated this might seem! More often, but still rare, is something like dsimp (config := {zeta := false}) only to prevent reducing let expressions.

[Giacomo Stevanato]

Kyle Miller said:

Are you wanting to avoid simp for some reason?

In the long run I will probably be fine with using simp, but at least initially I would like to avoid it in favour of doing things manually, in order to understand what's going on under the hood.

[Giacomo Stevanato]

Kyle Miller said:

It's mostly fine except one step where I need to simplify { get := x, seq := y }.get into just x. simp works but set_option trace.Meta.Tactic.simp true doesn't tell me what it's doing.

This { get, seq : Sequence α }.get = get reduction is built in to simp/dsimp. There are a number of basic reductions these tactics will do, and you can take a look at docs#Lean.Meta.Simp.Config to see most of them.

If you want to only do these reductions without any rewriting, you can do dsimp only.

If this is built into the tactic then how does it work when I "force" it with a separate definition? I'm not using any tactic there.

[Daniel Weber]

rfl works because the two sides are defeq. I'm not sure exactly how that works, but you can probably trace it

[Kyle Miller]

If this is built into the tactic then how does it work when I "force" it with a separate definition? I'm not using any tactic there.

The simp/dsimp tactics are pretty much doing the same thing. They have code that can reduce e to e' using some rules, and then in the proof term they make use of the fact that rfl : e = e' (you might see @id e' p, where p : e, to change the type of the proof p). That is to say, they know that e and e' are defeq, so they can replace e with e' without changing whether the expression is type correct.

[Kyle Miller]

Something you can do yourself is use the change tactic to replace the goal with something that's defeq.

The convenience of dsimp is that it computes what the new goal should be and does change for you.

[Giacomo Stevanato]

Kyle Miller said:

If this is built into the tactic then how does it work when I "force" it with a separate definition? I'm not using any tactic there.

The simp/dsimp tactics are pretty much doing the same thing. They have code that can reduce e to e' using some rules, and then in the proof term they make use of the fact that rfl : e = e' (you might see @id e' p, where p : e, to change the type of the proof p). That is to say, they know that e and e' are defeq, so they can replace e with e' without changing whether the expression is type correct.

Let me see if I properly understood. The compiler will automatically use definitional equality to convert between terms but only when "prompted" somehow (for example when unifying, e.g. what happened in the Sequence.get.eq_def' above), meaning it won't happen if I'm just trying to do a plain rewriting. Then what simp/dsimp do is to automatically find when such conversions are needed (i.e. when some e' is needed but an e is present, and they are definitionally equal) and behave as if a rewrite by rfl : e = e' was used.

Moreover the automatically generated x.eq_def are basically just a definitions of type e = e' with e and e' definitionally equal and rfl as body.

One thing I'm missing is how to trace this behaviour of simp/dsimp. Using set_option trace.Meta.Tactic.simp true doesn't seem to show when definitional equality is used (it will show unification attemps with the already simplified term according to definition equality).

Kyle Miller said:

you might see @id e' p, where p : e, to change the type of the proof p

Where would I see this?

[Giacomo Stevanato]

Giacomo Stevanato said:

Kyle Miller said:

you might see @id e' p, where p : e, to change the type of the proof p

Where would I see this?

Oh nevermind, I see the environment can show the expanded term after tactics are applied.