Arguments with infinite sets and decidability

Stream: new members

[Alfie Richards]

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:

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

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.
Thanks

[Anne Baanen]

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]

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:

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

[Alfie Richards]

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

[Alfie Richards]

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]

src/topology/ contains boatloads of topology :wink:

[Alfie Richards]

Thank you!

[Alfie Richards]

Is that in the lean3 GitHub repo?

[Martin Dvořák]

Alfie Richards said:

Is that in the lean3 GitHub repo?

https://github.com/leanprover-community/mathlib/tree/master/src/topology

[Eric Wieser]

For finite sets you can use docs#finset.cons_induction

[Alfie Richards]

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]

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

[Eric Wieser]

Or coe '' coe s

[Alfie Richards]

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]

Alfie Richards said:

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

docs#finset.inf should work

[Eric Wieser]

Did library_search find anything?

[Alfie Richards]

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]

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

[Alfie Richards]

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

[Eric Wieser]

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

[Yaël Dillies]

docs#set.finite.powerset

[Yaël Dillies]

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

[Alfie Richards]

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 :=
begin
  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,
end

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]

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

[Yaël Dillies]

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

[Alfie Richards]

Thank you so much for your help

[Eric Wieser]

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

[Yaël Dillies]

Can you search through PR-less branches as well?

[Eric Wieser]

That's what the above does

[Eric Wieser]

Maybe it's in a branch you never pushed?

[Eric Wieser]

In which case you need to run that on your machine

[Yaël Dillies]

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

[Eric Wieser]

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

lemma set.finite.powerset {α} {s : set α} (h : s.finite) : (𝒫 s).finite :=
begin
  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,
  classical,
  refine ⟨s'.filter (∈ x), _⟩,
  rwa [finset.coe_filter, set.sep_mem_eq, set.inter_eq_right_iff_subset],
end

[Eric Wieser]

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

[Yaël Dillies]

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 :=
begin
  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

end finset

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

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

end set

[Alfie Richards]

Thank you both thats great