FOL logic with unary predicates

Stream: mathlib4

[Yury G. Kudryashov]

Are there effective algorithms to prove statements in FOL if only one-variable predicates are involved? I tried to golf docs4#isPreconnected_closed_iff and after

  rw [IsPreconnected, compl_surjective.forall]
  refine forall_congr' fun u ↦ compl_surjective.forall.trans <| forall_congr' fun v ↦ ?_
  simp only [isOpen_compl_iff]
  refine forall_congr' fun hu ↦ forall_congr' fun hv ↦ ?_

I've got the goal

s ⊆ uᶜ ∪ vᶜ → Set.Nonempty (s ∩ uᶜ) → Set.Nonempty (s ∩ vᶜ) → Set.Nonempty (s ∩ (uᶜ ∩ vᶜ)) ↔
    s ⊆ u ∪ v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))

This is a statement that is true for any three sets s, u, v. It would be nice to have a tactic that closes this goal automatically.

[Yury G. Kudryashov]

I guess, in this case one can reformulate each atom like s ⊆ u ∪ v as a statement about parts of the corresponding Venn diagram being (non)empty, then get a statement in propositional logic.

[Mario Carneiro]

there was a tactic along those lines

[Yury G. Kudryashov]

There was or there is?

[Mario Carneiro]

it was a zulip discussion

[Mario Carneiro]

I forget how far along it actually got, it did not land in mathlib

[Mario Carneiro]

the simple version is to introduce x, simp everything to propositional logic and call tauto

[Yury G. Kudryashov]

What do you mean by "introduce x"?

[Mario Carneiro]

well I guess your goal is more complicated because you have multiple existential quantifiers

[Yury G. Kudryashov]

  simp [subset_def, Set.Nonempty]
  tauto

[Mario Carneiro]

the version that was in the discussion only handled universal quantifiers IIRC

[Mario Carneiro]

for stuff like subset masquerading as implication

[Yury G. Kudryashov]

Leaves many goals like

case mp.inl.h.right.right
α : Type u
β : Type v
ι : Type ?u.23250
π : ι → Type ?u.23255
inst : TopologicalSpace α
s t u v s u v : Set α
hu : IsClosed u
hv : IsClosed v
em : (a : Prop) → Decidable a
h : ¬∀ (x : α), x ∈ s → ¬x ∈ u ∨ ¬x ∈ v
a⁴ : ∀ (x : α), x ∈ s → x ∈ u ∨ x ∈ v
x¹ : α
a³ : x¹ ∈ s
a² : x¹ ∈ u
x : α
a¹ : x ∈ s
a : x ∈ v
⊢ x¹ ∈ v

[Yury G. Kudryashov]

(deleted)

[Mario Carneiro]

yeah I think we need a FOL tactic to prove this

[Mario Carneiro]

if you instantiate the quantifiers manually it can probably be done with the existing tools

[Yury G. Kudryashov]

What means instantiate the quantifiers manually?

[Mario Carneiro]

have := a⁴ _ a¹; have := a⁴ _ a³; tauto

[Mario Carneiro]

something like that

[Yury G. Kudryashov]

(a) my goal is to avoid intervention; (b) those a^k only appear after the call to tauto.

[Mario Carneiro]

(a) yes I'm aware

[Mario Carneiro]

the tactic doesn't exist

[Mario Carneiro]

at least not until the likes of duper make it to mathlib

[Yury G. Kudryashov]

What is duper?

[Yury G. Kudryashov]

Should I open a github issue?

[Mario Carneiro]

https://github.com/leanprover-community/duper, WIP superposition prover in lean 4

[Mario Carneiro]

For FOL proving? This is a long standing issue, we've known about it since the beginning of lean 3

[Yury G. Kudryashov]

No README... Probably, a clear sign of "WIP"

[Mario Carneiro]

making a good FOL prover is really challenging, especially when you mix it with all the higher order stuff in lean

[Yury G. Kudryashov]

