1

I am new at lean - prover and I am trying to solve the examples on the online tutorial.

I am stuck at this example and I need to prove that "false implies q" or something like that. My code is :

variables p q : Prop
example : ¬ p → (p → q) := 
    assume h : ¬ p,
    assume hp : p,
    --have hnpq : ¬ p ∨ q, from or.inl h,
    have hf : false, from h hp,
    --show q, from hf
    sorry

I do not think that defining hnpq can help because this proof is part of the (¬ p ∨ q) → (p → q). In set theory I think that false implies everything.

Any suggestions or thoughts?

Georgios Papanikolaou
  • 21
  • 4
  • 1
    In Lean it is also true that `false` implies everything, see `false.elim`. So, you are almost there! (Hint: if you have `mathlib` installed, you can try `by library_search` and it will tell you if there is a lemma that proves the current goal under the available hypotheses.) – jmc Oct 18 '19 at 08:48
  • Thank you. It worked!! One question, that is mathlib!? Is it an extension for lean? Can you sent a link? – Georgios Papanikolaou Oct 18 '19 at 10:20
  • It's the main maths library for Lean. See https://github.com/leanprover-community/mathlib. The README contains links to installation instructions (which are somewhat nontrivial). – jmc Oct 18 '19 at 11:18
  • Thank you a lot!! I'll check it! – Georgios Papanikolaou Oct 18 '19 at 17:32

0 Answers0