Как доказать два утверждения в логах высказываний c, используя LEAN?

Question

Два доказательства в конце главы 3 урока LEAN, с которыми я до сих пор борюсь (и, следовательно, мешаю мне продолжать читать руководство), следующие:

theorem T11 : ¬(p ↔ ¬p) := sorry

, для которых моя попытка чтобы доказать правильное значение, остановился на этом этапе:

theorem T11R : ¬(p → ¬p) := 
begin 
    assume hyp : p → ¬ p, 
    cases (em p) with hp hnp, 
    exact (hyp hp) hp, 
    exact sorry 
end

, поскольку, очевидно, я пока не знаю, как использовать ¬p. Не уверен, как показать левую импликацию. Другой - это:

theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
begin
    intros porqr, sorry
end

, который я предположительно использую (как правильное следствие), чтобы показать следующее:

theorem T2 : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := 
begin    
    have goR : ((p ∨ q) → r) → (p → r) ∧ (q → r), from T2R p q r,
    have goL : (p → r) ∧ (q → r) → ((p ∨ q) → r), from T2L p q r,
    exact iff.intro (goR) (goL)
end

Здесь я получил движение левой стороны:

theorem T2L : (p → r) ∧ (q → r) → ((p ∨ q) → r) := 
begin
    intros prqr,
    assume porq : p ∨ q,
    exact or.elim porq prqr.left prqr.right
end

Answer 1

theorem T11R неверно, например, если p равно false, тогда p → ¬ p истинно.

¬(p ↔ ¬p) не эквивалентно (¬ (p → ¬ p)) ∧ ¬ (¬ p → p); это эквивалентно ¬ ((p → ¬ p) ∧ (¬ p → p)), что отличается.

Для theorem T2R, если вы используете split tacti c, это даст вам две цели, по одной на каждую сторону and. Вы можете использовать тактику left и right, чтобы превратить цель p ∨ q в p или q. Теоремы or.inl и or.inr также могут быть использованы для доказательства or.

Вот доказательство T2R

theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
begin
    intros porqr,
    split,
    { assume hp : p,
      apply porqr,
      left,
      exact hp },
    { assume hq : q,
      apply porqr,
      right,
      exact hq },
end