2022.1 FMC1, turma de Thanos

Pontos de participação

Homework (HW)

Leia bem o FAQ sobre hw. Note também que:

• Homeworks são atribuidos também durante as aulas e no Zulip.
• Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

2022-03-31

1. Capítulo 1.

2022-04-04

1. Capítulo 3.
2. Complete o «Introduction World» do Natural Number Game.
3. Para cada uma das proposições acima tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Evite os LEM e RAA quando possível.
   1. Proposições de dupla negaço:
      1. P ⇒ ¬¬P
      2. ¬¬P ⇒ P
   2. Comutatividade dos ∨,∧:
      1. (P ∨ Q) ⇒ (Q ∨ P)
      2. (P ∧ Q) ⇒ (Q ∧ P)
   3. Proposições de interdefinabilidade dos ⇒,∨:
      1. (P ⇒ Q) ⇒ (¬P ∨ Q)
      2. (P ⇒ Q) ⇐ (¬P ∨ Q)
      3. (P ∨ Q) ⇒ (¬P ⇒ Q)
      4. (P ∨ Q) ⇐ (¬P ⇒ Q)
   4. Proposições de contraposição:
      1. (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
      2. (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
   5. A irrefutabilidade do LEM:
      1. ¬¬(P∨¬P)
   6. A lei de Peirce e sua versão “fraca”:
      1. ((P ⇒ Q) ⇒ P) ⇒ P
      2. ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
   7. Proposições de interdefinabilidade dos ∨,∧:
      1. P∨Q ⇒ ¬(¬P∧¬Q)
      2. P∨Q ⇐ ¬(¬P∧¬Q)
      3. P∧Q ⇒ ¬(¬P∨¬Q)
      4. P∧Q ⇐ ¬(¬P∨¬Q)
   8. As leis de De Morgan para ∨,∧:
      1. ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
      2. ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
      3. ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
      4. ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
   9. Proposições de distributividade dos ∨,∧:
      1. P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
      2. P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
      3. P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
      4. P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
   10. Currificação
       1. ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
       2. ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
   11. Reflexividade da ⇒:
       1. P ⇒ P
   12. Weakening and contraction:
       1. P ⇒ (P∨Q)
       2. Q ⇒ (P∨Q)
       3. (P∧Q) ⇒ P
       4. (P∧Q) ⇒ Q
       5. P ⇒ (P∧P)
       6. (P∨P) ⇒ P
   13. As leis de De Morgan para ∃,∀:
       1. ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
       2. ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
       3. ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
       4. ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
   14. Proposições de interdefinabilidade dos ∃,∀:
       1. (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
       2. (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
       3. (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
       4. (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
   15. Proposições de distributividade de quantificadores:
       1. (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
       2. (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
       3. (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
       4. (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
       5. (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
       6. (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
       7. (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
       8. (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]

2022-04-10

• (i) instale o Lean no teu computador; (ii) configure teu editor (sendo ou um editor que presta (emacs ou neovim), ou o VS Code) para ativar o modo Lean; (iii) numa pasta no teu computador use o comando leanpkg new fmclean; (iv) baixe o arquivo logic.lean que tem os enunciados prontos, e o coloca na pasta fmclean/src; (v) substitua todos os sorry, do arquivo com código que compila para demonstrar tudo. Dúvidas nos #proofassistants e #tech, obviamente!

2022-04-11

• Demonstre os teoremas seguintes sobre os inteiros a partir dos axiomas (procure esclarecimentos no Zulip). Tome cuidado com umas das quantificações que deixei implicitas.
  1. unicidade da $(+)$-identidade (0)
  2. unicidade da $(⋅)$-identidade (1)
  3. leis de $(+)$-cancelamento
  4. unicidade dos $(+)$-inversos (opostos)
  5. 0 é um $(⋅)$-anulador: $0⋅x = 0 = x⋅0$
  6. $-(-x) = x$
  7. $(-1)x = -x$
  8. $(-x)y = -(xy) = x(-y)$
  9. $(-x)(-y) = xy$
  10. leis de $(⋅)$-cancelamento
  11. (|) é reflexiva: (∀a)[a | a]
  12. (|) é transitiva: (∀a,b,c)[a | b & b | c ⇒ a | c]
  13. qualquer inteiro divide o 0
  14. tem inteiros que o 0 divide?
  15. os $1$ e $-1$ dividem qualquer inteiro?
  16. d | a & d | b ⇒ d | ax + by
  17. a | b & b | a ⇒ a = b ?

2022-04-19

1. Estude bem o gabarito da Prova 1.1

2022-04-19

1. Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência entre:
   • NZD: (∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]
   • LC: (∀a,b,d)[ ca = cb ⇒ c = 0 ou a = b ]
2. Demonstre os teoremas seguintes (cuidado: nuns enunciados tem quantificadores implícitos!):
   1. Os quadrados de membros não nulos são positivos.
   2. 1 é positivo.
   3. $<$ é transitiva: para quaisquer $a,b,c$, se $a < b$ e $b < c$, então $a < c$.
   4. Adicionar em inegualdade: $a < b \implies a + c < b + c$.
   5. Multiplicar em inegualdade: se $c > 0$, então $a < b$ implica $ac < bc$.
   6. Lei da tricotomia: para quaisquer $a,b$, exatamente uma das seguinte é válida: $a < b$; $a = b$; $a > b$.
   7. $|ab| = |a||b|$.
   8. $|a+b| \leq |a| + |b|$.
   9. $a - x < a - y$ sse $x > y$.
   10. $a < 0 \implies (ax > ay \iff x < y)$.
   11. Se $c > 0$, então $ac < bc$ implica $a < b$.
   12. Se $x + x + x + x = 0$, então $x = 0$.
   13. Se $a < b$, então $a^3 < b^3$.
   14. Se $c \geq 0$, então $a \geq b$ implica $ac \geq bc$.
   15. $||a|-|b|| \leq |a - b|$.
   16. Se $|x| = |y|$, então $x = y$ ou $x = -y$.
3. Demonstre que a equação $x^2 + 1 = 0$ não possui resolução no incógnito $x$.
4. Demonstre que, adicionando o predicado ou relação sobre ordem e seus axiomas, o axioma NZD/LC é dispensável (ou seja, demonstre um deles como teorema).
5. Demonstre que as duas abordagens são equivalentes:
   1. $(\mathbb Z ; 0, 1, +, -, \cdot, <)$ com ${<} : \mathsf{Int} \times \mathsf{Int} \to \mathsf{Prop}$ e os axiomas:
      • os 4 aditivos, os 3 multiplicativos, distributividade, não zerodivisores
      • tricotomia da ($\lt$)
      • transitividade da ($\lt$)
      • $a < b \implies a + c < b + c$
      • se $0 < c$, então $a < b \implies ac < bc$
   2. $(\mathbb Z ; 0, 1, +, -, \cdot, P)$ com $P : \mathsf{Int} \to \mathsf{Prop}$ e os axiomas:
      • os 4 aditivos, os 3 multiplicativos, distributividade, não zerodivisores
      • $P$ é (+)-fechado
      • $P$ é (·)-fechado
      • para todo $a$, exatamente uma das seguinte é válida: $a$ é positivo; $a=0$; $-a$ é positivo.

2022-04-26

1. Usando o princípio da boa ordem (qualquer conjunto não vazio de inteiros positivos possui mínimo) demonstre: não existe inteiro $c$ tal que $0 < c < 1$.
2. O «não vazio» acima é redundante?

2022-05-02

1. Capítulo «Os inteiros»: tudo até o primeiro intervalo de problemas.

2022-05-10

1. Demonstre como teorema o princípio da indução com 2 bases.
2. Demonstre como teorema o princípio da indução forte.
3. Escreva a demonstração completa, com todos os detalhes, do Lema da Divisão de Euclides.
4. Como definirias a idéia de “tijolinho atómico” para uma operação binária?
5. Demonstre que todo inteiro positivo pode ser escrito como produtório de primos em maneira “única”. Por quê o única tá dentro de aspas?

2022-05-12

1. Demonstre o Teorema Fundamental da Aritmética
2. Demonstre o Teorema dos Sistemas Posicionais (expansão em base $b$)
3. Tente demonstrar equivalências entre as afirmações seguintes para um p≠0:
   • (i) Irreducible(p) (⇐≝⇒ (∀a,b)[ p = ab ⇒ a unit ou b unit ])
   • (ii) Primo(p) (⇐≝⇒ divs(p) = { 1, -1, p, -p })
   • (iii) Prime(p) (⇐≝⇒ (∀a,b)[ p | ab ⇒ a unit ou b unit ])

2022-05-21

1. Capítulo «Os inteiros»: até o 3o intervalo de problemas.
2. Jogue o NNG. Tente completar o mais rápido possivel. Veja o FAQ relevante também.

2022-05-28

1. Capítulo «Os naturais; recursão; indução»: até o 1o intervalo de problemas.
2. (i) instale a Haskell no teu computador; (ii) Completa o getting started e o first steps do ghcup; (iii) configure teu editor (sendo ou um editor que presta (emacs ou neovim), ou o VS Code) para integrar com Haskell. Dúvidas nos #programming e #tech, obviamente!
3. Brinque com Elm, especialmente se tu tens interesse em web-devel ou se tu tá sofrendo escrevendo JavaScript (mesmo se não percebes tal sofrimento).

2022-05-31

1. Olhando para as funçoẽs binárias e famosas que definimos até agora (adição, multiplicação, exponenciação), perceba que tem um “padrão”. Use isso para definir a “próxima” operação. Denote por ⇈.
2. Defina a função Pd : Nat → Nat de “predecessor”, onde consideramos que o predecessor de zero é o próprio zero mesmo.
3. Defina a função ∸ : Nat → Nat → Nat que comporta como subtração, mas caso que o resultado era pra ser negativo, retorna O mesmo.
4. Defina as funções:
   • fact : Nat → Nat
   • fib  : Nat → Nat
   • div  : Nat × Nat → Nat × Nat
   • quot : Nat × Nat → Nat
   • rem  : Nat × Nat → Nat
   • mod  : Nat → Nat → Nat que dou de presente: mod m n = rem (n,m)
   • gcd  : Nat × Nat → Nat
   • lcm  : Nat × Nat → Nat
   • comb : Nat → Nat → Nat
   • perm : Nat → Nat → Nat
5. Como definirias um tipo de dados Bool para os booleanos?

2022-06-03

1. Até a §«Demonstrando propriedades de naturais sem indução».

2022-06-04

1. Até a §«Indução».

2022-06-09

1. §«Ordem nos naturais»
2. Demonstre que a (≤) : Nat → Nat → Prop é:
   • reflexiva
   • transitiva
   • antissimétirca
   • total
3. Demonstre que todo Nat é par ou ímpar.
4. Demonstre a corretude das:
   • leq      : Nat → Bool
   • isMul₃   : Nat → Bool
5. Defina as:
   • length   : ListNat → Nat
   • elem     : Nat → ListNat → Bool
   • sum      : ListNat → Nat
   • product  : ListNat → Nat
   • (++)     : ListNat → ListNat → ListNat
   • reverse  : ListNat → ListNat
   • min      : Nat → Nat → Nat
   • max      : Nat → Nat → Nat
   • allEven  : ListNat → Bool
   • anyEven  : ListNat → Bool
   • allOdd   : ListNat → Bool
   • anyOdd   : ListNat → Bool

2022-06-11

1. Defina as:
   • ifthenelse  : Bool → α → α → α
   • isZero      : Nat → Bool
   • allZero     : ListNat → Bool
   • anyZero     : ListNat → Bool
   • addNat      : Nat → ListNat → ListNat
   • multNat     : Nat → ListNat → ListNat
   • expNat      : Nat → ListNat → ListNat
   • enumFromTo  : Nat → Nat → ListNat
   • enumTo      : Nat → ListNat
   • take        : Nat → ListNat → ListNat
   • drop        : Nat → ListNat → ListNat
   • elemIndices : Nat → ListNat → ListNat
   • pwAdd       : ListNat → ListNat → ListNat
   • pwMult      : ListNat → ListNat → ListNat
   • isSorted    : ListNat → Bool
   • filterEven  : ListNat → ListNat
   • filterOdd   : ListNat → ListNat
   • minimum     : ListNat ⇀ Nat
   • maximum     : ListNat ⇀ Nat
   • isPrefixOf  : ListNat → ListNat → Bool
   • mix         : ListNat → ListNat → ListNat
   • intersperse : Nat → ListNat → ListNat
2. Demonstre os teoremas (escolhe algo interessante para botar nos ??)
   1. (∀xs,ys:ListNat)        [ length (xs ++ ys) = ?? ]
   2. (∀xs,ys:ListNat)        [ reverse (xs ++ ys) = ?? ]
   3. (∀xs,ys:ListNat)        [ sum (xs ++ ys) = ?? ]
   4. (∀xs,ys:ListNat)        [ product (xs ++ ys) = ?? ]
   5. (∀n:Nat)(∀xs,ys:ListNat)[ addNat n (xs ++ ys) = ?? ]
   6. (∀ℓ:ListNat)            [ reverse (reverse ℓ) = ?? ]
   7. (∀ℓ:ListNat)            [ length (reverse ℓ) = ?? ]
   8. (∀ℓ:ListNat)            [ length (filterEven ℓ ++ filterOdd ℓ) = ?? ]
   9. (∀ℓ:ListNat)            [ reverse (filterEven ℓ) = ?? ]
   10. (∀n:Nat)(∀ℓ:ListNat)    [ length (addNat n ℓ) = ?? ]
   11. (∀n:Nat)(∀ℓ:ListNat)    [ sum (addNat n ℓ) = ?? ]
   12. (∀n:Nat)(∀ℓ:ListNat)    [ sum (multNat n ℓ) = ?? ]
   13. (∀n:Nat)(∀ℓ:ListNat)    [ product (multNat n ℓ) = ?? ]
   14. (∀n:Nat)(∀ℓ:ListNat)    [ product (expNat n ℓ) = ?? ]
   15. (∀n:Nat)(∀ℓ:ListNat)    [ isSorted (addNat n ℓ) = ?? ]
   16. (∀ℓ:ListNat)            [ isEven (product ℓ) = anyEven ℓ ]
   17. (∀ℓ:ListNat)            [ isEven (sum ℓ) = isEven (length (filterOdd ℓ)) ]
   18. (∀ℓ:ListNat)            [ isZero (sum ℓ) = ?? ]
   19. (∀ℓ:ListNat)            [ isZero (product ℓ) = ?? ]
   20. Associatividade da (++)
   21. [] é uma (++)-identidade
3. Pense em mais propriedades, enuncie, e demonstre!
4. Defina a (<) : Nat → Nat → Prop e sua internalização, e demonstre a sua corretude.

2022-06-14

1. Defina as:
   • and        : List Bool → Bool
   • or         : List Bool → Bool
   • replicate  : Nat → α → List α
   • map        : (α → β) → List α → List β
   • concat     : List (List α) → List α
   • a generalização all das: allZero, allEven, allOdd
   • a generalização any das: anyZero, anyEven, anyOdd
   • a generalização filter das: filterEven, filterOdd
   • a generalização pointwise das: pwAdd, pwMult
   • a generalização fold das: sum, product, and, or, concat
2. Demonstre:
   1. (∀n,m:Nat)(∀ℓ:List Nat)[ addNat (n + m) ℓ = ?? ]
   2. (∀n,m:Nat)(∀ℓ:List Nat)[ multNat (n · m) ℓ = ?? ]

2022-06-19

1. Defina tipos para cada um estilo de árvore que a gente viu nas aulas
2. Defina funções treemap, que seriam para seus tipos de arvores o que a map é para as listas.
3. Defina as:
   • takeWhile   : (α → Bool) → List α → List α
   • dropWhile   : (α → Bool) → List α → List α
   • head        : List α → Maybe α
   • tail        : List α → Maybe (List α)
   • init        : List α → Maybe (List α)
   • last        : List α → Maybe α
   • pick        : Nat → List α → Maybe α
   • findFirst   : α → List α → Maybe Nat
   • find        : α → List α → List Nat

2022-06-23

1. Defina tipos para representar expressões de aritmética sem variáveis, expressões de aritmética com variáveis, e expressões de lógica proposicional
2. Defina as:
   • splitAt       : Nat → List α → (List α × List a)
   • flip          : Tree α → Tree α 
   • findFirstTree : α → Tree α → Maybe (List Nat)
   • findTree      : α → Tree α → List (List Nat)
   • sumTree       : Tree Nat → Nat
3. Demonstre:
   1. (∀t:Tree α)                [ height t ≤ length (flatten t) ]
   2. (∀t:Tree α)                [ flip (flip t) = ?? ]
   3. (∀t:Tree α)                [ flatten (flip t) = ?? ]
   4. (∀t:Tree α)                [ height (flip t) = ?? ]
   5. (∀t:Tree α)(∀f:α→β)        [ height (fmap f t) = ?? ]
   6. (∀t:Tree α)(∀f:α→β)        [ height (fmap f t) = ?? ]
   7. (∀t:Tree α)(∀f:α→β)        [ fmap f (flip t) = ?? ]
   8. (∀ℓ:List α)                [ fmap id ℓ = ?? ]
   9. (∀ℓ:List α)(∀f:α→β)(∀g:β→γ)[ fmap g (fmap f ℓ) = ?? ]
   10. (∀t:Tree α)(∀f:α→β)(∀g:β→γ)[ fmap g (fmap f t) = ?? ]

2022-06-25

1. Demonstre:
   1. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ drop n (drop m ℓ) = ?? ]
   2. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ take n (take m ℓ) = ?? ]
   3. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ take n (drop m ℓ) = ?? ]
   4. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ drop n (take m ℓ) = ?? ]
   5. (∀f:α→β)(∀p:β→Bool)        [ filter p ∘ map f = map f ∘ filter (p ∘ f) ]
   6. (∀f:α→β)(∀g:β→γ)           [ map g ∘ map f = map (g∘f) ]

2022-06-26

1. Qual seria uma melhor tipágem para a pw : (α → α → α) → List α → List α → List α?
2. Defina as:
   • zip       : List α → List β → List (α × β)
   • unzip     : List (α × β) → (List α × List β)

2022-07-02

1. Investigue a (ir)racionalidade do ³√2
2. Generalize para ᵏ√n
3. Resolva todos os exercícios da §101.
4. Resolva o Problem Set 2 de 2021.2.

2022-07-04

1. Resolva todos os exercícios da §«Primeiros passos».
2. Resolva todos os exercícios da §«Ordem e positividade».

2022-07-11

1. Resolva tudo até o §«Mínima e Máxima»

2022-07-16

1. Demonstre a unicidade dos limites
2. Demonstre que a seqüência ( (-1)ⁿ )ₙ não tende a nenhum ℓ

2022-07-17

1. Θ: Qualquer seqüência constante é convergente
2. Θ: Qualquer seqüência eventualmente constante é convergente
3. Θ: Qualquer seqüência eventualmente constante é cotada
4. Θ: Qualquer seqüência convergente é cotada
5. Θ: (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → a + b
6. Θ: (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ab
7. Θ: (aₙ)ₙ → a & (cₙ)ₙ → c & (aₙ)ₙ ≤ (bₙ)ₙ ≤ (cₙ)ₙ ⇒ ??
8. ?: Seja (aₙ)ₙ seqüência de reais. (aₙ)ₙ convergente ⇒ (∀ε>0)(∃N)(∀n,m≥N)[d(aₙ,aₘ) < ε]?
9. ?: Seja (aₙ)ₙ seqüência de reais. (∀ε>0)(∃N)(∀n,m≥N)[d(aₙ,aₘ) < ε] ⇒ (aₙ)ₙ convergente?
10. ?: Seja (aₙ)ₙ seqüência de reais. (∀ε>0)(∃N)(∀n,m≥N)[d(aₙ,aₘ) < ε] ⇒ (aₙ)ₙ cotada?
11. ?: Seja (aₙ)ₙ seqüência de reais. (aₙ)ₙ cotada por cima e crescente ⇒ (aₙ)ₙ convergente?

2022-07-19

1. Θ: $\{a_n\}_n \subseteq {\mathbb R}_{\mathbb Z}$ e $(a_n)_n$ convergente ⇒ ??
2. Θ: (aₙ)ₙ crescente e cotada por cima ⇒ ??

Histórico

2022-03-28: Aula 01: Overview; tipos

• tipos e type errors
• proposiões vs objetos
• sintaxe vs semântica

2022-03-30: Aula 02: Definições

• comandos vs proposições
• se..então.. vs como..logo..
• variáveis ligadas vs livres
• escopos de variáveis
• sombreamento (shadowing) de variáveis
• abuso de gerúndios, vírgula mágica, etc.
• definição e seu contexto
• açúcar sintáctico, abreviações
• convenção: notação infixa
• os conectivos ⇐,⇒,⇔

2022-04-01: Aula 03: Tipos; definições; linguagem de demonstrações

• = vs ⇔
• «def»
• intensão vs extensão
• o resto dos conectivos para nossa linguagem de demonstrações
• escolha boa de variável, variável fresca
• bairros de variáveis

2022-04-04: Aula 04: Tipos; linguagem de demonstrações

2022-04-06: Aula 05: Os inteiros (1)

• Proposição mais forte vs mais fraca que outra
• Necessário e suficiente, se e somente se
• P ⇒ ¬¬P
• ¬¬P ⇒ P
• RAA (Reductio ad Absurdum)
• LEM (Law of Excluded Middle)
• Tentativa de demonstrar: para todo a inteiro, a divide a
• Axiomas sobre os inteiros $(\mathbb Z;+,\cdot,-,0,1)$.
• Operações primitivas vs definidas: a operação binária da subtração

2022-04-08: Os inteiros (2)

• As primeiras conseqüências dos axiomas

2022-04-11: Aula cancelada

2022-04-13: Aula cancelada

2022-04-15: Feriado

2022-04-18: Prova 1.1

2022-04-20: Os inteiros (3)

• Mini-sermão sobre a prova 1.1
• Operações e relações primitivas vs. definidas
• Axiomas sobre ordem: duas maneiras de axiomatizar
• Conjunto fechado sob operação
• A ≤ nos naturais é definível
• Como tratar um subconjunto como predicado unário
• O módulo (absolute value) |_| : Int → Int

2022-04-22: "Feriado"

2022-04-25: Os inteiros (4)

• Recap
• Como demonstrar a indemonstrabilidade de proposições
• 1 é positivo
• A indemonstrabilidade do 0 ≠ 1

2022-04-27: Os inteiros (5)

• Dica sobre como enxergar alvos
• Exemplo: (∀a)[(-1)a = -a]
• A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
• Exemplo: (∀a)[0a = a]
• Transitividade da $\lt$
• Como escrever cálculos corretamente numa demonstração

2022-04-29: Os inteiros (6)

• Mais sobre a independência duma proposição: indemonstrabilidade e irrefutabilidade
• Umas propriedades do valor absoluto
• Princípio da boa ordem ($\mathbb Z_{>0}$ é bem ordenado)
• Como usar o PBO na prática
• Não existe inteiro estritamente entre 0 e 1

2022-05-02: Os inteiros (7)

• Como escrever definições
• Duas maneiras que uma definição pode ser errada
• Quando precisamos demonstrar algo para justificar uma definição ou uma notação
• Existência e unicidade
• Duas maneiras diferentes para conseguir unicidade
• o mínimo dum conjunto, quando existe é único
• uso de lemmas numa demonstração

2022-05-04: Os inteiros (8)

• como definir «ser fechado sob uma operação n-ária (para n=1,2)
• a notação set-builder: como ler e escrever, e como não ler e como não escrever
• um pleno «tal que» é capaz de destruir uma frase e torná-la pior-que-errada
• O que significa «_ ∈ { 3x | x ∈ ℤ }»
• A diferença intensional entre os extensionalmente iguais conjuntos: {x ∈ A | x ∈ B} e {x ∈ B | x ∈ A}
• o 3ℤ é fechado sob adição e subtração
• como generalizar para o mℤ
• Lema de divisão de Euclides: enunciado
• a justificativa «pela escolha de»
• Números, numerais, dígitos
• O logaritmo como tamanho de númerais melhor que o length deles como strings

2022-05-06: Os inteiros (8)

• Princípio da indução para os inteiros: se $S$ é (+1)-fechado e $1 \in S$, então $\mathbb Z_{>0} \subseteq S$
• Outras versões de PBO e de Indução e como obtê-las “hackeando” as originais

2022-05-09: Os inteiros (9)

• Regras de inferência; como escrever, o que significa, como ler de cima pra baixo e de baixo pra cima
• Indução com mais que uma base
• Indução forte (“course-of-values”)
• Lema de Divisão de Euclides e sua demonstração usando o PBO
• Quebrando os inteiros em tiholinhos atômicos usando como cimento: (i) adição; (ii) multiplicação
• Enunciado do Teorema Fundamental de Aritmética (fatorização única)

2022-05-11: Os inteiros (10)

• Definição de invertível
• Definição de irredutível
• Definição de primo
• Explicação intuitiva sobre como sistemas posicionais funcionam
• Esboço de demonstração do teorema dos sistemas posicionais (expansão em base $b$): qualquer inteiro $b>1$ serve como base para um sistema posicional de numerais para inteiros.
• Esboço do Teorema Fundamental de Aritmética

2022-05-13: Os inteiros (11)

• generalização da palavra “maior” para outras ordens
• diagrama Hasse para os $\mathbb{Z}_{\geq 0}$
• mdc: definição
• O conjunto {ax + by | x ∈ ℤ, y ∈ ℤ} é fechado sob adição e subtração
• Existência de mdc

2022-05-16: Os inteiros (11)

• os coeficientes Bézout
• mdc e mmc e demonstrações das suas propriedades
• Algoritmo de Euclides: corretude e terminação
• Algoritmo estendido de Euclides

2022-05-18: Os inteiros (12)

• Algo que parece LEM, mas não é
• Lema de Euclides e sua generalização
• Dum lemma para uma ideia: n² (im)par ⇔ n (im)par

2022-05-20: Os inteiros (13)

• Congruência módulo um inteiro e demonstrações das suas propriedades
• Aritmética modular e propriedades do $\mathbb Z / m\mathbb Z$
• Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva
• (·)-inversos módulo um inteiro m

2022-05-23: Os inteiros (14)

• Invertibilidade módulo $m$
• Unicidade de inverso módulo $m$ e o que significa
• Uns casos extremos: módulo 1, módulo 0
• Algumas conjecturas da teoria dos números

2022-05-25: Os inteiros (15)

• Mais conjecturas
• Revisão da invertibilidade e unicidade de inversos módulo um inteiro
• Densidade de primos e gaps

2022-05-27: Prova 1.3; Recursão, Indução (1): Nat

• 4 maneiras de definir um tipo de dados recursivamente
• O tipo Nat
• Naturais vs Nats
• Linguagem vs Metalinguagem; Variáveis vs Metavariáveis
• Como mostrar que algo é um Nat
• Regras de inferência e lida de cima para baixo e de baixo para cima
• Casamento de padrão com expressão
• Definição da adição para os Nats

2022-05-30: Recursão, Indução (2): Nat

• associatividade sintáctica vs associatividade
• currificação
• notação: prefixa, postfixa, infixa, mixfixa
• valores canônicos
• construtor vs função
• o presente da recursão
• definições: multiplicação, exponenciação, double
• o uso de lemmas: m-idR, e-idR
• umas demonstrações simples
• ∀: como usar
• ∀: como atacar
• Recursão vs tijolo
• redexes

2022-06-01: Recursão, Indução (3): Nat

• AST (Abstract Syntax Tree)
• Parser e Lexer
• qual resultado incompleto é melhor?
• estratégia de evaluação vs precedência de operador
• notação de aplicação de função por espaço: f x
• sua associatividade sintáctica à esquerda: f x y z ≡ ((f x) y) z
• aplicação parcial
• parity = mod 2
• casamento de padrões: o que é um padrão mesmo?
• escolhendo o padrão na direita duma equação para substituir na direção (←)
• Θ. Associatividade da (+)
• A disjunção escondida em cada Nat.
• ∃: como usar
• ∨: como usar
• tem como continuar a demonstração?
• escolhendo variáveis com «linhas»: x’, x’’, etc.
• igualdade entre Nats
• o problema que temos demonstrando esse teorema

2022-06-03: Recursão, Indução (4): Nat, Bool, Weekday

• Como definir o tipo de dados Bool e suas operações
• Como representar predicados sobre os naturais (Nat → Prop, Nat→Nat→Prop, etc.) como se fossem funções que retornam Bool.
• Mais tipos de dados simples: Weekday
• A regra de inferência Ind-Nat-φ. (Onde φ : Nat → Prop.)
• Demonstração por indução
• O presente de recursão vs o presente da indução
• Definição por recursão vs Demonstração por indução
• A associatividade da (+): duas demonstrações por indução diferentes.

Para quem perdeu esta aula, a última parte dela é parecida com esta aula gravada de FMC1-2019.2

2022-06-06: Recursão, Indução (5): Nat, Bool

• Análise das duas demonstrações da (+)-associatividade
• Como usar o underscore (_) como «variável sem nome» num padrão.
• ev, od : Nat → Bool
• Recursão mútua
• Relações vs funções-com-codomínio-Bool
• (≤) : Nat → Nat → Prop
• leq : Nat → Nat → Bool
• A corretude da leq

2022-06-08: Prova 2.1; Recursão, Indução (6): Nat, Bool, Unit, ListNat

• isMul₃ : Nat → Bool vs isMul : Nat → Nat → Bool
• isMul₃ : Nat → Bool vs mod₃ : Nat → Nat
• O tipo Unit com seu único habitánte/construtor: ⋆ : Unit
• Uma primeira idéia para o tipo Int, e uns problemas
• Como implementar listas: ListNat
• Os construtores Empty (ou Nil) e Cons

2022-06-10: Recursão, Indução (7): Nat, Bool, Unit, ListNat

• Podemos implementar o Prop como um data type?
• A idéia de internalizar uma noção
• Tipos dependentes: comparação e teaser
• O problema com os head e tail
• Runtime Error vs. Honesty Error vs. Type error
• o tipo de error
• o tipo de id
• polimorfismo de tipos
• Idéia ruim: usar um valor arbitrário para o head []
• Gambiarra 1: safeHead : ListNat → ListNat
• Gambiarra 2: safeHead : ListNat → Bool × Nat
• Gambiarra 3: defaultHead : Nat → ListNat → Nat
• Construtores vs Destrutores
• Definições de sum : ListNat → Nat e product : ListNat → Nat
• Um benefício da estratégia preguiçosa
• Como escolher o valor certo para o sum [] e o product []
• Defina a addNat : Nat → ListNat → ListNat

2022-06-13: Recursão, Indução (8): Nat, Bool, Unit, List α

• O conceito de «respeitar uma propriedade».
• Do $\mathrm{Ind}^{\mathtt{Nat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$.
• Do $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{α}}_{\varphi}$.
• Θ: (∀xs,ys:ListNat)[ length (xs ++ ys) = length xs + length ys ]
• Do tipo ListNat para o tipo List Nat
• List : Type → Type
• Construtores de tipos (type constructors) vs Construtores de valores (data constructors)
• type variables vs data variables
• polimorfismo: de lengthNat : List Nat → Nat para length : List α → Nat
• abstração de ordem superior: de addNat : Nat → List Nat → List Nat para mapNat : (Nat → Nat) → List Nat → List Nat
• abstração de ordem superior: de mapNat : (Nat → Nat) → List Nat → List Nat para map : (α → β) → List α → List β

2022-06-15: Recursão, Indução (9): Nat, Bool, Unit, List α

• mais uma análise entre a definição dum tipo de dados inductivo e o princípio da indução associado a ele
• “inventando” propriedades dos nossos programas para demonstrar, e as demonstrando
• Maybe
• as versões não-gambiarrosas de head e tail
• vários tipos de árvores freqentemente usados em computação

2022-06-22: Recursão, Indução (9): Nat, Bool, Unit, List α, Tree α

• NonEmptyList α
• O principio da indução para um tipo de arvores
• height
• flatten
• map, mapTree
• Functors, fmap, deriving ( Functor )
• takeWhileTree
• Either α β
• O que usar para representar erros em vez de gambiarras

2022-04-22: "Feriado"

2022-06-24: Recursão, Indução (10)

• Sintaxe vs semântica
• ArEx, ArExV
• Fórmulas de Lógica Proposicional
• Numerais binários
• Composição (∘)
• fmap g (fmap f xs) = fmap (g ∘ f) xs

2022-06-25: Reposição de 3 aulas

• Preguiça e infinidade
• enumFrom, infty, ones
• primes
• pw (zipWith)
• fibs
• fold, fold1
• sepBy
• let-in expressions
• Ordenação: Ord, sorted, quicksort, mergesort
• igualdade entre funções
• Recursão aninhada
• Ackermann

2022-06-27: Prova 2.3

2022-06-29: IRI; IDMb

• insertAt e recursão/indução bem-fundada: um teaser prático
• Os números: naturais, inteiros, racionais, reais
• A irracionalidade do √2
• Lemma-chave: x² par ⇒ x par
• A “existência” do √2, pelo teorema pithagoreano
• Generalização para outros √n
• Buracos na linha dos racionais
• A linha continua dos reais
• Primeiros axiomas para o (ℝ;+,·,-,0,1,<)

2022-07-01

• A irracionalidade de √3
• Como abstrair para ganhar um teorema mais geral
• A unicidade da identidade aditiva

2022-07-04

• Reposição remota de aula [video]
  • Teorema de Fermat
  • O «sonho de calouro»
  • Teorema de Fermat: demonstração
  • um sistema de duas congruências
    • como achar inversos
    • únicidade
• Reposição remota de aula [video]
  • Fermat e potências positivas de números módulo m
  • A função φ de Euler
  • 4 teoremas sobre φ
  • φ(pᵃ) = pᵃ-pᵃ⁻¹
  • n ≥ 3 ⇒ φ(n) par
• Exercícios sobre os números reais envolvendo a parte algébrica e teoremas sobre a ordem

2022-07-06

• igualdade não é exatamente simétrica
• como interpretar uma igualdade no alvo aproveitando definições e unicidades
• subconjuntos notáveis de reais; type coercing e type casting
• umas demonstrações dos primeiros teoremas sobre reais
• notação sobre intervalos e seqüências

2022-07-08

• valor absoluto e sua interpretação geométrica
• demonstração de (∀a,b,c)[ |a - c| ≤ |a - b| + |b - c| ]
• como definir uma distância nos reais, e suas propriedades
• a desigualdade triangular e sua interpretação geométrica
• epsilons e seus usos em matemática
• conjuntos: o que significa em saber qual é um conjunto
• como definir conjuntos e suas operações
• o que significa (=) entre conjuntos
• as relações (⊆) e (⊇)
• Como generalizar as operações binárias ∪,∩ para serem aplicáveis numa coleção arbitrária de conjuntos

2022-07-11

• como definir conjuntos e suas operações
• o que significa (=) entre conjuntos
• Como generalizar as operações binárias ∪,∩ para serem aplicáveis numa coleção arbitrária de conjuntos
• Seqüências: notação, igualdade
• seqüência limitada superiormente/inferiormente
• seqüência crescente/descendente

2022-07-13

• intervalos abertos e fechados: uma seqüência de abertos com interseção fechada e o dual: uma seqüência de fechados com união aberta
• ε-bola

2022-07-15

• Unicidade de mínima
• (≤)-bounded ⇔ (<)-bounded
• Frases legais do ♡:
  • eventualmente
  • ε-perto
  • ε-bola, ε-bairro/vizinhança
• Igualdades que não são igualdades
• Definição de limite de seqüência
• Unicidade dos limites
• x : α vs x ∈ A

2022-07-16: Reposição de aula

• Aplicações da teoria dos números em criptografia
• Quantificadores e estratégia vencedora em jogos
• Θ: Qualquer seqüência constante é convergente
• Θ: Qualquer seqüência eventualmente constante é convergente
• Θ: Qualquer seqüência eventualmente constante é cotada
• Θ: Qualquer seqüência convergente é cotada

2022-07-18

• Quantificadores e estratégia vencedora em jogos
• cotas superiores / upper bounds / majorantes
• cotas inferiores / lower bounds / minorantes
• melhor cota superior/inferior
• least upper bound (lub) / suprémo / supremum (sup) / join
• greatest lower bound (glb) / ínfimo / infimum (inf) / meet
• O último axioma sobre os reais (axioma da completude)

2022-07-20

• “Escolhendo epsilons”
• Umas conseqüências da completude
• O sistema posicional de numerais para os reais

2022-07-22: Prova 3.2

Futuro (fluido)