2022.2 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-08-23 (Intro)

1. Capítulo 1.

2022-08-25 (Intro)

1. Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também.
2. Capítulo 3.

2022-08-25 (Intro)

1. Demonstre o teoremas seguintes escrevendo demonstrações “low-level”, mantendo também os DADOS/ALVO atualizados com cada linha da sua demonstração:
   1. Θ. Todo inteiro divide ele mesmo.
   2. Θ. Para quaisquer inteiros a,b, se a divide b e b divide 0, então a divide 0 ou 1 divide b.
   3. Θ. Seja a inteiro. Para quaisquer inteiros x,y, se a | x e a | y, então a | x + y.
   4. Θ. Seja a inteiro. Para todo inteiro x, se a | x, então para todo inteiro u, a | ux.
   5. Θ. Para quaisquer inteiros a,x,y,r,s, se a | x e a | y, então a | rx + ys.
2. Para cada um dos ¬,⇒,&,ou,⇔,∀,∃,= pense como que pode ser usado (sendo nos DADOS) ou atacado (sendo no ALVO). Escreva os comandos correspondentes e para cada um deles, esclareça: qual é o efeito no tabuleiro da demonstração (tanto na parte dos DADOS quanto no ALVO), como e quando é que tal comando pode ser executado.

2022-08-29 (Intro)

1. Para cada uma das proposições acima tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Se colar em algum sem conseguir fechar, mostre teu progresso no zulip e peça ajuda; enquanto isso, continua para a próxima!
   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)]
2. Demonstre os teoreams em cima no Lean (veja o FAQ!): baixe o arquivo logic.lean que tem os enunciados prontos, e o coloca na pasta fmclean/src; substitua todos os sorry, do arquivo com código que compila para demonstrar tudo. Dúvidas nos #proofassistants e #tech, obviamente!

2022-09-02 (IDMa)

1. Cap «Os inteiros», «§. Primeiros passos»
2. 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-09-06 (IDMa)

1. Cap «Os inteiros», até «§. Conjuntos fechados sobre operações»
2. Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência entre:
   • (Z-NZD): (∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]
   • (Z-LC): (∀a,b,c)[ ca = cb ⇒ c = 0 ou a = b ]

2022-09-09 (IDMa)

1. Demonstre que as duas abordagens vistas na aula são equivalentes:
   • (ℤ;0,1,+,-,·,<) + (ZO-Trans) + (ZO-A) + (ZO-M) + (ZO-Tri)
   • (ℤ;0,1,+,-,·,Pos) + (ZP-ACl) + (ZP-MCl) + (ZP-Tri)
2. Cap «Os inteiros», até «§. Ordem e positividade»

2022-09-12 (IDMa)

1. Considere os inteiros das peimeiras aulas, até a especificação (2/5).
   1. Demonstre que o 0≠1 não é demonstrável a partir desses axiomas.
2. Considere o (A; ♡, κ) com a especificação seguinte, e demonstre que não tem como demonstrar a Comutatividade de (♡), nem como refutá-la.
   • (♡) : A × A → A
   • κ : A
   • (Ass) : (∀a,b,c)[ (a ♡ b) ♡ c = a ♡ (b ♡ c) ]
   • (IdR) : (∀a)[ a ♡ κ = a ]

2022-09-15 (IDMa)

1. Até o «§. Valor absoluto»
2. Π4.1, Π4.2, Π4.3, Π4.4

2022-09-16 (IDMa)

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?
3. Demonstre que um conjunto vazio é subconjunto de qualquer conjunto.
4. Demonstre ou refute: «o Ø é bem-ordenado».
5. Até o primeiro intervalo de problemas.
6. Demonstre ou refute: «qualquer conjunto de inteiros X finito é bem ordenado».
7. Escreva os comandos que temos sobre ataques e usos dos conectivos (∧),(∨),(⇒) como regras de inferência.
8. Demonstre como teorema o princípio da indução.
9. Demonstre como corolário o princípio da indução com 2 bases.

2022-09-23 (IDMa)

1. Resolva em condições de prova as provas seguintes:
   1. Prova 2.X de 2019.2
   2. Prova 2.Y de 2019.2
   3. Prova 2.Z de 2019.2
2. Resolva em condições tranqüilas as mesmas provas.

2022-09-26 (IDMa)

1. Escreva sozinho a definição de m.d.c.
2. Troque o que precisa trocar para virar a definição de mínimo.
3. Troque o que precisa trocar para virar a definição de máximo.
4. Troque o que precisa trocar para virar a definição de m.m.c.
5. Dados inteiros a,b, demonstre a existência dum m.d.c. deles, e mostre que ele pode ser escrito como combinação linear dos a,b.
6. Demonstre as propriedades básicas dum m.d.c., que denotamos aqui simplesmente por (_,_), exceto uma, que é refutável (e logo refute e depois obviamente tente a ajustar para virar demonstrável, e demonstre–phew!):
   1. (a,b) = (a,-b) = (-a,b) = (-a,-b)
   2. (a,a) = ?
   3. (a,0) = ?
   4. (a,1) = ?
   5. (a,b) = (b,a)
   6. ((a,b),c) = ?
   7. (a,b) = (a, a + b)
   8. (a,b) = (a, a - b)
   9. (ca,cb) = c(a,b)
   10. (uv,a) = (u,a)(v,a)
   11. (a,b) = (b, rem(a,b))
7. Demonstre: Invertible(x) ⇔ Unit(x)
8. Demonstre: Irreducible(x) ⇔ Prime(x)
9. Demonstre ou refute: apra quaisquer primos distintos p,q, pq | n² ⇒ pq | n.
10. 🚀 Bora viajar legal!
    1. Num universo de conjuntos (por exemplo no Set(Int)) considere a mesma definição de m.d.c., mas essa vez usando como guia a ordem de (⊆). Qual conceito definiu? O que acontece se virar as direções? (⊇).
    2. Tendo P, Q : Prop, escrevemos P ⊢ Q para a (meta)proposição «Dado a P, podemos demonstrar a Q.». No universo de proposições, mostre que (⊢) é uma pré-ordem. Qual seria o “m.d.c.” de duas props, e qual o “m.m.c” delas?

2022-09-28 (IDMa)

1. Troque o (Z-PBO) pelo princípio da indução (Z-Ind). Demonstre o (Z-PBO).

2022-09-29 (IDMa)

1. 💻 Na aula foi óbvio que ninguém merece fazer contas na mão, mesmo utilizando um algoritmo eficiente. Mas somos programadores—right?—e logo: programe na tua linguagem favorita uma função que dados dois inteiros a, b, retorna seu m.d.c. d, e também coeficientes Bézout x,y tais que d = ax + by. Dica: caso que tua linguagem favorita não seja a Haskell, troque e tente novamente.
2. L: a ≥ b > 0 ⇒ r < a/2. (Aqui a/2 é o quot(a,2).)
3. Θ: Para todo n ≥ 1, e quaisquer inteiros a > b > 0, se o algoritmo de Euclide precisa n passos (divisões) para terminar, então a ≥ fib(n+2) e b ≥ fib(n+1), onde fib(i) é o i-ésimo número Fibonacci.

2022-09-30 (IDMa)

1. Demonstre o que faltou para a demonstração do Lemma de Bézout: p irredutível & p ∤ a ⇒ (p,a) = 1.
2. Como podemos generalizar o Lemma de Bézout sobre p’s não-necessariamente-irredutíveis?
3. Demonstre o Teorema Fundamental da Aritmética
4. Dado as «formas canônicas» de inteiros a e b, descreva os m.d.c. e m.m.c. deles
5. Demonstre que dado um inteiro x, se não há primos divisores de 2 até ⌊√x⌋, então x é primo

2022-10-05 (IDMa)

1. Seja n > 0. Ache n inteiros consecutivos tais que nenhum deles é primo.
2. Seja m inteiro. Demonstre que (≡ₘ) é uma relação de equivalência: (i) reflexiva; (ii) transitiva; (iii) simétrica
3. Seja m inteiro. Demonstre que (≡ₘ) é uma congruência para a estrutura (ℤ; 0, 1, +, ·, -), ou seja, que é compatível com essa estrutura, ou seja, que:
   1. a ≡ₘ a’ & b ≡ₘ b’ ⇒ a + b ≡ₘ a’ + b’
   2. a ≡ₘ a’ & b ≡ₘ b’ ⇒ a · b ≡ₘ a’ · b’
   3. a ≡ₘ a’ ⇒ -a ≡ₘ -a’
4. Seja m inteiro. Demonstre ou refute, se puder:
   1. a ≡ₘ b ⇒ a + x ≡ₘ b + x
   2. a ≡ₘ b ⇒ a · x ≡ₘ b · x
   3. a ≡ₘ b ⇒ -a ≡ₘ -b
   4. a ≡ₘ b ⇒ aˣ ≡ₘ bˣ
5. O «planeta 1» faz sentido? Como é?
6. O «planeta 0» faz sentido? Como é?
7. Demonstre o que consegues da equivalência das duas sugestões do que deveria significar o a ≡ₘ b.

2022-10-07 (IDMa)

1. Sejam $a$ inteiro e $p$ primo tais que $(a,p) = 1$. Seja $R_p = \{0,1, \dotsc, p-1\}$. Demonstre que $aR_p$ possui exatamente um representante de cada classe (time).
2. $a$ invertível módulo $m$ sse (a,m) = 1.
3. Unicidade de inversos módulo $m$.
4. Mostre que a (≡ₘ) não é compatível com a exponenciação.
5. Elabore e justifique critério de divisibilidade para os 2,3,4,5,9,11

