19.2. 逻辑连接词🔗

连词被实现为归纳定义的命题 And。构造函数 And.intro 表示合取的引入规则：要证明一个合取，只需证明两个合取即可。类似地，And.elim 表示消除规则：给定一个合取的证明和一个假设两个合取的其他陈述的证明，另一个陈述可以被证明。由于 And 是 subsingleton，因此 And.elim 也可以用作计算数据的一部分。但是，不应将其与 PProd 混淆：使用不可计算的推理原理（例如选择公理）来定义数据（包括 Prod）会导致 Lean 无法编译和运行生成的程序，而在命题证明中使用它们则不会导致此类问题。

在策略证明中，可以通过 apply 显式使用 And.intro 来证明合取，但 constructor 更常见。当多个连词嵌套在证明目标中时，and_intros 可用于在每个相关位置应用 And.intro。可以使用 cases、模式匹配与 let 或 match 或 rcases 来简化上下文中连词的假设。

structure

And (a b : Prop) : Prop
And (a b : Prop) : Prop

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.

Conventions for notations in identifiers:

The recommended spelling of ∧ in identifiers is and.

Constructor

And.intro

And.intro : a → b → a ∧ b is the constructor for the And operation.

Fields

left : a

Extract the left conjunct from a conjunction. h : a ∧ b then h.left, also notated as h.1, is a proof of a.

right : b

Extract the right conjunct from a conjunction. h : a ∧ b then h.right, also notated as h.2, is a proof of b.

def

And.elim.{u_1} {a b : Prop} {α : Sort u_1} (f : a → b → α) (h : a ∧ b) :
  α
And.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : a → b → α) (h : a ∧ b) : α

Non-dependent eliminator for And.

析取作为归纳定义的命题 Or 来实现。它有两个构造函数，每个引入规则都有一个：任一析取的证明都足以证明该析取。虽然 Or 的定义与 Sum 的定义类似，但在实践中却有很大不同。由于 Sum 是一种类型，因此可以检查使用哪个构造函数来创建任何给定值。另一方面，Or 形成命题：证明析取的项不能被询问来检查哪个析取是正确的。换句话说，由于 Or 不是 subsingleton，因此它的证明不能用作计算的一部分。

在策略证明中，可以通过 apply 使用任一构造函数（Or.inl 或 Or.inr）显式证明析取。可以使用 cases、模式匹配与 match 或 rcases 来简化上下文中的析取假设。

inductive predicate

Or (a b : Prop) : Prop
Or (a b : Prop) : Prop

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.

Conventions for notations in identifiers:

The recommended spelling of ∨ in identifiers is or.

Constructors

Or.inl {a b : Prop} (h : a) : a ∨ b

Or.inl is "left injection" into an Or. If h : a then Or.inl h : a ∨ b.

Or.inr {a b : Prop} (h : b) : a ∨ b

Or.inr is "right injection" into an Or. If h : b then Or.inr h : a ∨ b.

当任一析取为可判定时，就可以使用 Or 来计算数据。这是因为决策过程的结果提供了合适的分支条件。

def

Or.by_cases.{u} {p q : Prop} [Decidable p] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α
Or.by_cases.{u} {p q : Prop} [Decidable p]
  {α : Sort u} (h : p ∨ q) (h₁ : p → α)
  (h₂ : q → α) : α

Construct a non-Prop by cases on an Or, when the left conjunct is decidable.

def

Or.by_cases'.{u} {q p : Prop} [Decidable q] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α
Or.by_cases'.{u} {q p : Prop}
  [Decidable q] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α

Construct a non-Prop by cases on an Or, when the right conjunct is decidable.

¬P 不是将否定编码为归纳类型，而是定义为表示 P → False。换句话说，为了证明一个否定，只需假设否定的陈述并导出矛盾即可。这也意味着 False 可以立即从命题及其否定的证明中导出，然后用于证明任何命题或栖息于任何类型。

def

Not (a : Prop) : Prop
Not (a : Prop) : Prop

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

Conventions for notations in identifiers:

The recommended spelling of ¬ in identifiers is not.

def

absurd.{v} {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b
absurd.{v} {a : Prop} {b : Sort v}
  (h₁ : a) (h₂ : ¬a) : b

Anything follows from two contradictory hypotheses. Example:

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

For more information: Propositional Logic

def

Not.elim.{u_1} {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) : α
Not.elim.{u_1} {a : Prop} {α : Sort u_1}
  (H1 : ¬a) (H2 : a) : α

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.

使用命题的宇宙中的函数类型表示蕴涵。为了证明A → B，在假设A之后证明B就足够了。这对应于 Lean.Parser.Term.fun : termfun 的键入规则。类似地，函数应用的类型规则对应于modus ponens：给定A → B的证明和A的证明，可以证明B。

Truth-Functional Implication

将蕴涵表示为命题域中的函数相当于传统定义，其中 A → B 被定义为 (¬A) ∨ B。这可以使用命题外延性和排中律来证明：

theorem truth_functional_imp {A B : Prop} :
    ((¬ A) ∨ B) = (A → B) := byA:PropB:Prop⊢ (¬A ∨ B) = (A → B)
  apply propextA:PropB:Prop⊢ ¬A ∨ B ↔ A → B
  constructormpA:PropB:Prop⊢ ¬A ∨ B → A → BmprA:PropB:Prop⊢ (A → B) → ¬A ∨ B
  .mpA:PropB:Prop⊢ ¬A ∨ B → A → B rintro (h | h) amp.inlA:PropB:Proph:¬Aa:A⊢ Bmp.inrA:PropB:Proph:Ba:A⊢ B <;>mp.inlA:PropB:Proph:¬Aa:A⊢ Bmp.inrA:PropB:Proph:Ba:A⊢ B trivialAll goals completed! 🐙
  .mprA:PropB:Prop⊢ (A → B) → ¬A ∨ B intro hmprA:PropB:Proph:A → B⊢ ¬A ∨ B
    by_cases AposA:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ BnegA:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B
    .posA:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ B apply Or.inrposA:PropB:Proph:A → Bh✝:A⊢ B; solve_by_elimAll goals completed! 🐙
    .negA:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B apply Or.inlnegA:PropB:Proph:A → Bh✝:¬A⊢ ¬A; trivialAll goals completed! 🐙

Live ↪

逻辑等价，或“当且仅当”，使用相当于蕴涵两个方向的合取的结构来表示。

structure

Iff (a b : Prop) : Prop
Iff (a b : Prop) : Prop

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.

Conventions for notations in identifiers:

The recommended spelling of ↔ in identifiers is iff.
The recommended spelling of <-> in identifiers is iff (prefer ↔ over <->).

Constructor

Iff.intro

If a → b and b → a then a and b are equivalent.

Fields

mp : a → b

Modus ponens for if and only if. If a ↔ b and a, then b.

mpr : b → a

Modus ponens for if and only if, reversed. If a ↔ b and b, then a.

def

Iff.elim.{u_1} {a b : Prop} {α : Sort u_1} (f : (a → b) → (b → a) → α)
  (h : a ↔ b) : α
Iff.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : (a → b) → (b → a) → α)
  (h : a ↔ b) : α

Non-dependent eliminator for Iff.

syntaxPropositional Connectives

除蕴涵之外的逻辑连接词通常使用专用语法来引用，而不是通过其定义的名称：

term ::= ...
    | `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`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.term ∧ term

term ::= ...
    | `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.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.term ∨ term

term ::= ...
    | `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://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.¬ term

term ::= ...
    | 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.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.term ↔ term

19.1.	真相
19.2.	逻辑连接词
19.3.	量词
19.4.	命题等价