Do I understand correctly that FOL with unary predicates is doable, FOL with binary predicates is undecidable? Is it undecidable in practice or there is an algorithm that works for reasonably sized formulas provided that they're true?

[Mario Carneiro]

It's not undecidable in practice, but it is heuristic

[Mario Carneiro]

The success rate depends quite strongly on the complexity of the goal

[Yury G. Kudryashov]

BTW, are there any prover-independent solutions to this? Like an external tool or a C/C++ library that can take an input formula and give you a proof in some machine-readable format?

[Mario Carneiro]

Z3 (leo's project before lean) is an SMT solver (aka FOL plus theories like linear arithmetic)

[Yury G. Kudryashov]

Can we somehow call it (or another similar tool) from Lean 4?

[Mario Carneiro]

there are other SMT solvers as well like vampire (which had an open PR to mathlib for a long time)

[Mario Carneiro]

the other problem with calling such tools is that you often don't get a proof back, just an assertion "it's true"

[Mario Carneiro]

or at least not something which can be externally checked, much less reconstructed into a lean proof

[Mario Carneiro]

many of these properties disqualify them from being used in mathlib proofs

[Yury G. Kudryashov]

Of course, "it's true" is not enough.

[Mario Carneiro]

As for unary predicates... it's plausible to me that this fragment is decidable (at least, assuming the term language isn't too fancy), but I assume you want to include equality, and that's a binary predicate

[Mario Carneiro]

I'm not sure how useful that fragment is in practice

[Yury G. Kudryashov]

In this example I don't need equality.

[Mario Carneiro]

you are using a binary predicate though (actually, probably a 4-ary predicate since lean has implicits everywhere) so writing a tactic that knows what to ignore is quite a tricky part of this goal

[Mario Carneiro]

I think it would be more useful to just have a general FOL instantiation tactic rather than a decision procedure for unary predicate FOL

[Yury G. Kudryashov]

OK, I'll just leave the proof we had.

[Mario Carneiro]

I mean, in this case you can just instantiate all quantifiers at all ground terms and get a proof by propositional logic

[Yury G. Kudryashov]

There are many statements in Topology/Connected that are repeated for open and closed sets

[Yury G. Kudryashov]

And in most cases one can go from one statement to another by something I wrote in the first few lines: replace all open sets by their complements which are closed.

[Mario Carneiro]

the fact that your theorem is not quantified over u and v makes it a lot less obvious to me

[Yury G. Kudryashov]

It is quantified. The first 2 lines get rid of that.

[Mario Carneiro]

I mean that while

(\forall u v, s ⊆ uᶜ ∪ vᶜ → Set.Nonempty (s ∩ uᶜ) → Set.Nonempty (s ∩ vᶜ) → Set.Nonempty (s ∩ (uᶜ ∩ vᶜ))) ↔
(\forall u v, s ⊆ u ∪ v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v)))

looks obviously true to me,

(s ⊆ uᶜ ∪ vᶜ → Set.Nonempty (s ∩ uᶜ) → Set.Nonempty (s ∩ vᶜ) → Set.Nonempty (s ∩ (uᶜ ∩ vᶜ))) ↔
(s ⊆ u ∪ v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v)))

looks a lot harder and possibly false

[Mario Carneiro]

If you were to keep the quantifiers and substitute u |-> uᶜ and v |-> vᶜ then simp could probably do this proof

[Yury G. Kudryashov]

Let me try

[Yury G. Kudryashov]

  rw [IsPreconnected, compl_surjective.forall]
  refine forall_congr' fun u ↦ compl_surjective.forall.trans ?_
  revert u
  simp [subset_def, Set.Nonempty]

fails

[Mario Carneiro]

what's the goal?

[Mario Carneiro]

you don't need to unfold subset_def or Set.Nonempty for this proof

[Yury G. Kudryashov]

