2.7. Exercícios
Prove cada enunciado em Lean, substituindo sorry por uma prova. Baixe o arquivo de exercícios Lecture02.lean e abra-o no VS Code. O arquivo já contém as definições de Set, pertinência, inclusão, união e interseção.
Exercício 1. O quantificador universal distribui sobre a implicação.
theorem exercise1 (α : Type) (P Q : α → Prop)
(h : ∀ x, P x → Q x) (hP : ∀ x, P x) : ∀ x, Q x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhP:∀ (x : α), P x⊢ ∀ (x : α), Q x
All goals completed! 🐙
Exercício 2. O quantificador existencial distribui sobre a disjunção.
theorem exercise2 (α : Type) (P Q : α → Prop) :
(∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ (∃ x, Q x) := α:TypeP:α → PropQ:α → Prop⊢ (∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ ∃ x, Q x
All goals completed! 🐙
Exercício 3. Elimine a hipótese existencial e então instancie a universal na testemunha.
theorem exercise3 (α : Type) (P : α → Prop) (Q : Prop)
(h : ∃ x, P x → Q) (hP : ∀ x, P x) : Q := α:TypeP:α → PropQ:Proph:∃ x, P x → QhP:∀ (x : α), P x⊢ Q
All goals completed! 🐙
Exercício 4. A inclusão é transitiva.
theorem exercise4 (α : Type) (s t u : Set α)
(hst : s ⊆ t) (htu : t ⊆ u) : s ⊆ u := α:Types:Set αt:Set αu:Set αhst:s ⊆ thtu:t ⊆ u⊢ s ⊆ u
All goals completed! 🐙
Exercício 5. A interseção distribui sobre a união.
theorem exercise5 (α : Type) (s t u : Set α) :
s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := α:Types:Set αt:Set αu:Set α⊢ s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u
All goals completed! 🐙