Dwa dowody na końcu rozdziału 3 W leniwym samouczku, z którym wciąż walczę (a dlatego powstrzymaj mi przed przeczytaniem podręcznika) są następujące:

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

Dla których moja próba udowodnienia właściwego implikacji zatrzymała się w tym momencie:

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

Jak najwyraźniej nie wiem, jak używać ¬p. Nie jesteś pewien, jak pokazać lewą implikację. Drugi to to:

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

Które rzekomo używam (jako właściwe implikacje), aby pokazać następujące informacje:

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

Tutaj miałem lewicę:

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
0
Vox 17 styczeń 2020, 23:45

1 odpowiedź

Najlepsza odpowiedź

theorem T11R nie jest prawdą, na przykład, jeśli p jest false następnie p → ¬ p jest prawdziwe.

¬(p ↔ ¬p) nie jest równoważny (¬ (p → ¬ p)) ∧ ¬ (¬ p → p); Jest to odpowiednik ¬ ((p → ¬ p) ∧ (¬ p → p)), który jest inny.

Dla theorem T2R Jeśli używasz taktyki split, da Ci dwa cele, jeden z każdej strony and. Możesz użyć taktyki left i right, aby obrócić cel p ∨ q do p lub q. Teoremy or.inl i or.inr mogą być używane do udowodnienia {{x10}}.

Oto dowód 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
1
Christopher Hughes 17 styczeń 2020, 21:06