⊢ ∀ (u : Set α),
    (∀ (x : Set α),
        IsClosed u →
          IsClosed x →
            (∀ (x_1 : α), x_1 ∈ s → ¬x_1 ∈ u ∨ ¬x_1 ∈ x) →
              ∀ (x_1 : α), x_1 ∈ s → ¬x_1 ∈ u → ∀ (x_2 : α), x_2 ∈ s → ¬x_2 ∈ x → ∃ x_3, x_3 ∈ s ∧ ¬x_3 ∈ u ∧ ¬x_3 ∈ x) ↔
      ∀ (t' : Set α),
        IsClosed u →
          IsClosed t' →
            (∀ (x : α), x ∈ s → x ∈ u ∨ x ∈ t') →
              ∀ (x : α), x ∈ s → x ∈ u → ∀ (x : α), x ∈ s → x ∈ t' → ∃ x, x ∈ s ∧ x ∈ u ∧ x ∈ t'

[Mario Carneiro]

I guess I don't understand what the original goal was and how you want to prove it

[Yury G. Kudryashov]

Here is the original proof from mathlib4:

  ⟨by
      rintro h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩
      rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
      intro h'
      have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
      have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
      have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
      rw [← compl_union] at this
      exact this.ne_empty htt'.disjoint_compl_right.inter_eq,
    by
      rintro h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩
      rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
      intro h'
      have xv : x ∉ v := (h' xs).elim (absurd xu) id
      have yu : y ∉ u := (h' ys).elim id (absurd yv)
      have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩
      rw [← compl_union] at this
      exact this.ne_empty huv.disjoint_compl_right.inter_eq⟩

[Mario Carneiro]

ah yeah that can be golfed

[Mario Carneiro]

and your replacement?

[Yury G. Kudryashov]

The problem is that while the formulas are equivalent (in FOL, after the cleanup I made), it is not "obvious": the terms in the implications do not correspond to each other.

[Yury G. Kudryashov]

The replacement I tried to write starts with

  rw [IsPreconnected, compl_surjective.forall]
  refine forall_congr' fun u ↦ compl_surjective.forall.trans ?_
  simp only [isOpen_compl_iff]

and leaves a goal that is true in FOL.

[Yury G. Kudryashov]

(at least if you unfold definitions of subset and nonempty)

[Mario Carneiro]

what happened to t and t'?

[Mario Carneiro]

from the original theorem

[Yury G. Kudryashov]

I used compl_surjective.forall.trans _ to unify sets in LHS and RHS.

[Yury G. Kudryashov]

As you can see, the original proof calls h with the complements of the available sets.

[Yury G. Kudryashov]

Anyway, this is a low priority question (at least, for me and now). Sorry for taking so much of your time.

[Yury G. Kudryashov]

I mean, there is no theorem I can't prove without it, it's only about hiding technical details of some proofs.

[Mario Carneiro]

Here's my golf of the proof:

  rw [IsPreconnected, compl_surjective.forall]
  let P u u' := s ⊆ u ∪ u' → (s ∩ u).Nonempty → (s ∩ u').Nonempty → (s ∩ (u ∩ u')).Nonempty
  suffices ∀ {u u'}, P u u' → P (uᶜ) (u'ᶜ) by
    refine forall_congr' fun u ↦ compl_surjective.forall.trans ?_
    simp only [isOpen_compl_iff]
    constructor <;> exact fun H v hu hv ↦ by simpa using this (H v hu hv)
  simp only [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter,
    compl_compl] at *
  refine fun h huv hu hv huv' ↦ h huv' ?_ ?_ huv
  · exact fun h' ↦ hv fun x hx ↦ (huv' hx).resolve_left (h' hx)
  · exact fun h' ↦ hu fun x hx ↦ (huv' hx).resolve_right (h' hx)

[Mario Carneiro]

it could be golfed a bit more with the lemma a ⊆ b ∪ c → a ⊆ bᶜ → a ⊆ c (i.e. resolve_left for subsets)

[Yury G. Kudryashov]

Thanks!