No news is good news?

Stream: new members

[Robert Culling]

Kia ora! If Lean doesn't tell me off, then is my proof correct? I put the following (part of an answer to one of the TPiL4) in and Lean doesn't have any red anywhere. So I presume it is happy.

variable (α : Type) (p q : α → Prop)

example : (∀ x, p x ∧ q x) → (∀ x, p x) ∧ (∀ x, q x) :=
  (λ w : ∀ x, p x ∧ q x => -- This abstraction is for the implication
    have t : (∀ x, p x) :=
      λ a : α => (w a).left -- This abstraction is the ∀ abstraction

    have s : (∀ x, q x) :=
      λ b : α => (w b).right -- This abstraction is the ∀ abstraction

    show (∀ x, p x) ∧ (∀ x, q x) from And.intro t s)

But I am used to the "proof complete" note from the Natural Number Game. So I am just wondering how I know when lean is happy?

Thanks :)

[Andrew Yang]

"proof complete" only appears when you are in tactic mode. As you are currently using proof terms, there won't be such a message. But if there are no error messages, then lean should be happy.

[Robert Culling]

@Andrew Yang Thank you, Andrew. I see tactics is the next chapter, so I'll be onto that soon.

[Kevin Buzzard]

This is lean 4, right? What happens if you put your cursor just to the right of the last character in the proof?

[Kyle Miller]

@Kevin Buzzard "No info found" in VS Code

[Kyle Miller]

If anyone want's their well-deserved "goals accomplished", you can artificially go into tactic mode:

example : (∀ x, p x ∧ q x) → (∀ x, p x) ∧ (∀ x, q x) :=
  by exact (λ w : ∀ x, p x ∧ q x => -- This abstraction is for the implication
    have t : (∀ x, p x) :=
      λ a : α => (w a).left -- This abstraction is the ∀ abstraction

    have s : (∀ x, q x) :=
      λ b : α => (w b).right -- This abstraction is the ∀ abstraction

    show (∀ x, p x) ∧ (∀ x, q x) from And.intro t s)

[Robert Culling]

@Kyle Miller I know I will get to it in TPiL4, but can you please tell me how to artificially go into tactic mode?

[Arien Malec]

The by exact right after the := in @Kyle Miller's example

[Arien Malec]

It takes your term mode solution that typechecks and makes it a tactics mode exact solution that "tada"s.

[Robert Culling]

Does the "exact" in "by exact" just prove the goal for me? It seems to me if I comment out my proof and just write "by exact", then Lean is still happy that all goals are accomplished. It gives me the party emoji - but not for my proof.

Is there a way to get the party, goals accomplished, emoji for my proof? This one, for example.

example : ¬(p ↔ ¬p) :=
  (λ x : p ↔ ¬p =>
    have y : p → ¬p := Iff.mp x
    have z : ¬p → p := Iff.mpr x
    have wnp : ¬p :=
      (λ wp : p =>
        have w : ¬p := y wp
        show False from w wp)
    have wnnp : ¬¬p :=
      (λ np : ¬p =>
        have w : p := z np
        show False from np w)
    show False from wnnp wnp)

In answer to @Kevin Buzzard's comment above: if my cursor is next to the last character of the proof, the information window reads "No info found."

[Niels Voss]

I'm not really familiar with lean 4 but writing by exact without a term won't just prove the goal, it generates an error but the error is hard to see because it appears a few lines below the proof.
I'm not really sure if you can get "goals accomplished" to appear outside of tactic mode, but if you write by exact and don't comment out your proof it shows "goals accomplished" at the end
I think you can also write #print axioms mytheorem to check your proof, which will also tell you if your proof relies on sorry

[Robert Culling]

@Niels Voss thank you I will try the print command you suggest

[Bjørn Kjos-Hanssen]

You can always check if your code is being checked by typing something that's clearly wrong, like "dfjdfhjb"