2024.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.

2024-09-18: IntroProof (hw1)

1. Capítulo 1
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.

2024-09-22: IntroProof (hw2)

1. Capítulo 2: até o primeiro intervalo de problemas
2. Para cada uma das proposições seguintes tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Se travar 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)]

2024-09-27: IntroProof (hw3)

1. Mostre que, tendo qualquer um dos 3 comandos “mágicos” (LEM, RAA, Contrapositive), consegue inferir os outros dois assim os ganhando como açúcares sintácticos sem precisar tê-los como comandos primitivos no sistema.
2. Volte às proposições que não conseguiu demonstrar, mas essa vez use ⛤: LEM, RAA, Contrapositive. Conseguindo fechar, altere o enunciado para ficar mais honesto (e fraco) mas compilável sem ⛤.

2024-09-30: IDMa (hw1)

1. Demonstre (nos ? precisa enunciar também)
   1. (+)-id: (∀x)[ 0+x = x & x+0 = x ]
   2. (+)-inv: ?
   3. (·)-id: ?
   4. (+)-id-!: ? (unicidade de (+)-identidade)
   5. (·)-id-!: ?
   6. (+)-inv-!: ?
   7. (+)-canR: (∀c,x,y)[ x + c = y + c ⇒ x = y ]
   8. (+)-canL: ?
   9. (·)-can: ?
   10. (+)-ann-0: (∀x)[ 0·x = 0 & x·0 = 0 ]
   11. (+),(·)-distR: (∀x,y,d)[ (x+y)d = xd + yd ]
   12. neg-1: (∀x)[x·(-1) = ?]
   13. neg-0: ?
   14. neg-neg: (∀x)[-(-x) = ?]
   15. neg-(+): ?
   16. neg-(·): ?

2024-10-03: IRI (hw1)

1. Defina (sem consulta) a adição, a multiplicação, e a exponenciação (nos Nats).
2. Calcule os:
   1. 2 + 3
   2. 3 + 2
   3. um dos: 4 · 1; 1 · 4
3. Defina uma função double que retorna o dobro da sua entrada.
4. Calcule os:
   1. double (double (S O))
   2. double ((S O) + (S (S O)))
5. Demonstre uma das: (·)-idL, (·)-idR
6. Demonstre uma das: (^)-idL, (^)-idR
7. Defina a função pred : 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 e de 2022.2 usou a pred em outras definições, estava errando
8. Defina as funções:
   1. fact : Nat → Nat
   2. fib  : Nat → Nat
   3. min  : Nat × Nat → Nat
   4. max  : Nat × Nat → Nat
   5. div  : Nat × Nat → Nat × Nat
   6. quot : Nat × Nat → Nat
   7. rem  : Nat × Nat → Nat
   8. gcd  : Nat × Nat → Nat
   9. lcm  : Nat × Nat → Nat

2024-10-07: IDMa (hw2)

1. Instale Lean e Haskell no teu computador (veja o FAQ de instalações).
2. Demonstre?:
   1. (·),(+)-distr: ?
   2. (+)-res: ?
   3. (·)-res: ?
   4. (·)-can∗: ?
   5. nzd: (∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]

2024-10-08: IRI (hw2)

1. Jogue (complete) o nng. (Recomendo trabalhar no «editor mode» (botão na top-right corner do jogo).)

2024-10-11: IDMa (hw3)

1. Cap «Os interios»: §«Primeiros passos»
2. Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência: nzd ⊣⊢ (·)-can*R

2024-10-11: IRI (hw3)

1. Cap «Recursão; Indução»: até a §«Demonstrando propriedades de naturais sem indução»

2024-10-14: IDMa (hw4)

1. Cap «Os inteiros»: até a §«Conjuntos fechados sob operações»

2024-10-16: IRI (hw4)

1. Cap «Recursão; Indução»: até a §«Por que aceitar o princípio da indução?»

2024-10-18: IDMa (hw4)

1. Resolva tudo que não resolveu na Prova IDMa.1.

2024-10-21: IDMa (hw5)

1. Cap «Inteiros»: até o §«Mínima e máxima»

2024-10-24: IDMa (hw6)

1. Cap «Inteiros»: até o primeiro intervalo de problemas

2024-11-18: IDMa (hw7)

1. Cap «Inteiros»: até a §«Melhor divisor comum»

2024-11-25: IRI (hw5)

1. Implemente como novo tipos, tendo já definido o Nat:
   1. os parzinhos-de-Nats
   2. listas-finitas-de-Nats como Nat
