demo1 for LEAN

demo1.lean

-- Mostly taken from Xena project at 
-- https://github.com/ImperialCollegeLondon/M40001_lean/blob/master/src/2021/logic/README.md

import tactic -- imports all the Lean tactics

variables (P Q R W S: Prop)

/-
## Tactics:

* `intro`
* `exact`
* `apply`
-/

example (hP : P) (hQ : Q) (hR : R) : P :=
begin
  sorry
end

-- Assume `Q` is true. Prove that `P → Q`. 
example (hQ : Q) : P → Q :=
begin
  sorry
end

-- Assume `P → Q` and `P` is true. Deduce `Q`.
example (h : P → Q) (hP : P) : Q :=
begin
  sorry
end

example : P → P :=
begin
  sorry
end

example : P → Q → P :=
begin
  sorry
end

example : P → (P → Q) → Q :=
begin
  sorry
end

example (hPR : P → R) (hQR : Q → R) : (P ∨ Q) → R :=
begin
  sorry
end

example (hPQ : P → Q) (hPnQ : P → ¬Q) : ¬P :=
begin
  sorry
end