forcing evaluation

Stream: general

[Kris Brown]

I want to write examples to document the behavior of functions I write. I don't want to have to write proofs, rather just enforce that the output matches the expected string. When things get 'complicated enough' I cannot prove that a to_string method yields a particular string via refl. E.g.

inductive A | a : A
def ts_a (a:A) : string := to_string 0
instance: has_to_string A := ⟨ts_a⟩
#eval to_string a -- "0"...as expected
example: to_string (0,0) = "(0, 0)" := by refl -- works
example: to_string a ="0" := by refl -- doesn't work

Is there anything at the term level that forces evaluation?

[Bryan Gin-ge Chen]

Hmm, they both work for me if I add open A after inductive A.

[Bryan Gin-ge Chen]

(without open A, neither of them work...)

[Kris Brown]

hm I have open A in my machine (forgot to paste it into zulip)

[Bryan Gin-ge Chen]

This is my full file:

inductive A | a : A
open A
def ts_a (a:A) : string := to_string 0
instance: has_to_string A := ⟨ts_a⟩
#eval to_string a -- "0"...as expected
example: to_string (0,0) = "(0, 0)" := rfl
example: to_string a ="0" := rfl

I'm using Lean 3.17.1, though I don't think the version should matter...

[Bryan Gin-ge Chen]

Oh, I changed the by refls to rfls when I was messing around, but it works either way.

[Bryan Gin-ge Chen]

What's the full error you're seeing for the one that doesn't work?

[Kris Brown]

I'm using 3.16.5

Error is "invalid apply tactic, failed to unify to_string a = "a" with ?m_2 = ?m_2

[Kris Brown]

oh oops, I had changed the value from "0" to "a" at some point.

But the problem is still real for more complicated things - I was just trying to come up with a minimal example on the fly.

[Kris Brown]

Let me try to dig up a not-too-big one

[Bryan Gin-ge Chen]

I think I know what you're getting at, and I seem to recall someone joking (?) about us needing a norm_string tactic (like norm_num for strings).

[Bryan Gin-ge Chen]

Found it: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deep.20recursion.20with.20append/near/201199589

[Kris Brown]

the ugly example

  import data.list.alist
  abbreviation pairmap (α β: Type*) := alist (λ _: α, Σ _: unit, β)
  def to_pairmap: Π{α β : Type*} [decidable_eq α],
                               list (α × β) → pairmap α β
    | α β d []         := @list.to_alist α d (λ _: α, Σ _: unit, β) []
    | α β d ((a,b)::t) := @alist.insert α (λ _: α, Σ _: unit, β)
                              d a ⟨(), b⟩
                              (@to_pairmap α β d t)
#eval (to_string (alist.lookup "r" (to_pairmap [("x","a")]))) -- none
example: (to_string (alist.lookup "r" (to_pairmap [("x","a")])))="none" := by refl

and the error

/-
invalid apply tactic, failed to unify
  to_string (alist.lookup "r" (to_pairmap [("x", "a")])) = "none"
with
  ?m_2 = ?m_2
state:
⊢ to_string (alist.lookup "r" (to_pairmap [("x", "a")])) = "none"
-/

[Kris Brown]

yeah if there were a way to capture the output of #eval and use it in a meta example that would work

[Bryan Gin-ge Chen]

Depending on what you're aiming for, you could do this:

run_cmd guard $ to_string (alist.lookup "r" (to_pairmap [("x","a")])) = "none"

edit: the do was unnecessary

[Kris Brown]

that works perfectly for this example! I'll have to look up how it works

[Kris Brown]

It would be great to be able to put this inside a function that takes something with has_to_string and a string to test against

[Kris Brown]

though naively trying that I get type of sorry macro is not a sort

[Kris Brown]

I don't know yet if we can define our own macros

[Bryan Gin-ge Chen]

Is this close to what you want?

meta def test_string {α : Type} [has_to_string α] (a : α) (b : string) : tactic unit :=
guard $ to_string a = b

run_cmd test_string (alist.lookup "r" (to_pairmap [("x","a")])) "none"

[Kris Brown]

yes! this is exactly what I need to write a test suite - thank you!

[Mario Carneiro]

There is no need to call to_string for this kind of test

[Mario Carneiro]

you can just guard $ alist.lookup "r" (to_pairmap [("x","a")]) = none