FOL reasoning in Lean4

Stream: lean4

[Alexandre Rademaker]

I want to prove the equivalence of a formula and its prenex normal form. That should be simple, right? The formula came from a natural language sentence:

Goals (1)
⊢ (∃ e2 i8 e9 e10 x11 x24,
      named x11 "Apple Store" ∧
        store x11 ∧
          _electronics_n_1 x24 ∧
            ∀ (x3 : u), _people_n_of x3 i8 ∧ _go_v_1 e9 x3 ∧ _to_p_dir e10 e9 x11 → _buy_v_1 e2 x3 x24) ↔
    ∃ e2 i8 e9 e10 x11 x24,
      ∀ (x3 : u),
        named x11 "Apple Store" ∧
          store x11 ∧
            _electronics_n_1 x24 ∧ (_people_n_of x3 i8 ∧ _go_v_1 e9 x3 ∧ _to_p_dir e10 e9 x11 → _buy_v_1 e2 x3 x24)

image.png

At this point of the proof, I have a few questions:

1. can I simplify it? repeat constructor didn't give me the same result. Can I deal with the existential more simply?
2. Is there a tactic that would help me to substitute ?mp.intro.intro.intro.intro.intro.intro.h.h.h.h.w with a in the premisses?

References are welcome... I remember that @Sebastian Ullrich has some slides for a logic course using Lean 4. Trying to find the link..

[Alexandre Rademaker]

I got some good progress!

 theorem t1 : a2 ↔ a21 := by
  unfold a2
  unfold a21
  apply Iff.intro
  intro h
  cases h with
  | intro a pa => cases pa with
    | intro b pb => cases pb with
      | intro c pc => cases pc with
        | intro d pd => cases pd with
          | intro e pe => cases pe with
            | intro f pf => exists a; exists b; exists c; exists d; exists e; exists f; intro g; sorry

gives me

Goals (1)
case mp.intro.intro.intro.intro.intro.intro
a b c d e f : u
pf :
  named e "Apple Store" ∧
    store e ∧ _electronics_n_1 f ∧ ∀ (x3 : u), _people_n_of x3 b ∧ _go_v_1 c x3 ∧ _to_p_dir d c e → _buy_v_1 a x3 f
g : u
⊢ named e "Apple Store" ∧
    store e ∧ _electronics_n_1 f ∧ (_people_n_of g b ∧ _go_v_1 c g ∧ _to_p_dir d c e → _buy_v_1 a g f)

[David Renshaw]

Can you provide a #mwe in text format?

[Mac]

@Alexandre Rademaker Once simplification that immediately comes to mind is that instead of doing intro h; cases h with | intro ... a number of times you could use the anonymous constructor and pattern matching like so: intro ⟨a, ⟨b, ⟨c, ...⟩⟩⟩⟩

[Yakov Pechersky]

In mathlib3, I'd use simp, which would move the forall as far to the right as possible, that is, the things that don't rely on the binder out of if.

[Yakov Pechersky]

And after, use simp [and.comm, and.left_comm, and.assoc] as a way to reorder terms under the existential binder

[Yakov Pechersky]

If that's not enough, use docs#exists_congr several times and reorder after the unwrapping

[Alexandre Rademaker]

Maybe too much complicated, but I done https://gist.github.com/arademaker/b42a5348697dcb8b5c391f4f82d13cb3

[Alexandre Rademaker]

Yes, @Yakov Pechersky in Lean3 with mathlib I would have done that quickly. I am still adapting myself to Lean4.

[Alexandre Rademaker]

@Mac I didn't understand... can you elaborate on your suggestion on using intro? the existential are in the premisses, so I still need to make intro work in the premises, right? How? One cases h with ...?

[Mac]

@Alexandre Rademaker The following are essentially equivalent:

theorem withCases :
(∃ a b c d e f : Nat, α) → α := by
  intro h
  cases h with
  | intro a pa => cases pa with
    | intro b pb => cases pb with
      | intro c pc => cases pc with
        | intro d pd => cases pd with
          | intro e pe => cases pe with
            | intro f pf => exact pf

theorem withAnonCtor :
(∃ a b c d e f : Nat, α) → α := by
  intro ⟨a, ⟨b, ⟨c, ⟨d, ⟨e, ⟨f, pf⟩⟩⟩⟩⟩⟩
  exact pf

One is just much more concise. :grinning_face_with_smiling_eyes:

[Mac]

You can then use the anonymous constructor again to rebuild the exists like so:

theorem reorder (f : Nat → Nat → Nat → Prop) :
(∃ a b c : Nat, f a b c) → (∃ c b a : Nat, f a b c) := by
  intro ⟨a, ⟨b, ⟨c, p⟩⟩⟩
  exact ⟨c, ⟨b, ⟨a, p⟩⟩⟩

[Mac]

If you want, you could even drop the tactics altogether:

theorem reorderNoTactics (f : Nat → Nat → Nat → Prop) :
(∃ a b c : Nat, f a b c) → (∃ c b a : Nat, f a b c) :=
  λ ⟨a, ⟨b, ⟨c, p⟩⟩⟩ => ⟨c, ⟨b, ⟨a, p⟩⟩⟩

