Created
June 10, 2020 22:27
-
-
Save avigad/3e4d9d270773b1f3bc41970e942f2fab to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import tactic | |
open classical | |
/- | |
Cheat sheet: | |
to prove `p → q`, use `intro h` | |
to use `h : p → q`, use `apply h` | |
to prove `p ∧ q`, use `split` | |
to use `h : p ∧ q`, use `cases h with hp hq` | |
to prove `p ∨ q`, use `left` or `right` | |
to use `p ∨ q`, use `cases h with h1 h1` | |
to prove `¬ p`, use `intro h` | |
to use `h : ¬ p`, use `apply h` (when the goal is false) | |
to prove `p ↔ q`, use `split` | |
to use `h : p ↔ q`, use `cases h with h1 h2` | |
to prove a change a goal to `false`: `exfalso` | |
to prove a goal by contradiction: use `by_contradiction h` | |
-/ | |
/- Some exercises -/ | |
section | |
variables p q r s : Prop | |
example : (p → q) ∧ (q → r) → p → r := | |
begin | |
sorry | |
end | |
example : (p ∨ q) ∧ ¬ p → q := | |
begin | |
sorry | |
end | |
end | |
/- Exercises from Theorem Proving in Lean -/ | |
section | |
variables p q r s : Prop | |
-- commutativity of ∧ and ∨ | |
example : p ∧ q ↔ q ∧ p := sorry | |
example : p ∨ q ↔ q ∨ p := sorry | |
-- associativity of ∧ and ∨ | |
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry | |
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry | |
-- distributivity | |
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry | |
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry | |
-- other properties | |
example : (p → (q → r)) ↔ (p ∧ q → r) := sorry | |
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry | |
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry | |
example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry | |
example : ¬(p ∧ ¬p) := sorry | |
example : p ∧ ¬q → ¬(p → q) := sorry | |
example : ¬p → (p → q) := sorry | |
example : (¬p ∨ q) → (p → q) := sorry | |
example : p ∨ false ↔ p := sorry | |
example : p ∧ false ↔ false := sorry | |
example : (p → q) → (¬q → ¬p) := sorry | |
example : ¬ (p ↔ ¬ p) := sorry | |
-- these require classical logic | |
example : (p → r ∨ s) → ((p → r) ∨ (p → s)) := sorry | |
example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry | |
example : ¬(p → q) → p ∧ ¬q := sorry | |
example : (p → q) → (¬p ∨ q) := sorry | |
example : (¬q → ¬p) → (p → q) := sorry | |
example : p ∨ ¬p := sorry | |
example : (((p → q) → p) → p) := sorry | |
end | |
/- | |
Quantifiers | |
-/ | |
section | |
variables (α : Type) (p q : α → Prop) | |
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := sorry | |
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := sorry | |
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := sorry | |
end | |
/- | |
Equality | |
-/ | |
section | |
variables (real : Type) [ordered_ring real] | |
variables (log exp : real → real) | |
variable log_exp_eq : ∀ x, log (exp x) = x | |
variable exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x | |
variable exp_pos : ∀ x, exp x > 0 | |
variable exp_add : ∀ x y, exp (x + y) = exp x * exp y | |
-- this ensures the assumptions are available in tactic proofs | |
include log_exp_eq exp_log_eq exp_pos exp_add | |
example (x y z : real) : | |
exp (x + y + z) = exp x * exp y * exp z := | |
by rw [exp_add, exp_add] | |
example (y : real) (h : y > 0) : exp (log y) = y := | |
exp_log_eq h | |
theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : | |
log (x * y) = log x + log y := | |
sorry | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment