s
Когда же
P ∧ Q это как пара: одно значение, содержащее сразу два.Size: a a a
2021 November 26
ツダ
Что?
ツダ
>Если P land Q, то это как пара
P land Q -- функция?
"Это" -- функция P land Q?
>одно значение содержит сразу два значения
Что значит содержит сразу?
P land Q -- функция?
"Это" -- функция P land Q?
>одно значение содержит сразу два значения
Что значит содержит сразу?
ツダ
Похоже сильно туплю
s
Как и в случае с программирование, такие вещи лучше потрогать. Lean 3 с этим сильно помогает, так как показывает контекст доказательства.
s
(если, конечно, ты поставил расширение для VS Code)
ツダ
Мне сложно читать методичку
s
Вот на примере sunny_rainy. В самом начале контекст выглядит так:
1 goal
sunny rainy: Prop
sr: sunny ∨ rainy
ns: ¬sunny
⊢ rainy
ツダ
Я должен понять, что в ней записано
s
Мы знаем, что sunny и ranny это утверждения. Кроме того, вы знаем, что
sunny ∨ rainy и ¬sunny.s
И есть цель: доказать
rainy.s
После того, как вводишь
cases sr with s r,, цели меняются:case or.inl
sunny rainy: Prop
ns: ¬sunny
s: sunny
⊢ rainy
case or.inr
sunny rainy: Prop
ns: ¬sunny
r: rainy
⊢ rainy
s
Мы рассматриваем два случая: в одном мы знаем, что
sunny истинно, в другом — что rainy истинно.s
В первом случае мы можем вывести абсурд, так как у нас есть и
sunny, и ¬sunny. Из абсурда следует что угодно, в том числе и rainy.s
Во втором случае, у нас есть
rainy и нам надо доказать, что rainy. Ну, следует прямо из предположения.s
Ты можешь смотреть на доказательство утверждения как на сборку пазла: у тебя есть начальные предположения, и есть правила вывода, которые позволяют преобразовать эти предположения во что-то другое.
s
Задача же — вывести цель доказательства.
s
Смотри какие есть правила для «и»:
conjI: "⟦P; Q⟧ ⟹ P ∧ Q"
conjunct1: "(P ∧ Q) ⟹ P"
conjunct2: "(P ∧ Q) ⟹ Q"
s
А теперь смотри аналогию с обычными туплами: если есть какие-то два значения
a ∈ A и b ∈ B, то мы можем построить (a, b) ∈ A × B.s
И если у нас есть
(a, b) ∈ A × B, то из этой пары мы можем достать значение a ∈ A.