[Alexandre Rademaker]

Oh, that was great !!! https://gist.github.com/arademaker/b42a5348697dcb8b5c391f4f82d13cb3#file-all-people-lean-L56-L73 Thank you @Mac

[Mario Carneiro]

the anonymous constructor notation is right associative, so you can also write that as λ ⟨a, b, c, p⟩ => ⟨c, b, a, p⟩

[Alexandre Rademaker]

Even better, https://gist.github.com/arademaker/b42a5348697dcb8b5c391f4f82d13cb3#file-all-people-lean-L56-L73, thank you @Mario Carneiro

[Mac]

@Alexandre Rademaker
You can also use the anonymous constructor on the ands and to form the result like so (for mp):

case mp =>
  intro ⟨a, b, c, d, e, f, ha, hs, he, fa⟩
  refine ⟨a, b, c, d, e, f, ?_⟩
  intro x
  refine ⟨ha, hs, he, ?_⟩
  intro ⟨hp, hg, hd⟩
  exact fa x ⟨hp, hg, hd⟩

[Mac]

And since that last part is in the same order, you can also do:

intro ⟨a, b, c, d, e, f, ha, hs, he, fa⟩
refine ⟨a, b, c, d, e, f, ?_⟩
intro x
exact ⟨ha, hs, he, fa x⟩

[Mac]

Using a term mode function, we can narrow it down farther to:

intro ⟨a, b, c, d, e, f, ha, hs, he, fa⟩
exact ⟨a, b, c, d, e, f, λ x => ⟨ha, hs, he, fa x⟩⟩

[Mac]

@Alexandre Rademaker So, in summary, here is the simplified theorem:

theorem t1 : a2 ↔ a21 := by
  unfold a2, a21
  apply Iff.intro
  case mp =>
    intro ⟨a, b, c, d, e, f, ha, hs, he, fa⟩
    exact ⟨a, b, c, d, e, f, λ x => ⟨ha, hs, he, fa x⟩⟩
  case mpr =>
    intro ⟨a, b, c, d, e, f, fa⟩
    have ⟨ha, hs, he, _⟩ := fa a
    exact ⟨a, b, c, d, e, f, ha, hs, he, λ x => (fa x).2.2.2⟩

[Alexandre Rademaker]

Oh, nice, I will explore that @Mac! But the unfold a2, a21 didn't work for me.

[Mac]

@Alexandre Rademaker Oh yeah, I noticed you were on a very old version of Lean 4 (constant has been renamed opaque for one). That is probably the problem.

[Alexandre Rademaker]

Oh, now I have to learn how to update the project. It seems that it is something more than edit the file lean-toolchain. Elan shows me

% elan show
installed toolchains
--------------------

leanprover-community/lean:3.21.0
leanprover-community/lean:3.23.0
leanprover/lean4:nightly-2022-02-02
leanprover/lean4:stable (default)

active toolchain
----------------

leanprover/lean4:stable (default)
Lean (version 4.0.0, commit 96de208a6b1a, Release)

[Mac]

Stable is really old (and outside a small window around its release is usually that way), so it is generally recommended to use a recent nightly.

[Mac]

For instance, you can edit your lean-toolchain file to leanprover/lean4:nightly-2022-07-25 (the 4-5 day old nightly I am using to test)

[Alexandre Rademaker]

perfect. I need to run elan update inside the project's folder.

[Kyle Miller]

With the mild additional assumption that u is nonempty, t1 reduces to a single simp. I think this is what Yakov was getting at with the mathlib3 suggestion -- you can write these general lemmas in Lean 4 easily enough.

@[simp]
theorem and_exists (p) (q : α → Prop) : p ∧ (∃ a, q a) ↔ ∃ a, p ∧ q a := by
  apply Iff.intro
  case mp =>
    intro ⟨a, b, c⟩
    exact ⟨b, a, c⟩
  case mpr =>
    intro ⟨a, b, c⟩
    exact ⟨b, a, c⟩

@[simp]
theorem and_forall [Nonempty α] (p) (q : α → Prop) : p ∧ (∀ a, q a) ↔ ∀ a, p ∧ q a := by
  apply Iff.intro
  case mp =>
    intro ⟨a, b⟩ c
    exact ⟨a, b c⟩
  case mpr =>
    intro a
    refine ⟨(a Classical.ofNonempty).1, ?_⟩
    intro b
    exact (a b).2

 axiom u.nonempty : Nonempty u
 instance : Nonempty u := u.nonempty

 theorem t1 : a2 ↔ a21 := by simp [a2, a21]

[Mac]

@Kyle Miller Those simp lemmas look like they should be the other way around. Shouldn't the normal form be taking the proposition that does not use the bound variable out of the formula not putting it into it? Or am I missing something? (I would not be surprised if I am -- my experience proof techniques is not great).

[Kyle Miller]

My thought was to put everything into prenex normal form if possible. Maybe they're not good simp lemmas in general, but they do seem to do the trick.