Prove P → Q ∧ R, P : Q in purely tactic style.

Stream: Is there code for X?

[Richard Dudek]

Hello, I am making an automated theorem prover, that uses Lean. To keep things simple, I would like to completely avoid term style proofs (that use tactics such as have, show, exact...). However, I came across problem: I am not able to prove

example (P Q R : Prop) (h1 : P → Q ∧ R)(h2 : P) : Q

Is it possible to do in purely tactic style, without using tactics such as have, show, exact and preferaby without any theorems?

[Yury G. Kudryashov]

by simp [*] works

[Richard Dudek]

Thanks for your answer. Although this can prove this specific example, it can fail at more complex proofs so it does not solve my problem. Is there a general way of manually proving statements in the form I presented?

[Ruben Van de Velde]

tauto?

[Richard Dudek]

I don't know why, but this tactic is not recognized by my installation of Lean. Also, I am interested in exploring non-automated proofs. Is there any way of proving this statement using only "simple/elementary" tactics?

[Timo Carlin-Burns]

have and exact are pretty elementary tactics.. Here is a version using apply, but maybe you'll say it uses a theorem? You have an ∧ in your hypotheses so it seems reasonable to expect you'll need some theorems characterizing that symbol.

example (P Q R : Prop) (h1 : P → Q ∧ R)(h2 : P) : Q := by
  apply And.left
  apply h1
  apply h2

[Timo Carlin-Burns]

I would say this is a more straightforward elementary tactic proof but it uses have and exact

example (P Q R : Prop) (h1 : P → Q ∧ R)(h2 : P) : Q := by
  have ⟨hq, _⟩ := h1 h2
  exact hq

[Timo Carlin-Burns]

Richard Dudek said:

I don't know why, but this tactic is not recognized by my installation of Lean

The tauto tactic is from mathlib. You might need to add an import to the top of your file or set up mathlib as a dependency. If you've set up mathlib this should work:

import Mathlib.Tactic

example (P Q R : Prop) (h1 : P → Q ∧ R)(h2 : P) : Q := by
  tauto

[Richard Dudek]

I appreciate your answer. I have tried the second way, but it still has some problems. However, The first way looks like it should work. Thanks for your effort.

[Richard Dudek]

I wanted to avoid allowing my code to combine assumptions, without looking at goal, because then it starts proving unnecessary statements and they amount grows rapidly.

[Yury G. Kudryashov]

What's your goal? Do you want to write meta code that solves this kind of goal? Autogenerate a proof via some API? Something else?

[Richard Dudek]

I am writing code in Python that should be able to solve any goal of supported form (so far propositional logic) using axioms. I basically rewrote tiny part of Lean into Python and made BFS to search all possible proofs of specified form. It has managet to solve most of levels in game A Lean Intro to Logic (hhu.de) (redux worlds only), but it struggles with levels 5 and 7 of ↔ World. Aside from goals that need special theorems or manipulation with assumptions, it works pretty well.