mathlib と Std.logic も必要。
| 論理記号 | 導入規則 | 除去規則 |
|---|---|---|
| 連言∧ | And.intro | And.left, And.right |
| 選言∨ | Or.intro_left, Or.intro_right | Or.elim |
| 否定￢ | Not.intro | Not.elim〈absurd〉 |
| 真T | True.intro | 通常の証明 |
| 偽⊥ | 背理法の証明 | False.elim |
| 含意→ | ラムダ抽象（fun） | 適用（空白） |
| 同値 ←→ | Iff.intro | Iff.elim |
| 全称∀ | 依存ラムダ抽象 | 依存適用 |
| 存在∃ | Exists.intro | Exists.elim |
| 一意存在∃! | ExistsUnique.intro | ExistsUniwque.elim |
And
/-- `And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. -/ structure And (a b : Prop) : Prop where /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/ intro :: /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then `h.left`, also notated as `h.1`, is a proof of `a`. -/ left : a /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then `h.right`, also notated as `h.2`, is a proof of `b`. -/ right : b
Or
/--
`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.
-/
inductive Or (a b : Prop) : Prop where
/-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/
| inl (h : a) : Or a b
/-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/
| inr (h : b) : Or a b
/-- Alias for `Or.inl`. -/
theorem Or.intro_left (b : Prop) (h : a) : Or a b :=
Or.inl h
/-- Alias for `Or.inr`. -/
theorem Or.intro_right (a : Prop) (h : b) : Or a b :=
Or.inr h
/--
Proof by cases on an `Or`. If `a ∨ b`, and both `a` and `b` imply
proposition `c`, then `c` is true.
-/
theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :=
match h with
| Or.inl h => left h
| Or.inr h => right h
Not
/--
Anything follows from two contradictory hypotheses. Example:
```
example (hp : p) (hnp : ¬p) : q := absurd hp hnp
```
For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
(h₂ h₁).rec/-- `Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`, so if your goal is `¬p` you can use `intro h` to turn the goal into `h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False` and `(hn h).elim` will prove anything. For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic) -/ def Not (a : Prop) : Prop := a → False
-! ## not -/
theorem Not.intro {a : Prop} (h : a → False) : ¬a := h
/-- Ex falso for negation. From `¬a` and `a` anything follows. This is the same as `absurd` with
the arguments flipped, but it is in the `not` namespace so that projection notation can be used. -/
def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
True/False
/--
`True` is a proposition and has only an introduction rule, `True.intro : True`.
In other words, `True` is simply true, and has a canonical proof, `True.intro`
For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
inductive True : Prop where
/-- `True` is true, and `True.intro` (or more commonly, `trivial`)
is the proof. -/
| intro : True
/--
`False` is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. `False` elimination rule, `False.rec`,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
inductive False : Prop
/--
`False.elim : False → C` says that from `False`, any desired proposition
`C` holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.
The target type is actually `C : Sort u` which means it works for both
propositions and types. When executed, this acts like an "unreachable"
instruction: it is **undefined behavior** to run, but it will probably print
"unreachable code". (You would need to construct a proof of false to run it
anyway, which you can only do using `sorry` or unsound axioms.)
-/
@[macro_inline] def False.elim {C : Sort u} (h : False) : C :=
h.rec
Iff
/-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa. By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a` is equivalent to the corresponding expression with `b` instead. -/ structure Iff (a b : Prop) : Prop where /-- If `a → b` and `b → a` then `a` and `b` are equivalent. -/ intro :: /-- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`. -/ mp : a → b /-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/ mpr : b → a @[inherit_doc] infix:20 " <-> " => Iff @[inherit_doc] infix:20 " ↔ " => Iff
Exists
/--
Existential quantification. If `p : α → Prop` is a predicate, then `∃ x : α, p x`
asserts that there is some `x` of type `α` such that `p x` holds.
To create an existential proof, use the `exists` tactic,
or the anonymous constructor notation `⟨x, h⟩`.
To unpack an existential, use `cases h` where `h` is a proof of `∃ x : α, p x`,
or `let ⟨x, hx⟩ := h` where `.
Because Lean has proof irrelevance, any two proofs of an existential are
definitionally equal. One consequence of this is that it is impossible to recover the
witness of an existential from the mere fact of its existence.
For example, the following does not compile:
```
example (h : ∃ x : Nat, x = x) : Nat :=
let ⟨x, _⟩ := h -- fail, because the goal is `Nat : Type`
x
```
The error message `recursor 'Exists.casesOn' can only eliminate into Prop` means
that this only works when the current goal is another proposition:
```
example (h : ∃ x : Nat, x = x) : True :=
let ⟨x, _⟩ := h -- ok, because the goal is `True : Prop`
trivial
```
-/
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
/-- Existential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/
| intro (w : α) (h : p w) : Exists p/-! # Exists -/
theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
(h₁ : Exists (fun x => p x)) (h₂ : ∀ (a : α), p a → b) : b :=
match h₁ with
| intro a h => h₂ a h
ExistsUnique
theorem ExistsUnique.intro {p : α → Prop} (w : α)
(h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x := ⟨w, h₁, h₂⟩
theorem ExistsUnique.elim {α : Sort u} {p : α → Prop} {b : Prop}
(h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
Exists.elim h₂ (λ w hw => h₁ w (And.left hw) (And.right hw))
