Zulip Chat Archive

Stream: new members

Topic: Arguments with infinite sets and decidability

Alfie Richards (Mar 07 2023 at 17:19):

Hi, Im new here so apologies if I make any faux pas.

I'm currently working on my masters project in Lean 3 and really enjoying it but struggling to make arguments regarding infinite sets and intersections? I think? and was wondering if you guys could help any?
For background I'm encoding logic on language semantics, I have states

def state: Type := string -> 

and expressions

def expression: Type := state -> 

I want to encode the idea of the free variables of the expression (ie. the strings that if they change then the expression changes.
I came up with this encoding

def expression.Free (e: expression): set string :=
  λ x,  σ v, e σ  e (σ{x  v})

ie. the set of strings such that the outcome of the expression with some state will be changed by the value of that string changing. (state{var ↦ val} ) simply maps that variable to the value and every other variable to the states value for that variable.

I want to prove the main characteristic I want free variables to have which is that if they are all the same for 2 states, then the expression evaluated at those states will be the same:

lemma for_all_free_expression {e: expression} {σ σ': state }
  (H:  x  e.Free, σ x = σ' x): e σ = e σ'

Which I believe is a true result, and sort of is the fundamental property I'd like Free to have!

I have so far been unable to make any progress on this as all the arguments I can come up with require reasoning over the set of strings and I don't know how to do that sort of argument in Lean.

For example, one argument I tried is to instead encode the free variables as the intersection of all the sets with the property that if the variables are all the same, then the expressions are the same:

def expression.FreeProp (e: expression): set string  Prop :=
  (λ F,  σ σ': state, ( f: F, σ f = σ' f)  e σ = e σ' )

def expression.Free (e: expression): set string :=
  λ x,  F: set string, expression.FreeProp e F  x  F

I was able to show these two encodings are equivalent and then the problem reduces to showing that the expression.Free has FreeProp! On paper I can make this argument by showing that the intersection of any two sets that satisfy the FreeProp for some e will satisfy FreeProp itself.

lemma expression.FreeProp.intersection {e: expression} {s} {A B: set string}  :
  e.FreeProp A  e.FreeProp B  e.FreeProp (A  B) := ...

Then expanding this for the set of all infinite sets? (Which I am aware is a bit of a shaky argument)
However, for this argument I wanted to construct some intermediate state:

  intros σ₁ σ₃ h,
  have σ₂: state := λ s, if s  A then σ₁ s else σ₃ s,

Which runs into a problem with decidability? I can't seem to find much helpful online.
I keep running into similar problems whichever way I try argue this where decidability and infinite sets.
If anyone could point me in the right direction for this sort of thing? Or let me know if I am barking up the wrong tree.

Anne Baanen (Mar 07 2023 at 17:23):

Welcome to the Zulip chat, congratulations on nicely formatting your first post :)

To start with your last question, you can use the tactic classical before the definition of σ₂ to allow you to arbitrary case distinctions in if.

Anne Baanen (Mar 07 2023 at 17:25):

I would also suggest using let instead of have, since have forgets the body of the definition. So the following (untested) should get you going again:

  intros σ₁ σ₃ h,
  let σ₂: state := λ s, if s  A then σ₁ s else σ₃ s,

Alfie Richards (Mar 07 2023 at 17:32):

Thank you for the welcome! Thats awesome, thank you that's has definitely got me unstuck at least for now!

Alfie Richards (Mar 08 2023 at 11:24):

I've now reached a problem with formulating an argument about infinite intersections.
I have successfully argued for binary intersections:

lemma expression.FreeProp.intersection
  {e: expression} {s: string} {A B: set string}:
  e.FreeProp A  e.FreeProp B  e.FreeProp (A  B) :=

And now want to argue that the infinite intersection of all sets that satisfy this.
Any idea how I could make such an argument? Is there any topology code that I can look at as that that may cover similar arguments?

Johan Commelin (Mar 08 2023 at 11:25):

src/topology/ contains boatloads of topology :wink:

Alfie Richards (Mar 08 2023 at 11:26):

Thank you!

Alfie Richards (Mar 08 2023 at 11:27):

Is that in the lean3 GitHub repo?

Martin Dvořák (Mar 08 2023 at 11:28):

Alfie Richards said:

Is that in the lean3 GitHub repo?


Eric Wieser (Mar 08 2023 at 15:35):

For finite sets you can use docs#finset.cons_induction

Alfie Richards (Mar 11 2023 at 11:53):

Is there an equivalent of set.sInter for finset (finset X) or a way to easily get from a finset (finset X)) to set (set X))?

Eric Wieser (Mar 11 2023 at 11:58):

Something like ↑(s.map ⟨coe, finset.coe_injective⟩) should work

Eric Wieser (Mar 11 2023 at 11:59):

Or coe '' coe s

Alfie Richards (Mar 12 2023 at 22:38):

That worked perfectly thank you, unfortunately I had so many headaches going back and forth between finset and set I decided to use set everywhere and keep around the set.finite hypotheses instead. Im pretty much there except I need to show B.finite → 𝒫B.finite, any ideas?

Eric Wieser (Mar 12 2023 at 22:39):

Alfie Richards said:

Is there an equivalent of set.sInter for finset (finset X)

docs#finset.inf should work

Eric Wieser (Mar 12 2023 at 22:40):

Did library_search find anything?

Alfie Richards (Mar 12 2023 at 22:41):

No, and Ive had a look through the mathlib documentation and soundly find anything along those lines. though its possible I missed it because I find them a bit hard to read

Eric Wieser (Mar 12 2023 at 22:41):

It likely just missing, though should follow trivially from docs#finset.coe_powerset

Alfie Richards (Mar 12 2023 at 22:42):

Ah okay, I'll try make it as a separate lemma, thank you for your help!

Eric Wieser (Mar 12 2023 at 22:45):

docs#set.finite.of_finset and docs#set.finite.exists_finset_coe should do the rest of the work

Yaël Dillies (Mar 13 2023 at 00:18):


Yaël Dillies (Mar 13 2023 at 00:19):

Oh well, I have it in a PR somewhere and it mustn't have been merged yet.

Alfie Richards (Mar 13 2023 at 10:03):

I have wrestled with this a bit but am still having issues with the types.
This is what I have currently

lemma finite_powerset (B: set string) : B.finite  (𝒫 B).finite :=
  intro h,

  have hA := set.finite.exists_finset_coe h,
  cases hA,

  have hB := finset.coe_powerset (hA_w),
  rw hA_h at hB,

  exact set.finite.of_finset (hA_w.powerset) hB,

However, I'm having issues with it wanting to have a finset (set string) rather than finset (finset string).
I did try the map you suggested earlier but it spawned a bunch of other goals that I couldn't solve.
Is there anywhere I can read about coe or what's going on here?

Alfie Richards (Mar 13 2023 at 10:03):

Ooh, could I see the PR? Is it public?

Yaël Dillies (Mar 13 2023 at 10:09):

Yeah, I just need to find it back :sweat_smile:

Alfie Richards (Mar 13 2023 at 10:10):

Thank you so much for your help

Eric Wieser (Mar 13 2023 at 10:11):

git log -S 'lemma powerset' --all ^master --author=Yael only has three results

Yaël Dillies (Mar 13 2023 at 10:11):

Can you search through PR-less branches as well?

Eric Wieser (Mar 13 2023 at 10:12):

That's what the above does

Eric Wieser (Mar 13 2023 at 10:12):

Maybe it's in a branch you never pushed?

Eric Wieser (Mar 13 2023 at 10:12):

In which case you need to run that on your machine

Yaël Dillies (Mar 13 2023 at 10:12):

It's possible it's on another repo. At any rate, it's not too hard to reprove. Give me 5 minutes.

Eric Wieser (Mar 13 2023 at 10:21):

import data.finset.powerset
import data.set.finite

lemma set.finite.powerset {α} {s : set α} (h : s.finite) : (𝒫 s).finite :=
  obtain s', hs' := set.finite.exists_finset_coe h,
  refine set.finite.of_finset (s'.powerset.map _, finset.coe_injective⟩) _,
  simp_rw [finset.mem_coe, set.ext_iff, finset.coe_map, finset.coe_powerset,
    function.embedding.coe_fn_mk, hs', set.image_preimage_eq_iff],
  intros x hx,
  rw set.mem_powerset_iff at hx,
  refine s'.filter ( x), _⟩,
  rwa [finset.coe_filter, set.sep_mem_eq, set.inter_eq_right_iff_subset],

Eric Wieser (Mar 13 2023 at 10:22):

I bet @Yaël Dillies can come up with a shorter one

Yaël Dillies (Mar 13 2023 at 10:37):

The final proof is shorter, but that's because I split off a lemma (analogous to docs#finset.coe_powerset).

import data.finset.powerset
import data.set.finite

namespace finset
variables {α : Type*}

lemma image_coe_coe_powerset (s : finset α) :
  coe '' (s.powerset : set (finset α)) = (s : set α).powerset :=
  ext t,
  simp only [coe_powerset, set.mem_image, set.mem_preimage, set.mem_powerset_iff, coe_subset],
  refine _, λ ht, _⟩,
  { rintro t, hts, rfl⟩,
    exact coe_subset.2 hts },
  { lift t to finset α using s.finite_to_set.subset ht,
    exact t, coe_subset.1 ht, rfl }

end finset

namespace set
variables {α : Type*} {s : set α}

protected lemma finite.powerset (hs : s.finite) : s.powerset.finite :=
  lift s to finset α using hs,
  rw finset.image_coe_coe_powerset,
  exact s.powerset.finite_to_set.image _,

end set

Alfie Richards (Mar 13 2023 at 10:40):

Thank you both thats great

Last updated: Dec 20 2023 at 11:08 UTC