search

leanprover / fp-lean

Functional Programming in Lean
Other
71 stars 20 forks source link

Ch 8.3 example 2 error #167

Open rongcuid opened 3 weeks ago

rongcuid commented 3 weeks ago

Please quote the text that is incorrect:

open Query in
def example2 :=
  let mountain := table mountainDiary |>.prefixWith "mountain"
  let waterfall := table waterfallDiary |>.prefixWith "waterfall"
  mountain.product waterfall (by simp)
    |>.select (.eq (c! "mountain.location") (c! "waterfall.location"))
    |>.project [⟨"mountain.name", .string⟩, ⟨"waterfall.name", .string⟩] (by repeat constructor)

In what way is this incorrect?

Lean (4.12.0) cannot prove disjoint just by simp. I needed rfl as well:

open Query in
def example2 :=
  let mountain := table mountainDiary |>.prefixWith "mountain"
  let waterfall := table waterfallDiary |>.prefixWith "waterfall"
  mountain.product waterfall (by simp; rfl) -- <-
    |>.select (.eq (c! "mountain.location") (c! "waterfall.location"))
    |>.project [⟨"mountain.name", .string⟩, ⟨"waterfall.name", .string⟩] (by repeat constructor)
rongcuid commented 3 weeks ago

Probably #137