Zulip Chat Archive

Hello lean hivemind :) I am making my first steps after playing the number game and trying to formalise my favorite modal logic. Could someone help me how I could prove something about lfp from order.complete_lattice? (I am also new to zulip, hope this goes into the right place...)

Malvin Gattinger (Jul 06 2021 at 20:12):

Concretely, I am trying to show this which should follow easily from the function ~~being reflexive~~ explicitly mentioning w:

w ∈ lfp (λ (ws : set W), {w} ∪ ws ∪ { v : W | .... extra stuff } )

Malvin Gattinger (Jul 06 2021 at 20:13):

So would I then unfold lfp or is there a theorem like https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html#complete_lattice.le_refl which I could use? And how would I apply it to change my goal?

Kyle Miller (Jul 06 2021 at 20:18):

Maybe you could use docs#lfp_fixed_point

Kyle Miller (Jul 06 2021 at 20:20):

rewriting leftwards, and then it should simp immediately (probably through docs#set.mem_union and docs#set.mem_singleton)

Malvin Gattinger (Jul 06 2021 at 20:27):

Thanks! I feel stupid now: I added "import order.fixed_points" but still get "unknown identifier for lfp_fixed_point". Also, I assume this will need a proof that my function is monotone?

Kyle Miller (Jul 06 2021 at 20:38):

I'm not sure about the error you're seeing without a MWE but, yeah, you would need a monotonicity proof to use the lemma

Malvin Gattinger (Jul 06 2021 at 20:47):

import data.set.lattice
import order.fixed_points

def myFunction : ℕ → set ℕ
| n := lfp (λ ws, ws ∪ { 42 } ∪ { k | k ≤ n } )

lemma myFunctionIncludesN (n : ℕ): n ∈ myFunction n :=
begin
  unfold myFunction,
  rw ← lfp_fixed_point, -- unknown identifier lfp_fixed_point ??
  sorry
end

I guess I am using rw ← wrong here?

Eric Rodriguez (Jul 06 2021 at 20:51):

this works on my computer; do you have the latest mathlib?

Malvin Gattinger (Jul 06 2021 at 20:52):

ohh, good point. I assume for this I should change the commit mentioned in leanpkg.toml?

Eric Rodriguez (Jul 06 2021 at 20:52):

yeah, you can just open the vscode terminal and type leanproject up

Eric Rodriguez (Jul 06 2021 at 20:53):

(also may be good to do leanproject get-mathlib-cache after)

Malvin Gattinger (Jul 06 2021 at 20:54):

ohh, nice. Turns out I was using mathlib from September last year ;)

Kyle Miller (Jul 06 2021 at 20:54):

and this lemma was by @Yaël Dillies two months ago :smile:

Malvin Gattinger (Jul 06 2021 at 20:56):

Eric Rodriguez said:

(also may be good to do leanproject get-mathlib-cache after)

What does this do? And when I run "leanpkg build" in a terminal outside of VS code, does this use a different cache? (And do emacs and vs code share caches?)

Eric Rodriguez (Jul 06 2021 at 20:57):

basically, Lean stores "precompiled" info about files in ".olean" files

Eric Rodriguez (Jul 06 2021 at 20:57):

this gets the oleans for mathlib, leanproject build will make them for your current project (which could also be mathlib!)

Malvin Gattinger (Jul 06 2021 at 21:04):

Thanks! Another stupid question though: from where do I get the leanproject command? I only have elan and leanpkg, and also ~/.elan/toolchains/stable/bin/ has no leanproject :thinking: