4
$\begingroup$

As is perhaps obvious from the question, I am just starting with Lean and am missing some very basic knowledge about what features are available. Anyways, I'm trying to prove not (false = true) and I have this:

example : not (false = true) := not.intro (
    assume H: false = true,
    show false, from begin
        rw H,
        -- now I need to prove "true"
    end
)

The thing that's really confusing is me is that the program is telling me I have an unsolved goal, which is to prove the vacuous statement "true". I figure there's some boilerplate "cmon it's already true" statement like "qed" or "vacuous" or something but I have no idea what it is and I wasn't able to find it by skimming the documentation.

Also I'm sure this can be more succinct. But first I need it to work at all before I worry about succinct!

$\endgroup$
4
  • $\begingroup$ I do not have much experince with lean, but I have heard that there is some difference between the lattest versions lean3 and lean4. Which one do you use? $\endgroup$ Commented Aug 18, 2022 at 12:04
  • $\begingroup$ @ThomasPreu I actually do not know! I'm using the online editor at leanprover.github.io/live/master $\endgroup$ Commented Aug 18, 2022 at 12:05
  • 1
    $\begingroup$ The tactic trivial can close out a goal of true. $\endgroup$ Commented Aug 18, 2022 at 12:14
  • $\begingroup$ @DanielHast Ah! That's the one. $\endgroup$ Commented Aug 18, 2022 at 12:15

1 Answer 1

3
$\begingroup$

The exact axiom that accepts true is called true.intro:

example : not (false = true) := not.intro (
    assume H: false = true,
    show false, from begin
        rw H,
        exact true.intro
    end
)

From https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html :

Incidentally, just as false has only an elimination rule, true has only an introduction rule, true.intro : true, sometimes abbreviated trivial : true. In other words, true is simply true, and has a canonical proof, trivial.

Other more general tactics that would have worked are trivial and simp.

From the documentation:

Trivial

Tries to solve the current goal using a canonical proof of true, or the reflexivity tactic, or the contradiction tactic.

$\endgroup$
2
  • 1
    $\begingroup$ You could also do it with "exact true.intro" (since "true.intro" is a term of type "true", and that's exactly what you need to produce in order to complete the proof). $\endgroup$ Commented Aug 19, 2022 at 7:21
  • $\begingroup$ @HansLundmark Thanks, I was wondering what the underlying axiom was called. $\endgroup$ Commented Aug 19, 2022 at 10:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .