21 enero 2021 – Vestigium

Pruebas en Lean de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

PorJosé A. Alonso 21 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 12 pruebas en Lean de la ley de De Morgan:

¬(P ∧ Q) ↔ ¬P ∨ ¬Q

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic
variables (P Q : Prop)

-- ----------------------------------------------------
-- Ejercicio. Demostrar que
--    ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
-- ----------------------------------------------------

-- 1ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      apply h,
      split,
      { exact hP, },
      { exact hQ, }},
    { left,
      exact hP, }},
  { intros h h',
    cases h' with hP hQ,
    cases h with hnP hnQ,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end

-- 2ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      exact h ⟨hP, hQ⟩, },
    { left,
      exact hP, }},
  { rintros (hnP | hnQ) ⟨hP, hQ⟩,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end

-- 3ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        ( assume hnP : ¬P,
          show ¬P ∨ ¬Q,
            from or.inl hnP))
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          ( assume hnQ: ¬Q,
            show false,
              from hnQ (and.right hPQ)))

-- 4ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))

-- 5ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          (λ hnP, hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))

-- 6ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              show false,
                from h (and.intro hP hQ) },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      λ hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))

-- 7ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))

-- 8ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))

-- 9ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  (λ h, or.elim (classical.em P)
          (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
          or.inl)
  (λ h hPQ, or.elim h
              (λ hnP, hnP (and.left hPQ))
              (λ hnQ, hnQ (and.right hPQ)))

-- 10ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
⟨λ h, or.elim (classical.em P) (λ hP, or.inr (λ hQ, h ⟨hP, hQ⟩)) or.inl,
 λ h hPQ, or.elim h (λ hnP, hnP hPQ.1) (λ hnQ, hnQ hPQ.2)⟩

-- 11ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by library_search
not_and_distrib

-- 12ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by hint
by finish

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

import tactic

variables (P Q : Prop)

-- ----------------------------------------------------

-- Ejercicio. Demostrar que

-- ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

-- ----------------------------------------------------

-- 1ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

begin

split,

{ intro h,

by_cases hP : P,

{ right,

intro hQ,

apply h,

split,

{ exact hP, },

{ exact hQ, }},

{ left,

exact hP, }},

{ intros h h',

cases h' with hP hQ,

cases h with hnP hnQ,

{ exact hnP hP, },

{ exact hnQ hQ, }},

end

-- 2ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

begin

split,

{ intro h,

by_cases hP : P,

{ right,

intro hQ,

exact h ⟨hP, hQ⟩, },

{ left,

exact hP, }},

{ rintros (hnP | hnQ) ⟨hP, hQ⟩,

{ exact hnP hP, },

{ exact hnQ hQ, }},

end

-- 3ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

( assume hP : P,

have hnQ : ¬Q,

{ assume hQ : Q,

have hPQ: P ∧ Q,

from and.intro hP hQ,

show false,

from h hPQ },

show ¬P ∨ ¬Q,

from or.inr hnQ)

( assume hnP : ¬P,

show ¬P ∨ ¬Q,

from or.inl hnP))

( assume h: ¬P ∨ ¬Q,

show ¬(P ∧ Q), from

assume hPQ : P ∧ Q,

show false, from

or.elim h

( assume hnP: ¬P,

show false,

from hnP (and.left hPQ))

( assume hnQ: ¬Q,

show false,

from hnQ (and.right hPQ)))

-- 4ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

( assume hP : P,

have hnQ : ¬Q,

{ assume hQ : Q,

have hPQ: P ∧ Q,

from and.intro hP hQ,

show false,

from h hPQ },

show ¬P ∨ ¬Q,

from or.inr hnQ)

or.inl)

( assume h: ¬P ∨ ¬Q,

show ¬(P ∧ Q), from

assume hPQ : P ∧ Q,

show false, from

or.elim h

( assume hnP: ¬P,

show false,

from hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 5ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

( assume hP : P,

have hnQ : ¬Q,

{ assume hQ : Q,

have hPQ: P ∧ Q,

from and.intro hP hQ,

show false,

from h hPQ },

or.inr hnQ)

or.inl)

( assume h: ¬P ∨ ¬Q,

show ¬(P ∧ Q), from

assume hPQ : P ∧ Q,

show false, from

or.elim h

(λ hnP, hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 6ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

( assume hP : P,

have hnQ : ¬Q,

{ assume hQ : Q,

show false,

from h (and.intro hP hQ) },

or.inr hnQ)

or.inl)

( assume h: ¬P ∨ ¬Q,

show ¬(P ∧ Q), from

λ hPQ, or.elim h (λ hnP, hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 7ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

( assume hP : P,

or.inr (λ hQ, h (and.intro hP hQ)))

or.inl)

( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 8ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

( assume h : ¬(P ∧ Q),

show ¬P ∨ ¬Q, from

or.elim (classical.em P)

(λ hP, or.inr (λ hQ, h (and.intro hP hQ)))

or.inl)

( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 9ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

iff.intro

(λ h, or.elim (classical.em P)

(λ hP, or.inr (λ hQ, h (and.intro hP hQ)))

or.inl)

(λ h hPQ, or.elim h

(λ hnP, hnP (and.left hPQ))

(λ hnQ, hnQ (and.right hPQ)))

-- 10ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

⟨λ h, or.elim (classical.em P) (λ hP, or.inr (λ hQ, h ⟨hP, hQ⟩)) or.inl,

λ h hPQ, or.elim h (λ hnP, hnP hPQ.1) (λ hnQ, hnQ hPQ.2)⟩

-- 11ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

-- by library_search

not_and_distrib

-- 12ª demostración

example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=

-- by hint

by finish