2. Defina as:
   1. length      : List α → Nat
   2. elem        : Nat → List Nat → Bool
   3. sum         : List Nat → Nat
   4. product     : List Nat → Nat
   5. (⧺)         : List Nat → List Nat → List Nat
   6. reverse     : List α → List α
   7. min         : Nat → Nat → Nat
   8. max         : Nat → Nat → Nat
   9. allEven     : List Nat → Bool
   10. anyEven     : List Nat → Bool
   11. allOdd      : List Nat → Bool
   12. anyOdd      : List Nat → Bool
   13. allZero     : List Nat → Bool
   14. anyZero     : List Nat → Bool
   15. addNat      : Nat → List Nat → List Nat
   16. multNat     : Nat → List Nat → List Nat
   17. expNat      : Nat → List Nat → List Nat
   18. enumFromTo  : Nat → Nat → List Nat
   19. enumTo      : Nat → List Nat
   20. take        : Nat → List α → List α
   21. drop        : Nat → List α → List α
   22. elemIndices : α → List α → List Nat
   23. pwAdd       : List Nat → List Nat → List Nat
   24. pwMult      : List Nat → List Nat → List Nat
   25. isSorted    : List Nat → Bool
   26. filterEven  : List Nat → List Nat
   27. filterOdd   : List Nat → List Nat
   28. minimum     : List Nat ⇀ Nat
   29. maximum     : List Nat ⇀ Nat
   30. isPrefixOf  : List Nat → List Nat → Bool
   31. mix         : List α → List α → List α
   32. intersperse : α → List α → List α
3. Defina as:
   1. head        : List α → α
   2. tail        : List α → List α
   3. init        : List α → List α
   4. last        : List α → α
4. 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) ℓ = ?? ]
5. 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
6. Pense em mais propriedades, enuncie, e demonstre!

2024-11-27: IDMa (hw8)

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.
3. Escreva sozinho a definição de m.d.c.
4. Troque o que precisa trocar para virar a definição de mínimo.
5. Troque o que precisa trocar para virar a definição de máximo.
6. Troque o que precisa trocar para virar a definição de m.m.c.
7. 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.
8. 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))
9. Demonstre: Invertible(x) ⇔ Unit(x)
10. Demonstre: Irreducible(x) ⇔ Prime(x)
11. Demonstre ou refute: para quaisquer primos distintos p,q, pq | n² ⇒ pq | n.
12. 🚀 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?

2024-12-06: IDMa (hw9)

1. Cap «Inteiros»: até o terceiro intervalo de problemas

2024-12-10: IDMa (hw10)

1. Investiga a aritmética dos planetas 1–6:
   1. Completa as tabelas de adição e de multiplicação.
   2. Para quais deles temos: (·)-inversos, (+)-inversos, (·)-cancelamento, (·)-inversos, zerodivisores, resoluções únicas
   3. Os inversos (quando tem) são únicos?

2024-12-16: IRI (hw6)

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 α?

Histórico

Quadros das aulas

• Quadro IDMa: lec09 – lec20
  Last update: 2024-12-18

• Quadro IRI: lec12
  Last update: 2024-12-16

2024-09-16: Meta & IntroProof (1)

• Overview
• tipos e type errors
• intensão vs extensão
• (=) vs (≡)
• type inference
• Os construtores de tipos (→) e (×)
• diss valores-de-verdade
• açúcar sintáctico

2024-09-18: IntroProof (2)

• umas definições bugadas de «_ é par»
• duas maneiras que uma definição pode ser errada
• REPLs e demonstrações
• proposiões vs objetos
• Prop vs Bool
• juízos (judgements) vs proposições
• comandos vs proposições
• Exemplos de teoremas e seus tabuleiros (estados) iniciais
• Dados e Alvo
• construtores de props e seus tipos
• os ¬,⇒,⇔,&,ou,∀,∃,=
• (∃): como usar
• variáveis frescas e nomes bons
• ocorrência de variável ligada e livre

2024-09-20: IntroProof (3)

• (∀): como atacar
• (⇒): como atacar
• (∃): como usar
• (ou): como atacar
• (&): como usar
• (=): como usar (substituição)
• contra o poeminha: «não podes supor seu próprio alvo»
• nomes bons e bairros
• mais açúcar sintáctico (Sejam …, (∀,,)[…])
• precedências entre (⇒),(&),(ou)

2024-09-23: IntroProof (4)

• o resto dos conectivos para nossa linguagem de demonstrações
• os ⇒,&,ou,∀,∃,=,⊥ como primitivos
• os ⇔,¬,⇐ como açúcar sintáctico
• como usar e como atacar (cada um dos conectivos)
• quando e como aceitar uma suposta “lei de lógica”
• conexões entre ataques/usos de disjunção/conjunção e usos/ataques de conjunção/disjunção
• conexões entre disjunção/conjunção e quantificação existencial/universal
• conexões entre implicação e quantificação universal
• umas “leis de lógica” e como demonstrá-las
• a linguagem low-level
• o «xou»