2022-10-08 (IRI)

1. Jogue o NNG. Tente completar o mais rápido possivel; possivelmente sua entregá será a Prova 2.2. Veja o FAQ relevante também.

2022-10-14 (IDMa)

1. Encontre um inverso de 18, módulo 125.
2. Encontre inteiro x tal que $6^{1032} \equiv x \pmod {11}$.
3. Dados inteiros $a,b,m$ quantas multiplicações tu precisa fazer para achar um inteiro $x$ tal que $a^b \equiv x \pmod m$?
4. Querendo escrever um guia para alunos (ou maquinas!) saber como resolver congruências e sistemas de congruências, o que tu escreveria sobre:
   1. $\phantom a x \equiv b \pmod m$
   2. $ax \equiv 1 \pmod m$
   3. $ax \equiv b \pmod m$
   4. Um sistema de $n$ congruências $x \equiv b_i \pmod {m_i}$. (Dica: resolva primeiro para o caso $n = 2$.)
5. Demonstre que existe uma infinidade de primos «da forma 4n+3».
6. Depois de resolver o problema anterior, explique por que sua resolução não é adaptável para primos «da forma 4n+1».
7. Demonstre: p primo ⇔ (p-1)! ≡ -1 (mod p).

2022-10-14 (IRI)

1. Calcule os:
   1. double (double (S O))
   2. double ((S O) + (S (S O)))
2. Defina multiplicação e exponenciação.
3. Olhando para as funçoẽs binárias e famosas que temos 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 ⇈.
4. Defina a função Pd : Nat → Nat de “predecessor”, onde consideramos que o predecessor de zero é o próprio zero mesmo: AVISO: a maioria das vezes que um aluno de 2022.1 usou a Pd em outras definições, estava errando
5. Defina a função ∸ : Nat → Nat → Nat que comporta como subtração, mas caso que o resultado era pra ser negativo, retorna O mesmo.
6. Defina as funções:
   1. fact : Nat → Nat
   2. fib  : Nat → Nat
   3. dist : Nat → Nat → Nat
   4. min  : Nat → Nat → Nat
   5. max  : Nat → Nat → Nat
   6. div  : Nat × Nat → Nat × Nat
   7. quot : Nat × Nat → Nat
   8. rem  : Nat × Nat → Nat
   9. gcd  : Nat × Nat → Nat
   10. lcm  : Nat × Nat → Nat
   11. comb : Nat → Nat → Nat
   12. perm : Nat → Nat → Nat

2022-10-17 (IDMa)

1. Demonstre o «sonho do calouro»: Para qualquer primo $p$, $(x + y)^p \equiv x^p + y^p \pmod p$.
2. Demonstre por indução o teorema binomial: $(x + y)^n = \sum_{i=0}^n {n \choose i} x^iy^{n-i}$, onde ${n \choose r} = C(n,r)$.
3. Demonstre que $(\forall 0 < i < p)[p \mid C(p,i)]$.
4. Consiga como corolario desses teoremas o «Teorema pequeno de Fermat»: $a^p \equiv a \pmod p$.
5. AINDA?!: Sejam $a$ inteiro e $p$ primo tais que $(a,p) = 1$. Seja $R_p = \{0,1, \dotsc, p-1\}$. Demonstre que $aR_p$ possui exatamente um representante de cada classe (time). [foi postado 10 dias atrás].
6. Ache a pior entrada para euclides e justifique tua resposta.
7. Termine a implementação recursiva do $C({-},{-})$.
8. Demonstre que $C(n,r) = \dfrac {n!}{r! (n-r)!}$.
9. Sejam n,r inteiros. Demonstre: $r! (n-r)! \mid n!$.
10. As duas métodos que descrevemos sobre a resolução de $ax \equiv 1 \pmod m$ e de $ax \equiv b \pmod m$ em algum ponto mandaram checar se $a,m$ são coprimos. Caso que não são, podemos concluir que tais congruências não possuem resolução?
11. Infira o “princípio” multiplicativo de contagem a partir do princípio aditivo.

2022-10-17 (IRI)