2024-09-25: IntroProof (5)

2024-09-27: IntroProof (6)

• Vou demonstrar _.
• Θ. a irrefutabilidade do LEM
• magias ⛤
• LEM
• RAA
• Contrapositiva
• a briga Brouwer vs Hilbert

2024-09-30: IDMa (1)

• Convenção sobre (∀)[…]
• «_ é um _-inverso de _» e predicados similares
• Igualdade: refl, sym, trans, subst/repl
• refl e subst são suficientes para inferir as sym e trans
• Θ. (+)-idL
• Calculamos: notação, efeitos, convenções

2024-10-02: IRI (1)

IntroProof

• IntroProof: existência e unicidade
• IntroProof: (∃!x:α)[φ(x)] como açúcar sintáctico
• IntroProof: $\exists_{\geq n} x : \alpha)[ \varphi(x) ]$
• IntroProof: $\exists_{\leq n} x : \alpha)[ \varphi(x) ]$
• IntroProof: definição vs especificação: Nat de IRI vs Int de IDMa
• IntroProof: números vs numerais
• 4 maneiras de definir o tipo de dados Nat
• casamento de padrões
• notação de cálculos e suas justificativas
• 2 + 3 = 5
• 2 + 3 ≢ 3 + 2

2024-10-04: IDMa (2)

• IntroProof: (≝) vs (=)
• funções anônimas
• muitos teoremas parecidos e como demonstrá-los
• (+)-id vs (+)-id-0
• currificação teaser: α×β→γ vs α→β→γ
• duas maneiras de demonstrar o (+)-canR
• como justificar o «aplique a (+ (-c)) nos dois lados»

2024-10-07: IDMa (3)

• IntroProof: açúcar: (∀x legal)[φ(x)] e (∃x legal)[φ(x)]
• IntroProof: zoom-in/out de modo rua para modo formal e vice-versa
• IntroProof: DRY: não re-demonstre as mesmas idéias em novas demonstrações
• (·)-canR*: 3 intensões
• subtração como operação definida: _-_ : Int × Int → Int
• mais uma convenção sintáctica: justaposição
• mundo aditivo vs mundo aplicativo
• necessidade de algum axioma os conectando
• specification update: (·),(+)-distrR
• 3 proposições difíceis de demonstrar
  • (·)-annR-0
  • (·)-canR∗
  • nzd
• Θ. (·)-annR-0

2024-10-09: IRI (2)

• pattern-matching com match-with expressions
• definição da (·)
• especificação vs implementação: por que não podemos considerar o (+)-ass como axioma aqui
• tentativa sem sucesso: demonstrar o (+)-ass
• dois princípios sobre construtores
• lazy vs strict evaluation

2024-10-11: IRI (3); IDMa (3⁺)

• buraquizando subexpressões
• limitações da notação de buracos
• a notação ↦
• a notação λ
• currificação
• nzd e (·)-can*R: axiomas ou teoremas?

2024-10-14: IDMa (4)

• terminologia de ordens
• D. (|) : Int × Int → Prop
• divide, mede, é multiplo de, é (|)-maior de, é (|)-menor de, …
• Θ. (|)-refl
• Θ. (|)-trans
• Θ. (|)-bottom-1
• Θ. (|)-top-0
• maneiras alternativas de rotular dados
• criando dados on the fly
• «pela escolha de»
• notação de conjuntos; set comprehension
• conjunto fechado sobre operação binária
• novamente: os açúcares (∀x∈A)[φ(x)] e (∃x∈A)[φ(x)]

2024-10-16: IRI (4)

• Indução
• O comando Por indução.
• 3 demonstrações da associatividade da (+)
• Indução como regra de inferência
• Base & Passo indutivo como regras de inferência

2024-10-18: IDMa (5⁻); Prova IDMa.1

• Conjuntos e sua notação, incluindo o set builder (comprehension)
• gerador x ∈ A vs proposição x ∈ A
• Prova IDMa.1

2024-10-21: IDMa (5)

• Set : Type → Type
• Positividade e ordem, e sua “equivalência”
• Especificação de inteiros v3/?: Pos & seus axiomas
• Θ. (∀a ≠ 0)[ a² positivo ]
• Θ?. 1 é positivo

2024-10-23: IDMa (6); IRI (5)