1. (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!
2. Implementa o Nat num módulo Haskell, junto com todas as funções que definimos até agora, incluindo os hw. Comece teu arquivo assim:

   module Nat where
   
   data Nat = O | S Nat
       deriving ( Eq , Show )
   

2022-10-20 (IRI)

1. Resolva tudo na §«Demonstrando propriedades de naturais com indução»
2. Asserte propriedades sobre teus programas do hw do dia 2022-10-14, e demonstre cada uma delas!
3. Enuncie e demonstre que quaisquer fibonaccis consecutivos são coprimos.

2022-10-22 (IDMa)

1. Seja $R_m = \{r_1,\dotsc,r_{\varphi(m)}\}$ é um sistema reduzido de resíduos módulo $m$. Demonstre:
   1. Se (a,m)=1, então aRₘ também é um s.r.r. módulo m.
   2. $\sum_{r\in R_m} r \equiv 0 \pmod m$.
   3. Rₘ é (·)-“fechado módulo m”.
   4. (∀r ∈ Rₘ)(∀x ∈ ℤ)(∃u ∈ ℤ)[ x ≡ₘ ru ]
2. (qm + r, m) = (r,m)
3. (a,nm) = 1 ⇔ (a,m) = 1 & (a,n) = 1
4. φ(p) = p-1
5. φ(pᵏ) = pᵏ - pᵏ⁻¹
6. Calcule um dos φ(2), φ(3), φ(4), …, φ(13)
7. φ é multiplicativa, ou seja: (m,n)=1 ⇒ φ(mn) = φ(m) φ(n). Dica: escreva todos os números de 1 até mn numa tabela de m × n.
8. Calcule de novo, essa vez todos os φ(2), φ(3), φ(4), …, φ(13). (Não se engane: fatorização demora!)
9. φ(n) é par para qualquer n > 2.
10. Calcule o valor do somatório $\sum_{i=0}^k \varphi(p^i)$.
11. $a^{\varphi(m)} \mathrel{\equiv_m} 1 \iff (a,m) = 1$. Dica: φ e sistemas reduzidos de resíduos são intimamente relacionados, né?
12. Mostre que o Fermatinho é um corolário da proposição anterior!
13. Seja $p$ primo e defina a função $V_p : \mathsf{Int} \to \mathsf{Int}$ pelas:
    $V_p~a = \max\{ i\;\mid\; p^i \mid a\}$ para $a \neq 0$ e para $a = 0$, decida tu!
    Demonstre:
    1. V (a+b) ≥ min (V a) (V b)
    2. V (ab) = V a + V b
    3. V (a,b) = min (V a) (V b)
    4. V [a,b] = max (V a) (V b)
    5. Defina $\Vert a \Vert_p = p^{- (V_p\,a)}$. Demonstre: $$ \begin{gathered} \Vert ab \Vert = \Vert a \Vert \, \Vert b \Vert \\ \Vert a + b\Vert \leq \max \{\Vert a \Vert, \Vert b \Vert \} \leq \Vert a \Vert + \Vert b \Vert \\ \prod_{p~\text{primo}} \Vert a \Vert_p = \frac 1 {|a|} \\ \end{gathered} $$

2022-10-27 (IDMa)

1. Demonstre, depois do esboço/dica da aula: φ é multiplicativa.
2. Demonstramos a propriedade principal de descryptografar, mas nela a gente supôs que $m,N$ são coprimos. Temos mesmo como garantir isso? Se sim, por quê? Se não, o que acontece se por sorte (i.e., azar) a mensagem $m$ que queremos mandar não é coprima com o $N$?
3. Considere que temos acesso numa função $h : D \to H$ que dada um valor de informação $d \in D$, retorna o seu hash $h(d) \in H$. Suponha que ela, mesmo sendo conhecida por todos, tem a propriedade seguinte: dado um $s \in H$, é difícil achar um valor $d_s \in D$ tal que $h(d_s) = s$. Pense numa maneira de usar o sistema RSA que a gente discutiu na aula para conseguir assinaturas digitais: queremos uma maneira de ter certeza que a mensagem que recebemos supostamente escritar por Alice, foi escrita por Alice mesmo. Dica 1. Temos que $e$ é um inverso de $d$, e logo $d$ é um inverso de $e$ também. Observem que $(m^e)^d=(m^d)^e$. Dica 2. A chave privada deve ser usada para trancar(cryptografar) algo, que qualquer pessoa pode destrancar(descryptografar) mas apenas quem está em posse da chave privada poderia ter sido o trancador.

2022-10-28 (IRI)

1. Defina e demonstre a corretude das funções:
   • leq     : Nat → Bool
   • ev      : Nat → Bool
   • od      : Nat → Bool
   • isMul₃  : Nat → Bool
   • divides : Nat → Nat → Bool
   • congmod : ?
   • isZero  : Nat → Bool
2. Demonstre que a (≤) : Nat → Nat → Prop é: reflexiva; transitiva; antissimétrica; total
3. Demonstre que todo Nat é par ou ímpar.
4. Defina os operadores booleanos.
5. Como definarias uma função if_then_else_ : Bool → Nat → Nat → Nat?
6. Demonstre a corretude das funções definidas no hw do dia 2022-10-14.
7. O lemma de divisão de Euclides para os Nats:
   • enuncie
   • demonstre

2022-10-31 (IRI)

1. Implemente como Nats:
   1. os inteiros (já sabes a sua especificação pelo IDMa!)
   2. os parzinhos-de-Nats
   3. s vetores-de-Nats como Nat
2. Implemente como novo tipos, tendo já definido o Nat:
   1. os inteiros
   2. os parzinhos-de-Nats
   3. os vetores-de-Nats como Nat
3. 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
   • 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
4. Defina as:
   • head        : ListNat → Nat
   • tail        : ListNat → ListNat
   • init        : ListNat → ListNat
   • last        : ListNat → Nat
5. Defina a (<) : Nat → Nat → Prop e sua internalização, e demonstre a sua corretude.

2022-11-04

• IRI
  1. Demonstre os teoremas (escolhe algo interessante para botar nos ??)
     1. (∀xs,ys:ListNat)        [ sum (xs ++ ys) = ?? ]
     2. (∀xs,ys:ListNat)        [ product (xs ++ ys) = ?? ]
     3. (∀ℓ:ListNat)            [ length (filterEven ℓ ++ filterOdd ℓ) = ?? ]
     4. (∀ℓ:ListNat)            [ reverse (filterEven ℓ) = ?? ]
     5. (∀n:Nat)(∀ℓ:ListNat)    [ length (addNat n ℓ) = ?? ]
     6. (∀n:Nat)(∀ℓ:ListNat)    [ sum (addNat n ℓ) = ?? ]
     7. (∀n:Nat)(∀ℓ:ListNat)    [ sum (multNat n ℓ) = ?? ]
     8. (∀n:Nat)(∀ℓ:ListNat)    [ product (multNat n ℓ) = ?? ]
     9. (∀n:Nat)(∀ℓ:ListNat)    [ product (expNat n ℓ) = ?? ]
     10. (∀n:Nat)(∀ℓ:ListNat)    [ isSorted (addNat n ℓ) = ?? ]
     11. (∀ℓ:ListNat)            [ isEven (product ℓ) = anyEven ℓ ]
     12. (∀ℓ:ListNat)            [ isEven (sum ℓ) = isEven (length (filterOdd ℓ)) ]
     13. (∀ℓ:ListNat)            [ isZero (sum ℓ) = ?? ]
     14. (∀ℓ:ListNat)            [ isZero (product ℓ) = ?? ]
     15. (∀n,m:Nat)(∀ℓ:List Nat) [ addNat (n + m) ℓ = ?? ]
     16. (∀n,m:Nat)(∀ℓ:List Nat) [ multNat (n · m) ℓ = ?? ]
  2. Demonstre também:
     1. (∀xs,ys:ListNat)        [ length (xs ++ ys) = ?? ]
     2. (∀xs,ys:ListNat)        [ reverse (xs ++ ys) = ?? ]
     3. (∀n:Nat)(∀xs,ys:ListNat)[ addNat n (xs ++ ys) = ?? ]
     4. (∀ℓ:ListNat)            [ reverse (reverse ℓ) = ?? ]
     5. (∀ℓ:ListNat)            [ length (reverse ℓ) = ?? ]
     6. Associatividade da (++)
     7. [] é uma (++)-identidade
  3. Pense em mais propriedades, enuncie, e demonstre!
• INTRO
  1. Demonstre ou refute as leis seguintes (cada uma tem duas proposições independentes para investigar, e para cada uma tome o cuidado seguinte: se precisar saber que o tipo A é habitado, veja se e como isso afeta a tua resposta):
     1. (∀x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∀x:A)[ψ(x)]
     2. (∀x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∀x:A)[φ(x)] ⇒ ψ
     3. (∃x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∃x:A)[ψ(x)]
     4. (∃x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∃x:A)[φ(x)] ⇒ ψ

2022-11-05

• IDMb
  1. ³√2 é irracional? ³√3? ᵏ√n?
  2. §«Primeiros passos»
  3. §«Ordem e positividade»
  4. §«Subconjuntos notáveis e inaceitáveis»
• IDMa
  1. Para quais naturais n temos mesmo que (∀x : Int)[n | x² ⇒ n | x]?

2022-11-07 (IRI)

1. Generalize todas as funções dos hw 2022-11-04 e 2022-10-31 que envolvem ListNat para funções que envolvem List α ou, se não for possível, List Nat.
2. Defina as:
   • concat     : List (List α) → List α
   • ifthenelse : Bool → α → α → α
   • and        : List Bool → Bool
   • or         : List Bool → Bool
   • splitAt    : Nat → List α → (List α × List a)
   • zip        : List α → List β → List (α × β)
   • unzip      : List (α × β) → (List α × List β)
3. Defina um tipo para conseguir uma resolução no problema de querer listas cujos membros podem ser Nat ou Bool.
4. Defina um tipo cujos habitantes serão usados para representar listas que garantam:
   1. ter tamanho ≥ 1 (IList)
   2. ter tamanho par (EList)
   3. ter tamanho ímpar (OList)

2022-11-08 (IRI)

1. URGENTE! Continua (ou começa, pelamor de Curry) o hw do dia 2022-10-17, para incluir as funções que envolvem listas. O arquivo poderia começar assim:

   {-# LANGUAGE GADTs, EmptyDataDecls #-}
   
   module IRI where
   
   data Nat where
       O :: Nat
       S :: Nat -> Nat
     deriving (Eq, Show) 
   
   data Unit where
       Star :: Unit
   
   data Empty
   
   data List a where
       Nil  :: List a
       Cons :: a -> List a -> List a
     deriving (Eq, Show) 
   
   

2022-11-10 (IRI)

1. Defina as:
   • replicate  : Nat → α → List α
   • map        : (α → β) → List α → List β
   • filter     : (α → Bool) → List α → List α
   • a generalização all das: allZero, allEven, allOdd
   • a generalização any das: anyZero, anyEven, anyOdd
   • a generalização pointwise das: pwAdd, pwMult
   • a generalização fold das: sum, product, and, or, concat
   • simplifique as definições antigas para aproveitar essas funções poderosas
   • 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
   • curry       : ?
   • uncurry     : ?
   • flip        : ?
2. Qual seria uma melhor tipágem para a pw : (α → α → α) → List α → List α → List α?

2022-11-11

• IRI
  1. Descubra o foldNat: defina e mostre um uso dele
• IDMb
  1. Até o «§. Valor absoluto»

2022-11-17 (IDMb)

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

2022-11-18 (IRI)

1. Demonstre a associatividade da (∘)
2. Defina tipos para cada um estilo de árvore que tu já viu ou imaginou
3. Formulize os correspondentes princípios/regras de indução para cada um deles
4. Mostre como cada um deles pode virar um Functors
5. Demonstre as leis de Functor para o List : Type → Type com o map que definimos:

   map id = id                  [functor law 1]
   map (f . g) = map f . map g  [functor law 2]
   

6. Demonstre:

   (∀f:α→β)(∀p:β→Bool)  [ filter p ∘ map f = map f ∘ filter (p ∘ f) ]
   

7. Adivinha um lado direito certo e interessante, e demonstre:

   take n xs ++ drop n xs  =
   take m . take n  =
   take m . drop n  =
   drop m . take n  =
   drop m . drop n  =
   map g . map f  =
   sum . map double  =
   sum . map sum  =
   sum . sort  =
   map f . reverse  =
   concat . map concat  =
   filter p . map f  =
   length . reverse = 
   reverse . reverse = 
   

8. Quais das seguintes são válidas e quais não?

   map f . take n     =?=  take n . map f
   map f . reverse    =?=  reverse .map f
   map f . sort       =?=  sort . map f
   reverse . concat   =?=  concat . reverse . map reverse
   filter p . concat  =?=  concat . map (filter p)
   

9. Demonstre:

   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs       [associatividade da (++)]
   length (xs ++ ys) = length xs + length ys
   filter p (xs ++ ys) = filter p xs ++ filter p ys
   map f (xs ++ ys) = map f xs ++ map f ys
   

10. Demonstre:

    sum (xs ++ ys) = sum xs + sum ys
    product (xs ++ ys) = product xs * product ys
    concat (xss ++ yss) = concat xss ++ concat yss
    

11. Podemos definir uma generalização da pw : (α → β → γ) → (F α → F β → F γ) sabendo apenas que o F possui um fmap com qual ele se torna um Functor?
12. Implemente os racionais!

2022-11-20 (IRI)

1. Na última aula percebemos que Either não tinha sequer chances de se candidatar para virar um Functor, pois Either não é um Type → Type (mas sim um Type → Type → Type. Mesmo assim, conseguimos verificar que aplicando parcialmente o Either num tipo ε só, chegamos mesmo no Either ε que é mesmo um Type → Type, e logo tem chances de ser um Functor, e descubrimos qual seria a fmap certa pra isso (demonstre se não demonstrou—o que é pra demonstrar mesmo??). Aqui mais duas coisinhas que estão também Type → Type → Type: o próprio (→) e o (×). Investigue para cada um deles, e para cada aplicação parcial dele, se pode ser munida com um fmap para conseguir ser um Functor:
   1. (δ →) : Type → Type
   2. (→ γ) : Type → Type
   3. (α ×) : Type → Type
   4. (× β) : Type → Type

2022-11-24 (IDMb)

1. Resolva tudo até o §«Infimum e supremum»
2. Formulem bem o critério-Davi sobre infimum/supremum (usando epsilons ♡), e demonstrem
3. Demonstre a unicidade de infima/suprema
4. (IRI) Tendo um tipo Real, defina um data type XReal para representar os reais extendidos.
5. Enuncie e demonstre o teorema da indução para os reais-naturais.
6. Ache alguma propriedade que é satisfeita no $\mathbb R_{\mathbb Q}$ mas não no $\mathbb R$. Cuidado: a resposta “óbvia” é errada.

2022-11-28 (IRI)

1. Prática para indução nos naturais: resolva o Problem Set 2 de 2021.2.
2. Na aula de IDMb definimos uma (·) : Real × Seq(Real) → Seq(Real) em duas formas: implemente ambas em Haskell e demonstre a sua equivalência.

2022-11-29 (IDMb)

1. Defina as $\mathtt{toNat} : \mathbb R_{\mathbb N} \to \mathsf{Nat}$ e $\mathtt{toRealNat} : \mathsf{Nat} \to \mathbb R_{\mathbb N}$; enuncie o que significa que comportam na maneira desejada; demonstre.
2. Seja (Aₙ)ₙ : Seq(α) uma (⊇)-chain. Demonstre que ⋃ₙAₙ = A₀
3. Seja (Aₙ)ₙ : Seq(α) uma (⊆)-chain. Demonstre que ⋂ₙAₙ = A₀
4. Demonstre que não muda nada se a gente trocar o (≥) por (>) e o (≤) por (<) nas definições de «valores-suficientemente-grandes» e de «eventualmente».
5. Na aula cairam na mesa 3 possíveis definições do que significa «(aₙ)ₙ é constante». Investigue se são equivalentes “duas a duas”:
   1. (∃k)(∀n)[ aₙ = k ]
   2. (∀n)(∀m)[ aₙ = aₘ ]
   3. (∀n)[ aₙ = aₙ₊₁ ]

2022-11-30 (IDMb)

1. Θ. eventualmente constante ⇒ cotada
2. Θ. convergente ⇒ cotada
3. Θ. autoconvergente ⇒ cotada
4. Θ. convergente ⇒ autoconvergente
5. Θ. Comportamento algébrico de limites
   1. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → a + b
   2. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ab
   3. (aₙ)ₙ → a ⇒ (caₙ)ₙ → ca
   4. ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → a/b
6. Alguma das recíprocas das implicações acima é válida?
7. Θ (sanduíche): (aₙ)ₙ → ℓ & (cₙ)ₙ → ℓ & (aₙ)ₙ ≤ (bₙ)ₙ ≤ (cₙ)ₙ ⇒ ??
8. Θ: $\{a_n\}_n \subseteq {\mathbb R}_{\mathbb Z}$ e $(a_n)_n$ convergente ⇒ ??
9. Definição. Seja $(a_n)_n$ uma seqüência de reais. Seja $(n_i)_i$ uma seqüência de naturais estritamente crescente. Chamamos a $(a_{n_i})_i$ uma subseqüência de $(a_n)_n$.
   1. Θ. autoconvergente com subseq convergente ⇒ convergente
10. Depois de resolver os anteriores, tente demonstrar/refutar os:
    1. autoconvergente ⇒ convergente
    2. cotada superiormente & crescente ⇒ convergente

2022-12-03 (IRI)

• Ordenação (sorting)
  1. Defina sozinhos os: merge sort; quick sort ;insertion sort
• ASTs
  1. Defina tipos para representar:
     1. expressões de aritmética sem variáveis:
     2. expressões de aritmética com variáveis;
     3. expressões de lógica proposicional
  2. Defina funções de eval e step apropriadamente para cad um dos teus tipos
• Arvores
  1. Defina as:
     • nodeSize  : BinTree α → Nat
     • size      : BinTree α → Nat
     • depth     : BinTree α → Nat
     • leaves    : BinTree α → List α
     • mapTree   : ?
     • mirror    : BinTree α → BinTree α 
     • flatten   : BinTree α → List α
     • findTree  : α → BinTree α → List (List Nat)
     • sumTree   : BinTree Nat → Nat
  2. Adivinhe uma conexão entre o número size t e o número nodes t: enuncie e demonstre!
  3. Θ. size t ≤ 2 ^ depth t
  4. Θ. depth t ≤ length (flatten t)
  5. Verifique que tu passou EM & ME mesmo, reescrevendo o que demonstrou acima utilizando log₂
  6. Defina o resto dos tipos de arvores discutidos nas aulas (peça detalhes no Zulip!)
     1. BinSearchTree α
     2. BinLabTree α β
     3. RoseTree α
  7. Demonstre como todos teus típos de árvores viram Functors
  8. Demonstre:
     1. length ∘ flatten = ??
     2. flatten ∘ mirror = ??
     3. mirror ∘ mirror = ??
     4. depth ∘ mirror = ??
     5. depth ∘ fmap f = ??
     6. fmap f ∘ mirror = ??
• Eficiência “por indução” / parametro acumuladora: use a metodo que encontramos na aula eliminando o (⧺) da reverse para:
  1. eliminá-lo da tua flatten
  2. eliminá-lo da tua leaves
• Folds & lists
  1. Defina uma foldT para os tipos de arvores que faz sentido definir
  2. Defina uma foldE para os tipos de Either
  3. Discuta qual deveria ser o tipo de uma unfold que cria listas a partir de outros valores; depois defina!
  4. reverse (xs ⧺ ys) = reverse ys ⧺ reverse xs
  5. Demonstre a lei de fusão do foldr que é: dado ??, temos:

     f ∘ foldr g a = foldr h b
     

2022-12-12 (IDMb)

1. Resolva sozinho os teoremas seguintes que demonstramos na aula passada:
   1. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → ??
   2. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ??
2. …e o resto do Θ. Comportamento algébrico de limites:
   1. (aₙ)ₙ → a ⇒ (caₙ)ₙ → ??
   2. ?? & (bₙ)ₙ → b ⇒ (bₙ⁻¹)ₙ → ??
   3. ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → ??
   4. (aₙ)ₙ → a & ?? ⇒ (aₙᵏ)ₙ → ??
3. Θ. conv ⇒ autoconv
4. Θ. autoconv ⇒ cotada
5. C. conv ⇒ cotada
6. Θ. autoconvergente com subseq convergente ⇒ convergente
7. Θ. 0 < ϑ < 1 ⇒ (ϑⁿ)ₙ → ??
8. Θ. Toda seq possui subseq “monótona”
   • Dica 1: Def. Chamamos o natural k de pico para a (aₙ)ₙ sse (∀n≥k)[ aₖ ≥ aₙ ]
   • Dica 2: Separe em casos: Caso (aₙ)ₙ tem quantidade infinita de picos; Caso contrário.
9. «Agora sim!» Demonstre os: Nested Interval Property de [Cantor][Cantor]; Monotone Convergence Theorem; [Bolzano][Bolzano]–[Weierstrass][Weierstrass] Theorem; [Cauchy][Cauchy] convergence critérion
   1. Θ. (NIP): Teorema dos intervalos aninhados:
      Se (Iₙ)ₙ é uma (⊇)-cadeia de intervalos fechados habitados da forma Iₙ = [aₙ,bₙ],
      então ⋂ₙIₙ habitado.
      Ainda mais: Se (diam(Iₙ))ₙ → 0, então ⋂ₙIₙ é um singleton!
      • Dica 1: a₀ ≤ a₁ ≤ a₂ ≤ ⋯ ≤ b₂ < b₁ ≤ b₀
      • Dica 2: (aₙ)ₙ sup-cotada; (bₙ)ₙ inf-cotada
      • Dica 3: Encontre a≤b tais que ⋂ₙIₙ = [a,b]
   2. Θ. (MC): cotada & “monótona” ⇒ convergente
   3. Θ. (BW): cotada ⇒ conv subseq
   4. Θ. (CC): autoconvergente ⇒ convergente
10. [Αρχιμήδης][Archimedes]:
    1. Θ. Os reais naturais não são cotados
    2. Θ. (∀ε>0)(∃n)[ 1/n < ε ]
    3. Θ. (∀s≠0)(∃n)[ ns > 1 ]
    4. Θ. (∀ε>0)[ε$\mathbb R_{\mathbb N}$ não é cotado]
    5. Θ. (∀s≠0)(∀b)(∃n)[ b < ns ]
    6. Θ. (∀b)(∀s≠0)(∃n)[ ns > b ]
    7. Q. Há diferença entra as duas últimas? Como chamarias cada uma no «nível coração»?
11. Existência de raizes
    1. Θ. Raizes de pequenos: a < 1 ⇒ (aₙ)ₙ → √a, onde: $$\begin{align*} a_0 &= 0 \\ a_{n+1} &= a_n + \frac 1 2 (a - a_n^2) \end{align*}$$
       • Dica 1: cotada…
       • Dica 2: …crescente…
       • Dica 3: …logo conv. O que falta agora?
    2. Θ. «[Ἵππασος][Hippasus] precisa morrer» (aka: «√2 é real»)
       • Dica 1: Considere o H ≝ { x | x² < 2 }
       • Dica 2: Seja h = sup H. Elimine as possibilidades h² < 2 e h² > 2
       • Dica 3: Lembrete: o dado h = sup H é uma conjunção e vamos precisar ambas as suas partes: uma para eliminar o caso h² < 2 e a outra para eliminar o caso h² > 2.
       • Dica 4: Para eliminar caso h² < 2: calcule o (h + 1/n)² para conseguir supcotá-lo por h² + (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «cota superior».
       • Dica 5: Para eliminar caso h² > 2: calcule o (h - 1/n)² para conseguir infcotá-lo por h² - (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «melhor».
    3. Θ. Existência das raizes ²√
    4. Θ. Existência das raizes ᵏ√
12. Densidades:
    1. Θ. dos reais racionais nos reais
    2. Θ. dos reais irracionais nos reais
13. Cardinalidades (1):
    1. Ache seqüência de reais que “ocupa” os reais naturais
    2. Ache seqüência de reais que “ocupa” os reais inteiros
    3. Ache seqüência de reais que “ocupa” os reais racionais
14. Chega sozinho nas definições de liminf / limsup e depois…:
    1. Θ. (aₙ)ₙ → ℓ ⇒ liminfₙ aₙ = ℓ = limsupₙ aₙ
    2. Θ. infₙ aₙ ≤ liminfₙ aₙ ≤ limsupₙ aₙ ≤ supₙ aₙ
    3. Θ. (∀ε>0)(∃K)(∀k≥K)[ liminfₙ aₙ - ε ≤ aₖ ≤ limsupₙ aₙ + ε ]
    4. Θ. x ≥ limsupₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x + ε ]
    5. Θ. x ≤ liminfₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x - ε ]
    6. Θ. x ≤ limsupₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ > x - ε ]
    7. Θ. x ≥ liminfₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ < x + ε ]
    8. Θ. liminfₙ aₙ + liminfₙ bₙ ≤ liminfₙ (aₙ+bₙ) ≤ limsupₙ (aₙ+bₙ) ≤ limsupₙ aₙ + limsupₙ bₙ
    9. Q. liminfₙ(pₙ₊₁ - pₙ) = ? onde pₙ é o n-ésimo primo
    10. Q. liminfₙ (sin(n)) = ?
    11. Q. limsupₙ (sin(n)) = ?
15. Algébricos vs Transcedentais
    1. Existem transcedentais?
16. Qualquer conjunto de reais habitado e finito possui mínimo e máximo

2022-12-15 (IDMb)

1. Resolva o hw do dia 2022-12-12 que não foi resolvido na aula; re-resolva sozinho o que foi.
2. Termine para cada uma das séries que encontramos o que faltou:
   1. $\sum_{n=1}^\infty \frac 1 {2^n}$
   2. $\sum_{n=1}^\infty \frac 1 {n^2}$
   3. $\sum_{n=1}^\infty \frac 1 n$
3. O conjunto dos irracionais é (+)-fechado? (·)-fechado? (^)-fechado?
4. Na aula anterior mostrei um esboço para demonstrar o (BW) a partir do (MCT). Ache em uma outra maneira, a partir do (NIP).
5. Na aula anterior demonstramos o Θ. ϑ pequeno ⇒ (ϑⁿ)ₙ → 0. Ache uma outra demonstração, começando com a observação (justificada!) que $\frac 1 \vartheta = \delta + 1$ para algum $\delta > 0$. Use o teorema binomial! (Podemos mesmo?)

Histórico

2022-08-22: INTRO (1): Overview; tipos [video]

• Overview
• tipos e type errors
• proposiões vs objetos
• Prop vs Bool

2022-08-24: INTRO (2): Definições [video]

• intensão vs extensão
• = vs ⇔
• «def»
• comandos vs proposições
• REPL
• Exemplos de teoremas e seus tabuleiros (estados) iniciais
• Dados e Alvo
• açúcar sintáctico
• sintaxe vs semântica
• variáveis ligadas vs livres
• escopos de variáveis
• capturamento de variável
• definição e seu contexto
• escolha boa de variável, variável fresca
• bairros de variáveis
• os ¬,⇒,⇔,&,ou,∀,∃,=

2022-08-26: INTRO (3): Demonstrações [video]

• ocorrências ligadas vs livres de variáveis e ligadores
• sombreamento (shadowing) de variáveis
• Propriedades da igualdade: refl, sym, trans, e substituição
• «Calculamos»: seu uso, sua escrita, e seus efeitos
• definições como abreviações

2022-08-29: INTRO (4): Demonstrações [video]

• o resto dos conectivos para nossa linguagem de demonstrações
• os ⇔, ¬, ⇐, como açúcar sintáctico
• o ⊥ como conectivo primitivo
• umas “leis de lógica” e como demonstrá-las

2022-08-31: Prova 1.1

2022-09-02: INTRO (5): Demonstrações; IDMa (1) [video]

Demonstrações

• Proposição mais forte vs mais fraca que outra
• P ⇒ ¬¬P
• ¬¬(P ∨ ¬P)
• ¬¬P ⇒ P
• RAA (Reductio ad Absurdum)
• LEM (Law of Excluded Middle)
• Matemática não-construtiva

IDMa: IDMa (1)

• Especificação × Implementação
• Os inteiros $(\mathbb Z;0,1,+,-,\cdot)$
• Axiomas sobre os inteiros
• Axiomas vs Teoremas

2022-09-05: IDMa (2) [video]

• bom dia / recap
• Teoremas x axiomas; dependências de demonstrações
• Q: por que não aparece (=) na estrutura dos inteiros?
• Q: como rotular teoremas?
• Sintaxe vs Semântica; convenções sintácticas
• juxtaposição; notação infixa/postfixa/prefixa
• arvore sintáctica; parsing; precedência sintáctica de operadores
• associatividade sintáctica
• Operações primitivas vs. definidas
• subtração como operação definida e não primitiva
• uns numerais para ajudar: 2, 3, …
• potências com expoentes naturais; convenção sobre associatividade sintáctica da exponenciação
• Q: igualdade sintáctica vs intensional
• Q: o parsing se trata de quais operações?
• Cancelamento multiplicativo
• Q: qual a associatividade sintáctica da (⇒)?
• Q: refutação..?
• Não-zerodivisores.
• Q: o «ou» é exclusivo?
• (Plicker) axiomas ou teoremas?
• A resposta certa; mais teoremas
• Existência e unicidade; artigo indefinido vs definido; proof by fight club; alternativa conhecendo já um legal

2022-09-09: IDMa (3) [video]

• Dica sobre como enxergar alvos
• A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
• Exemplos: (∀a)[(-1)a = -a]; (∀a)[0a = a]
• Axioma x Teorema; Noção primitiva x definida
• Axiomas sobre ordem: duas maneiras de axiomatizar
• A (≤) nos naturais é definível
• Conjunto fechado sob operação
• Notação set-builder (com comprehension)
• interpretação de (∈)
• Como tratar um subconjunto como predicado unário
• 1 é positivo: teorema ou axioma?
• O módulo (absolute value) |_| : Int → Int
• Para refletir: a independência duma proposição: indemonstrabilidade e irrefutabilidade

2022-09-12: IDMa (4) [video]

• como definir «ser fechado sob uma operação n-ária (para n=1,2)
• uma primeira conversa “adulta” sobre conjuntos
• um preconceito sobre as () na notação f(x)
• a notação set-builder: como ler e escrever, e como não ler e como não escrever
• 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ℤ
• Θ. 1 é positivo
• Como demonstrar a indemonstrabilidade de proposições
• A indemonstrabilidade do 0 ≠ 1
• notação infixa x postfixa x prefixa x mixfixa

2022-09-14: IDMa (5) [video]

• Não existe inteiro estritamente entre 0 e 1: teorema ou axioma?
• 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
• o mínimo dum conjunto, quando existe é único
• Umas propriedades do valor absoluto

2022-09-16: IDMa (6) [video]

• um pleno «tal que» é capaz de destruir uma frase e torná-la pior-que-errada
• Princípio da boa ordem ($\mathbb Z_{>0}$ é bem ordenado)
• Como usar o PBO na prática
• Principios de indução como teoremas
• 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
• Indução com mais que uma base

2022-09-19: IDMa (7) [video]

• uma interpretação geométrica dos inteiros
• PBO shiftado e demais versões
• Indução forte (“course-of-values”)
• Quebrando os inteiros em tijolinhos atômicos usando como cimento: (i) adição; (ii) multiplicação
• Definição de invertível
• Definição de irredutível

2022-09-21: IDMa (8) [video]

• O que queremos? (Wishlist)
  • Divisão (quot e rem)
  • algoritmo para calcular os quot e rem
  • definir e justificar sistemas posicionais de numerais
  • mdc e mmc
  • fatorização única (ao menos de coisas sensatas) de inteiros (teorema fundamental de aritmética)
• O lemma da divisão de Euclides: enunciado
• Números, numerais, dígitos
• Expansão e sistemas posicionais
• Notação Σ de somatórios
• O logaritmo como tamanho de númerais melhor que o length deles como strings
• Enunciado do Teorema Fundamental de Aritmética (fatorização única)
• Explicação intuitiva sobre como sistemas posicionais funcionam
• generalização da palavra “maior” para outras ordens
• diagrama Hasse para os $\mathbb{Z}_{\geq 0}$
• mdc: definição nível coração

2022-09-23: IDMa (9) [video]

• O lemma da divisão de Euclides: esboço de demonstração
• 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.
• “mℤ” ⇔ “fechado sob ops”: concretização e esboço
• Duas maneiras de obter membros arbitrários de um conjunto indexado
• Esboço do Teorema Fundamental de Aritmética (fatorização única de inteiros)

2022-09-26: IDMa (10) [video]

• Invertible, Unit, Irreducible
• Prime
• m.d.c.
• Um exemplo: m.d.c. dos 12,18; divs; comdivs
• Q: como assim um-maior? A: hmm-maior
• O que acontece se trocar de (|) para (≤)?
• O que acontece se trocar de direção nas ordens?
• Q: qual o tipo desse min?
• Dados a,b, existe mesmo um m.d.c. deles?
• Como vou escolher o m.d.c. se os comdivs são esses?
• Θ. Existência de m.d.c.
• Q: qual o nome da alma que os m.d.c. e o min compartilham?
• Duas maneiras de obter membro arbitrário de conjunto indexado
• Q: Como exatamente funciona essa notação set builder?
• m.d.c. vs m.m.c (teaser de dualidade)
• mesmo demonstrando a existência, queremos algoritmo e de preferência eficiente

2022-09-28: Prova 1.3; IDMa (11) [video]

• Como demonstrar (a,b)=(c,d).
• Algoritmo de Euclides: corretude e terminação
• Terminação, Corretude, Eficiência
• Algoritmo estendido de Euclides
• coprimos

2022-09-30: IDMa (12) [video]

• 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
• “unicidade” de m.d.c.
• Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva
• sermão sobre x² par ⇒ x par
• generalizações
• m.d.c. e os coeficientes Bézout
• Lemma de Euclides: x irredutível ⇒ x primo
• Momentos que parecem LEM mas não são
• Sobre a contaminação de demonstrações com magias ⛤
• [Erdős][Erdos]: «proofs from [The Book][proofs-from-the-book]»
• Teorema de Euclides: há uma infinidade de primos
• Como decidir se um inteiro é primo.
• Sobre Euclides e seus Elementos
• Sobre o teorema fundamental de aritmética
• Como codificar listas de inteiros nos inteiros?

2022-10-05: IDMa (13) [video]

• Correção sobre o «algoritmo da criança» vs «algoritmo de Euclides»
• Fatorização é lenta
• Densidade de primos e gaps
• Algumas conjecturas da teoria dos números: Gêmeos, Goldbach, Collatz, Legendre
• O enunciado do teorema dos números primos (PNT)
• O enunciado do teorema Chebyshev (postulado de Bertrand)
• Congruência módulo um inteiro e demonstrações das suas propriedades
• Aritmética modular e propriedades do $\mathbb Z / m\mathbb Z$
• (·)-inversos módulo um inteiro m

2022-10-07: IDMa (14) [video]

• por que as duas definições de congruência não são mesmo equivalentes
• o planeta 0: a terra
• o planeta 1: o {⋆}
• as notações mA e A+k e os mℤ, mℤ+k
• Aritmética módular, pouco mais adulta
• Θ: Invertibilidade módulo m
• D: Congruência, compatibilidade com operações
• Θ: Unicidade de inversos módulo m
• Critéria de divisibilidade
• O Teorema Fundamental de Aritmética para os racionais
• Sobre um sistema de resíduos módulo p
• Plicker: «Existem quantos planetas onde todos os não nulos são invertíveis?»

2022-10-10: IRI (1) [video]

• introdução
• um resumo da abordagem (axiomática) que usamos em IDMa
• especificação vs implementação; implementação-agnóstico
• a abordagem desta disciplina (IRI): mais contrastes de abordagem
• [algebraic data types][algebraic-data-types]
• o tipo Nat: espectativas e 4 maneiras de definir um tipo de dados recursivamente
• sintaxe: o que queremos descrever
• o desafio dos «…» numa definição
• exemplo de chefe de programação sem noção comunicando pedido
• Naturais vs Nats; Números vs Numerais
• Linguagem vs Metalinguagem; Variáveis vs Metavariáveis
• «Nada mais»
• Regras de inferência e lida de cima para baixo e de baixo para cima
• Como mostrar que algo é um Nat
• arvores de inferência, folhas abertas e fechadas; regras e comandos
• casamento de padrão com expressão: primeiro encontro
• gramáticas e a [notação BNF][bnf]: nada demais!
• Mal entendido: «os inteiros que a gente conheceu»—Nope.
• Mal entendido: «uns inteiros são naturais»—Nope.
• type casting
• a aplicação duma função no seu argumento, e a inferncia de tipo relevante
• Tem como implementar os inteiros usando os naturais, e mais uns teasers
• Regras e arvores de inferência, comandos vs proposições
• Um exemplo de inferência: SSSO : Nat
• Definição recursiva vs tijolo
• um exemplo: fact : Nat → Nat
• Como traduzir uma linha sem premissas para código

2022-10-14: IRI (2) [video]

• ocorrências livres e ligadas de variáveis
• construtor vs função
• uns açúcares sintácticos
• uns preconceitos sobre funções e sua notação
• ocorrências ligadas e livres de variáveis
• double : Nat → Nat; id : Nat → Nat
• padrões de argumentos
• o presente da recursão
• Como calcular (modelo computacional)
• double 2 = ?
• valores canônicos
• casamento de padrões
• Duas maneiras de escrever cálculos
• A adiçaõ: (+)
• prefix, postfix, infix, mixfix
• Um cálculo e teorema: 2 + 3 ≟ 5
• [Arvore sintáctica (Abstract Syntax Tree)][ast], [parsing][parser], (veja também: [lexer][lexer])
• Precedência sintáctica
• Associatividade sintáctica
• Associatividade vs associatividade sintáctica: axiomas e especificação vs implementação
• Currificação
• como definir o addFive nível boss
• Aplicação parcial

X 2022-10-15: IRI (3,4) [video]

• construtor vs função
• D: multiplicação
• o uso de lemmas: m-idR, e-idR
• uma demonstração simples: (·)-idR
• ∀: como usar
• ∀: como atacar
• qual resultado incompleto é melhor?
• lazy vs strict
• estratégia de evaluação vs precedência de operador
• notação de aplicação de função por espaço: f x
• acordos sintácticos sobre a aplicação-de-função: precedência, associatividade sintáctica à esquerda: f x y z ≡ ((f x) y) z, e os seus porquês
• Θ. 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-10-17: IDMa (15) [video]

• Decepção de falta de hw
  • Achando inversos modulares
  • Exponenciação modular
  • Resolvendo congruências
  • Resolvendo sistemas de congruências
  • Θ. infinidade de primos da forma 4k+1 e da forma 4k+3
  • Θ. teorema de Wilson
• Ferramentas até agora: rápidos vs lentos
• Pouco de análise combinatória
• Θ. Teorema pequeno de Fermat: enunciado
• Teorema e coeficientes de binomial
• Θ. O sonho do calouro
• $p$ divide o $C(p,i)$ para $0 < i < p$

2022-10-19: IRI (5): Nat [video]

• dois princípios sobre os construtores e os valores construidos
• escolhendo o padrão na direita duma equação para substituir na direção (←)
• o problema que temos demonstrando a (+)-associatividade
• A regra de inferência Ind-φ. (Onde φ : Nat → Prop.)
• Demonstração por indução
• A associatividade da (+): umas demonstrações por indução diferentes.
• Análise das duas melhores demonstrações da (+)-associatividade: legalzinho vs legalzão
• Inventar teoremas-propriedades sobre nossos programas

2022-10-21: IDMa (16) [video]

• Θ. Teorema binomial
• Θ. O sonho do calouro
• Θ. “Fermatinho” de Fermat (demonstração de Euler, por indução)
• A hipotese (errada) “chinesa”
• Enganadores do Fermatinho: Carmichael
• Teste de primalidade de Fermat
• Se tem ilegais, pelo menos a metade é ilegal
• Como gerar primos
• Sistemas de resíduos módulo m: completos e reduzidos
• A função totiente de Euler

2022-10-24: IDMa (17) [video]

• p-valuações, tamanho e distância p-adica
• raizes quadradas e resíduos quadráticos módulo p
• Euler entra!
• Umas aplicações da teoria dos números inteiros
• Sobre criptografia
• Criptografia vs [steganografia][steganography]
  • (see also: [lipograma][lipogram], [La Disparition][la-disparition], [Oulipo][oulipo])
• Cæsar, rot13
• one-time pad
• Plicker survey

2022-10-26: IDMa (18); Prova 1.4 [video]

• φ(pᵃ) = pᵃ - pᵃ⁻¹
• φ é multiplicativa
• criptografia RSA
• assinaturas digitais: objetivo

X 2022-10-27: IRI (6,7): Nat, Bool [video]

• currificação: versão currificada vs descurrificada da mesma função
• associatividade sintáctica
• inferência de tipo de aplicação de função
• conexão com uso de implicação; [propositions-as-types][propositions-as-types]
• prerequisito para perguntar sobre igualdade: mesmos tipos!
• Como implementar o tipo Bool (e suas operações) em termos de Nat: problemas
• pra quem esse return 0 está retornando tal 0 nas mains dos programas?
• os booleanos precisam suas operações também
• booleanos em python e type casting
• a diferença entre a parte (e tipagem) estática e a parte (e tipagem) dinâmica
• type sistem e checagem de tipo vs evaluação de expressão para achar um valar
• O tipo Bool (de verdade)
• Ordem: (≤) vs leq: mundo-objeto e mundo-meta
• corretude (soundness & completeness) de programas
• (≤) : Nat → Nat → Prop
• leq : Nat → Nat → Bool
• Relações vs funções-com-codomínio-Bool
• Como representar predicados sobre os naturais (Nat → Prop, Nat→Nat→Prop, etc.) como se fossem funções que retornam Bool.
• A corretude da leq
• internalização de conceito
• O uso de underscore nos padrões
• uma convenção sobre a ordem de equações numa definição recursiva
• Sobre funções parciais vs totais
• side effects (efeitos colaterais) e funções puras
• Type inference; como/quando aproveitar a inferência de tipos
• even e odd (pares e impares): como internalizar e como demonstrar corretude
• ev, od : Nat → Bool
  • treis maneiras diferentes de definir: precisando 3 equações; precisando o not; com recursão mútua
• recursão mútua
• backticks para notação infixa
• Como usar o underscore (_) como «variável sem nome» num padrão.

2022-10-31: IRI (8): Nat, Bool, Weekday, Unit, Empty, ListNat [video]

• Type synonym
• Desafio: Int parzinhos-de-Nats, vetores-de-Nats
• isBool : Nat → “Bool”
• O que acontece em linguagem que autoafirmam ter «tipos dinâmicos»
• Corretude de definição de função (programa): correção e completude
• Mais tipos de dados simples: Weekday
• O tipo Unit com seu único habitánte/construtor: ⋆ : Unit
• Quem é mesmo esse void?
• Indução do Nat e quando não usar
• Q: faz sentido adicionar como açúcar sintáctico para o lem n m assumir papel de Prop? A: Não.
• Como implementar listas: ListNat
• Os construtores Empty (ou Nil) e Cons
• ListNat: sintaxe, açúcar e associatividade sintáctica
• Como escolher a ordem dos argumentos: aplicação parcial e currificação
• ListNat é um tipo recursivo
• Como representar a lista [2,0,8] com nosso tipo
• definindo a length : ListNat → Nat
• Calculando o length [3,2,0]
• Plicker: quantos construtores preciso para definir o tipo Int?

2022-11-04: IRI (9): Nat, Bool, Unit, Empty, ListNat [video]

• Definições de sum : ListNat → Nat e product : ListNat → Nat
  • como escolher o valor certo para o sum [] e o product []
• reverse, append, e concatenação binária (⧺)
• parenteses e convenções sintácticas do ␣
• mal-entendido entre função currificada-vs-descurrificada e notação infixa-vs-prefixa
• aplicação parcial e um cálculo relacionado
  • «redex»
• a notação de “sections” de operadores binários
• um problema com as head e tail
• um teaser sobre a soma de tipos
• Construtores vs Destrutores
• Corretude de programas sobre ListNat: propriedades que gostariamos de demonstrar
• Tentativa de demonstrar uma delas
• Como chegar aos principios de indução para os outros tipos
• O conceito de «respeitar/preservar uma propriedade».
• Do $\mathrm{Ind}^{\mathsf{Nat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathsf{ListNat}}_{\varphi}$.
  • Indução do Bool
  • Indução do Unit
  • Indução do Empty
  • Indução do ListNat
• Como interpretar a indução e suas várias versões dos inteiros agora
• Uma maneira de pensar sobre indução: como separação-em-casos-com-extras
• Conexão entre recursão e indução
  • Definição por recursão vs Demonstração por indução
  • O presente de recursão vs o presente da indução
• Quantos quantificadores e por quê?
• Quantos destrutores e por quê?

X 2022-11-05: IDMb (1,2) [video]

• Pythagoreanos e a interpretação de número na grécia antiga
• Os números: naturais, inteiros, racionais, reais
• Θ. O √2 é irracional
• Lemma-chave: x² par ⇒ x par
• A “existência” do √2, pelo teorema pythagoreano
• E quem se importa sobre a racionalidade do √2?
• Buracos na linha dos racionais
• A linha continua dos reais
• De √2 para √3
• E sobre o √4?
• Tentativa de generalização para outros √n
• Como demonstrar a parte de: «não há outra saida»
• Especificação dos reais (1/3): parte algébrica (aditiva e multiplicativa)
• O que podemos aproveitar «de graça» dos teoremas da teoria dos números inteiros?
• Uma divulgação/propaganda de álgebra abstrata
• Especificação dos reais (2/3): parte relacional (ordem)
• Definições usando as noções primitivas da especificação, e qual o trabalho dum implementador
• Notação: a⁻¹ e a/b; o uso do artigo definido, e a necessidade de demonstrar existência e unicidade
• A unicidade da identidade aditiva: o que significa
• Definições dos a⁻¹ e a/b
• O que precisamos demonstrar sobre nossas novas noções definidas
• potências de um real elavado a um natural
• potências de um real elavado a um inteiro
• potências de um real elavado a um racional
• potências de um real elavado a um real: impossível conseguir isso ainda

2022-11-07: Prova 2.1; IRI (10a) [video]

• Polimorfismo de tipos, e o type constructor 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

2022-11-09: IRI (10b, 11) [video]

• polimorfismo: função(ões) id
• o tipo de bottom
• Nats bottomosos (⊥, nats parciais, o nat infinito)
• mais um tira-gosto/teaser da idéia de [propositions-as-types][propositions-as-types]
• funções de ordem superior (higher-order functions)
• como agir se precisar numa lista ter naturais e booleanos: NatOrBool
• 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 β
• [a função map][map]: map : (α → β) → List α → List β
• [a função filter][filter]: a filter : (α → Bool) → List α → List α
• novas implementações das funções antigas
• Do $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{List~α}}_{\varphi}$.
• o Maybe : Type → Type
• comparação dos tipos Maybe (List α) e List (Maybe α)
• Idéia ruim: usar um valor arbitrário para o head []
• as versões não-gambiarrosas de head e tail
• Resolução legal: safeHead : List α → Maybe α
• Resolução legal: safeTail : List α → Maybe (List α)
• desafio: como generalizar as sum, product, concat
• por que não podemos tipar a sum com List α → α?
• Uma find melhor que as gambiarras C’osas: findFirst : α → List α → Maybe α

2022-11-11: IDMb (3,4) [video]

• Θ. cancelamento aditivo pela esquerda (RA-CanL)
• Θ. resoluções únicas
• duas maneiras diferentes de escrever uma demonstração
• como justificar o “somar o mesmo real nos dois lados”
• funções anônimas, notação lambda, notação “mapsto” (↦)
• umas demonstrações dos primeiros teoremas sobre reais
• valor absoluto nos reais: definição e sua interpretação geométrica
• distância: especificação e implementação
• a desigualdade triangular e sua interpretação geométrica
• demonstração de (∀a,b,c)[ |a - c| ≤ |a - b| + |b - c| ]
• subconjuntos notáveis de reais; [type coercing e type casting][type-coercion]

2022-11-16: IDMb (5,6) [video]

• conjuntos: o que significa em saber qual é um conjunto
• como definir operações entre conjuntos
• como generalizar as operações binárias ∪,∩ para serem aplicáveis em coleções de conjuntos
  • ⋃,⋂ : Set(Set(α)) → Set(α)
  • ⋃,⋂ : Seq(Set(α)) → Set(α)
• as relações (⊆) e (⊇)
• distância e espaços métricos: especificação vs implementações
• Frases legais do ♡:
  • ε-perto
  • ε-vizinhança, ε-bola (aberta/fechada)
• Seqüências: notação e interface e type coercion
• notação sobre intervalos e seqüências
• cota inferior/superior de conjunto, e notação sobrecarregada dos (≤) e (<)
• Igualdades que não são igualdades
• Unicidade de mínima/máxima
• intervalos abertos e fechados e notações que envolvem os -∞/+∞

2022-11-18: IRI (12,13) [video]

• os destrutores são, em geral, parciais; versões seguras
• de NatOrBool para Either α β
• [Produto de tipos][product-type]: α × β
• [Soma de tipos (coproduto)][sum-type]: α + β
• O que usar para representar erros em vez de gambiarras tipo Strings e Números
• pw (zipWith, zip; [veja sobre zipping][zip])
• findFirst: primeira tentativa
• uma idéia sobre como resolver nosso problema: (⟨$⟩)/fmap
• uma outra idéia sobre como resolver nosso problema: pattern matching: match-expression
• de volta para a primeira idéia: fmap e Functors
• [Functors][functor], fmap, deriving ( Functor )
  • Leis de Functor
• Abuso de List α para assumir papel de Maybe α
• Duas interpretações computacionais dos habitantes de List α
• Functorialidade do Either ε
• Composição de funções: (∘)
• [programação tácita][tacit-programming]: point-free, point-less, …
• Como implementar os Ints usando Nats: igualdade
• Teaser sobre arvores

2022-11-23: IDMb (7,8) [video]

• seqüências são [cidadãos da primeira classe][first-class-citizen]
• cota superior/inferor dum conjunto
• infimum/supremum dum conjunto
• [coerção de tipo][type-coercion]
• duas maneiras de desenhar seqüências: uma 1-dimensional e uma 2-dimensional
• dando significado para 1 + (aₙ)ₙ e para o (aₙ)ₙ + (bₙ)ₙ
• como definir mesmo uma seqüência que desejamos
• seqüência limitada superiormente/inferiormente
• investigação: a (aₙ)ₙ é cotada?
• seqüência (estritamente) crescente/decrescente
• crescente não implica não-cotada-superiormente
• como demonstrar que uma alegada cota inferior é realmente uma cota inferior
• Conexões com IRI: listas, Empty, Unit, habitantes de α como habitantes do Unit → α
• a melhor cota inferior e a melhor cota superior
• unicidade de supremum e de infimum
• conjuntos sem sup/inf, e sup/inf do ℝ e do Ø
• um mal-entendido comum sobre demonstrações por vacuidade e propriedades dos membros do Ø
• Esboço para definir o conjunto dos reais-naturais
  • Def: conjunto naturalmente indutivo
  • o «melhor» naturalmente indutivo significa o «menor», e «menor» significa «(⊆)-menor»
  • top-down: seja ℐ a coleção de todos os conjuntos indutivos, e considere sua interseção
  • uns não-exemplos de indutivos
  • definição dos reais-naturais $\mathbb R_{\mathbb N}$
  • o que demonstrar sobre o $\mathbb R_{\mathbb N}$
• Plicker: infA ≤ supA ?

2022-11-25: IRI (14) [video]

• corretude: estipular e demonstrar propriedades dos nossos programas
• e sobre igualdade intensional entre funções
• uns tipos de arvores
• a map das listas e outras fmaps e as leis de Functor
• maneiras de escrever uso de indução é os detalhes possivelmente enganadores e implícitos
• a List com o map é um Functor: demonstração da 2a lei
• demonstração: a segunda lei de Functor para a map de List α
• Composição de Functors
• a propaganda mentirosa de «tipos dinâmicos» e a verdade decepcionante
• como funcionam linguagens de “tipos dinâmicos” e runtime errors

2022-11-28: IDMb (9) [video]

• (–)ₙ é um ligador da variável n no escopo de –
• Novamente sobre conjuntos:
  • o que preciso fazer para definir/determinar um conjunto
  • o que significa (=) entre conjuntos
  • união e interseção de uma coleção de conjuntos de α
• Seq(Set(Real)) e Seq(Seq(Real))
• Seqüências são cidadãos da primeira classe; pointwise (∗)
• duas maneiras de definir (∗) entre um Real e um Seq(Real)
• união e interseção de uma coleção de conjuntos
• Exemplos de umas seqüências de conjuntos de reais, suas uniões e suas interseções:
  • ( [0,n) )ₙ
  • ( [n,n+1) )ₙ
• Como demonstrar que 1 ∈ ⋂ₙGₙ
• Desenhando os primeiros membros de seqüências de conjuntos de reais
• a união de uma seqüência decrescente ((⊇)-chain).
• Reais naturais vs naturais: type casting e type coercion
• os ⌊–⌋ e ⌈–⌉ (piso e teto)
• uma seqüência de abertos com interseção fechada e o dual: uma seqüência de fechados com união aberta
• Uma seqüência decrescente ((⊇)-chain) de intervalos abertos com interseção intervalo fechado
• Frases legais do ♡:
  • para valores suficientemente grandes de
  • eventualmente
• Seqüência constante: 3 candidatos para definição
• Seqüência eventualmente constante
• Mais umas gírias:
  • «para valores suficientemente grande de»
  • «eventualmente»

2022-11-30: IDMb (10,11) [video]

• “Escolhendo N(ε)’s”
• Tantando ficar implementação-agnósticos
• Q: «para valores suficientemente grandes de» vs «eventualmente»
• cuidado com a comparação com a notação-O (que é abusiva demais)
• (cont.)
• Q: o que significa «a igualdade não é exatmente simétrica»?
• como interpretar “igualdades” como a inf A = sup B.
• giria: «frequentemente»
• sinônimos de inf/sup: glb/lub, meet/join, ∧/∨
• Chegando na definição de limite
• O tipo de «_ tende ao _»
• Um primeiro palpite
• Duas maneiras que uma definição pode ter «erro de tradução» (de cabeça para o papel)
• • Briga contra o primeiro palpite
• Girias que envolvem tempo/futuro com seqüências: «nunca», «sempre»
• Um segundo palpite
• • Briga contra o primeiro palpite
• Terceiro (e último) palpite: usando «para valores suficientemente grandes de»
• Uma maneira que envolve o «eventualmente»
• Q: podemos definir o que significa «_ tende ao +∞» ?
• traduzindo de nível coração com gírias, para um nível low level e explicito
• uma métrica bem diferente nos reais: a métrica discreta
• Quantificadores, complexidade de entendimento, importância de gírias, estratégia vencedora de jogo
• Interpretação dos ∀∃ em termos jogos
• Def: «convergente»
• Θ. constante ⇒ convergente
• Q. A gente não precisou olhar no ε que o jogador ∀ escolheu
• Def: «divergente»
• Θ. eventualmente constante ⇒ convergente
• • copycat strategy em jogos
• • Demonstração
• Umas seqüências divergentes
• Θ. a ( (-1)ⁿ )ₙ não tende a nenhum ℓ (ela é divergente)
• Def: «autoconvergente»
• Θ. Unicidade dos limites
• Plicker: (i) cotada & crescente ⇒ convergente? (ii) autoconvergente ⇒ convergente?

2022-12-03: IRI (15,16) [video]

• Eficiência “por algebra”
• Eficiência “por indução”
  • eliminando o (⧺) da reverse “por indução”
• Arvores
  • típos de árvores e umas funções relevantes
  • size, nodes, depth, flatten, mapTree, foldTree, …
• Sintaxe vs semântica
• Numerais binários
• Um toque de expressões e ASTs
  • BNF
  • ArEx, ArExV
  • semântica operacional
  • semântica denotacional
  • eval, step, bigstep
• [funções fold][fold]: fold

2022-12-07: ☠ Prova 2.3; Prova 3.1 ☠

2022-12-12: IDMb (12,13) [video]

• epsilons e como encontrá-los
• umas perguntas ainda abertas
• recap de uns teoremas demonstrados
  • Θ. convergente ⇒ autoconvergente
  • Θ. autoconvergente ⇒ cotada
• recap de umas proposições não demonstradas
  • ?. crecente & supcotada ⇒ cotada
  • ?. conjunto supcotado ⇒ possui supremum
  • ?. propriedade dos intervalos aninhados
  • ?. autoconvergente ⇒ convergente
  • ?. cotada ⇒ subseq convergente
• a seqüência (log n)ₙ não é autoconvergente
• def: subseqüência
• [liminf e limsup][liminf-limsup]
• epsilons e «como encontrá-los»
  • Θ. limₙ (aₙ+bₙ) = limₙ aₙ + limₙ bₙ
  • Θ. limₙ (aₙ·bₙ) = limₙ aₙ · limₙ bₙ
• O último axioma da especificação dos reais: axioma da completude
• Preview de umas conseqüências:
  • Θ. Existência de raizes
  • Θ. Sistema posicional para numerais dos reais
  • Θ. os reais racionais são densos nos reais
  • Θ. os reais irracionais são densos nos reais

2022-12-14: IDMb (14,15) [video]

• Construções de conjuntos/tipos numéricos
• Podemos dizer que o ℝ não tem buracos?
• Igualdade para tipos; igualdade para o Seq(α)
• Seqüências com índices diferentes de naturais, seqs implementadas como funções
• lembrete: teoremas sobre o lado algébrico de limites
• o que significam igualdades que envolvem lim.
• duas notações de operadores aplicados em seqüências
• diagramas comutativos e o teorema de limites algébricos
• Dado um tipo A, o que seriam os tipos A², Aⁿ, A⁰?
• Axioma da completude dos reais: nível-♡
• Θ. sobre inf-cotada ⇒ possui ínfimo?
• Θ. Propriedades arquimedeanas
• Θ. Densidades: dos racionais e dos irracionais nos reais
• Θ. NIP: Nested Interval Property (Cantor); Θ. MCT: Monotone Convergence Theorem
• Sistemas posicionais de numerias para reais: interpretação geométrica (via NIP)
• Θ. [Bolzano–Weierstrass][bolzano-weierstrass]: cotada ⇒ possui subseq convergente
• Q: convergente ⇒ todas as subseq convergentes?
• Cauchy
• Θ. 0 < θ < 1 ⇒ (θⁿ)ₙ → 0
• Séries, somatórios parciais: uma maneira de interpretar um «somatório infinito»
• dois exemplos de séries convergentes
• um exemplo de série divergente: a séries harmônica

2022-12-15: IDMb (16,17) [video]

• (NIP) ⇒ (BW)
• Um toque de espaços métricos: como definir a diam
• Θ. raizes para reais pequenos
• Θ. √2
• O teorema de rearranjo de Riemann (e um problema com soma telescópica infinita)
• polinômios: algébricos vs transcedentais
• Algébricos vs transcedentais
• [Euler][Euler], a [constante e][number-e], [Liouville][Liouville]
• [Cantor][Cantor]: cobririndo uns subconjuntos de reais com seqüências
• Cantor: primeira demonstração que qualquer seqüência de reais
• Cantor: diagonalização
• [Borel][Borel], [Lebesgue][Lebesgue], [Kolmogorov][Kolmogorov]: um toque de teoria da medida: probabilidade de acertar um racional no [0,1] dos reais
• Integral Riemann vs Integral Lebesgue

2022-12-16: Prova 3.2

Futuro (fluido)