• 0≠1?
• (Meta)demonstrando a não-demonstrabilidade e a não-refutabilidade de proposições
• Inteiros, especificação v4/?
• Entendendo o princípio da indução em mais uma forma
• Os construtores preservam/respeitam uma propriedade
• teoremas sobre Nats, suas operações, e suas relações principais
• implementando as ev e od
• Não abusarás tipos e seus habitantes.
• reimplementando as ev e od
• O tipo Bool

2024-10-25: IDMa (7)

• valor absoluto
• mínima e máxima
• unicidade de mínimo de conjunto
• valor absoluto

2024-10-30: IRI (6)

• Internalização de conceitos
• Corretude (soundess and completeness)
• leq : Nat → Nat → Bool
• eq : Nat → Nat → Bool
• 3 maneiras diferentes de implementar os ev e od
• Recursão mútua
• O tipo ListNat

2024-11-01: IRI (7)

• List : Type → Type
• length, sum, prod
• abstraindo de doubles e triples para mults e para map

2024-11-04: IDMa (8)

• Especificação de inteiros (v5/5)
• O princípio da indução
• O princípio da boa ordem

2024-11-06: IRI (8)

• recursão/indução de ListNat
• presentes de recursão
• index : Nat → ListNat → Nat
• head, last : ListNat → Nat
• init, tail : ListNat → ListNat
• Θ. (∀f : Nat → Nat)(∀ℓ : ListNat)[ length (map f ℓ) = length ℓ ]

2024-11-08: IDMa (9)

• Justificando versões de indução nos inteiros
• Indução «a partir de c»
• Indução para os negativos
• Indução para os pares
• Indução com b bases
• Indução forte

2024-11-11: IRI (9)

• Tentativas de implementar os inteiros
• Polimorfismo
• de ListNat para List α

2024-11-13: IDMa (10)

• PBO e versões inferíveis
• Como usar o PBO na prática
• Θ. ¬(∃x)[ 0 < x < 1 ]
• Wishlist

2024-11-18: IDMa (11)

• Sistemas posicionais de numerais
• Θ. Divisão (de Euclides)
• mdc: melhor divisor comum
• Desenhando a (|) no $\mathbb Z_{\geq 0}$

2024-11-22: IDMa (12)

• Desenhando a (|) nos inteiros
• Vocabulário: associados, invertíveis, unidades, irredutíveis, primos
• Propriedades da (|)
• Desenhar a busca de mdc
• mais 3 teoremas de Euclides:
  • infinitude dos irredutíveis
  • irredutível ⇔ primo
  • existência de mdc

2024-11-25: IRI (10)

• Recursão e indução em listas
• (⧺) : L α → L α → L α
• Θ. sum (xs ⧺ ys) = sum xs + sum ys

2024-11-27: IDMa (13)

• existência de mdc
• conjuntos fechados sob operações
• membros arbitrários
• propriedades de mdc
• algoritmo de Euclides para mdc

2024-11-29: IDMa (14)

• Θ. (a,b) = (b,r)
• teorema de existência mdc (com PBO)
• teorema de existência mdc (de Euclides)
• algoritmo de Euclides para mdc
• corretude e terminação
• eficiência: criança-BR vs euclides
• Lemma de Euclides: p irredutível ⇒ p primo

2024-12-02: IRI (11)

• abstraindo
• pw (pointwise)
• fold
• let-in expressions

2024-12-04: IDMa (15)

• Teorema de Euclides (infinidade de irredutíveis)
• Teorema Fundamental de Aritmética

2024-12-06: IDMa (16)

• Logaritmos
• Θ. Sistemas posicionais de numerais
• Somatórios e produtórios, notação Σ–Π
• Lemmas spoilerosos de irracionalidades

2024-12-09: IDMa (17)

• comb(r,n): definição
• Teorema binomial
• “planetas” e aritmética modular

2024-12-11: IDMa (18)

• tabelas de operações
• planetas com zerodivisores
• planetas sem (·)-cancelamento*
• congruência modulo um inteiro
• (≡ₘ) é uma congruência
• compatibilidade com operações
• o planeta 0

2024-12-13: IDMa (19)

• invertibilidade modulo m
• critéria de divisibilidade

2024-12-16: IRI (12)

• a verdadeira cara do void da C
• a verdadeira interpretação da f() da C
• o tipo Unit (𝟙)
• o tipo Empty (𝟘)
• funções saindo e entrando de 𝟙
• funções saindo e entrando de 𝟘
• teaser: aritmética de tipos
• Maybe α
• Either α β
• soma de tipos
• billion dollar mistake

2024-12-18: IDMa (20)

• exponenciação modulo m
• Θ. Sonho do calouro
• Θ. Fermatinho
• Sistemas (completos e reduzidos) de resíduos

Futuro (fluido)