Introdução

Olá, mundo! Sejam bem-vindos ao maravilhoso mundo da programação. Este é um campo incrivelmente emocionante e desafiador, repleto de possibilidades e oportunidades. Estamos ansiosos para ver o que vocês irão criar e construir durante sua jornada de aprendizado.

Quando se trata de programação, é fundamental entender a importância da precisão e da segurança no código. É por isso que gostaríamos de falar sobre o Kind, um poderoso verificador formal de modelos de sistemas de tempo real. Ele permite que você especifique propriedades desejadas para seu sistema e gera automaticamente casos de teste para garantir que o sistema atenda a essas propriedades. Isso é particularmente valioso para projetos críticos, como sistemas de segurança, onde a precisão e a segurança são fundamentais.

A programação é uma jornada constante de aprendizado e desenvolvimento pessoal. Não se sinta desanimado se encontrar dificuldades no caminho, essas dificuldades fazem parte do processo de aprendizado e são oportunidades para crescer e evoluir. Lembre-se de que estamos aqui para ajudá-los ao longo do caminho, não hesite em pedir ajuda se precisar.

Esteja preparado para trabalhar duro e enfrentar desafios, mas também esteja preparado para celebrar suas conquistas e realizações. Lembre-se de se divertir e aproveitar cada momento dessa incrível jornada de aprendizado.

Boas sorte em sua jornada de aprendizado e estamos ansiosos para ver o que vocês irão criar e construir.

Começando

Seja bem-vindo ao Kind

Para uma linguagem eficiente, minimalista e prática, que visa repensar a programação funcional do zero, com um design moderno e consistente.

O objetivo desta documentação é ser tão simples quanto possível para aprender o Kind. Por isso, decidimos adotar um design minimalista e simples, para que você possa encontrar rapidamente o que precisa.

Índice de navegação rápida

• Sobre o Kind;
• Guia de instalação para MacOS, Linux e Windows;
• Guia de Comandos;
• Aprendendo os conceitos básicos do Kind;

Olá, Kind

Kind é uma linguagem de programação que tem como objetivo ser prática e convencional. Ela é tipada estaticamente, o que significa que os tipos de dados são definidos previamente e verificados em tempo de compilação. Esses tipos são poderosos o suficiente para permitir a prova de teoremas matemáticos.

Ao criar um novo programa em Kind, você tem acesso a um vasto universo de recursos e funcionalidades. É como se todas as ferramentas que você precisa já estivessem lá, prontas para serem utilizadas. A cada nova função ou biblioteca que você descobre, é como se uma nova parte desse universo fosse revelada.

Assim como em um universo real, há sempre algo novo para ser descoberto em Kind. Há uma infinidade de recursos e ferramentas disponíveis para você explorar e usar em seus programas. Com tanta variedade, é possível criar soluções para praticamente qualquer problema que você possa imaginar.

Se você está interessado em aprender mais sobre programação e explorar o vasto universo de Kind, então se tornar um programador Kind pode ser uma aventura emocionante e gratificante. Há muitos outros programadores Kind lá fora para colaborar e aprender junto com você, tornando essa jornada ainda mais emocionante.

Em resumo, Kind é uma linguagem de programação moderna, poderosa e versátil, que oferece muitas oportunidades para quem quer aprender e explorar o vasto universo da programação. Se você está interessado em se tornar um programador Kind, há muitos recursos disponíveis para ajudá-lo a começar, desde documentação oficial até comunidades ativas de usuários e desenvolvedores.

Instalação

Este guia ensina como baixar e instalar o Kind através do Rust, Com o "Cargo" uma ferramenta usada para gerenciar pacotes. É possível que seja necessário ter uma conexão com a internet para prosseguir com este guia.

Primeiramente, instale o Rust usando este link

• Atualmente, o Cargo é a única maneira de instalar o Kind.
• Este guia foi escrito quando o Kind estava na versão em beta. Portanto, é necessário instalar a versão do Channel nightly.

Instalando o Kind no Linux ou MacOS

Use seu gerenciador de pacotes (Cargo) para instalar o Kind. Para isso, abra o terminal e digite o seguinte código:

cargo +nightly install kind2

Instalando o Kind no Windows

Para usuários do Windows, é possível usar o Kind através do CMD ou WSL2. Se escolher o WSL o método de instalação está neste link.

Use seu gerenciador de pacotes (Cargo) para instalar o Kind. Para isso, abra o Bash(WSL2) ou Terminal(CMD) e digite o seguinte comando:

cargo +nightly install kind2

Clonando o Repositório do Kind - Método 1

Clone o repositório do Kind usando o comando do git "git clone", da seguinte forma:

git clone https://github.com/HigherOrderCO/Kind

Depois do passo de clone, use o seguente comando para a instalação

cargo +nightly install --path crates/kind-cli --force

Clonando o Repositório do Kind - Método 2

O cargo permite instalar usando o git, sem a necessidade de clonar algum repositório, da seguinte forma:

cargo +nightly install --git https://github.com/HigherOrderCO/kind.git 

Ao seguir os passos acima, podemos começar a usar o Kind.

Olá, Mundo

Neste ponto, o Kind já deve estar instalado em sua máquina. Se não, volte para a instalação e siga as instruções.

Neste guia, serão usadas linhas de comando e editores de texto, então certifique-se de que o terminal esteja aberto para prosseguir com os passos.

Criando os documentos

Primeiro de tudo, crie um diretório para armazenar os arquivos do Kind. É recomendável usar um diretório dedicado para manter todos os exercícios e exemplos, mas sinta-se à vontade para fazer o que quiser. Os três comandos abaixo criarão um diretório chamado 'KindExamples' e um arquivo chamado 'hello_world.kind2' dentro do diretório do projeto. Use-os na ordem:

mkdir KindExamples
cd    KindExamples
touch hello_world.kind2 //CMD use "copy nul hello_world.kind2 > nul"

A extensão .kind2 é o que faz dele um arquivo Kind. Por exemplo, um arquivo que termina com .exe é um executável; .js é um arquivo JavaScript; .rs é um arquivo Rust, etc. Se os comandos foram usados corretamente, o arquivo hello_world.kind2 deve estar dentro da pasta KindExamples. Então é hora de se divertir, CODING!

Hello World

Abra o arquivo hello_world.kind2 no editor de texto, ele estará vazio, mas não se preocupe. A partir de agora, haverão alguns conceitos avançados. Tudo fará sentido no futuro, esses conceitos que são pertinentes serão explicados no tempo devido. É recomendado que você digite manualmente os códigos, em vez de copiá-los e colá-los em seu arquivo.

Vamos escrever seu primeiro código no arquivo hello_world.kind2:

Main {
  "Hello, Kind!"
}

Type Checking

Com o código pronto, você deve usar a Verificação de Tipo para verificar se tudo está em ordem. O verificador de tipo ainda é desconhecido neste guia, mas será explicado com mais detalhes posteriormente. Por enquanto, basta entendê-lo como um verificador que verifica se o arquivo está corretamente "tipado".

Para verificar o tipo de um arquivo Kind, basta usar o comando kind2 check nomeDoArquivo.kind2. Para o arquivo hello_world.kind2, seria:

kind2 check hello_world.kind2

A mensagem "All terms check." significa que seu arquivo está pronto!

All terms check.

A verificação de tipo está correta? Então vamos executar o código.

Executando o código

Para executar um arquivo no Kind, use o comando kind2 run nomeDoArquivo.kind2. Deve parecer assim:

kind2 run hello_world.kind2

E pronto! seu terminal deve imprimir "Hello, Kind!" de volta para você.

Lembre-se de todos os passos acima, verifique o tipo e depois execute

Ótimo, agora que você tem seu primeiro programa Kind rodando, você pode começar a explorar mais sobre a linguagem e suas funcionalidades. Parabéns pelo seu progresso!

Se tiver alguma dúvida ou precisar de ajuda, não hesite em perguntar. Estou sempre à disposição para ajudar!

Olá Kind

Agora que você aprendeu como criar um arquivo Kind e executá-lo, vamos aprofundar mais nas bases do Kind. Na próxima seção, você aprenderá sobre o sistema de tipos do Kind, sintaxe, variáveis e funções.

Sistema de tipos do Kind

O Kind possui um sistema de tipos estático, o que significa que o tipo de uma variável deve ser conhecido em tempo de compilação. O Kind possui um sistema de tipos rico que inclui tipos primitivos, tipos de dados algébricos e parâmetros de tipo.

Sintaxe do Kind

A sintaxe do Kind é inspirada em linguagens de programação funcional como Haskell. A sintaxe é concisa e expressiva, tornando fácil de ler e escrever código. Ela usa indentação em vez de chaves para definir blocos de código.

Variáveis

No Kind, as variáveis são declaradas usando a palavra-chave let seguida pelo nome da variável. Por exemplo:

let x = 42

Funções

As funções no Kind são declaradas usando a primeira letra maiúscula. A função pode recebe parâmetros ou não e retorna um valor. Por exemplo:

Nat.add (a: Nat) (b: Nat) : Nat

Este é apenas um breve resumo das bases do Kind. Você aprenderá mais sobre esses conceitos conforme progredir na guia. Agora que você aprendeu sobre as bases do Kind, é hora de seguir para a próxima seção e aprender sobre conceitos avançados na programação do Kind.

Básico

Introdução

O estilo de programação funcional traz programação mais perto da simples e cotidiana matemática: Se um procedimento ou método não tem efeitos colaterais, então (ignorando eficiência) só o que precisamos entender sobre ele é como mapear entradas para saídas - ou seja, podemos pensar nele como um método concreto que computa uma função matemática. Esse é um dos sentidos do "funcional" em "programação funcional". A conexão direta entre programas e objetos matemáticos simples suporta tanto a formalidade de provas de corretude quanto a racionalização informal sobre o comportamento do programa.

O outro sentido na qual programação funcional é "funcional" é que ela enfatiza o uso de funções "ou métodos" como valores de primeira classe - ou seja, valores que podem ser passados como argumentos para outras funções, retornados como resultados, incluídos em estruturas de dados, etc. O reconhecimento de que funções podem ser tratadas desse jeito como dados habilita uma gama de comandos úteis.

Outras funcionalidades comuns de linguagens funcionais incluem algebraic data types e pattern matching, o que torna fácil construir e manipular estruturas de dados, e sistemas de tipo polimórficos sofisticados, suportando abstração e reuso de código. Kind contém todas essas funcionalidades.

A primeira metade desse capítulo introduz os elementos mais básicos da linguagem de programação funcional Kind. A segunda metade introduz algumas técnicas básicas que podem ser usadas para provar propriedades em programas em Kind.

Tipos Enumerados

Um aspecto incomum do Kind, similar a outras linguagens de prova como Idris e Coq, é que o seu conjunto de ferramentas built-in é bastante pequeno. Por exemplo, ao invés de fornecer o leque usual de tipos primitivos (booleanos, listas, strings, etc), Kind tem apenas dois tipos primitivos (U60: números inteiros em 60 bits binários, sem sinal) e (F60: números de ponto flutuante em 60 bits binários, sem sinal) e oferece um mecanismo poderoso para definir novos tipos de dados do zero, do qual pode-se derivar todos esses tipos já familiares e outros.

Para demonstrar como funciona o mecanismo de definição, vamos começar com um exemplo simples.

Dias da semana

A declaração a seguir diz para o Kind que estamos declarando um novo conjunto de dados - um Tipo.

type Dia { // Dia é um Tipo
  segunda  // Segunda é um Dia
  terca    // Terça   é um Dia
  quarta   // Quarta  é um Dia
  quinta   // Quinta  é um Dia
  sexta    // Sexta   é um Dia
  sabado   // Sábado  é um Dia
  domingo  // Domingo é um Dia
  }

O tipo se chama Dia, e seus membros são Segunda, Terça, Quarta, etc. A definição <nome> : <tipo> pode ser lida como: "nome é um tipo". Acima temos tanto um exemplo de criar um tipo novo Dia : Type, quanto a de declarar um elemento de um tipo existente Quarta : Dia.

Agora que temos definido o que é um Dia, podemos escrever funções que operam usando esse tipo. Digite o seguinte:

ProximoDiaUtil (d: Dia) : Dia

Isso declara que temos uma função chamado ProximoDiaUtil, que recebe um argumento chamado d, do tipo Dia, e retorna um Dia. Continue a definição da função da seguinte forma:

ProximoDiaUtil Dia.segunda  = ?
ProximoDiaUtil Dia.terca    = ?
ProximoDiaUtil Dia.quarta   = ?
ProximoDiaUtil Dia.quinta   = ?
ProximoDiaUtil Dia.sexta    = ?
ProximoDiaUtil Dia.sabado   = ?
ProximoDiaUtil Dia.domingo  = ?

O que estamos fazendo aqui é o que chamamos de pattern matching. Estamos declarando como a função deve rodar para cada possibilidade da entrada d. Nem sempre será necessário fazer isso, como será mostrado em exemplos mais a frente.

Por fim, complete as funções escrevendo o que cada uma deve retornar, e use espaços para estilizar como preferir:

ProximoDiaUtil Dia.segunda = Dia.terca
ProximoDiaUtil Dia.terca   = Dia.quarta
ProximoDiaUtil Dia.quarta  = Dia.quinta
ProximoDiaUtil Dia.quinta  = Dia.sexta
ProximoDiaUtil Dia.sexta   = Dia.segunda
ProximoDiaUtil Dia.sabado  = Dia.segunda
ProximoDiaUtil Dia.domingo = Dia.segunda

Com a função finalizada, nós podemos checar o funcionamento dela com alguns exemplos. O jeito principal de fazer isso em Kind é criar uma função Main no seu arquivo, e rodando ele com o comando kind2 run <file>.

Por exemplo, se você escrever a seguinte Main e rodar o arquivo

Main {
  // Dois dias úteis depois do sábado
  ProximoDiaUtil (ProximoDiaUtil Sabado)
}

Deve ser retornado pra você algo como:

(Dia.terca)

Outro jeito de testar seu código, é dizer o que esperamos que o código retorne, por meio de uma prova:

// O terceiro dia útil depois de uma segunda é uma quinta
TesteDiaUtil : Equal Dia (ProximoDiaUtil (ProximoDiaUtil (ProximoDiaUtil Dia.segunda))) Dia.quinta
TesteDiaUtil = Equal.refl

Os detalhes de como provas funcionam serão explicados mais a frente. No momento, o que precisa ser entendido disso é:

• Tem-se a constatação de que (ProximoDiaUtil (ProximoDiaUtil (ProximoDiaUtil Dia.segunda))) é igual a Dia.quinta
• Essa constatação foi nomeada TesteDiaUtil
• TesteDiaUtil = Equal.refl diz que constatação pode ser provada usando apenas simplificação nos dois lados

Para testar que essa prova (e qualquer outra prova adiante) está correta, você precisa checar o arquivo, usando o comando kind2 check <file>, que deve te retornar algo como:

All terms check.

Booleanos

Semelhantemente, podemos declarar o tipo Bool, para booleanos:

type Bool {
	true
	false
}

Nós estamos declarando nossos próprios booleanos só para demonstrar como fazer tudo do zero. O Kind tem a sua implementação padrão de booleanos no pacote padrão (o Wikind), junto de várias outras estruturas e provas. Na verdade, no momento de escrita, é necessário que você esteja trabalhando dentro da pasta Wikind para fazer provas e teoremas, pois ainda não temos um gerenciador de pacote e os utilitários de resolução de provas não são built-in.

Funções que funcionam sobre booleanos são definidas do mesmo jeito que visto anteriormente:

// Negação lógica
Notb (b: Bool) : Bool
Notb Bool.true  = Bool.false
Notb Bool.false = Bool.true

// E lógico
Andb (b1: Bool) (b2: Bool) : Bool
Andb Bool.true  b2 = b2
Andb Bool.false b2 = Bool.false

// OU lógico
Orb (b1: Bool) (b2: Bool) : Bool
Orb Bool.true  b2 = Bool.true
Orb Bool.false b2 = b2

As últimas duas funções demonstram como é a sintaxe do Kind para funções de múltiplos argumentos, e também mostra que é possível fazer pattern matching apenas em parte das variáveis da função, não necessariamente todas.

Os casos da última função podem ser testados exaustivamente (todas as possibilidades) como mostrado a seguir, criando a tabela verdade da operação lógica.

TestOrb1 : Equal Bool (Orb Bool.true Bool.false) Bool.true
TestOrb1 = Equal.refl

TestOrb2 : Equal Bool (Orb Bool.false Bool.false) Bool.false
TestOrb2 = Equal.refl

TestOrb3 : Equal Bool (Orb Bool.false Bool.true) Bool.true
TestOrb3 = Equal.refl

TestOrb4 : Equal Bool (Orb Bool.true Bool.true) Bool.true
TestOrb4 = Equal.refl

Nandb

Substitua o buraco "?", completando a função seguinte; então confira se ela está correta usando as constatações a seguir (Análogo a como foi feito para a função Orb). A função retorna Bool.true se qualquer uma de suas entradas for Bool.false

Nandb (b1: Bool) (b2: Bool) : Bool
Nandb b1 b2 = ?

Test_nandb1 : Equal Bool (Nandb Bool.true Bool.false) Bool.true
Test_nandb1 = ?

Test_nandb2 : Equal Bool (Nandb Bool.false Bool.false) Bool.true
Test_nandb2 = ?

Test_nandb3 : Equal Bool (Nandb Bool.false Bool.true) Bool.true
Test_nandb3 = ?

Test_nandb4 : Equal Bool (Nandb Bool.true Bool.true) Bool.false
Test_nandb4 = ?

And3

Faça o mesmo para a função Andb3 abaixo. Essa função deve retornar Bool.true se todas as entradas forem Bool.true, e Bool.false caso contrário

Andb3 (b1: Bool) (b2: Bool) (b3: Bool) : Bool
Andb3 b1 b2 b3 = ?

Test_andb3_1 Equal Bool (Andb3 Bool.true Bool.true Bool.true) Bool.true
Test_andb3_1 = ?

Test_andb3_2 Equal Bool (Andb3 Bool.false Bool.true Bool.true) Bool.false
Test_andb3_2 = ?

Test_andb3_3 Equal Bool (Andb3 Bool.true Bool.false Bool.true) Bool.false
Test_andb3_3 = ?

Test_andb3_4 Equal Bool (Andb3 Bool.true Bool.true Bool.false) Bool.false
Test_andb3_4 = ?

Tipos de função

Todas as expressões em Kind tem um tipo, descrevendo que tipo de coisa ela computa. Por exemplo: Bool.true tem tipo Bool, assim como Notb Bool.true também tem tipo Bool.

Funções como Notb, antes de receberem argumentos, também tem um tipo, tal qual Bool.true ou Bool.false. Os seus tipos são chamados de Tipo de Função, e são denotados com setas.

Notb, por exemplo, seria denotado como Bool -> Bool, que pode ser lido como "uma função que recebe um Bool como entrada, e retorna um valor de tipo Bool". Similarmente, o tipo da função Andb é Bool -> Bool -> Bool, significando "uma função que recebe dois argumentos do tipo Bool e retorna um valor de tipo Bool".

Módulos

Não temos sistema de módulos ainda :pensive:. Para usar funções de outros arquivos, precisa-se criar um arquivo dentro do mesmo diretório (Exemplo: a pasta raiz do Wikind).

Números

Os tipos que definimos até agora são exemplos de tipos enumerados: suas definições enumeram explicitamente um conjunto finito de elemento. Um jeito mais interessante de definir um tipo é estabelecer uma coleção de regras indutivas descrevendo seus elementos. Por exemplo, nós podemos definir os números naturais da seguinte maneira:

type Nat {
  zero
  succ (pred: Nat)
}

Essa definição pode ser lida como:

• Nat.zero é um número natural;
• Nat.succ é um construtor que recebe um número natural, construindo outro número natural;
  • Ou seja, se n é um número natural, então (Nat.succ n) também será.

Todo tipo definido indutivamente (Como Nat, Bool ou Dia) é um conjunto de expressões. A definição de Nat diz como expressões do tipo Nat podem ser construídas:

• A expressão Nat.zero pertence ao conjunto dos Nat;
• Se n é uma expressão do conjunto dos Nat, então (Nat.succ n) também é uma expressão do conjunto dos Nat; e
• Expressões formadas dessas duas formas são as únicas que pertencem à Nat.

As mesmas regras se aplicam para nossas definições de Dia e Bool. As anotações que usamos para eles são análogas à do construtor Nat.zero, indicando que não recebem nenhum argumento.

Essas três condições demonstram o poder das declarações indutivas. Elas implicam que a expressão Nat.zero, a expressão (Nat.succ Nat.zero), a expressão (Nat.succ (Nat.succ Nat.zero)) e assim por diante, são do conjunto Nat, enquanto outras expressões como Bool.true, (Andb Bool.true Bool.false), e (Nat.succ (Nat.succ Bool.false)) não são.

Nós podemos escrever funções simples usando pattern matching em números naturais da mesma forma que fizemos acima - por exemplo, a função predecessor:

Pred (n: Nat) : Nat
// Como números naturais são estritamente não-negativos,
// usamos como convenção que qualquer coisa que seria
// menor do que 0 retorna 0
Pred  Nat.zero    = Nat.zero
Pred (Nat.succ k) = k

O segundo pattern pode ser lido como: "se n tem a forma (Nat.succ k) para algum k, retorne k."

MinusTwo (n: Nat) : Nat
MinusTwo  Nat.zero               = Nat.zero
MinusTwo (Nat.succ  Nat.zero)    = Nat.zero
MinusTwo (Nat.succ (Nat.succ k)) = k

Para evitar ter que escrever uma sequência de Nat.succ toda vez que você quiser um Nat, é possível usar sufixo n ao final de número qualquer, exemplo o5n, que recebe um número escrito no tipo primitivo U60 mais o sufixo n e retorna o Nat correspondente. {...}

Test : Equal Nat 6n (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))
Test = Equal.refl

O construtor Nat.succ tem tipo Nat -> Nat, assim como as funções MinusTwo e Pred. Todos eles são coisas que, ao serem aplicadas a um Nat, retornam um Nat. A diferença essencial entre o Nat.succ e os outros dois, no entanto, é que funções vem com regras de redução - por exemplo, Pred (Nat.succ Nat.zero) é reduzível para Nat.zero - enquanto que o Nat.succ não. Apesar de ele ser uma função aplicável a um argumento, ela não computa nada.

Para a maioria das definições de funções de números, só pattern matching não é suficiente: nós precisaremos também de recursão. Por exemplo, para checar que um número n é par, nós podemos checar recursivamente se n-2 é par.

Evenb (n: Nat) : Bool
Evenb  Nat.zero               = Bool.true
Evenb (Nat.succ  Nat.zero)    = Bool.false
Evenb (Nat.succ (Nat.succ k)) = Evenb k

Nós podemos definir Oddb (função para checar se um número é ímpar) com uma declaração recursiva semelhante, mas também temos uma definição mais simples e um pouco mais fácil de trabalhar:

Oddb (n: Nat) : Bool
Oddb n = Notb (Evenb n)

TestOddb1 : Equal Bool (Oddb 1n) Bool.true
TestOddb1 = Equal.refl

TestOddb2 : Equal Bool (Oddb 4n) Bool.false
TestOddb2 = Equal.refl

Naturalmente, nós também podemos definir funções com múltiplos argumentos por recursão.

Plus (n: Nat) (m: Nat) : Nat
Plus  Nat.zero    m = m
Plus (Nat.succ k) m = Nat.succ (Plus k m)

Somar 3n e 2n retornará 5n como esperado. A simplificação que o Kind realiza para chegar a esse valor pode ser visualizada assim:

Plus (Nat.succ (Nat.succ (Nat.succ Nat.zero))) (Nat.succ (Nat.succ Nat.zero))

> Nat.succ (Plus (Nat.succ (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Plus (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Nat.succ (Plus Nat.zero (Nat.succ (Nat.succ Nat.zero)))))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))
pela primeira regra de Plus

A multiplicação pode ser definida usando a definição de Plus, da seguinte forma:

Mult (n: Nat) (m: Nat) : Nat
Mult  Nat.zero    m = Nat.zero
Mult (Nat.succ k) m = Plus m (Mult k m)

TestMult1 : Equal Nat (Mult 3n 3n) 9n
TestMult1 = Equal.refl

Você também pode usar pattern matching em duas expressões ao mesmo tempo:

Minus (n: Nat) (m: Nat) : Nat
Minus  Nat.zero     m           = Nat.zero
Minus  n            Nat.zero    = n
Minus (Nat.succ k) (Nat.succ j) = Minus k j

O função Exp pode ser definida usando Mult (de forma análoga a como se define Mult usando Plus):

Exp (base: Nat) (power: Nat) : Nat
Exp base  Nat.zero    = Nat.succ Nat.zero
Exp base (Nat.succ k) = Mult base (Exp base k)

Factorial

Lembrando da definição matemática básica de fatorial:

\[\mathrm factorial(n) = \begin{cases} \text{se $n$} = 0\,& 1\\ \text{caso contrário}, & n * factorial(n-1) \end{cases} \]

\[ f(x)=\begin{cases}x&(x = 1)\\xf(x-1)&(x\gt 1)\end{cases} , x\in \Bbb{N} \] Traduza a função fatorial para Kind2:

Factorial (n: Nat) : Nat
Factorial n = ?

TestFactorial1 : Equal Nat (Factorial 3n ) 6n
TestFactorial1 = ?

TestFactorial2 : Equal Nat (Factorial 5n) 120n
TestFactorial2 = ?

A função Eql testa a igualdade entre Naturais, retornando um booleano

Eql (n: Nat) (m: Nat) : Bool
Eql  Nat.zero     Nat.zero    = Bool.true
Eql  Nat.zero    (Nat.succ j) = Bool.false
Eql (Nat.succ k)  Nat.zero    = Bool.false
Eql (Nat.succ k) (Nat.succ j) = Eql k j

A função Lte testa se o primeiro argumento é menor ou igual ao segundo, retornando um booleano

Lte (n: Nat) (m: Nat) : Bool
Lte  Nat.zero     m           = Bool.true
Lte (Nat.succ k)  Nat.zero    = Bool.false
Lte (Nat.succ k) (Nat.succ j) = Lte k j

TestLte1 : Equal Bool (Lte 2n 2n) Bool.true
TestLte1 = Equal.refl

TestLte2 : Equal Bool (Lte 2n 4n) Bool.true
TestLte2 = Equal.refl

TestLte3 : Equal Bool (Lte 4n 2n) Bool.false
TestLte3 = Equal.refl

Blt_nat

A função Blt_nat testa a relação "menor que" em números naturais. Em vez de criar uma nova função recursiva, defina ela usando funções previamente definidas.

Blt_nat (n: Nat) (m: Nat) : Bool
Blt_nat n m = ?

Test_blt_nat_1 : Equal Bool (Blt_nat 2n 2n) Bool.false
Test_blt_nat_1 = ?

Test_blt_nat_2 : Equal Bool (Blt_nat 2n 4n) Bool.true
Test_blt_nat_2 = ?

Test_blt_nat_3 : Equal Bool (Blt_nat 4n 2n) Bool.false
Test_blt_nat_3 = ?

Prova por Simplificação

Agora que definimos alguns tipos de dados e funções, vamos começar a provar propriedades de seus comportamentos. Na verdade, já estamos fazendo isso: cada função das seções anteriores que começa com Test, faz uma afirmação precisa sobre o comportamento de alguma função para algumas entradas especificas. As provas dessas afirmações foram sempre a mesma: use Equal.refl para checar que ambos os lados são de fato idênticos.

O mesmo tipo de "prova por simplificação" pode ser usada para provar propriedades mais interessantes. Por exemplo, o fato que o Nat.zero é um "elemento neutro" no lado esquerdo da adição pode ser provado apenas observando que Plus Nat.zero n reduz para n, independente do que é n, fato que pode ser lido diretamente na definição do Plus.

Plus_Z_n (n: Nat) : Equal Nat (Plus Nat.zero n) n
Plus_Z_n n = Equal.refl

Outros teoremas parecidos podem ser provados de forma parecida.

Plus_1_l (n: Nat) : Equal Nat (Plus (Nat.succ Nat.zero) n) (Nat.succ n)
Plus_1_l n = Equal.refl

Mult_0_l (n: Nat) : Equal Nat (Mult Nat.zero n) Nat.zero
Mult_0_l n = Equal.refl 

O _l indica que a prova envolve o valor no lado esquerdo. Por exemplo: A prova da soma por 1 no lado esquerdo (Plus_1_l) ou a prova da multiplicação por zero no lado esquerdo (Mult_0_l)

Embora a simplificação seja poderosa o suficiente para provar alguns fatos gerais, existem várias declarações que não podem ser demonstradas só com simplificação. Por exemplo, não podemos usá-la para provar que Nat.zero é um elemento neutro para adição no lado direito.

Plus_n_Z (n: Nat) : Equal Nat n (Plus n Nat.zero)
Plus_n_Z n = Equal.refl

- ERROR Type mismatch  

   • Got      : Equal Nat n n
   • Expected : Equal Nat n (Plus n 0n)

   • Context: 
   •   n : Nat 

   Plus_n_Z n = Equal.refl
                ┬─────────
                └Here!

(Você consegue explicar por que isso acontece?)

O próximo capítulo vai introduzir o conceito de indução, uma técnica poderosa que pode ser usada para demonstrar esse teorema. Por agora, no entanto, vamos ver mais alguns tipos simples de prova.

Prova por aplicação

A nossa primeira ferramenta para resolver provas que não são reduzíveis de cara será a aplicação dos dois lados. Para isso, usaremos a função Equal.apply, que recebe uma igualdade (um Equal) e uma função, e aplica essa função dos dois lados da igualdade, gerando uma nova igualdade.

Por exemplo:

Example_apply (n: Nat) (m: Nat) (e: Equal Nat m n) : Equal Nat (Nat.succ m) (Nat.succ n)
Example_apply n m e = ?

O que exatamente temos aqui? Temos uma prova que recebe como argumento uma outra prova/igualdade. Isso quer dizer que vamos realizar a nossa prova supondo que a prova dada como argumento também é verdadeira. Então, lendo a declaração da prova, temos que: "Dados dois naturais, m e n, e uma prova de que eles são iguais, provar que Nat.succ m e Nat.succ n também são iguais".

Nós aprendemos, nas nossas aulas de matemática, que aplicar uma função dos dois lados de uma igualdade mantém a igualdade (x/2 = 3 -> 2*x/2 = 2*3), e podemos ver que para provar o que a gente quer, precisamos aplicar a função Nat.succ nos dois lados de e, usando Equal.apply

+ INFO  Inspection.

  • Expected: (Equal Nat (Nat.succ m) (Nat.succ n)) 

  • Context: 
  •   n : Nat 
  •   m : Nat 
  •   e : (Equal Nat m n) 

  Example_apply n m e = ?
                        ┬
                        └Here!

Como o Equal.apply funciona: Ele recebe como primeiro argumento a função a ser aplicada dos dois lados, e como segundo argumento a igualdade aonde aplicar a função. Se você não entendeu muito bem a passagem da função de argumento (x => Nat.succ x), ela é o que chamamos de função lambda, e é também conhecida como função anônima. Funções lambda são identificadas pela sua seta =>, sendo que do lado esquerdo da seta fica o nome do argumento da função - use o nome que quiser - e do lado direito fica o corpo da função: o que ela retorna. A nossa função lambda atual é uma função que recebe um x qualquer e retorna Nat.succ x.

Podemos ver o resultado disso dando check no arquivo:

+ INFO  Inspection.

  • Expected: (Equal Nat (Nat.succ m) (Nat.succ n)) 

  • Context: 
  •   n : Nat 
  •   m : Nat 
  •   e       : (Equal Nat m n) 
  •   e_apply : (Equal Nat (Nat.succ m) (Nat.succ n)) 
  •   e_apply = (Equal.apply Nat Nat m n (x => (Nat.succ x)) e) 

  let e_apply = Equal.apply (x => Nat.succ x) e
      ?
      ┬
      └Here!

Como e_apply é uma igualdade do tipo Equal Nat (Nat.succ m) (Nat.succ n), a prova que procuramos, é só retornar ele e concluiremos a nossa prova.

Example_apply (n: Nat) (m: Nat) (e: Equal Nat m n) : Equal Nat (Nat.succ m) (Nat.succ n)
Example_apply n m e =
  let e_apply = Equal.apply (x => Nat.succ x) e
  e_apply

  All terms checked.

Prova por análise de casos

A próxima ferramenta de provas formais será análise de casos, que significa usar pattern matching na prova. Por exemplo, vamos provar que o E lógico de qualquer coisa e Falso sempre é falso:

Example_case_analysis (b: Bool) : Equal Bool (Andb b1 Bool.false) Bool.false
Example_case_analysis b = ?

Apesar de parecer uma prova que deveria ser resolvida simplesmente com Equal.refl, não é o caso. Isso é por conta de a função Andb fazer pattern matching no primeiro argumento, e nós não temos o valor dele na prova, então ele fica "agarrado".

Para darmos um valor pra ele, e mostrar que a prova está correta para ambos os valores de Bool, nós fazemos pattern matching na prova, criando assim duas provas diferentes: uma pra quando b for Bool.true e uma pra quando for Bool.false.

Example_case_analysis (b: Bool) : Equal Bool (Andb b Bool.false) Bool.false
Example_case_analysis Bool.true  = ?
Example_case_analysis Bool.false = ?

E ambas essas provas são resolvíveis diretamente com Equal.refl, pois o type checker consegue reduzir ambos para Equal Bool.false Bool.false direto.

Example_case_analysis (b: Bool) : Equal Bool (Andb b Bool.false) Bool.false
Example_case_analysis Bool.true  = Equal.refl
Example_case_analysis Bool.false = Equal.refl

Prova por Reescrita

Esse teorema é um pouco mais interessante que anteriores:

Plus_id_example (n: Nat) (m: Nat) (e: Equal Nat n m) : Equal Nat (Plus n n) (Plus m m)

Assim como mostrado anteriormente, essa é uma prova que dentro de seus argumentos temos uma outra prova, ou hipótese: no caso, temos Equal n m - ou seja, n e m são iguais.

Como n e m são números arbitrários, não podemos só usar simplificação para demonstrar o teorema. Em vez disso, nós observando que, já que assumimos Equal n m, poderíamos substituir n por m no objetivo e os dois lados ficarão iguais. A função que usamos para fazer essa substituição é a Equal.rewrite.

Como não podemos reescrever diretamente no objetivo, nós usamos uma outra igualdade e fazemos ela ser igual ao objetivo. No nosso caso, usaremos um Equal.apply em e para conseguir essa igualdade.

Plus_id_example (n: Nat) (m: Nat) (e: Equal Nat n m) : Equal Nat (Plus n n) (Plus m m)

Plus_id_example n m e =
  let app = Equal.apply (k => Plus k n) e
  ? 

+ INFO  Inspection.

   • Expected: Equal Nat (Plus n n) (Plus m m) 

   • Context: 
   •   n   : Nat 
   •   m   : Nat 
   •   e   : Equal Nat n m 
   •   app : Equal Nat (Plus n n) (Plus m n) 
   •   app = Equal.apply Nat Nat n m (k => (Plus k n)) e
    
   let app = Equal.apply (k => Plus k n) e
      ?
      ┬
      └Here!

Esse app será do tipo Equal (Plus n n) (Plus m n), como mostrado no comentário. Com isso feito, precisamos trocar o n por m no lado direito da igualdade, e pra isso usamos o rewrite:

Plus_id_example (n: Nat) (m: Nat) (e: Equal Nat n m) : Equal Nat (Plus n n) (Plus m m)
Plus_id_example n m e =
  let app = Equal.apply (k => Plus k n) e
  let rrt = Equal.rewrite e (x => Equal (Plus n n) (Plus m x)) app
  rrt

+ INFO  Inspection.

   • Expected: Equal Nat (Plus n n) (Plus m m) 

   • Context: 
   •   n   : Nat 
   •   m   : Nat 
   •   e   : Equal Nat n m 
   •   app : Equal Nat (Plus n n) (Plus m n) 
   •   app = Equal.apply Nat Nat n m (k => (Plus k n)) e 
   •   rrt : Equal Nat (Plus n n) (Plus m m) 
   •   rrt = Equal.rewrite Nat n m e (x => Equal Nat (Plus n n) (Plus m x)) app

O retorno da operação Equal.rewrite já será a prova que precisamos, então só retornamos direto o resultado da função.

Plus_id_exercise

Prove que:

Plus_id_exercise (n: Nat) (m: Nat) (o: Nat) (e1: Equal Nat n m) (e2: Equal Nat m o) : Equal Nat (Plus n m) (Plus m o)
Plus_id_exercise n m o e1 e2 = ?

Equal.chain e Equal.mirror

Nessa parte não falaremos de nenhuma ferramenta inerentemente nova, mas sim de alguns utilitários de provas para facilitar o uso das ferramentas anteriores.

Imagine o exemplo:

Example_mirror (a: Nat) (b: Nat) (e: Equal Nat a b) : Equal Nat b a

Parece um exemplo trivial. Se a é igual a b, b é igual a a, correto? Apesar de correto, o type checker do Kind não reconhece essa igualdade, pois para ele, a ordem é importante. Para esse tipo de situação, temos a função Equal.mirror, que simplesmente troca os lados de uma igualdade.

Example_mirror (a: Nat) (b: Nat) (e: Equal Nat a b) : Equal Nat b a
Example_mirror a b e = 
   let mir = Equal.mirror e
   mir

+ INFO  Inspection.

   • Expected: Equal Nat b a 

   • Context: 
   •   a   : Nat 
   •   b   : Nat 
   •   e   : Equal Nat a b
   •   mir : Equal Nat b a 
   •   mir = Equal.mirror Nat a b e

Apesar de não parecer muito útil no momento, essa operação é muito útil para nosso segundo utilitário: Equal.chain. Equal.chain é um caso específico do Equal.rewrite, no qual você reescreve um lado inteiro de uma igualdade usando outra.

Example_chain (a: Nat) (b: Nat) (c: Nat) (e1: Equal Nat b (Plus a a)) (e2 : Equal Nat c (Plus a a)) : Equal Nat b c

Como nós já conhecemos o Equal.rewrite, poderíamos usar ele para resolver esse teorema, mas ao invés disso vamos usar o Equal.chain. Equal.chain funciona "encadeando" duas igualdades que tenham a mesma expressão no lado direito da primeira igualdade e no lado esquerdo da segunda, "grudando" essas igualdades pela expressão em comum, gerando uma nova igualdade com as outras duas expressões (Equal.chain (a=b) (b=c) = (a=c)). Por exemplo, no nosso exemplo, o lado direito das duas igualdades é igual. Se usarmos Equal.mirror em uma delas, podemos dar Equal.chain nelas:

Example_chain (a: Nat) (b: Nat) (c: Nat) (e1: Equal Nat b (Plus a a)) (e2 : Equal Nat c (Plus a a)) : Equal Nat b c
Example_chain a b c e1 e2 =
  let e3 = Equal.mirror e2
  let chn = Equal.chain e1 e3

+ INFO  Inspection.

   • Expected: Equal Nat b c

   • Context: 
   •   a   : Nat 
   •   b   : Nat 
   •   c   : Nat 
   •   e1  : Equal Nat b (Plus a a) 
   •   e2  : Equal Nat c (Plus a a) 
   •   e3  : Equal Nat (Plus a a) c
   •   e3  = Equal.mirror Nat c (Plus a a) e2
   •   chn : Equal Nat b c
   •   chn = Equal.chain Nat b (Plus a a) c e1 e3

Mais exercícios

Boolean_functions

Use os conhecimentos ensinados até aqui para resolver o teorema:

Identity_fn_applied_twice (f: Bool -> Bool) (e: (x: Bool) -> Equal Bool (f x) x) (b : Bool) : Equal Bool (f (f b)) b
Identity_fn_applied_twice f e b = ?

Depois, resolva o teorema negation_fn_applied_twice, que é o mesmo que o anterior, mas mudando a hipótese para Equal (f x) (Not x)

Andb_eq_orb

Prove o seguinte teorema (Lembre-se que voce pode provar teoremas intermediários separadamente)

Andb_eq_orb (b: Bool) (c: Bool) (e: Equal Bool (Andb b c) (Orb b c)) : Equal Bool b c
Andb_eq_orb b c prf = ?

Binary

Considere uma representação diferente de números naturais, usando um sistema binário ao invés de unário. Ou seja, ao invés de termos apenas zero ou um sucessor de um número, nós podemos ter:

• zero;
• o dobro de um número;
• o dobro de um número mais 1.

1. Primeiro, escreva uma definição indutiva desse tipo, chamando-o de Bin. (Lembre-se que, no fundo, a própria definição de Nat como zero ou succ n não tem sentido intrínseco. Ela só diz que um elemento de Nat pode ser um zero ou um succ n se n também for Nat. A interpretação disso como um sistema de valores 0, 1, 2, etc, vem de como nós trabalhamos com esse tipo Nat. A sua definição de Bin idealmente também será tão simples quanto. Serão as funções que você fizer sobre Bin que darão sentido matemático a ele).
2. Então, escreva uma função Incr para incrementar um Bin, e uma função Bin_to_nat para converter de Bin para Nat.
3. Escreva cinco provas que testam suas funções de incremento e de conversão. Note que incrementar um binário e então convertê-lo deve ser chegar no mesmo resultado que convertê-lo primeiro e então incrementar o Nat.

Indução: Prova por Indução

Módulo de indução

Nesse capítulo nós veremos sobre provas por indução, mas antes de prosseguirmos para a indução em si, podemos analisar casos simples onde apenas a reflexão do caso já prova o teorema.

Problems.t0 (n: Nat) : Equal Nat (Plus Nat.zero n) n

Ao verificar verificar o objetivo do teorema, recebemos a seguinte resposta:

+ INFO  Inspection.

   • Expected: (Equal Nat n n) 

   • Context: 
   •   n : Nat 

    Problems.t0 n = ?
                    ┬
                    └Here!

No Problems.t0 o Kind reduz a soma de "0 + n" automaticamente para n e que devemos provar a igualdade entre n e n. Nesse caso basta escrever "Equal.refl" e obtemos a resposta de confirmação:

All terms check.

Problems.t1 (n: Nat) : Equal Nat (Plus n Nat.zero) n

Feito o primeiro problema, o seguinte é muito similar, é a soma de "n + 0 = n" e essa similaridade pode nos levar a crer que basta invocar a reflexão. Entretanto, no primeiro caso o Kind reduz automaticamente e nesse nós obtemos o seguinte retorno:

+ INFO  Inspection.

   • Expected: (Equal Nat (Plus n 0n) n) 

   • Context: 
   •   n   : Nat 

   Problems.t1 n = ?
                   ┬
                   └Here!

No primeiro caso o Kind reduz pois o zero está à direita e o Type Checker já reduz automaticamente, a soma de entre 0 e n para n. Entretanto, quando o primeiro input é uma variável, o Kind necessita verificar para cada caso e como é um número natural, há infinitos casos a serem testados, isto é, de zero a infinito.

De início podemos pensar que são tantos casos e que é impossível analisar todos eles, já que são infinitos, mas logo percebemos que é possível reduzir a dois, um é o número zero e o outro é um número que sucede o zero n vezes depois.

Analisando para o caso de zero nosso objetivo é provar que zero é igual a zero:

• Expected: Equal Nat Nat.zero Nat.zero

Agora basta dar o Equal.refl e o caso zero já foi comprovado, basta apenas responder para o sucessor de zero

Nosso objetivo é provar que para todo número n, ao adicionar 0 o resultado será n, mas já temos uma nova ferramenta que nos auxilia nessa prova e é a prova para o caso zero, basta reduzir n até que o necessário seja apenas a reflexão e podemos fazer isso por meio da recursão e para isso definimos o novo n como o antecessor dele. No Kind nós podemos fazer isso simplesmente definindo o n atual como sendo o sucessor do próximo n e chamar a função para n recursivamente. Isso é feito da seguinte forma:

Problems.t1 (Nat.succ n)   = ?

e temos como novo objetivo provar que o sucessor da soma entre n e 0 é igual ao sucessor de n

- Expected: Equal Nat (Nat.succ (Plus n Nat.zero)) (Nat.succ n)

Para trabalhar com a indução nessa recursão, devemos definir uma variável para o caso original de n

Problems.t1 (n: Nat)       : Equal (Plus n Nat.zero) n
Problems.t1 Nat.zero       = Equal.refl
Problems.t1 (Nat.succ n)   =
    let ind = Problems.t1 n
    ?

Ao dar o Type Check temos como retorno a seguinte resposta:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 

   • Context: 
   •   n   : Nat 
   •   ind : (Equal Nat (Plus n 0n) n) 
   •   ind = (Problems.t1 n) 

   let ind = Problems.t1 n
     ?
     ┬
     └Here!

Ao analisar nosso objetivo e a indução, percebemos que a única diferença entre o objetivo e a nossa variável ind é o Nat.succ, basta então incrementar a variável ind com o Nat.succ, para isso nós criamos uma nova variável e usamos uma função lambda:

let app = Equal.apply (x => (Nat.succ x)) ind

No caso acima nós chamamos a função Equal.apply para aplicar a nossa função lambda ao ind. A função x => (Nat.succ x) serve para adicionar Nat.succ a todo elemento recebido na variável. Como nossa variável ind é uma função que recebe uma outra variável n, a nossa função lambda incrementa a n com Nat.succ, o que retorna exatamente o nosso objetivo:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 

   • Context: 
   •   n   : Nat 
   •   ind : (Equal Nat (Plus n 0n) n) 
   •   ind = (Problems.t1 n) 
   •   app : (Equal Nat (Nat.succ (Plus n 0n)) (Nat.succ n)) 
   •   app = (Equal.apply Nat Nat (Plus n 0n) n (x => (Nat.succ x)) ind)  

   let app = Equal.apply (x => (Nat.succ x)) ind
      ?
      ┬
      └Here!

Podemos perceber que o app é exatamente igual ao Expected, que é o nosso objetivo e basta apenas retornar ele, o app para que o Type Check valide a nossa prova:

All terms check.

Há casos em que a indução é ainda mais simples, basta compreender o que está acontecendo. Imagine que você quer provar que um número n menos ele mesmo é igual a zero, independente de qual seja esse número. Como faríamos? Primeiro, nós verificamos para o caso dele ser zero e é uma igualdade verdadeira, zero menos zero é igual a zero. Depois, nós induzimos o caso para o caso de zero, que sabemos ser verdadeiro. Parece complicado? Não é, é absurdamente simples, vamos ver como fica isso em Kind:

Minus_diag (n: Nat)     : Equal Nat (Minus  n n) Nat.zero
Minus_diag Nat.zero     = Equal.refl
Minus_diag (Nat.succ n) = Minus_diag n

Perceba, essa é uma indução simples, nós falamos que a prova vale para o número e o antecessor dele e, por usarmos uma recursão, para todos os antecessores até zero, que é o caso que verificamos ser verdadeiro. Ou seja, provamos, em apenas três linhas, que um número natural menos ele mesmo sempre dará zero, independente de qual for esse número.

Exercícios

Prove o seguinte usando indução. Você pode precisar de resultados previamente comprovados.

Mult_0_r (n: Nat) : Equal Nat (Mult n Nat.zero) Nat.zero
Mult_0_r n = ?

Plus_n_sm (n: Nat) (m: Nat) : Equal Nat (Nat.succ (Plus n m)) (Plus n (Nat.succ m))
Plus_n_sm n m = ?

Plus_comm (n: Nat) (m: Nat) : Equal Nat (Plus n m) (Plus m n)
Plus_comm n m = ?

Add_0_r (n: Nat) : Equal Nat (Plus n Nat.zero) n
Add_0_r n = ?

Plus_assoc (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Plus n (Plus m p)) (Plus (Plus n m) p)
Plus_assoc n m p = ?

Considere a seguinte função que dobra o argumento recebido

Double (n: Nat)     : Nat
Double Nat.zero     = Nat.zero
Double (Nat.succ n) = Nat.succ (Nat.succ (Double n))

Use indução para provar esses seguintes teoremas sobre Double:

Double_plus (n: Nat) : Equal Nat (Double n) (Plus n n)
Double_plus n = ?

Alguns teoremas é necessário analisar a melhor forma de se provar, por exemplo, para provar que um numero é par, poderíamos provar pelo sucessor dele, mas isso nos faria ter que provar para o sucessor do sucessor dele, isso faz com a que a prova de Evenb ser mais difícil por indução, então é importante perceber quando é necessário e quando não é.

Evenb_s (n: Nat) : Equal Bool (Evenb (Nat.succ n)) (Notb  (Evenb n))
Evenb_s n = ?

Outro caso

Vamos verificar se a a igualdade "n +(m + 1) = 1 + (n + m)" é verdadeira

Primeiro, o nosso problema:

Problems.t2 (n: Nat) (m: Nat) : Equal Nat (Plus n (Nat.succ m)) (Nat.succ(Plus n m))

Verificamos o primeiro caso, quando n é zero:

Problems.t2 Nat.zero m = Equal.refl

e partimos para o caso seguinte

Problems.t2 (Nat.succ n) m = ?

e o nosso objetivo atual vira:

• Expected: Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Traduzindo, o sucessor da adição de n e o sucessor de m é igual ao sucessor do sucessor da adição de n e m. Para resolver esse problema, invocaremos a indução:

let ind = Problems.t2 n m

e o nosso objetivo atual é provar que:

• Expected: Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Traduzindo novamente, que o sucessor da adição de n e o sucessor de m é igual ao sucessor do sucessor da adição de n e m.

mas agora nós temos uma ferramenta muito útil, a nossa variável ind que é:

Equal Nat (Plus n (Nat.succ m)) (Nat.succ (Plus n m))

Ora, analisando o nosso objetivo e a nossa variável ind, podemos perceber que basta dar um Nat.succ em ambos os lados da indução e ela ficará exatamente igual ao nosso objetivo, para isso usaremos uma função lambda:

let app = Equal.apply (x => (Nat.succ x)) ind

E a nossa variável app retornará o nosso objetivo:

Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Bastando apenas retornar o app para e o Kind nos retornará o tão almejado All terms check.

Usando outros teoremas

Em Kind, como na matemática informal, grandes provas são frequentemente divididas em uma sequência de teoremas, com provas posteriores referindo-se a teoremas anteriores. Mas às vezes uma prova exigirá algum fato variado que é muito trivial e de muito pouco geral interesse em dar-lhe o seu próprio nome de nível superior. Nesses casos, é conveniente ser capaz de simplesmente enunciar e provar o “sub-teorema” necessário exatamente no ponto onde é usado.

Analisemos o seguinte teorema da comutação da adição:

Problems.t3 (n: Nat) (m: Nat) : Equal Nat (Plus n  m) (Plus m n)

No primeiro caso, para n e m igual a zero nós temos uma reflexão:

Problems.t3 Nat.zero Nat.zero = Equal.refl

Então partimos para o próximo caso:

Problems.t3 (Nat.succ n) m = ?

E aqui parece que temos um novo problema:

Expected: Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))

Ao analisar o problema, percebemos que dentro dele há um teorema já provado, de que o sucessor da adição de dois números é igual a adição de um número com o sucessor dele, então podemos usar isso ao nosso favor.

Começaremos aplicando um Nat.succ no nosso problema original:

let ind_a = Equal.apply (x => (Nat.succ x)) (Problems.t3 n m )

Depois invocaremos nosso problema já resolvido, o Problems.t2:

let ind_b = Problems.t2 m n

Ao dar o Type Check, o terminal nos retorna:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))) 

   • Context: 
   •   n     : Nat 
   •   m     : Nat 
   •   ind_a : (Equal Nat (Nat.succ (Plus n m)) (Nat.succ (Plus m n))) 
   •   ind_a = (Equal.apply Nat Nat (Plus n m) (Plus m n) (x => (Nat.succ x)) (Problems.t3 n m)) 
   •   ind_b : (Equal Nat (Plus m (Nat.succ n)) (Nat.succ (Plus m n))) 
   •   ind_b = (Problems.t2 m n) 
 
   let ind_b = Problems.t2 m n
     ?
     ┬
     └Here!

Agora podemos perceber que a primeira parte da ind_a é igual ao inverso da primeira parte do nosso objetivo e a primeira parte da ind_b é igual a segunda do objetivo, basta apenas organizar e juntar as partes necessárias. Para isso usaremos a Equal.mirror e a Equal.chain.

let ind_c = Equal.chain ind_b Equal.mirror ind_a

E o ind_c nos retorna um valor similar ao desejado:

• Expected: Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))
•   ind_c : Equal Nat (Plus m (Nat.succ n)) (Nat.succ (Plus n m))

Podemos perceber que um é o outro espelhado, para torná-los iguais, usaremos o Equal.mirror novamente:

let app = Equal.mirror ind_c

Ao chamar o app o Type Check nos retorna a mensagem All terms checked e desta forma provamos, por meio da indução e usando uma outra prova, a comutação da adição, ou seja, que a soma de n e m é igual a soma de m e n.

Mais exercícios

Você pode usar a rewrite ou chain nessa prova, escolha o que achar mais fácil

Plus_swap (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Plus n (Plus m p)) (Plus m (Plus n p))
Plus_swap n m p = ?

Agora prove a comutatividade da multiplicação. (Você provavelmente precisará definir e provar um teorema auxiliar separado para ser usado na prova deste. Você pode descobrir que Plus_swap é útil.

Mult_comm (n: Nat) (m: Nat) : Equal Nat (Mult n m) (Mult m n)
Mult_comm n m = ?

Pegue um pedaço de papel. Para cada um dos teoremas a seguir, primeiro pense se (a) pode ser provado usando apenas simplificação e reescrita, (b) também requer análise de caso (destruição) ou (c) também requer indução. Anote sua previsão. Em seguida, preencha a prova. (Não há necessidade de entregar seu pedaço de papel; isso é apenas para incentivá-lo a refletir antes de hackear!)

Lte_refl (n: Nat) : Equal Bool Bool.true (Lte n n)
Lte_refl n = ?

Zero_nbeq_s (n: Nat) : Equal Bool (Eql (Nat.zero) (Nat.succ n)) Bool.false
Zero_nbeq_s n = ?

And_false_r (b: Bool) : Equal Bool (Andb b Bool.false) Bool.false
And_false b = ?

S_nbeq_0 (n: Nat) : Equal Bool (Eql (Nat.succ n) Nat.zero) Bool.false

Mult_1_l (n: Nat) : Equal Nat (Mult (Nat.succ Nat.zero) n) n
Mult_1_l n = ?

All3_spec (b: Bool) (c: Bool) : Equal Bool (Orb (Orb (Andb b c) (Notb  b)) (Notb  c)) Bool.true
All3_spec b c = ?

Mult_plus_distr_r (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Mult (Plus n m) p) (Plus (Mult n p) (Mult m p))
Mult_plus_distr_r n m p = ?

Mult_assoc (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Mult (Mult m p)) (Mult (Mult n m) p)
Mult_assoc n m p = ?

Estrutura de dados

Listas: trabalhando com dados estruturados

A partir de agora, veremos dados estruturados, em especial as listas e pares, e que podem conter elementos de diversos tipos. Na definição do tipo, já mostraremos eles com tipos polimórficos, mas não se assombre, veremos sobre isso no próximo capítulo, apenas vamos ignorar o tipo e acompanhar a explicação, fará mais sentido ao decorrer do nosso estudo.

Pares de Números

Em uma definição de tipo indutivo, cada construtor pode receber qualquer número de argumentos -- nenhum como o Bool, Empty ou um como o *Nat* -- e temos o Pair que recebe dois argumentos (podendo ser até mesmo outros dois pares) e retorna um tipo:

record Pair (a) (b) 

Os dois argumentos recebidos são transformados no primeiro componente, o fst, e o segundo, o snd.

record Pair (a) (b) {
  fst : a
  snd : b
} 

A forma de construir um par de Nat é a seguinte:

Pair.new Nat Nat a b  : (Pair a b)

Aqui estão duas funções simples para extrair o primeiro e o segundo componentes de um par. As definições também ilustram como fazer a correspondência de padrões em dois argumentos construtores.

Fst (pair: Pair Nat Nat) : Nat
Fst (Pair.new Nat Nat fst snd) = fst

Exemplo 1: (Fst Nat (List Nat) (Pair 2n [1n,2n,3n])) -> 2n

Snd (pair: Pair Nat Nat) : Nat
Snd (Pair.new Nat Nat fst snd) = snd

Exemplo 2: (Snd Nat (List Nat) (Pair 2n [1n,2n,3n])) -> [1n,2n,3n]

Algumas provas

Vamos tentar provar alguns fatos simples sobre pares. Se declararmos as coisas de uma maneira particular (e ligeiramente peculiar), podemos completar provas com apenas reflexividade:

Surjective_pairing (p: Pair Nat Nat) : Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))
Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

Mas *Equal.*refl não é suficiente caso a declaração seja:

Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

Já que o Kind espera

Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))

E recebeu

Equal p p

Nós devemos "expor" a estrutura interna do par para que o Type Checker possa verificar se p é realmente igual a Pair.new (Fst p) (Snd p)

Snd_fst_is_swap

Snd_fst_is_swap (p: Pair Nat Nat ) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.swap Nat Nat p) p)
Snd_fst_is_swap (Pair.new Nat Nat fst snd) = ? 

Fst_swap_is_snd

Fst_swap_is_inverse (p: Pair Nat Nat) (a: Nat) (b: Nat) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.new a b) (Pair.new b a))
Fst_swap_is_inverse p a b = ?

Listas de números

Generalizando a definição de pares, podemos descrever o tipo de listas de números assim: “Uma lista ou é a lista vazia ou então um conjunto de um elemento e outra Lista", esse tipo não é composto de um head e uma tail.

type List (t) {
  nil
  cons (head: t) (tail: List t)
}

Como vamos tratar de apenas um tipo, é interessante reescrever o tipo de lista para um definido, o escolhido foi o Nat:

type NatList {
  nil
  cons (head: Nat) (tail: NatList)
}

ou

type NatList {
   List Nat
}

Podemos perceber que em ambas as notações, há um head e um tail, sendo que o head recebe um elemento do tipo Nat e a tail recebe uma lista do tipo Nat.

Por exemplo, uma lista de três números naturais 1n, 2n e 3n seria escrita da seguinte forma:

[1n, 2n, 3n]

O Kind, entretanto, lê de outra forma:

[1n, [2n, 3n]]

onde o 1n é a head e o [2n, 3n] é a tail. Da mesma forma, ao olhar para uma lista de 4 elementos [1n, 2n, 3n, 4n], agora veremos da seguinte forma:

[1n, [2n, [3n, 4n]]]

A lista possui o head 1n e a tail [2n, [3n, 4n]], que, por sua vez, possui a head 2n e a tail [3n, 4n] que também possui sua head 3n e sua tail 4n.

Pode parecer assustador, mas é um monstro amigável:

[fonte da imagem: http://learnyouahaskell.com/starting-out]

Repeat

A função repeat recebe um número n e um valor, retornando uma lista de tamanho n onde todos os elementos é o valor declarado.

// Exemplo: (Repeat 3 Bool.true) -> [True, True, True]
Repeat (x: Nat) (count: Nat) : List Nat
Repeat x Nat.zero            = [] 
Repeat x (Nat.succ count)    = List.cons Nat x (Repeat count x)

Length

A função length calcula o tamanho da lista

// Exemplo: (Length [1,2,3]) -> 3
Length (xs: List Nat) : Nat
Length List.nil              = 0n
Length (List.cons head tail) = (Nat.succ (Length tail))

Concat

A função concat concatena (anexa) duas listas.

Concat (xs: List Nat) (ys: List Nat) : List Nat
Concat (List.nil)            ys = ys
Concat (List.cons head tail) ys = List.cons Nat head (Concat tail ys)

Head e Tail

A função head retorna o primeiro elemento (a “cabeça”) da list, enquanto tail retorna tudo menos o primeiro elemento (a “cauda”). Claro, o lista vazia não tem primeiro elemento, então devemos tratar esse caso com um tipo Maybe, recebendo um Maybe.none caso a lista seja vazia ou um Maybe.some caso tenha um valor.

// Exemplo: (Head 0n [1n,2n,3n]) -> 1n
Head (default: Nat) (xs: List Nat) :  Nat
Head default (List.nil)            = default
Head default (List.cons head tail) = head

// Exemplo: (Tail Nat [1,2,3]) -> [2,3]
Tail (xs: List Nat)        : List Nat
Tail (List.nil)            = []
Tail (List.cons head tail) = tail

Test_head1 : Equal Nat (Head 0n [1n,2n,3n]) 1n
Test_head1 = Equal.refl

Test_head2 : Equal Nat (Head 0n List.nil) 0n
Test_head2 = Equal.refl

Test_head3 : Equal (List Nat) (Tail [1n, 2n, 3n]) [2n, 3n]
Test_head3 = Equal.refl

Exercícios

List_funs

Complete as definições de Nonzeros, Oddmembers e Countoddmembers abaixo. Dê uma olhada nos testes para entender o que essas funções devem fazer.

Nonzeros (xs: List Nat) : List Nat
Nonzeros xs = ?

Test_nonzeros : Equal (List Nat) (Nonzeros [0n,1n,0n,2n,3n,0n,0n]) [1n,2n,3n]
Test_nonzeros = ?

Oddmembers (xs: List Nat) : List Nat
Oddmembers xs = ?

Test_oddmembers : Equal (List Nat) (Oddmembers [0n,1n,0n,2n,3n,0n,0n]) [1n,3n]
Test_oddmembers = ?

CountOddMembers (xs: List Nat)  : Nat
CountOddMembers xs = ?

Test_countoddmembers1 : Equal Nat (CountOddMembers [1n,0n,3n,1n,4n,5n]) 4n
Test_countoddmembers1 = ?

Alternate

Complete a definição de alternate, que “compacta” duas listas em uma, alternando entre os elementos tomados da primeira lista e elementos da segunda. Veja os testes abaixo para mais exemplos específicos.

Alternate (xs: List Nat) (ys: List Nat) : List Nat
Alternate xs ys = ?

Test_alternate1 : Equal (List Nat) (Alternate [1n,2n,3n] [4n,5n,6n]) [1n,4n,2n,5n,3n,6n]
Test_alternate1 = ?

Test_alternate2 : Equal (List Nat) (Alternate [1n] [4n,5n,6n]) [1n,4n,5n,6n]
Test_alternate2 = ?

Test_alternate3 : Equal (List Nat) (Alternate  [1n,2n,3n] [4n]) [1n,4n,2n,3n]
Test_alternate3 = ? 

Test_alternate4 : Equal (List Nat) (Alternate [] [20n,30n]) [20n,30n]
Test_alternate4 = ?

Functions

Complete as seguintes definições para as funções count, sum, add, e member das listas de naturais

Count (v: Nat) (xs: List Nat) : Nat
Count v xs = ?

Test_count1 : Equal Nat (Count 1n [1n,2n,3n,1n,4n,1n]) 3n
Test_count1 = ?

Test_count2 : Equal Nat (Count 6n [1n,2n,3n,1n,4n,1n]) 0n
Test_count2 = ?

Sum (xs: List Nat) (ys: List Nat) : List Nat
Sum xs ys = ?

Test_sum1 : Equal Nat (Count 1n (Sum [1n,2n,3n] [1n,4n,1n])) 3n
Test_sum1 = ?

Add (n: Nat) (xs: List Nat) : List Nat
Add n xs = ?

Test_add1 : Equal Nat (Count 1n (Add 1n [1n,4n,1n])) 3n
Test_add1 = ?

Test_add2 : Equal Nat (Count 5n (Add 1n [1n,4n,1n])) 0n
Test_add2 = ?

Member (v: Nat) (xs: List Nat) : Bool
Member v xs = ?

Test_member1 : Equal Bool (Member 1n [1n,4n,1n]) Bool.true
Test_member1 = ?

Test_member2 : Equal Bool (Member 2n [1n,4n,1n]) Bool.false
Test_member2 = ?

More_functions

Aqui estão mais algumas funções de List Nat para você praticar. Quando remove_one é aplicado a uma lista sem o número a ser removido, ele deve retornar a mesma lista inalterada

Remove_one (v: Nat) (xs: List Nat) : List Nat
Remove_one v xs = ?

Test_remove_one1 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,5n,4n,1n])) 0n
Test_remove_one1 = ?

Test_remove_one2 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,4n,1n])) 0n
Test_remove_one2 = ?

Test_remove_one3 : Equal Nat (Count 4n (Remove_one 5n [2n,1n,5n,4n,1n,4n])) 2n
Test_remove_one3 = ?

Test_remove_one4 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,5n,4n,5n,1n,4n])) 1n
Test_remove_one4 = ?

Remove_all (v: Nat) (xs: List Nat) : List Nat
Remove_all v xs = ?

Test_remove_all1  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,5n,4n,1n])) 0n
Test_remove_all1  = ?

Test_remove_all2  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,4n,1n])) 0n
Test_remove_all2  = ?

Test_remove_all3  : Equal Nat (Count 4n (Remove_all 5n [2n,1n,5n,4n,1n,4n])) 2n
Test_remove_all3  = ?

Test_remove_all4  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,5n,4n,5n,1n,4n,5n,1n,4n])) 0n
Test_remove_all4  = ?

Subset (xs: List Nat) (ys: List Nat)  : Bool
Subset xs ys = ?

Test_subset1 : Equal Bool (Subset [1n,2n] [2n,1n,4n,1n]) Bool.true
Test_subset1 = ?

Test_subset2 : Equal Bool (Subset [1n,2n,2n] [2n,1n,4n,1n]) Bool.false
Test_subset2 = ?

Theorem

Anote um teorema interessante, envolvendo as funções count e add e prove-o. Note que, como este problema é um pouco aberto, é possível que você venha com um teorema que seja verdadeiro, mas cuja prova requer técnicas que você ainda não aprendeu. Sinta-se à vontade para pedir ajuda se ficar preso!

Theorem : ?

Raciocínio sobre listas

Assim como os números, fatos simples sobre funções de processamento de lista podem às vezes ser provado inteiramente por simplificação. Por exemplo, a simplificação realizada por Equal.refl é suficiente para este teorema...

`List.nil`_app (xs: List Nat) : Equal (Concat (List.nil Nat) xs) xs
`List.nil`_app xs = Equal.refl

... isso porque o Kind "vê" o List.nil e já reduz automaticamente a igualdade da mesma forma que ocorre com os números naturais, com o Nat.zero

Além disso, como acontece com os números, às vezes é útil realizar uma análise de caso no possíveis formas (vazias ou não vazias) de uma lista desconhecida

Tl_length_pred (xs: List Nat)         : Equal Nat (Pred (Length xs)) (Length (Tail xs))
Tl_length_pred List.nil               = Equal.refl
Tl_length_pred (List.cons head tail)  = Equal.refl

Caso o usuário não abra os casos e use direto o Equal.refl, o Kind retorna um erro de tipo:

- ERROR  Type mismatch

   • Got      : Equal Nat (Nat.pred (Length xs)) (Nat.pred (Length xs)) 
   • Expected : Equal Nat (Nat.pred (Length xs)) (Length (Tail xs)) 

   • Context: 
   •   xs : (List Nat) 

   Tl_length_pred xs = Equal.refl
                       ┬─────────
                       └Here!

Da mesma forma, alguns teoremas precisam de indução para suas provas.

• Micro-Sermão. Simplesmente ler scripts de prova de exemplo não o levará muito longe! É importante trabalhar os detalhes de cada um, usando Kind e pensando no que cada passo alcança. Caso contrário, é mais ou menos garantido que os exercícios não farão sentido quando você chegar a eles. ( ಠ ʖ̯ ಠ)

Indução em Listas

Provas por indução sobre tipos de dados como List são um pouco menos familiares do que a indução de números naturais padrão, mas a ideia é igualmente simples. Cada declaração de dados define um conjunto de valores de dados que podem ser construídos usando os construtores declarados: um booleano pode ser True ou False; um número pode ser Zero ou Succ aplicado a outro número; uma lista de naturais pode ser List.nil ou List.cons aplicado a um número e uma lista.

Além disso, as aplicações dos construtores declarados entre si são as únicas possíveis formas que os elementos de um conjunto definido indutivamente podem ter, e este fato diretamente dá origem a uma maneira de raciocinar sobre conjuntos indutivamente definidos: um número é Zero ou então é Succ aplicado a um número menor; uma lista é List.nil ou então é um List.cons aplicado a algum número e a alguma lista menor; etc. Então, se tivermos e mente alguma proposição p que menciona uma lista l e queremos argumentar que p vale para todas as listas, podemos raciocinar da seguinte forma:

• Primeiro, mostre que p é verdadeiro para l quando l é List.nil.
• Então mostre que p é verdadeiro para l quando l é List.cons n l para algum número n e alguma lista menor l, assumindo que p é verdadeiro para l.

Como listas maiores só podem ser construídas a partir de listas menores, eventualmente chegando a List.nil, esses dois argumentos juntos estabelecem a verdade de p para todas as listas l. Aqui está um exemplo concreto:

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc List.nil                               ys zs = Equal.refl
Concat_assoc (List.cons Nat xs.head xs.tail)        ys zs = 
  let ind = Concat_assoc xs.tail ys zs
  let app = Equal.apply (x => (List.cons xs.head x)) ind
  app

Nós recebemos três listas xs, ys e zs e verificamos se a concatenação da de xs e ys com zs é igual a de xs com a de ys com zs Para isso nós verificamos para o caso de xs ser uma lista vazia, então recebemos uma reflexão da concatenação é entre ys e zs e basta dar um *Equal*.**refl**

Em seguida nós "abrimos" o xs para obter o xs.tail para a nossa indução, e recebemos como objetivo:

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs))) 

e a nossa variável ind é:

 • ind: Equal (List Nat) (Concat (Concat xs.tail ys) zs) (Concat xs.tail (Concat ys zs))

bastando apenas aplicar um List.cons xs.head em ambos os lados da igualdade para ter o objetivo final e é isso o que fazemos no app:

 • app : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

OBSERVAÇÃO O Type Check nos retorna tipos t2, t3 e outros gerados no mesmo estilo e podemos ignorar e até mesmo apagar na hora de comparar o retorno das variáveis como vemos no seguinte caso:

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs))) 
 •   app   : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

Dessa forma fica mais fácil perceber que o app e o Expected são idênticos, então não é necessário se assustar ao ver esses tipos gerados

Invertendo uma lista

Para um exemplo um pouco mais complicado de prova indutiva sobre listas, suponha que usamos Concat para definir uma função de reversão de lista Rev:

Rev (xs: List Nat)        : List Nat
Rev List.nil              = List.nil Nat
Rev (List.cons head tail) = Concat (Rev tail) [head]

Test_rev1 : Equal (List Nat) (Rev [1n,2n,3n]) [3n,2n,1n]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev List.nil) List.nil
Test_rev2 = Equal.refl

Propriedades da Rev

Agora vamos provar alguns teoremas sobre o rev que acabamos de definir. Para algo um pouco mais desafiador do que vimos, vamos provar que inverter uma lista não altera seu comprimento. Nossa primeira tentativa fica presa o caso sucessor...

Rev_length_firsttry (xs: List Nat)              : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length_firsttry List.nil                    = Equal.refl
Rev_length_firsttry (List.cons xs.head xs.tail) =
   let ind = Rev_length_firsttry xs.tail
   ?

O Type Check nos retorna o seguinte objetivo e contexto:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail)
   •   ind  = (Rev_length_firsttry tail) 

   let ind = Rev_length_firsttry tail
      ?
      ┬
      └Here!

Agora nós temos que provar que o tamanho da concatenação do reverso do tail da lista e a head dela é igual ao sucessor do tamanho da tail, então precisaremos usar algumas outras provas, uma dela é que o tamanho da concatenação de duas listas é o mesmo da soma do tamanho das de cada uma delas:

Concat_length (xs: List Nat) (ys: List Nat)  : Equal Nat (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length List.nil ys                    = Equal.refl
Concat_length (List.cons xs.head xs.tail) ys =
   let ind = Concat_length xs.tail ys
   let app = Equal.apply (x => (Nat.succ x)) ind
   app

Além dessa prova, usaremos outras já provadas nos capítulos anteriores:

Plus_n_z (n: Nat)     : Equal Nat n (Plus n Nat.zero)
Plus_n_sn (n: Nat) (m: Nat) : Equal Nat (Nat.succ (Plus n m)) (Plus n (Nat.succ m))
Plus_comm (n: Nat) (m: Nat) : Equal Nat (Plus n m) (Plus m n)

E agora é possível provar o nosso teorema:

Rev_length (xs: List Nat)               : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                     = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind   = Rev_length tail
   ?

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 

   let ind   = Rev_length tail
      ?
      ┬
      └Here!

Nós criamos uma variável com nossa auxiliar Concat_length:

Rev_length (xs: List Nat)             : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                   = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind  = Rev_length tail
   let aux1 = Concat_length (Rev xs.tail) [xs.head]
   ?

Recebemos um novo contexto para nos auxiliar, o

 • aux1: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n)

A aux1 é igual ao lado esquerdo do nosso Expected, então metade do trabalho já foi resolvido, basta o outro lado da igualdade e para isso nós criamos uma nova variável, a aux2:

let aux2 = Plus_comm (Length (Rev xs.tail)) (1n)

Agora nosso contexto está ainda melhor:

 • aux2: Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) 

Como estamos progredindo nas provas formais, é possível perceber que o lado esquerdo da aux2 é igual ao direito da aux1 e podemos encadear um no outro com o Equal.chain:

let chn = Equal.chain aux1 aux2

Ao dar o Type Check, vemos nosso novo contexto:

 • chn : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))

Nossa variável chn é praticamente idêntica ao nosso Expected só diferindo na parte final, pois Expected espera um Nat.succ (Length xs.tail) e o chn nos dá Nat.succ (Length (Rev xs.tail)), mas nós temos a variável ind que nos retorna essa igualdade. Vamos relembrar:

 • ind: Equal Nat (Length (Rev tail)) (Length tail) 

Incrível, não é? Ela nos retorna exatamente o que precisamos, que o tamanho do reverso da tail é igual ao tamanho da tail, então basta reescrever a variável ind na nossa chn:

let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons head (List.nil)))) (Nat.succ x )) chn

Vamos ver nosso novo contexto, apenas ocultando os tipos para uma leitura mais fácil:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons _ head (List.nil _)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 
   •   aux1 : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) 
   •   aux1 = (Concat_length (Rev tail) (List.cons Nat head (List.nil Nat))) 
   •   aux2 : Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) 
   •   aux2 = (Plus_comm (Length (Rev tail)) 1n) 
   •   chn  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))
   •   chn  = Equal.chain Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) aux1 aux2 
   •   rrt  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 
   •   rrt  = Equal.rewrite Nat (Length (Rev tail)) (Length tail) ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ x))) chn

Agora é muito mais fácil perceber que nosso rrt é exatamente o nosso Expected, então nossa prova fica assim:

Rev_length (xs: List Nat)            : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                  = Equal.refl
Rev_length (List.cons Nat head tail) =
   let ind   = Rev_length tail
   let aux1  = Concat_length (Rev tail) [head]
   let aux2  = Plus_comm (Length (Rev tail)) (1n)
   let chn   = Equal.chain aux1 aux2
   let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) [head])) (Nat.succ x)) chn
   rrt

Exercícios de Listas, parte 1

List_exercises

Vamos praticar um pouco mais com as listas:

Concat_nil_r (xs: List Nat) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc xs ys zs = ?

Rev_app_distr (xs: List Nat) (ys: List Nat) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive (xs: List Nat) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

Há uma solução curta para a próxima. Se você estiver achando muito difícil ou começar a ficar longo demais, recue e tente procurar uma maneira mais simples.

Concat_assoc4 (l1: List Nat) (l2: List Nat) (l3: List Nat) (l4: List Nat) : Equal (List Nat) (Concat l1 (Concat l2 (Concat l3 l4))) (Concat (Concat (Concat l1 l2) l3) l4)
Concat_assoc4 l1 l2 l3 l4 = ? 

Um exercício sobre sua implementação de Nonzeros:

Nonzeros_app (xs: List Nat) (ys: List Nat) : Equal (List Nat) (Nonzeros (Concat xs ys)) (Concat (Nonzeros xs) (Nonzeros ys))
Nonzeros_app xs ys = ?

Beq_NatList

Preencha a definição de beq_NatList, que compara listas de números para igualdade. Prove que beq_NatList xs ys produz Bool.true para cada lista.

Beq_NatList (xs: List Nat) (ys: List Nat) : Bool
Beq_NatList xs ys = ? 

Test_beq_natlist1 : Equal Bool (Beq_list List.nil List.nil) Bool.true
Test_beq_natlist1 = ?

Test_beq_natlist2 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,3n]) Bool.true
Test_beq_natlist2 = ?

Test_beq_natlist3 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,4n]) Bool.false
Test_beq_natlist3 = ?

Beq_natlist_refl (xs: List Nat) : Equal Bool Bool.true (Beq_list xs xs)
Beq_natlist_refl xs = ?

Exercícios de Listas, parte 2

Proofs

Prove o seguinte teorema, ele ajudará você na prova seguinte

Ble_n_succ_n (n: Nat) : Equal Bool (Lte n (Nat.succ n)) Bool.true
Ble_n_succ_n n = ? 

Aqui estão mais alguns pequenos teoremas para provar sobre suas definições sobre listas.

Count_member_nonzero (xs: List Nat) : Equal Bool (Lte 1n (Count 1n (List.cons 1n xs))) Bool.true
Count_member_nonzero xs = ?

Rev_injective

Prove que a função Rev é injetiva - isto é

Rev_injective (xs: List Nat) (ys: List Nat) (e: Equal (List Nat) (Rev xs) (Rev ys)) :tail Equal (List Nat) xs ys
Rev_injective xs ys e = ?  

Opcional: Count_sum

Escreva um teorema interessante sobre Listas envolvendo as funções count e sum, e prova-o. (Você pode encontrar que a dificuldade da prova depende de como você definiu o count!)

Count_sum : ?

Maybe

Suponha que a gente queira escrever uma função que retorna o enésimo número de uma lista. Nós então definimos um número que é aplicado a uma lista de naturais e então retorna o número que ocupa essa posição. Dessa forma, nós precisamos definir um número para ser retornado caso o número seja maior do que o tamanho da lista.

Nth_bad (n: Nat) (xs: List Nat)            : Nat
Nth_bad n List.nil                         = 42n // Valor arbitrário 
Nth_bad Nat.zero (List.cons head tail)     = head
Nth_bad (Nat.succ n) (List.cons head tail) = Nth_bad n tail

Esta solução não é tão boa: se nth_bad retornar 0, não podemos dizer se esse valor realmente aparece na entrada sem processamento adicional. Uma alternativa melhor é para alterar o tipo de retorno de nth_bad para incluir um valor de erro como um possível resultado. Chamamos esse tipo Maybe, pois ele pode ou não ter algo, se tiver é um Maybe.some desse algo, se não tiver, é um Maybe.none.

type Maybe (t) {
  none 
  some (value: t)
}

type NatMaybe {
  none 
  some (value: Nat)
}

ou

type NatMaybe { 
  Maybe Nat
}

Podemos então alterar a definição acima de nth_bad para retornar None quando a lista for muito curto e Some a quando a lista tem membros suficientes e aparece na posição n. Chamamos essa nova função de nth_error para indicar que pode resultar em um erro.

Essa prova ainda serve pra nos apresentar outro recurso do Kind, expressões condicionais, o if e else

Nth_error (n: Nat) (xs: List Nat) : Maybe Nat
Nth_error n List.nil              = Maybe.none
Nth_error n (List.cons head tail) = 
  let ind = Nth_error (Pred n) tail
  Bool.if (Eql n 0n) (Maybe.some Nat head) (ind)

Test_nth_error1 : Equal (Nth_error 0n [4n,5n,6n,7n]) (Maybe.some 4n)
Test_nth_error1 = Equal.refl

Test_nth_error2 : Equal (Nth_error 3n [4n,5n,6n,7n]) (Maybe.some 7n)
Test_nth_error2 = Equal.refl

Test_nth_error3 : Equal (Nth_error 9n [4n,5n,6n,7n]) Maybe.none
Test_nth_error3 = Equal.refl

Extract (d: Nat) (o: Maybe Nat) : Nat
Extract d (Maybe.some k)        = k
Extract d (Maybe.none)          = d

Head_error

Usando a mesma ideia, corrija a função Head de antes para que não tenhamos que passar um elemento padrão para o caso List.nil

Head_error (xs: List Nat) : Maybe Nat
Head_error xs = ?

Test_head_error1 : Equal (Head_error List.nil) Maybe.none
Test_head_error1 = ?

Test_head_error2 : Equal (Head_error [1n]) (Maybe.some Nat 1n)
Test_head_error2 = ?

Test_head_error3 : Equal (Head_error  [5n,6n]) (Maybe.some Nat 5n)
Test_head_error3 = ?

Opcional: Extract_head

Este exercício relaciona sua novo Head_error para o antigo Head.

Extract_head (l: List Nat) (default: Nat) : Equal Nat (Head default l)  (Extract default (Head_error l))
Extract_head l default = ?

Polimorfismo

Neste capítulo, continuamos nosso desenvolvimento de conceitos básicos de programação. Nossos novos princípios essenciais são o polimorfismo (funções de abstração sobre o tipos de dados que eles manipulam) e funções de ordem superior (funções de tratamento como dados). Começamos com o polimorfismo.

Listas Polimórficas

Nos últimos dois capítulos, trabalhamos com listas polimórficas, você pode só não ter percebido. Obviamente, programas interessantes também precisam ser capazes de manipular listas com elementos de outros tipos – listas de strings, listas de booleanos, listas de listas, etc. Poderíamos apenas definir um novo tipo de dados indutivo para cada um deles, por exemplo...

type BoolList {
   nil 
   cons (head: Bool) (tail: List Bool) 
}

.. mas isso rapidamente se tornaria tedioso, em parte porque temos que compensar nomes de construtor diferentes para cada tipo de dados, mas principalmente porque também precisamos definir novas versões de todas as nossas funções de manipulação de listas (length, rev, etc.) para cada nova definição de tipo de dados.

Para evitar toda essa repetição, o Kind suporta definições de tipos indutivos polimórficos. Por exemplo, aqui está um tipo de dados de lista polimórfica e que já vimos no capítulo anterior:

type List (t) {
   nil 
   cons (head: t) (tail: List t) 
}

Esse tipo já exite no Kind e podemos perceber que ele é idententico ao BoolList , mas com um tipo a, esse tipo recebe qualquer outro tipo, seja Nat, Bool, Maybe e etc. Não precisamos criar um tipo de lista para cada um dos tipos de dados, podemos usar esse que adota todas as formas existentes.

Que tipo de coisa é a própria Lista? Uma boa maneira de pensar sobre isso é que List é uma função de Tipos para defi nições indutivas; ou, em outras palavras, List é uma função de Tipos para Tipos. Para qualquer tipo específico x, o tipo List x é um conjunto indutivamente definido de listas cujos elementos são do tipo x.

Com esta definição, quando usamos os construtores List.nil e List.cons para construir listas, precisamos dizer ao Kind o tipo dos elementos nas listas que estamos construindo - isto é, que List.nil e List.cons agora são construtores polimórficos. Observe os tipos de construtores:

record Pair (a) (b) {
  fst : a
  snd : b
}

Nosso tipo Pair recebe outros dois tipos, o a e o b e retorna um par dos dois tipos. Não foi necessário definir se o par era de números naturais, booleanos, listas, bits ou outros pares, nós deixamos a função apta a tratar todos os pares possíveis e isso é graças ao polimorfismo.

Agora podemos voltar e fazer versões polimórficas de todas as listas de processamento funções que escrevemos antes. Aqui está a repetição, por exemplo:

Repeat <a: Type> (x: a) (count: Nat) : List a
Repeat a x Nat.zero                  = List.nil
Repeat a x (Nat.succ count)          = List.cons x (Repeat x count)

Tal como acontece com List.nil e Contras, podemos usar repeat aplicando-o primeiro a um tipo e depois a seu argumento de lista:

Test_repeat1 : Equal (Repeat 4n 2n) (List.cons 4n (List.cons 4n List.nil))
Test_repeat1 = Equal.refl

Para usar repeat para construir outros tipos de listas, simplesmente instanciamos com um parâmetro de tipo apropriado:

Test_repeat2 : Equal (Repeat Bool.false 1n) (List.cons Bool.false List.nil)
Test_repeat2 = Equal.refl

Inferência de anotação de tipo

Vamos escrever a definição do repeat novamente, mas dessa vez omitindo o tipo, mas atenção, essa não é uma boa prática usar o hole, servirá apenas para compreender o poder do Kind e como ele pode ajudar o usuário a encontrar o que deseja.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = ?

Ao rodar o Type Check o terminal nos retorna:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x : _ 

   Repeat x Nat.zero = ?
                       ┬
                       └Here!

Para o caso do contador ser zero, que é o nosso ponto de parada, nós precisamos retornar uma lista do tipo não definido. Como fizemos quando nosso tipo era definido, estamos criando uma lista que não repete o termo nenhuma vez, retornamos um List.nil, depois nós verificamos para o caso de uma lista que repetirá o valor count vezes, para isso nós usaremos a recursão por meio do Nat.succ pred, isto é, o nosso count é igual ao sucessor do predecessor dele.

Repeat x (Nat.succ count) = ?

E o o Type Check nos retorna:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x     : _ 
   •   count : Nat 

   Repeat x (Nat.succ count) = ?
                               ┬
                               └Here!

Agora basta construir a lista com o valor e chamar a função para o predecessor de count, assim construindo a lista até que chegue a zero.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = List.nil
Repeat x (Nat.succ count)  = List.cons x (Repeat x count)

Podemos perceber que, apesar de não definir o tipo de x, o Kind é poderoso para descobrir o tipo que é nosso x quando usamos o hole _. Embora seja possível e possa até facilitar construir uma aplicação inteira usando essa notação, não é uma boa prática, já que, a depender do caso, pode ser inferido um tipo diferente do que o desejado. É interessante sempre definir o tipo do nosso elemento, mesmo que seja um tipo polimórfico.

No primeiro caso, quando definimos o tipo a, já abarcamos todos os tipos possíveis, não sendo necessário o uso do hole e essa é a mágica do polimorfismo, ele nos permite usar uma mesma função para diversos tipos diferentes.

Para usar uma função polimórfica, nós precisamos passar um ou mais tipos em adição aos outros argumentos. Por exemplo, no caso do repeat, nós passamos o tipo <a: Type> e que cada elemento da nossa lista é desse tipo. Fizemos o mesmo com o tipo Pair, que recebia como argumento dois tipos a e b.

Agora fica muito mais fácil compreender os exemplos que usamos no capítulo anterior, quando apresentamos funções como a de length e append:

Length <a> (xs: List a) : Nat
Length (List.nil t)            = Nat.zero
Length (List.cons t head tail) = (Nat.succ (Length tail))

Concat <a: Type> (xs: List a) (ys: List a) : List a
Concat (List.nil)                     ys = ys
Concat (List.cons head tail)          ys = List.cons head (Concat tail ys)

Perceba, há duas notações, uma onde apenas usamos <a> e outra onde usamos <a: Type>, podemos usar qualquer uma delas, o Kind é capaz de compreender as duas formas, será de escolha do desenvolvedor qual ele usará e da complexidade do que será desenvolvido, uma vez que, em códigos muito complexos, talvez seja interessante deixar explícito a outros programadores o que é cada coisa.

Agora é a hora de implementar nossas funções com o tipo implícito, usando o hole e sugar syntax:

Concat_implicito (xs: List _) (ys: List _) : List _
Concat_implicito []                     ys = ys
Concat_implicito (List.cons head tail)  ys = List.cons head (Concat_implicito tail ys)

Aqui nós aprendemos mais uma coisa, o sugar syntax para uma lista vazia e que é apenas [], mas isso está errado, uma vez que o sugar syntax no kind não funciona no lado esquerdo do escopo da função, somente do lado direito funciona. Ao usar o sugar syntax errado, o que o Kind apresenta como erro:

- ERROR  Unexpected token '['.
    Concat_implicito []  ys = ys
                  ┬
                  └Here!

Portanto, é sempre importante saber exatamente o que está sendo feito, ainda mais quando usamos sugar syntax, ela serve pra facilitar a nossa vida, mas pode causar alguns problemas quando usada de forma indevida e isso serve igualmente para o hole e tipos polimórficos nos auxiliam a escrever um programa mais seguro e, ao mesmo tempo, capaz de servir para inúmeros casos.

Outra função que podemos reescrever é a de reverse:

Rev <a> (xs: List a) : List a
Rev List.nil              = [] // sugar syntax de List.nil
Rev (List.cons head tail) = Concat (Rev tail) [head] // sugar syntax de (List.cons head List.nil)

Length <a> (xs: List a) : Nat
Length List.nil              = 0n // sugar syntax de Nat.zero
Length (List.cons head tail) = Nat.succ (Length tail)

Feito isso, basta apenas provar que nossas funções são verdadeiras:

Test_rev1 : Equal (Rev [1,2,3]) [3,2,1]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev [Bool.true]) [Bool.true]
Test_rev2 = Equal.refl

Test_length1 : Equal (Length [1,2,3]) 3n
Test_length1 = Equal.refl

Exercícios polimórficos

Aqui estão alguns exercícios simples, semelhantes aos da seção de Listas, para praticar o polimorfismo. Complete as provas abaixo.

Concat_nil_r <a> (xs: List a) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc <a> (xs: List a) (ys: List a) (zs: List a) : Equal (Concat xs (Concat ys zs)) (Concat (Concat xs ys) zs)
Concat_assoc xs ys zs = ?

Concat_length <a> (xs: List a) (ys: List a) : Equal (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length xs ys = ?

Mais exercícios polimórficos

Aqui estão alguns um pouco mais interessantes...

Rev_app_distr <a> (xs: List a) (ys: List a) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive <a> (xs: List a) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

Pares polimórficos

Seguindo o mesmo padrão, a definição de tipo que demos no último capítulo para pares de números podem ser generalizados para polimórficos pares:

record Pair (a) (b) {
  fst : a
  snd : b
} 

Essa é exatamente a primeira definição de pares que vimos no capítulo anterior e, agora, podemos compreender perfeitamente o que são os tipos a e b na definição do tipo Pair.

Nós podemos refazer as funções de Pares, mas agora para tipos polimórficos:

Fst <a> <b> (pair: Pair a b) : a
Fst (Pair.new fst snd) = fst

Snd <a> <b> (pair: Pair a b) : b
Snd (Pair.new fst snd) = snd

A seguinte função recebe duas listas e combina elas numa lista de pares. Nas linguagens funcionais, isso é comumente chamada de Zip.

Zip <a> <b> (xs: List a) (ys: List b) : (List (Pair a b))
Zip [] ys = []
Zip xs [] = []
Zip (List.cons xs.h xs.t) (List.cons ys.h ys.t) = List.cons (Pair.new xs.h xs.t) (Zip xs.t ys.t)

Check

Sem rodar o programa, tente responder a seguinte pergunta:

• O que a combinação de [1, 2] e [Bool.true, Bool.false, Bool.false, Bool.true] retornará?

Agora rode o código e veja se acertou.

Split

A função Split é o inverso da Zip, ela recebe uma lista de pares e retorna um par de listas. Em muitas linguagens funcionais ela é chamada de Unzip.

Preencha a definição de divisão abaixo. Certifique-se de que ela passe no teste unitário fornecido.

Split <a> <b> (xs: List (Pair a b)) : Pair (List a) (List b)
Split xs = ?

Test_split : Equal (Split [(Pair.new 1 Bool.false), (Pair.new 2 Bool.false)]) (Pair.new ([1, 2]) ([Bool.false, Bool.false]))
Test_split = ?

Polimorfismo com maybe

No capítulo anterior, nós também vimos o tipo Maybe, só que para tipos naturais, entretanto, como vimos no capítulo atual, nossas estruturas de dados podem ser polimórficas, o que significa que o tipo Maybe também é polimórfico e é isso o que veremos agora.

type Maybe (t) {
  none 
  some (value: t)
}

Dessa forma, podemos escrever a função do enésimo erro para ele ser usado com todos os tipos de listas:

Nth_error <a> (n: Nat) (xs: List a) : Maybe a
Nth_error a n List.nil              = Maybe.none
Nth_error a n (List.cons head tail) =
  let ind = Nth_error (Pred n) tail
  Bool.if (Eql n 0n) (Maybe.some head) (ind)


Test_nth_error1 : Equal (Nth_error 0n [4n,5n,5n,7n]) (Maybe.some 4n)
Test_nth_error1 = Equal.refl

Test_nth_error2 : Equal (Nth_error 2n [Bool.true]) Maybe.none
Test_nth_error2 = Equal.refl

Test_nth_error3 : Equal (Nth_error 1n [[1n],[2n]]) (Maybe.some [2n])
Test_nth_error3 = Equal.refl

Hd_error

Complete a definição de uma versão polimórfica da função Hd_error do último capítulo. Certifique-se de que ele passe nos testes de unitários abaixo.

Hd_error <a> (xs: Lista a) : Maybe a
Hd_error xs = ?

Test_hd_error1 : Equal (Hd_error [1, 2]) (Maybe.some 1)
Test_hd_error1 = ?

Test_hd_error2 : Equal (Hd_error [[1], [2]]) (Maybe.some [1])
Test_hd_error2 = ?

Funções como dados

Como muitas outras linguagens de programação modernas – incluindo todas as linguagens funcionais (ML, Haskell, Scheme, Scala, Clojure etc.) – o Kind trata as funções como cidadãos de primeira classe, permitindo que sejam passadas como argumentos para outras funções, retornados como resultados, armazenados em estruturas de dados, etc.

Funções de Alta Ordem (Higher-Order Functions.)

Funções que manipulam outras funções são frequentemente chamadas de funções de alta ordem (ou ainda de "ordem superior"). Aqui está um exemplo simples:

Doit3times <x> (f: x -> x) (n: x) : x
Doit3times f x = (f (f (f x)))

Test_doit3times1 : Equal (Doit3times (x => MinusTwo x) 9n) 3n
Test_doit3times1 = Equal.refl

Test_doit3times2 : Equal (Doit3times (x => Notb x) Bool.true) (Bool.false)
Test_doit3times2 = Equal.refl

Filtro

Aqui está uma função de alta ordem mais útil, pegando uma lista de xs e um predicado em x (uma função de x para Bool) e “filtrando” a lista, retornando uma nova lista contendo apenas aqueles elementos para os quais o predicado retorna True.

Filter <x> (test: x -> Bool) (xs: List x) : List x
Filter test List.nil                      = []
Filter test (List.cons head tail)         =
   Bool.if (test head) (List.cons head (Filter test tail)) (Filter test tail)

Por exemplo, se aplicarmos o filtro de "é par" numa lista de números, ela nos retornará uma outra lista apena com os números pares

Test_filter1 : Equal (Filter (x => Evenb x) [1,2,3,4,5])  [2,4]  
Test_filter1 = Equal.refl

Length_is_one <x> (xs: List x) : Bool
Length_is_one xs               = Eql (Length xs) 1n

Test_filter2 : Equal (Filter (x => Length_is_one x) ([[1],[1,2],[3],[1,2,3],[21]])) ([[1],[3],[21]])
Test_filter2 = Equal.refl

Podemos usar filter para fornecer uma versão concisa da função Countoddmembers do capítulo Listas.

CountOddMembers (xs: List Nat) : Nat
CountOddMembers xs             = Length (Filter (x => Oddb x) xs)

Test_CountOddMembers1 : Equal (CountOddMembers  [1n,0n,3n,1n,4n,5n]) 4n
Test_CountOddMembers1 = Equal.refl

Test_CountOddMembers2 : Equal (CountOddMembers  [0n 2n,4n]) 0n
Test_CountOddMembers2 = Equal.refl

Test_CountOddMembers3 : Equal (CountOddMembers []) 0n
Test_CountOddMembers3 = Equal.refl

Funções anônimas

É indiscutivelmente um pouco triste, no exemplo acima, ser forçado a definir a função Length_is_one e dar-lhe um nome apenas para poder passá-la como um argumento para filtrar, já que provavelmente nunca a usaremos novamente. Além disso, este não é um exemplo isolado: ao usar funções de ordem superior, muitas vezes queremos passar como argumentos funções “únicas” que nunca mais usaremos; ter que dar um nome a cada uma dessas funções seria tedioso. Felizmente, existe uma maneira melhor. Podemos construir uma função “on the fly” sem declará-la no nível superior ou dar-lhe um nome.

Test_anon_fun : Equal (Doit3times (x => (Mult x x)) 2n) 256n
Test_anon_fun = Equal.refl

A expressão x => (Mult x x) pode ser lida como a função recebe um número n e retorna n * n

Aqui está o exemplo de Filter reescrita pra usar uma função anonima:

Test_filter2 : Equal (Filter (x => (Length_is_one x)) [[1],[1,2],[2],[1,2,3],[21]]) [[1],[2],[21]]
Test_filter2 = Equal.refl

Filter_even_gt7

Use Filter com funções anônimas (em vez de definição de função) para escrever uma função Filter_even_gt7 que recebe uma lista de números naturais como entrada e retorna uma lista apenas daqueles que são pares e maiores que 7.

Filter_even_gt7 (xs: List Nat) : List Nat
Filter_even_gt7 xs = ?

Test_filter_even_gt7a: Equal (Filter_even_gt7 [1n,2n,3n,4n,5n,7n,8n,9n,10n,11n,12n]) [8n,10n,12n]
Test_filter_even_gt7a = ?

Test_filter_even_gt7b : Equal (Filter_even_gt7 [5n, 2n, 6n, 19n, 129n]) []
Test_filter_even_gt7b = ?

Uma pequena observação, o leitor mais atento percebeu que usamos uma nova notação, os n após os números, esse é um sugar syntax que o Kind possui, nós podemos escrever números naturais apenas acrescentando um n ao número, entretanto essa é uma sintaxe que pode acabar pesando para Kind. Imagine que o usuário pretende apenas adicionar o número 1 ao 1000000, é um cálculo simples e que o Kind faz com uma mão nas costas, mas fica um pouco mais pesado quando usado o sugar syntax dos números naturais, a soma será um Plus 1n 1000000n, mas o Kind precisará verificar cada Nat.succ até o um milhão e um, ou seja, serão um milhão e um "Nat.succ" computados de forma desnecessárias. Essa sintaxe é bem útil, mas devemos usar com cuidado, o ideal é que para números grandes seja usado um U60.to_nat, que é bem mais leve para o Kind.

Partition

Use Filter para escrever uma função Partition em Kind

Partition <x> (test: x -> Bool) (xs: List x) : Pair (List x) (List x)
Partition test xs = ?

Dado um conjunto x, uma função de teste do tipo x -> Bool e uma Lista x, a função Partition deve retornar um par de listas. O primeiro membro do par é a sub-lista da lista original contendo os elementos que satisfazem o teste, e o segundo é a sub-lista contendo aqueles que falham no teste. A ordem dos elementos nas duas sub-listas deve ser a mesma da lista original.

Test_partition1 : Equal (Partition (x => Oddb x) [1n,2n,3n,4n,5n]) (Pair.new [1n,3n,5n] [2n,4n])
Test_partition1 = ?

Test_partition2 : Equal (Partition (x => Bool.false) [5n, 9n, 0n]) (Pair.new [] [5n, 9n, 0n])

Map

Outra função de alta ordem muito útil é a Map

Map <x> <y> (f: x -> y) (xs: List x)  : List y
Map f List.nil                        = List.nil
Map f (List.cons head tail)           = List.cons (f head) (Map f tail)

Ela recebe uma função f e uma lista xs = [n1, n2, n3, ...] e retorna a lista [f n1, f n2, f n3, ...], onde f é aplicado a cada elemento de xs. Por exemplo:

Test_map1 : Equal (Map (x => Plus 3n x) [2n, 0n, 2n]) [5n, 3n, 5n]
Test_map1 = Equal.refl

Os tipos de elementos da lista de entrada e saída não precisam ser os mesmos, pois Map aceita dois argumentos de tipo, x e y; dessa forma pode ser aplicada uma de números para booleanos para produzir uma lista de booleanos:

Test_map2 : Equal (Map (x => Nat.is_odd x) [2n, 1n, 2n, 5n]) [Bool.false, Bool.true, Bool.false, Bool.true]
Test_map2 = Equal.refl

Pode até ser aplicada a uma lista de números uma função que retorne uma lista de lista de booleanos:

Test_map3 = Equal (Map (x => [(Nat.is_even x), (Nat.is_odd x)]) [2n, 1n, 2n, 5n]) [[Bool.true, Bool.false], [Bool.false, Bool.true], [Bool.true, Bool.false], [Bool.false, Bool.true]]
Test_map3 = Equal.refl

Map_rev

Vamos dificultar um pouco mais as coisas. Mostre a comutatividade de Rev e Map, você pode precisar de uma função auxiliar:

Map_rev <x> <y> (f: x -> y) (xs: List x) : Equal (Map f (Rev xs)) (Rev (Map f xs))
Map_rev f xs = ?

Flat_equal

A função Map mapeia uma List x para uma List y usando uma função do tipo x -> y. Podemos definir uma função semelhante, Flat_map, que mapeia uma Lista x para uma Lista y usando uma função f do tipo x -> Lista y. Sua definição deve funcionar "achatando" os resultados de f, assim:

Flat_equal : Equal (Flat_map ( x => ([x , (Plus x 1n), (Plus x 2n)])) [1n, 5n, 10n]) [1n, 2n, 3n, 5n, 6n, 7n, 10n, 11n, 12n]
Flat_equal = Equal.refl

Flat_map <x> <y> (f: x -> List y) (xs: List x) : List y
Flat_map f xs = ?

Test_flat_map1 : Equal (Flat_map (x => [x, x, x]) [1n, 5n, 4n]) [1n, 1n, 1n, 5n, 5n, 5n, 4n, 4n, 4n]
Test_flat_map1 = ?

As listas não são o único tipo indutivo para o qual podemos escrever uma função Map. Aqui está a definição de mapa para o tipo Maybe:

Maybe_map <x> <y> (f: x -> y) (a: Maybe x)  : Maybe y
Maybe_map f Maybe.none                      = Maybe.none
Maybe_map f (Maybe.some x)                  = Maybe.some (f x)

Fold

Uma função de ordem superior ainda mais poderosa é chamada Fold. Esta função é a inspiração para a operação “reduce” que está no coração da estrutura de programação distribuída map/reduce do Google.

Fold <x> <y> (f: x -> y -> y) (xs: List x) (a: y)   : y
Fold f List.nil a                                   = a
Fold f (List.cons head tail) a                      = f head (Fold f tail a)

Test_fold1 : Equal (Fold (x => y => (Bool.and x y)) [Bool.true, Bool.true, Bool.false] Bool.false) Bool.false
Test_fold1 = ?

Test_fold2 : Equal (Fold (x => y => (* x y)) [1, 2, 3, 4] 1) 24
Test_fold2 = ?

Test_fold3 : Equal (Fold (x => y => (Concat x y)) [[1], [], [2, 3], [], [4]] [5, 6, 7]) [1, 2, 3, 4, 5, 6, 7]
Test_fold3 = ?

Fold_types_different

Observe que o tipo Fold é parametrizado por duas variáveis de tipo, x e y, e o parâmetro f é um operador binário que recebe um x e um y e retorna um y. Você consegue pensar em uma situação em que seria útil que x e y fossem diferentes?

Funções que constroem funções

A maioria das funções de ordem superior sobre as quais falamos até agora usam funções como argumentos. Vejamos alguns exemplos que envolvem o retorno de funções como resultados de outras funções. Para começar, aqui está uma função que recebe um valor x (extraído de algum tipo x) e retorna uma função de Nat para x que retorna x sempre que é chamada, ignorando seu argumento Nat

Constfun <y> (x: y) : Nat -> y
Constfun x = y => x

Ftrue : Nat -> Bool
Ftrue = Constfun Bool.true

Constfun_example1 : Equal ((Ftrue) 0n) Bool.true
Constfun_example1 = Equal.refl

Constfun_example2 : Equal ((Constfun 5n) 99n) 5n
Constfun_example2 = Equal.refl

Plus3 : Nat -> Nat
Plus3 = n => Plus 3n n

Test_plus3_1 : Equal ((Plus3) 4n) 7n
Test_plus3_1 = Equal.refl

Test_plus3_2 : Equal (Doit3times (Plus3) 0n) 9n
Test_plus3_2 = Equal.refl

Test_plus3_3 : Equal (Doit3times (x => Plus 3n x) 0n) 9n
Test_plus3_3 = Equal.refl

Exercícios adicionais

Muitas funções comuns em listas podem ser implementado em termos de Fold. Por exemplo, aqui está uma definição alternativa de comprimento:

Fold_length <x> (xs: List x) : Nat
Fold_length xs = Fold (x => y Nat.succ y) xs 0n

Test_fold_length1 : Equal (Fold_length [4, 7, 0]) 3n
Test_fold_length1 = Equal.refl

Prove a validade de Fold_length:

Fold_length_correct <x> (xs: List x) : Equal (Fold_length xs) (List.length xs)
Fold_length_correct xs = ?

Nós também podemos definir Map nos termos de Fold. Termine a função:

Fold_map <x> <y> (f: x -> y) (xs: List x) : List y
Fold_map f xs = ?

Escreva um teorema fold_map_correct em Kind declarando que Fold_map está correto e prove isso:

Fold_map_correct : ?

No Kind, uma função f: a -> b -> c realmente tem o tipo a -> (b -> c). Ou seja, se você der a f um valor do tipo a, ele fornecerá a função g: b -> c. Se você der a ´g´ um valor do tipo ´b´, ele retornará um valor do tipo ´c´. Isso permite a aplicação parcial, como em Plus3. Processar uma lista de argumentos com funções que retornam funções é chamado de currying, em homenagem ao lógico Haskell Curry.

Por outro lado, podemos reinterpretar a função f: a -> b -> c como (Pair a b) -> c. Isso é chamado de uncurrying. Com uma função binária uncurry, ambos os argumentos devem ser fornecidos ao mesmo tempo como um par; não há aplicação parcial.

Podemos definir o curry da seguinte forma:

Pair_curry <x> <y> <z> (f: (Pair x y) -> z) (x_val: x) (y_val: y) : z 
Pair_curry f x_val y_val = ?

Como exercício, defina seu inverso, Pair_uncurry. Em seguida, prove os teoremas abaixo para mostrar que os dois são inversos.

Pair_uncurry <x> <y> <z> (f: x -> y -> z) (p: Pair x y) : z
Pair_uncurry f p = ?

Como um exemplo (trivial) da utilidade do curry, podemos usá-lo para encurtar um dos exemplos que vimos acima:

Test_map2 : Equal (Map (x => Plus 3n x) [2n,0n,2n]) [5n,3n,5n]
Test_map2 = Equal.refl

Exercício de reflexão: antes de executar os comandos a seguir, você pode calcular os tipos de Pair_curry e Pair_uncurry?

Uncurry_curry <x> <y> <z> (f: x -> y -> z) (x_val: x) (y_val: y) : 
   Equal z (Pair_curry (p => Pair_uncurry f p) x_val y_val) (f x_val y_val)
Uncurry_curry f x_val y_val = ?

Curry_uncurry <x> <y> <z> (f:(Pair x y) -> z) (p: Pair x y) : 
   Equal z (Pair_uncurry (x => y => Pair_curry f x y) p) (f p)
Curry_uncurry f p = ?

Lembre-se da definição da função Nth_error(Nth_error_informal):

Nth_error_informal <x> (l: List x) (n: Nat) : Maybe x
Nth_error_informal List.nil n = Maybe.none 
Nth_error_informal (List.cons head tail) Nat.zero = Maybe.some head 
Nth_error_informal (List.cons head tail) (Nat.succ n) = Nth_error tail n

Escreva uma prova informal do seguinte teorema:

Nat -> List -> (Equal (Length List) Nat) : Equal (Nth_error_informal List Nat) Maybe.none

Nós podemos explorar uma forma alternativa de definir os números naturais, usando os Numerais de Church, nomeado em homenagem ao matemático Alonzo Church. Podemos representar um número natural n como uma função que recebe uma função s como parâmetro e retorna s iterado n vezes.

Num <x> : Type
Num x = (x -> x) -> x -> x

Vamos ver como escrever alguns números com esta notação. Iterar uma função uma vez deve ser o mesmo que apenas aplicá-la. Desta forma:

One : Num
One = s => z => s z 

Perceba, a função aplica um s a um z, se lermos o s como sucessor e o z como zero, temos que o One é igual ao sucessor de zero.

Similarmente, o Two aplica a função s duas vezes ao z:

Two : Num
Two = s => z => s (s z)

Definir zero é um pouco mais complicado: como podemos “aplicar uma função zero vezes”? A resposta é realmente simples: basta retornar o argumento intocado.

Zero : Num
Zero = s => z => z

Mais geralmente, um número n pode ser escrito como s => z => s (s ... (s z) ...), com n ocorrências de s. Observe em particular como a função doit3times que definimos anteriormente é, na verdade, apenas a representação de Church do 3.

Three : Num
Three = s => z => Doit3times s z

Complete as definições das seguintes funções. Certifique-se de que os testes unitários correspondentes sejam aprovados, provando-os com Equal.refl

Sucessor

Sucessor de um número natural:

Succ (n: Num) : Num
Succ n = ?

Succ_1 : Equal (Succ Zero) (One)
Succ_1 = ?

Succ_2 : Equal (Succ One) (Two)
Succ_2 = ?

Succ_3 : Equal (Succ Two) (Three)
Succ_3 = ?

Adição

Adição de dois números naturais:

Plus (n: Num) (n: Num) : Num
Plus n m = ?

Plus_1 : Equal (Plus One Zero) (One)
Plus_1 = ?

Plus_2 : Equal (Plus Two One) (Plus One Two)
Plus_2 = ?

Plus_3 : Equal (Plus (Plus Two Two) Three) (Plus One (Plus Three Three))
Plus_3 = ?

Multiplicação

Mult (n: Num) (m: Num) : Num
Mult n m = ?

Mult_1 : Equal (Mult One One) One
Mult_1 = ?

Mult_2 : Equal (Mult Zero (Plus Three Three)) Zero
Mult_2 = ?

Mult_3 : Equal (Mult Two Three) (Plus Three Three)
Mult_3 = ?

Exponenciação

Não é possível fazê-lo funcionar com Exp (n: Num) (m: Num) : Num. O polimorfismo desempenha um papel crucial aqui. No entanto, escolher o tipo certo para iterar pode ser complicado. Se você encontrar um erro de "inconsistência", tente iterar em um tipo diferente: o próprio Num geralmente é problemático.

Exp (n: Num) (m: Num -> Num) : Num
Exp n m = ?

Exp_1 : Equal (Exp Two Two) (Plus Two Two)
Exp_1 = ?

Exp_2 : Equal (Exp Three Two) (Plus (Mult Two (Mult Two Two)) One)
Exp_2 = ?

Exp_3 : Equal (Exp Three Zero) One
Exp_3 = ?

Predecessor

Pred (n: Num -> Num) : Num
Pred n = ?

Pred_1 : Equal (Pred Zero) (Zero)
Pred_1 = ?

Pred_2 : Equal (Pred Two) (One)
Pred_2 = ?

Pred_3 : Equal (Pred Three) (Two)
Pred_3 = ?

Subtração

Sub (n: Num) (m: Num) : Num
Sub n m = ?

Sub_1 : Equal (Sub One Zero) (One)
Sub_1 = ?

Sub_2 : Equal (Sub Two Two) (Sub One One)
Sub_2 = ?

Sub_3 : Equal (Sub Three One) Two
Sub_3 = ?

Lógica em Kind

Nos capítulos anteriores, vimos muitos exemplos de proposições e formas de apresentar evidências de sua veracidade (provas). Em particular, trabalhamos extensivamente com proposições de igualdade da forma e1 = e2, com implicações (p -> q), e com proposições quantificadas (x -> P(x)). Neste capítulo, veremos como Kind pode ser usado para realizar outras formas familiares de raciocínio lógico.

Antes de mergulhar nos detalhes, vamos falar um pouco sobre o status das declarações matemáticas em Kind. Lembre-se de que Kind é uma linguagem tipada, o que significa que toda expressão sensível em seu mundo tem um tipo associado. As afirmações lógicas não são exceção: qualquer afirmação que possamos tentar provar em Kind tem um tipo, ou seja, Type, o tipo de proposições. Podemos ver isso com o tipo Booleano:

Bool: Type
Bool.true  : Bool
Bool.false : Bool

No tipo Bool nós temos o Bool.true e o Bool.false. Para criar o tipo Bool nós declaramos que ele é um tipo (Type) e depois que o Bool.true e o Bool.false são do tipo Bool. Vendo como é, fica bem mais simples. Muitas vezes nos assombramos ao ver o nome "funcional", mas Kind é uma linguagem muito amigável, veremos bem sobre isso mais para a frente.

Outro exemplo possível é o Nat, dos números naturais. Números naturais são todos os números inteiros maiores ou igual a zero. Ou seja, eles começam com o número zero e vão até o infinito, mas não possuem valores decimais. Ou seja, o 3 é um número natural, mas o 3,14 não é, da mesma forma que o -3 também não é. Então sabemos que o número natural é feito de zero e dos sucessores dele. Vamos ver como isso é no kind:

Nat: Type
Nat.zero             : Nat
Nat.succ (pred: Nat) : Nat

Percebemos que a construção é similar aos Booleanos, mas há um elemento extra no Nat.succ, que é o "(pred: Nat)", e isso se deve ao fato de que, enquanto no outro nós tínhamos apenas duas opções de retorno (True ou False), agora temos uma infinidade de números que o código precisa compreender, além de que deve haver uma forma do código parar de rodar (veremos mais sobre isso ao decorrer desse estudo), uma vez que um código que nunca para de rodar é um código que nunca nos dará o resultado.

Porém, de qualquer forma, percebemos que a estrutura do Nat é basicamente a mesma do Bool, isso nos mostra que podemos criar qualquer tipo, desde que sigamos a mesma estrutura. Vamos criar o tipo suco:

Suco : Type
Suco.laranja : Suco
Suco.caju    : Suco

O suco de laranja possui dois construtores, o Suco.laranja e o Suco.caju. Esse tipo é fictício, ele não existia até então, mas agora podemos usar ele como um tipo e isso nos mostra que, graças ao design do Kind, podemos criar uma infinidade de tipos, pois todo tipo é uma função.

Entender a construção dos tipos impedirá que alguns erros de sintaxe ocorram.

Apenas revisando, nosso elemento Suco é do tipo Type e o Suco.laranja é do tipo Suco. Desta forma, em termos leigos, temos que o elemento fica a direita dos dois pontos e o tipo a esquerda

elemento : Tipo

Como dito antes, até mesmo os tipos são funções, logo podemos ter uma função como tipo. Por exemplo:

Problema : (Equal Bool Bool.true Bool.true

Podemos perceber que temos um elemento chamado "Problema" e ele é do tipo "(Equal Bool Bool.true Bool.true)". Nós já vimos essa estrutura diversas vezes nos últimos capítulos e agora é fácil entender que essa função é um tipo e, da mesma forma que não escrevemos

Suco: Type
Suco.laranja : Type

Não podemos simplesmente copiar a função para os construtores desse tipo. O Suco é tipo Type, mas o Suco.laranja não é do tipo Type, ele é do tipo Suco.

Mas atenção, observe que todas as proposições sintaticamente bem formadas têm o tipo Type em Kind, independentemente de serem verdadeiras ou não. Simplesmente ser uma proposição é uma coisa; ser demonstrável é outra coisa!

De fato, as proposições não têm apenas tipos: elas são objetos de primeira classe que podem ser manipulados da mesma forma que as outras entidades no mundo de Kind. Até agora, vimos um local primário onde as proposições podem aparecer: nas assinaturas de tipo das funções.

Plus_2_2_is_4 : Equal (Plus 2n 2n) 4n
Plus_2_2_is_4 = Equal.refl

Mas as proposições podem ser usadas de muitas outras maneiras. Por exemplo, podemos dar um nome a uma proposição como um valor próprio, assim como demos nomes a expressões de outros tipos.

Plus_fact : Type
Plus_fact = Equal (Plus 2n 2n) 4n

Posteriormente, podemos usar esse nome em qualquer situação em que uma proposição seja esperada – por exemplo, em uma declaração de função.

Plus_fact_is_true : Plus_fact
Plus_fact_is_true = Equal.refl

Também podemos escrever proposições parametrizadas – isto é, funções que recebem argumentos de algum tipo e retornam uma proposição. Por exemplo, a seguinte função pega um número e retorna uma proposição afirmando que esse número é igual a três:

Is_three (n: Nat) : Type
Is_three n = Equal Nat n 3n

Em Kind, diz-se que funções que retornam proposições definem propriedades de seus argumentos. Por exemplo, aqui está uma propriedade (polimórfica) que define a noção familiar de uma função injetiva

Injective <a> <b> (f: a -> b) : Type
Injective a b f = (x: a) -> (y: a) -> (e: Equal b (f x) (f y)) -> (Equal a x y)

Nós podemos instanciar uma regra de injetividade com

Nat.succ_injective : Injective ((x: Nat) => Nat.succ x)
Nat.succ_injective =
  (a: Nat) =>
  (b: Nat) =>
  (e: Equal Nat (Nat.succ a) (Nat.succ b)) =>
  Equal.apply (x => Nat.pred x) e

Conectivos Lógicos

Conjunção

A conjunção (ou lógico e) em kind recebe duas proposições a e b, que devem retornar um valor booleano true ou false.

Bool.and (a: Bool) (b: Bool) : Bool
Bool.and Bool.true  b = b
Bool.and Bool.false b = Bool.false

Se a é verdadeiro, basta apenas retornar o valor de b, agora se o a for falso, não há a necessidade de verificar o valor do segundo elemento.

Por se tratar de um caso limitado (há apenas duas opções) dá para verificar com uma prova simples:

ConjuntiveBool : Equal Bool (Bool.and Bool.true Bool.false) Bool.false
ConjuntiveBool = Equal.refl

And_exercise

And_exercise : Pair (Equal (Plus 3n 4n) 7n) (Equal (Mult 2n 2n) 4n)
And_exercise = ?

Tanto para provar declarações conjuntivas. Para ir na outra direção – ou seja, usar uma hipótese conjuntiva para ajudar a provar outra coisa – empregamos o pattern matching. Se o contexto de prova contiver uma hipótese h da forma (a,b), a divisão de caso irá substituí-la por um padrão de pares (a,b).

And_example2 (n: Nat) (m: Nat) (e: Pair (Equal n 0n) (Equal m 0n)) : Equal (Plus n m ) 0n
And_example2 Nat.zero Nat.zero e        = Equal.refl
And_example2 Nat.zero (Nat.succ m ) e   = 
    let p = (Equal.rewrite
    (Pair.snd e)
    (x => match Nat x {
        zero => Empty
        succ => Unit
    })
    (Unit.new))
    Empty.absurd p
And_example2 (Nat.succ n) m e           =
    let p = (Equal.rewrite
    (Pair.fst e)
    (x => match Nat x {
        zero => Empty
        succ => Unit 
    })
    (Unit.new))
    Empty.absurd p

Você pode se perguntar por que nos preocupamos em agrupar as duas hipóteses n = 0 e m = 0 em uma única conjunção, já que também poderíamos ter declarado o teorema com duas premissas separadas:

And_example2a (n: Nat) (m: Nat) (e1: Equal n 0n) (e2: Equal m 0n) : Equal (Plus n m) 0n
And_example2a Nat.zero Nat.zero e1 e2        = Equal.refl
And_example2a Nat.zero (Nat.succ m ) e1 e2   = 
    let p = (Equal.rewrite
    (e2)
    (x => match Nat x {
        zero => Empty
        succ => Unit
    })
    (Unit.new))
    Empty.absurd p
And_example2a (Nat.succ n) m e1 e2           =
    let p = (Equal.rewrite
    (e1)
    (x => match Nat x {
        zero => Empty
        succ => Unit 
    })
    (Unit.new))
    Empty.absurd p

Para este teorema, ambas as formulações são adequadas. Mas é importante entender como trabalhar com hipóteses conjuntivas porque as conjunções geralmente surgem de etapas intermediárias em provas, especialmente em desenvolvimentos maiores. Aqui está um exemplo simples:

And_example3 (n: Nat) (m: Nat) (e: Equal (Plus n m) 0n) : Equal (Mult n m) 0n
And_example3 Nat.zero m e =  Equal.refl
And_example3 (Nat.succ n) m e =
    let p = (Equal.rewrite 
        (e)
        (x => match Nat x {
            zero => Empty 
            succ => Unit                      
        })
        (Unit.new))
    Empty.absurd p

Outra situação comum com conjunções é que sabemos (a,b), mas em algum contexto precisamos apenas de a (ou apenas b). Os seguintes teoremas são úteis em tais casos:

Proj1 <p> <q> (a: Pair p q) : p
Proj1 (Pair.new fst snd)    = fst

Proj2

Proj2 <p> <q> (b: Pair p q) : q
Proj2 (Pair.new fst snd)    = ?

Por fim, às vezes precisamos reorganizar a ordem das conjunções e/ou agrupar as conjunções de múltiplas vias. Os seguintes teoremas de comutatividade e associatividade são úteis em tais casos.

And_commut <p> <q> (c: Pair p q) : Pair q p
And_commut (Pair.new fst snd)    = Pair.new snd fst

And_assoc

And_assoc <p> <q> <r> (a: Pair p (Pair q r))  : Pair (Pair p q) r
And_assoc (Pair.new p (Pair q r) fst (Pair.new snd trd)) = ?

Disjunção

Outro conectivo importante é a disjunção, ou lógico, de duas proposições: Either a b é verdadeiro quando a ou b é. O primeiro caso foi marcado com left e o segundo com right. Para usar uma hipótese disjuntiva em uma prova, procedemos pela análise de caso, que, como para Nat ou outros tipos de dados, pode ser feita com correspondência de padrões. Aqui está um exemplo:

Or_example (n: Nat) (m: Nat) (e: (Either (Equal n 0n) (Equal m 0n))) : Equal (Mult n m) 0n
Or_example Nat.zero m e     = Equal.refl
Or_example n Nat.zero e     = Mult_0_r n
Or_example (Nat.succ n) m (Either.left l r val) = 
    let p = (Equal.rewrite
        (val)
        ( x => match Nat x {
            zero => Empty 
            succ => Unit            
        })
        (Unit.new))
    Empty.absurd p
Or_example (Nat.succ n) (Nat.succ m) (Either.right l r val) = 
    let p = (Equal.rewrite 
        (val)
        ( x => match Nat x {
            zero => Empty
            succ => Unit                   
        })
        (Unit.new))
Empty.absurd p

Inversamente, para mostrar que uma disjunção é válida, precisamos mostrar que um de seus lados é válido. Isso pode ser feito por meio dos construtores Left e Right mencionados acima. Aqui está um uso trivial...

axiom
Or_intro_left <a> <b> (t: a) : Either a b
Or_intro_left t = Either.left t

axiom
Or_intro_right <a> <b> (t: b) : Either a b
Or_intro_right t = Either.right t

... e um exemplo um pouco mais interessante exigindo ambos

Zero_or_succ (n: Nat)     : Either (Equal n 0n) (Equal n (Nat.succ (Nat.pred n)))
Zero_or_succ Nat.zero     = Either.left  Equal.refl
Zero_or_succ (Nat.succ n) = Either.right Equal.refl

Mult_eq_0

axiom
Mult_eq_0 (n: Nat) (m: Nat) (e: Equal (Mult n m) 0n) : Either (Equal n 0n) (Equal m 0n)
Mult_eq_0 n m e = ?

Or_commut

Or_commut <p> <q> (e: Either p q) : Either q p
Or_commut e: ?

Falsidade e Negação

Até agora, nos preocupamos principalmente em provar que certas coisas são verdadeiras – adição é comutativa, anexação de listas é associativa, etc. Claro, também podemos estar interessados em resultados negativos, mostrando que certas proposições não são verdadeiras. Em Kind, tais declarações negativas são expressas com a função de nível de tipo de negação Not.

Para ver como a negação funciona, relembre a discussão do princípio da explosão do capítulo anterior; ela afirma que, se assumirmos uma contradição, então qualquer outra proposição pode ser derivada. Seguindo essa intuição, poderíamos definir Not p como q -> (p -> q). Kind realmente faz uma escolha ligeiramente diferente, definindo Not como p -> Empty, onde Empty é uma proposição contraditória específica definida na biblioteca padrão como um tipo de dados sem construtores.

Empty: Type

Not <p: Type>: Type
Not p = p -> Empty

Como Empty é uma proposição contraditória, o princípio da explosão também se aplica a ela. Se obtivermos Empty no contexto de prova, podemos chamá-lo de Empty ou absurd para completar qualquer objetivo:

Ex_falso_quodlibet <p> : Empty -> p
Ex_falso_quodlibet p   = e => Empty.absurd e

O latim ex falso quodlibet significa, literalmente, “da falsidade segue o que você quiser”; este é outro nome comum para o princípio da explosão.

Not_implies_our_not

Mostre que a definição da negação em Kind implica a intuitiva mencionada acima:

Not_implies_our_not <p> <q> (e: Not p) : q -> (p -> q)
Not_implies_our_not p q e = ?

É assim que usamos Not para afirmar que 0 e 1 são elementos diferentes de Nat:

Zero_not_one : Not (Equal Nat.zero (Nat.succ Nat.zero))
Zero_not_one = 
  (emp => 
    let app = Equal.apply (x => Nat.is_zero x) emp
    Equal.rewrite app (e => if e {Nat} else {Empty}) Nat.zero)

É preciso um pouco de prática para se acostumar a trabalhar com a negação em Kind. Mesmo que você possa ver perfeitamente por que uma afirmação envolvendo negação é verdadeira, pode ser um pouco complicado no começo colocar as coisas na configuração certa para que Kind possa entender! Aqui estão as provas de alguns fatos familiares para você se aquecer:

Not_false : Not Empty
Not_false = e => Empty.absurd e

Contradiction_implies_anythig <p> <q> (a: Pair p (Not p)) : q
Contradiction_implies_anythig p q (Pair.new fst snd) =
  let app = snd fst
  Empty.absurd app

Double_neg_inf

Escreva uma prova informal de Double_neg: Teorema: Se p, então (não (não p)), para qualquer proposição p.

Contrapositive

Contrapositive <p> <q> (f: p -> q) : (Not q -> Not p)
Contrapositive p q f = ?

Not_both_true_and_false

Not_both_true_and_false <p> : Not (Pair p (Not p))
Not_both_true_and_false p = ?

Da mesma forma, já que a desigualdade envolve uma negação, é preciso um pouco de prática para trabalhar com ela de forma fluente. Aqui está um truque útil. Se você estiver tentando provar uma meta que é absurda (por exemplo, o estado final é Bool.false == Bool.true), aplique Empty.absurd para mudar a meta para Empty. Isso facilita o uso de pressupostos do tipo (Not p) que podem estar disponíveis no contexto - em particular, pressupostos do tipo Not (x == y).

Not_true_is_false (b: Bool) (e: Not (Equal Bool b Bool.true)) : Equal Bool b Bool.false
Not_true_is_false Bool.false e = Equal.refl
Not_true_is_false Bool.true e = Empty.absurd (e Equal.refl)

Verdade

Além de Empty, a biblioteca padrão do Kind também define Unit, uma proposição que é trivialmente verdadeira. Para provar isso, usamos a constante:

True_is_true : Unit
True_is_true = Unit.new

Ao contrário de Empty, que é amplamente utilizado, Unit é usado bastante raramente em provas, já que é trivial (e, portanto, pouco interessante) provar como objetivo e não carrega nenhuma informação útil como hipótese. No entanto, pode ser bastante útil ao definir provas complexas usando condicionais ou como um parâmetro para provas de ordem superior. Veremos exemplos desse uso de Unit mais tarde.

Equivalência

Equivalência Lógica. A útil conectiva "se e somente se", que afirma que duas proposições têm o mesmo valor de verdade, é apenas a conjunção de duas implicações.

record Equivalence (p: Type) (q: Type) {
 lft: p -> q 
 rgt: q -> p
}

//#axiom
Equivalence.lft <p> <q> (e: Equivalence p q) : p 
Equivalence.lft (Equivalence.new l r)        = r (Equivalence.rgt (Equivalence.new l r))

//#axiom
Equivalence.rgt <p> <q> (e: Equivalence p q) : q 
Equivalence.rgt (Equivalence.new l r)        = l (Equivalence.lft (Equivalence.new l r))

Not_true_iff_false (b: Bool) : Equivalence (Not (Equal Bool b Bool.true)) (Equal Bool b Bool.false)
Not_true_iff_false  b = Equivalence.new (x => Not_true_is_false b x) (y => Not_true_and_false b y)

Not_true_and_false (b : Bool) (e: Equal Bool b Bool.false) : Not (Equal Bool b Bool.true)
Not_true_and_false Bool.false Equal.refl = 
 emp => 
 let p = Equal.rewrite emp
   (x => match Bool x {
    true => Empty
    false => Unit
    }) 
    (Unit.new)
 Empty.absurd p
Not_true_and_false Bool.true e = 
 let p = Equal.rewrite e 
  (x => if x 
  {Unit} 
  else 
  {Empty}) 
 (Unit.new)
 Empty.absurd p

Simétrica

Uma relação é simétrica se, para todos os elementos p e q em seu domínio, se p é equivalente a q, então q é equivalente a p. Isso pode ser provado com a seguinte regra:

Equivalence.mirror <p> <q> (e: Equivalence p q) : Equivalence q p
Equivalence.mirror p q (Equivalence.new lft rgt) = (Equivalence.new rgt lft)

Reflexividade

Uma relação é reflexiva se, para todo elemento p em seu domínio, p é equivalente a si mesmo. Isso pode ser provado com a seguinte regra:

Equivalence.refl <p> : Equivalence p p
Equivalence.refl p = ?

Transitividade

Uma relação é transitiva se, para todos os elementos p, q, e r em seu domínio, se p é equivalente a q e q é equivalente a r, então p é equivalente a r. Isso pode ser provado com a seguinte regra:

Equivalence.chain <p> <q> <r> (e0: Equivalence p q) (e1: Equivalence q r) : Equivalence p r
Equivalence.chain p q r e0 e1 = ?

Or_distributes_over_and

Or_distributes_over_and <p> <q> <r> : Equivalence (Either p (Pair q r)) (Pair (Either p q) (Either p r))
Or_distributes_over_and p q r = ?

Equivalência de forma especial, evitando a necessidade de alguma manipulação de estado de prova de baixo nível. Em particular, rewrite e reflexividade podem ser usados com afirmações iff, não apenas igualdades. Aqui está um exemplo simples demonstrando como essas táticas funcionam com iff. Primeiro, vamos provar algumas equivalências básicas de iff

Mult_0 (n: Nat) (m: Nat) : Equivalence (Equal Nat (Mult n m) 0n) (Either (Equal Nat n 0n) (Equal Nat m 0n))
Mult_0 n m = Equivalence.new (x => To_mult_0 n m x) (y => Or_example n m y)

To_mult_0 (n: Nat) (m: Nat) (e: Equal Nat (Mult n m) 0n) : (Either (Equal Nat n 0n) (Equal Nat m 0n))
To_mult_0 Nat.zero Nat.zero Equal.refl = Either.right Equal.refl
To_mult_0 Nat.zero (Nat.succ m) Equal.refl = Either.left Equal.refl
To_mult_0 (Nat.succ n) Nat.zero e = Either.right Equal.refl
To_mult_0 (Nat.succ n) (Nat.succ m) e = 
  let a = Plus_comm (Mult n (Nat.succ m)) (Nat.succ m)
  let b = Equal.chain (Equal.mirror e) a
  let c = (Equal.rewrite b
   (x => match Nat x {
    zero => Unit
    succ => Empty
    })
    (Unit.new)) 
  Empty.absurd c

Or_assoc <p> <q> <r> : Equivalence (Either p (Either q r)) (Either (Either p q) r)
Or_assoc = Equivalence.new (x => To_or_assoc x) (y => Fro_or_assoc y)

To_or_assoc <p> <q> <r> (e: Either p (Either q r)) : Either (Either p q) r
To_or_assoc (Either.left e) = Either.left (Either.left e)
To_or_assoc (Either.right p (Either q r) (Either.left e)) = Either.left (Either.right e)
To_or_assoc (Either.right p (Either q r) (Either.right e)) = Either.right e

Fro_or_assoc <p> <q> <r> (e: Either (Either p q) r) : Either p (Either q r)
Fro_or_assoc (Either.left (Either p q) r (Either.left e)) = Either.left e
Fro_or_assoc (Either.left (Either p q) r (Either.right e)) = Either.right (Either.left e)
Fro_or_assoc (Either.right (Either p q) r e) = Either.right (Either.right e)

Agora podemos usar esses fatos com Equal.rewrite e Equal.refl para fornecer provas suaves de afirmações envolvendo equivalências. Aqui está uma versão ternária do resultado anterior de Mult_0:

Mult_0_3 (n: Nat) (m: Nat) (p: Nat) : Equivalence (Equal Nat (Mult n (Mult m p)) 0n) (Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n)))
Mult_0_3 n m p = Equivalence.new (x => To_mult_0_3 n m p x) (y => Fro_mult_0_3 n m p y)

To_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: (Equal Nat (Nat.mul n (Nat.mul m p)) 0n)) : (Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n)))
To_mult_0_3 n m p e = Either.swap (Equivalence.rgt (Or_assoc (Equal m 0n) (Equal p 0n) (Equal n 0n)))

Fro_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n))) : (Equal Nat (Mult n (Mult m p)) 0n)
Fro_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n))) : (Equal Nat (Nat.mul n (Nat.mul m p)) 0n)
Fro_mult_0_3 Nat.zero m p (Either.left Equal.refl) = Equal.refl
Fro_mult_0_3 n Nat.zero p (Either.right a (Either b c) (Either.left Equal.refl)) = Mult_comm 0n n
Fro_mult_0_3 n m Nat.zero (Either.right a (Either b c) (Either.right Equal.refl)) = Equal.chain (Mult_assoc n m 0n) (Mult_0_r (Nat.mul n m))
Fro_mult_0_3 (Nat.succ n) m p (Either.left e) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p
Fro_mult_0_3 n (Nat.succ m) p (Either.right a (Either b c) (Either.left e)) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p
Fro_mult_0_3 n m (Nat.succ p) (Either.right a (Either b c) (Either.right e)) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p

A tática apply também pode ser usada com equivalência. Quando recebe uma equivalência como seu argumento, o apply tenta adivinhar em qual lado da equivalência usar.

Apply_iff_example (n: Nat) (m: Nat) (e: Equal Nat (Mult n m) 0n) : Either (Equal Nat n 0n) (Equal Nat m 0n) 
Apply_iff_example n m e = Equivalence.rgt (Mult_0 n m)

Quantificação Existencial

Outro importante conectivo lógico é a quantificação existencial. Para dizer que há algum x do tipo Type tal que alguma propriedade p é verdadeira para x, escrevemos (Sigma x p).

record Sigma (x: Type) (p: x -> Type) {
  fst : x
  snd : (p fst)
}

• Atualmente, o Kind-lang tem bug compilador que está afetando a aplicação lambda do Sigma.

Para provar uma afirmação da forma (Sigma x p), devemos mostrar que p é verdadeira para alguma escolha específica de valor para x, conhecido como testemunho do existencial. Isso é feito em duas etapas: Primeiro, explicitamente informamos ao Kind qual testemunho x temos em mente escrevendo-o no primeiro parâmetro. Então, provamos que p é verdadeira depois que todas as ocorrências de x são substituídas por Type.

Four_is_even : Sigma Nat (n => (Equal Nat 4n (Nat.add n n)))
Four_is_even = $ 2n Equal.refl

Por outro lado, se temos uma hipótese existencial (Sigma x p) no contexto, podemos fazer um pattern match nela para obter um testemunho x e uma hipótese afirmando que p é verdadeira para x.

Exists_example_2 (n: Nat) (m: Sigma Nat (m => (Equal Nat n (Nat.add 4n m)))) : Sigma Nat (o => (Equal Nat n (Nat.add 2n o)))
Exists_example_2 n (Sigma.new Nat s fst snd) = Sigma.new fst ?

Dist_not_exists

Prove que "p é verdadeira para todos os x" implica "não há x para o qual p não seja verdadeira".

Dist_not_exists <a> <p: a -> Type> (f: (x: a) -> (p x)) : Not (Sigma a (x => ( Not (p x))))
Dist_not_exists a p f = ?

Dist_exists_or

Prove que a quantificação existencial distribui-se sobre a disjunção.

Dist_exists_or <a> <p: a -> Type> <q: a -> Type> : Equivalence (Sigma a (x => (Either (p x) (q x)))) (Either (Sigma a (x => (p x))) (Sigma a (x => (q x))))
Dist_exists_or a p q = ?dist_exists_or_rhs

Programação com proposições

As conectivas lógicas que vimos fornecem um vocabulário rico para definir proposições complexas a partir de proposições mais simples. Para ilustrar, vamos ver como expressar a afirmação de que um elemento x ocorre em uma lista l. Observe que essa propriedade tem uma estrutura recursiva simples:

• Se l for a lista vazia, então x não pode ocorrer nela, portanto, a propriedade "x aparece em l" é simplesmente falsa.
• Caso contrário, l tem a forma List.cons xh xt. Nesse caso, x ocorre em l se ele é igual a xh ou se ocorre em xt.

Podemos traduzir isso diretamente em uma função recursiva simples que recebe um elemento e uma lista e retorna uma proposição:

In <a> (x: a) (l: List a)    : Type
In a x List.nil              = Empty
In a x (List.cons head tail) = Either (Equal a x head) (In a x tail) 

Quando In é aplicado a uma lista concreta, ele se expande em uma sequência concreta de disjunções aninhadas.

In_example_1 : In 4n [1n, 2n, 3n, 4n, 5n]
In_example_1 = (Either.right (Either.right (Either.right (Either.left Equal.refl))))

In_example_2 (n: Nat) (i: In n [2n, 4n]) : Sigma Nat (m => Equal Nat n (Nat.mul 2n m))
In_example_2 n (Either.left e)                                  = $ 1n e
In_example_2 n (Either.right l (Either rl rr) (Either.left e))  = $ 2n e
In_example_2 n (Either.right l (Either rl rr) (Either.right e)) = Empty.absurd e

Também podemos provar lemas mais genéricos e de nível superior sobre In. Observe, no próximo exemplo, como In começa sendo aplicado a uma variável e só é expandido quando fazemos análise de casos nessa variável:

In_map <a> <b> (f: a -> b) (l: List a) (x: a) (i: In x l) : In (f x) (List.map l f) 
In_map a b f (List.nil) x i = Empty.absurd i
In_map a b f (List.cons head tail) x (Either.right e) = Either.right (In_map f tail x e)
In_map a b f (List.cons head tail) x (Either.left e)  = 
    (Equal.rewrite e 
    (y => (Either (Equal (f x) (f y)) (In (f x) (List.map tail f)))) 
    (Either.left Equal.refl))

Essa forma de definir proposições recursivamente, embora conveniente em alguns casos, também tem algumas desvantagens. Em particular, está sujeita às restrições usuais do Kind em relação à definição de funções recursivas, por exemplo, o requisito de que elas sejam "obviamente terminantes". No próximo capítulo, veremos como definir proposições indutivamente, uma técnica diferente com seu próprio conjunto de pontos fortes e limitações.

In_map_equiv

In_map_equiv <a> <b> (f: a -> b) (l: List a) (y: b) :
   Equivalence (In y (List.map l f)) (Sigma a (x => (Pair (Equal (f x) y) (In x l))))
In_map_equiv a b f l y = ?

In_app_equiv

In_app_equiv <a> (x: a) (l1: List a) (l2: List a) :
  (Equivalence (In x (List.concat l1 l2)) (Either (In x l1) (In x l2)))
In_app_equiv a x l1 l2 = ?

All

Lembre-se de que funções que retornam proposições podem ser vistas como propriedades de seus argumentos. Por exemplo, se p tem o tipo Nat -> Type, então p n afirma que a propriedade p é verdadeira para n.

Inspirado em In, escreva uma função recursiva All afirmando que alguma propriedade p é verdadeira para todos os elementos de uma lista l. Para garantir que sua definição esteja correta, prove o lema All_In abaixo. (É claro que sua definição não deve apenas repetir o lado esquerdo de All_In.)

All <t> (p: t -> Type) (l: List t)  : Type
All t p l = ?

All_in <t> (p: t -> Type) (l: List t) : Equivalence ((x: t) -> (i: In x l) -> p x) (All p l)
All_in t p l = ?

Combine_odd_even

Complete a definição da função combine_odd_even abaixo. Ela recebe como argumentos duas propriedades de números, podd e peven, e deve retornar uma propriedade p tal que p n é equivalente a podd n quando n é ímpar e equivalente a peven n caso contrário.

Combine_odd_even (podd: Nat -> Type) (peven: Nat -> Type) : Nat -> Type
Combine_odd_even podd peven = ?

Para testar sua definição, prove os seguintes teoremas:

Combine_odd_even_intro
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p1: (Equal (Nat.is_odd n) Bool.true)  -> podd  n)
  (p2: (Equal (Nat.is_odd n) Bool.false) -> peven n) : (Combine_odd_even (podd) (peven)) n
Combine_odd_even_intro n podd peven p1 p2 = ?

Combine_odd_even_elim_odd
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.true) : podd n
Combine_odd_even_elim_odd n podd peven p e = ?

Combine_odd_elim_even
  (n: Nat)
  (podd: Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.false) : peven n
Combine_odd_elim_even n podd peven p e = ?

Aplicando Teoremas a Argumentos

Uma característica do Kind que o distingue de muitos outros assistentes de prova é que ele trata provas como objetos de primeira classe.

Há muito a ser dito sobre isso, mas não é necessário entender em detalhes para usar o Kind. Esta seção oferece apenas uma amostra, enquanto uma exploração mais profunda pode ser encontrada no capítulo ProofObjects.

Vimos que podemos usar o comando check para pedir ao Kind que imprima o tipo de uma expressão. Também podemos usar check para perguntar a qual teorema um identificador particular se refere.

PlusCommutative (m: Nat) (n: Nat) : Equal (Nat.add n m) (Nat.add m n)
PlusCommutative m n = ?

Kind imprime a declaração do teorema plusCommutative da mesma forma que imprime o tipo de qualquer termo que pedimos para verificar. Por quê?

A razão é que o identificador plusCommutative se refere na verdade a um objeto de prova - uma estrutura de dados que representa uma derivação lógica estabelecendo a verdade da declaração (n: Nat) (m: Nat) : n + m = m + n. O tipo desse objeto é a declaração do teorema do qual é uma prova. Intuitivamente, isso faz sentido porque a declaração de um teorema nos diz para que podemos usá-lo, assim como o tipo de um objeto computacional nos diz o que podemos fazer com esse objeto - por exemplo, se temos um termo do tipo Nat -> Nat -> Nat, podemos dar a ele dois Nats como argumentos e obter um Nat de volta. Da mesma forma, se temos um objeto do tipo n = m -> n + n = m + m e fornecemos a ele um "argumento" do tipo n = m, podemos derivar n + n = m + m. Operacionalmente, essa analogia vai ainda mais longe: aplicando um teorema, como se fosse uma função, a hipóteses com tipos correspondentes, podemos especializar seu resultado sem ter que recorrer a afirmações intermediárias. Por exemplo, suponha que quiséssemos provar o seguinte resultado:

Plus_comm3a: (n: Nat) (m: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)

À primeira vista, parece que deveríamos ser capazes de provar isso abrindo os casos, pra caso zero e succ _, mas isso nos daria um trabalho desnecessário. Vejamos um exemplo:

Plus_comm3a Nat.zero n p = ?

Nesse caso, o nosso objetivo é provar:

(Equal _ (Nat.add n p) (Nat.add (Nat.add p 0n) n)) 

Mas veja, para isso nós precisamos de outra prova, a de que

Equal Nat (Nat.add p 0n) p

Para resolver essa prova seria esse o caminho:

Add_n_z (n: Nat)       : (Equal (Nat.add n Nat.zero) n)
Add_n_z Nat.zero       = Equal.refl
Add_n_z (Nat.succ n)   =
     let ind = Add_n_z n
     let app = (Equal.apply (x => (Nat.succ x)) ind)
     app

Agora vamos provar:

Plus_comm3a (n: Nat) (m: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3a Nat.zero n p = 
  let pzr = Add_z_r p
  let com = Plus_comm n p
  let rwt = Equal.rewrite (Equal.mirror pzr) (x =>(Equal _ (Nat.add n p) (Nat.add (x) n))) com
  rwt

Agora só nos resta provar para o caso de Nat.succ n

Plus_comm3a (Nat.succ m) n p = ?

e o nosso objetivo é (Equal _ (Nat.succ (Nat.add m (Nat.add n p))) (Nat.add (Nat.add p n) (Nat.succ m))) e para isso precisaríamos de outras provas, como a que

Plus_n_sm (n: Nat) (m: Nat) : (Equal Nat (Nat.succ (Nat.add n m))(Nat.add n (Nat.succ m)))
Plus_n_sm Nat.zero m        = Equal.refl
Plus_n_sm (Nat.succ n) m    = (Equal.apply (x => (Nat.succ x)) (Plus_n_sm n m))

E reescrever na prova da comutatividade da adição entre n e p e depois usar a prova da comutatividade para isso tudo, um trabalho cansativo e, posso dizer, desnecessário.

Ao invés de abrir os casos, vamos trabalhar com eles como variáveis puras, quase sem valor

Plus_comm3 (m: Nat) (n: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3 m n p = ?

Nosso objetivo continua sendo (Equal _ (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)) e para entender isso, vamos analisar o nosso problema e os próximos passos serão triviais demais:

• n + (m + p) = (p + m) + n

Isso é exatamente a comutatividade da adição, então basta reescrever a nossa prova Plus_comm duas vezes, uma dentro da outra

let a = Equal.rewrite (Plus_comm p m) (x => (Equal (Nat.add n (Nat.add m p)) (Nat.add (x) n))) (Plus_comm3 m n p)

e veja o que nossa variável a retorna

(Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (Nat.add m p) n))

Estamos quase lá, basta apenas reescrever o segundo Plus_comm na adição mais interna do lado direito

let b = Equal.rewrite (Plus_comm m p) (x => (Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (x) n))) a

e o nosso b é exatamente igual ao nosso objetivo

(Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)) 

A prova completa fica:

Plus_comm3 (m: Nat) (n: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3 m n p = 
  let a = Equal.rewrite (Plus_comm p m) (x => (Equal (Nat.add n (Nat.add m p)) (Nat.add (x) n))) (Plus_comm3 m n p)
  let b = Equal.rewrite (Plus_comm m p) (x => (Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (x) n))) a
  b

Muito mais simples e elegante, não precisava de tanto trabalho, uma breve leitura do problema praticamente já nos entregava a solução. Perceba, isso não foi diferente de tudo o que já fizemos até aqui, é até uma repetição dos passos anteriores, é semelhante à aplicação de uma função polimórfica a um argumento de tipo.

Você pode "usar teoremas como funções" desta maneira com quase todas as táticas que recebem um nome de teorema como argumento. Note também que a aplicação de teorema usa os mesmos mecanismos de inferência que a aplicação de função; portanto, é possível, por exemplo, fornecer wildcards como argumentos a serem inferidos, ou declarar algumas hipóteses de um teorema como implícitas por padrão. Esses recursos são ilustrados na prova abaixo.

Kind vs Teoria dos Conjuntos

O núcleo lógico do Coq, o Cálculo das Construções Indutivas, difere de algumas maneiras importantes de outros sistemas formais que são usados pelos matemáticos para escrever provas precisas e rigorosas. Por exemplo, na fundação mais popular para a matemática em papel e lápis convencional, a Teoria dos Conjuntos de Zermelo-Fraenkel (ZFC), um objeto matemático pode potencialmente ser membro de muitos conjuntos diferentes; um termo na lógica de Kind, por outro lado, é membro de no máximo um tipo. Essa diferença muitas vezes leva a formas ligeiramente diferentes de capturar conceitos matemáticos informais, mas estes são, em grande parte, bastante naturais e fáceis de trabalhar. Por exemplo, em vez de dizer que um número natural n pertence ao conjunto de números pares, diríamos em Kind que ev n é verdadeiro, onde ev: Nat -> Tipo é uma propriedade que descreve os números pares.

No entanto, há alguns casos em que traduzir o raciocínio matemático padrão para Kind pode ser tanto trabalhoso quanto, às vezes, até impossível, a menos que enriqueçamos a lógica central com axiomas adicionais. Concluímos este capítulo com uma breve discussão de algumas das diferenças mais significativas entre os dois mundos.

Extensão Funcional.

As afirmações de igualdade que vimos até agora dizem principalmente respeito a elementos de tipos indutivos (Nat, Bool, etc.). Mas como o operador de igualdade de Kind é polimórfico, essas não são as únicas possibilidades - em particular, podemos escrever proposições que afirmam que duas funções são iguais uma à outra:

#![allow(unused)]
fn main() {
Function_equality_ex1 : Equal (Nat.succ 3n) (Nat.succ (Nat.pred 4n))
Function_equality_ex1 = Equal.refl
}

Na prática matemática comum, duas funções f e g são consideradas iguais se produzem as mesmas saídas:

(∀𝑥, 𝑓(𝑥) = 𝑔(𝑥)) → 𝑓 = 𝑔

Isto é conhecido como o princípio da extensão funcional.

De forma informal, uma "propriedade extensional" é aquela que diz respeito ao comportamento observável de um objeto. Assim, a extensão funcional significa simplesmente que a identidade de uma função é completamente determinada pelo que podemos observar a partir dela - isto é, em termos de Kind, os resultados que obtemos após aplicá-la.

A extensão funcional não faz parte dos axiomas básicos do Kind. Isso significa que algumas proposições "razoáveis" não são prováveis.

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 = ?
}

No entanto, podemos declarar um teorema e pular a sua prova ou usar um buraco

#![allow(unused)]
fn main() {
Functional_extensionality <a><b> (f: a -> b) (g: a -> b) (e: (x: a) -> Equal (f x) (g x)) : Equal f g
}

Agora podemos invocar a extensionalidade funcional em provas:

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 =
  Functional_extensionality ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x) (x => Plus_comm x 1n)
}

Naturalmente, devemos ter cuidado ao adicionar novos axiomas à lógica do Kind, pois eles podem torná-la inconsistente - ou seja, podem tornar possível provar todas as proposições, incluindo Void!

Infelizmente, não há uma maneira simples de saber se um axioma é seguro para adicionar: geralmente é necessário um trabalho árduo para estabelecer a consistência de qualquer combinação particular de axiomas.

No entanto, sabe-se que adicionar a extensionalidade funcional, em particular, é consistente.

Tr_rev

Um problema com a definição da função de reversão de lista "rev" que temos é que ela realiza uma chamada a "++" a cada passo. Executar "++" leva tempo assintoticamente linear no tamanho da lista, o que significa que "rev" tem tempo de execução quadrático. Podemos melhorar isso com a seguinte definição:

#![allow(unused)]
fn main() {
Rev_append <x> (l1: List x) (l2: List x)  : List x
Rev_append x List.nil l2                  = l2
Rev_append x (List.cons xs.h xs.t) l2     = Rev_append xs.t (List.cons xs.h l2)

Tr_rev <x> (l: List x) : List x
Tr_rev x l = Rev_append x l List.nil1
}

Esta versão é dita ser tail-recursive, porque a chamada recursiva à função é a última operação que precisa ser executada (ou seja, não precisamos executar ++ após a chamada recursiva); um compilador decente irá gerar um código muito eficiente neste caso. Prove que as duas definições são realmente equivalentes.

#![allow(unused)]
fn main() {
Tr_rev_correct <a> (xs: List a) : Equal (Tr_rev xs) (Rev xs)
Tr_rev_correct a xs = ?
}

Proposições e Booleans.

Vimos duas maneiras diferentes de codificar fatos lógicos em Kind: com booleanos (do tipo Bool) e com proposições (do tipo Type). Por exemplo, para afirmar que um número n é par, podemos dizer que • (1) evenb n retorna True, ou • (2) existe um k tal que n = double k. De fato, essas duas noções de paridade são equivalentes, como pode ser facilmente mostrado com um par de lemas auxiliares. Muitas vezes dizemos que o booleano evenb n reflete a proposição (n => Equal n (double k)).

#![allow(unused)]
fn main() {
Evenb_double (k: Nat)     : Equal (Nat.is_even (Nat.double k)) Bool.true
Evenb_double Nat.zero     = Equal.refl
Evenb_double (Nat.succ k) = Evenb_double k
}

Evenb_double_conv

#![allow(unused)]
fn main() {
Evenb_double_conv (n: Nat):
  Sigma Nat (k => (Equal n (Bool.if (Evenb n) (Nat.double k) (Nat.succ (Nat.double k)))))
Evenb_double_conv n = ?
}

TODO: terminar even_bool_prop

#![allow(unused)]
fn main() {
Even_bool_prop (n: Nat): 
  Equivalence (Equal (Evenb n) Bool.true) (Sigma Nat (k => Equal n (Nat.double k)))
}

Da mesma forma, para afirmar que dois números n e m são iguais, podemos dizer (1) que n == m retorna Bool.true ou (2) que n = m. Essas duas noções são equivalentes.

#![allow(unused)]
fn main() {
Beq_nat_true_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.true) (Equal n1 n2)
Beq_nat_true_equiv n1 n2 = Equivalence.new (x => To_beq_nat_true n1 n2 x) (y => Fro_beq_nat_true n1 n2 y)

To_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2  
To_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
To_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)

Fro_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal  n1 n2) : Equal (Nat.equal n1 n2) Bool.true
Fro_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
Fro_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Unit
      succ => Empty
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Empty
      succ => Unit
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) (Nat.succ n2) e =
  let e2  = Succ_n1_n2 n1 n2 e
  let ind = Fro_beq_nat_true n1 n2 e2
  ind

  Succ_n1_n2 (n1: Nat) (n2: Nat) (e : (Equal Nat (Nat.succ n1) (Nat.succ n2))) : Equal Nat n1 n2
Succ_n1_n2 Nat.zero Nat.zero e            = Equal.refl
Succ_n1_n2 (Nat.succ n1) Nat.zero e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 Nat.zero (Nat.succ n2) e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 (Nat.succ n1) (Nat.succ n2) e  = Equal.apply (x => Nat.pred x) e

Extract_equal (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2
Extract_equal Nat.zero Nat.zero (Equal.refl) = Equal.refl
Extract_equal Nat.zero (Nat.succ n2) (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) Nat.zero (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)
}

No entanto, enquanto as formulações booleanas e proposicionais de uma afirmação são equivalentes do ponto de vista puramente lógico, elas não precisam ser equivalentes operacionalmente. A igualdade fornece um exemplo extremo: saber que n == m = Verdadeiro geralmente é de pouca ajuda direta no meio de uma prova envolvendo n e m; no entanto, se convertermos a declaração para a forma equivalente n = m, podemos reescrevê-la.

O caso dos números pares também é interessante. Lembre-se de que, ao provar a direção inversa de even_bool_prop (ou seja, evenb_double, indo da afirmação proposicional para a booleana), usamos uma indução simples em k. Por outro lado, a conversa (o exercício evenb_double_conv) exigiu uma generalização inteligente, uma vez que não podemos provar diretamente (k => Equal n (Nat.double k)) = Bool.true

Para esses exemplos, as afirmações proposicionais são mais úteis do que suas contrapartes booleanas, mas nem sempre é o caso. Por exemplo, não podemos testar se uma proposição geral é verdadeira ou não em uma definição de função; como consequência, o seguinte trecho de código é rejeitado:

#![allow(unused)]
fn main() {
Is_even_prime : Nat -> Bool
Is_even_prime = (n: Nat) => Bool.if (Equal n 2n) Bool.true Bool.false
}

O Kind reclama que n = 2 tem o tipo Type, enquanto espera um elemento de Bool (ou algum outro tipo indutivo com dois elementos). A razão para esta mensagem de erro tem a ver com a natureza computacional da linguagem central de Kind, que é projetada de forma que cada função que ela possa expressar seja computável e total. Uma razão para isso é permitir a extração de programas executáveis a partir dos desenvolvimentos de Kind. Como consequência, em Kind, Type não tem uma operação de análise de caso universal que diga se uma dada proposição é verdadeira ou falsa, já que tal operação permitiria escrever funções não computáveis.

Embora propriedades gerais não computáveis não possam ser formuladas como computações booleanas, vale ressaltar que muitas propriedades computáveis ​​são mais fáceis de expressar usando Type do que Bool, já que definições de funções recursivas estão sujeitas a restrições significativas em Kind. Por exemplo, o próximo capítulo mostra como definir a propriedade de que uma expressão regular corresponde a uma determinada string usando Type. Fazer o mesmo com Bool seria equivalente a escrever um verificador de expressão regular, o que seria mais complicado, mais difícil de entender e mais difícil de raciocinar.

Por outro lado, um importante benefício adicional de afirmar fatos usando booleanos é habilitar alguma automação de prova por meio de computação com termos em Kind, uma técnica conhecida como prova por reflexão. Considere a seguinte afirmação:

#![allow(unused)]
fn main() {
Even_1000 : Sigma Nat (k => Equal 1000n (Nat.double k))
}

A prova mais direta desse fato é fornecer o valor de k explicitamente.

#![allow(unused)]
fn main() {
Even_1000 = $ 500n Equal.refl
}

Por outro lado, a prova da correspondente afirmação booleana é ainda mais simples:

#![allow(unused)]
fn main() {
Even_1000a : Equal (Evenb 1000n) Bool.true
Even_1000a = Equal.refl
}

O interessante é que, como as duas noções são equivalentes, podemos usar a formulação booleana para provar a outra sem mencionar explicitamente o valor 500:

#![allow(unused)]
fn main() {
Even_1000b : Sigma Nat (k => Equal 1000n (Nat.double k))
Even_1000b = ? //TODO: Terminar aqui
}

Embora não tenhamos ganhado muito em termos de tamanho de prova neste caso, provas maiores podem ser consideravelmente simplificadas pelo uso da reflexão. Como um exemplo extremo, a prova do teorema dos 4 cores em Coq usa reflexão para reduzir a análise de centenas de casos diferentes a uma computação booleana. Não abordaremos a reflexão em grande detalhe, mas ela serve como um bom exemplo que mostra as forças complementares dos booleanos e proposições gerais.

Logical_connectives

Os seguintes lemas relacionam os conectivos proposicionais estudados neste capítulo com as operações booleanas correspondentes.

#![allow(unused)]
fn main() {
Andb_true_equiv 
  (b1: Bool) 
  (b2: Bool) : Equivalence (Equal (Bool.and b1 b2) Bool.true) (Pair (Equal b1 Bool.true) (Equal b2 Bool.true))
Andb_true_equiv b1 b2 = ?


Orb_true_equiv 
  (b1: Bool) 
  (b2: Bool): Equivalence (Equal (Bool.or b1 b2) Bool.true) (Either (Equal b1 Bool.true) (Equal b2 Bool.true))
Orb_true_equiv b1 b2 = ?
}

Beq_nat_false_equiv

O teorema a seguir é uma formulação alternativa "negativa" de beq_nat_true_equiv que é mais conveniente em certas situações (veremos exemplos em capítulos posteriores).

#![allow(unused)]
fn main() {
Beq_nat_false_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.false) (Not (Equal n1 n2))
Beq_nat_false_equiv n1 n2 = ?
}

Beq_list

Dado um operador booleano beq para testar a igualdade de elementos de algum tipo a, podemos definir uma função beq_list beq para testar a igualdade de listas com elementos em a. Complete a definição da função beq_list abaixo. Para garantir que sua definição está correta, prove o lema beq_list_true_equiv.

#![allow(unused)]
fn main() {
Beq_list <a> (beq: a -> a -> Bool) (xs: List a) (ys: List a) : Bool
Beq_list a beq  xs ys = ?

Beq_list_true_equiv <a> 
  (beq: a -> a -> Bool) 
  (a1: a) 
  (a2: a) 
  (e: Equivalence (Equal (beq a1 a2) Bool.true) (Equal a1 a2))
  (xs: List a)
  (ys: List a): Equivalence (Equal (Beq_list beq xs ys) Bool.true) (Equal xs ys)
Beq_list_true_equiv a beq a1 a2 e xs ys = ?
}

All_forallb

#![allow(unused)]
fn main() {
Forallb <x> (t: x -> Bool) (xs: List x) : Bool
Forallb x t List.nil = Bool.true
Forallb x t (List.cons xs.h xs.t) = Bool.and (t xs.h) (Forallb t xs.t)

}

Prove o teorema abaixo, que relaciona forallb à propriedade All do exercício acima.

#![allow(unused)]
fn main() {
Forallb_true_equiv <x> 
  (t: x -> Bool) 
  (xs: List x) : 
  Equivalence (Equal (Forallb t xs) Bool.true) ((All ((k: x) => Equal (t k) Bool.true) xs))
Forallb_true_equiv x t xs = ?
}

Existem alguma propriedades importantes da função forallb que não são capturadas por esta especificação?

Lógica Clássica vs. Lógica Construtiva.

Vimos que não é possível testar se uma proposição p é verdadeira ou não ao definir uma função Kind. Você pode se surpreender ao descobrir que uma restrição semelhante se aplica às provas! Em outras palavras, o seguinte princípio de raciocínio intuitivo não é derivável em Kind:

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
}

Para entender operacionalmente por que esse é o caso, lembre-se de que, para provar uma declaração da forma Either p q, usamos as correspondências de padrão Left e Right, que exigem saber qual lado da disjunção é verdadeiro. Mas a proposição p universalmente quantificada em Excluded_middle é uma proposição arbitrária, sobre a qual não sabemos nada. Não temos informações suficientes para escolher qual de Left ou Right aplicar, assim como Kind não tem informações suficientes para decidir mecanicamente se p é verdadeira ou não dentro de uma função.

No entanto, se soubermos que p é refletida em algum termo booleano b, saber se ela é verdadeira ou não é trivial: basta verificar o valor de b.

#![allow(unused)]
fn main() {
Restricted_excluded_middle <p> <q> (b: Bool)(e: Equivalence p (Equal b Bool.true)) : Either p (Not p) 
Restricted_excluded_middle p q Bool.true  (Equivalence.new pb bp) = Either.left (bp Equal.refl)
Restricted_excluded_middle p q Bool.false (Equivalence.new pb bp) = Either.right (Empty.absurd (Not_implies_our_not pb))
}

Em particular, o terceiro excluído é válido para equações n = m, entre números naturais n e m.

#![allow(unused)]
fn main() {
//TODO: Terminar aqui
Restricted_excluded_middle_eq (n: Nat) (m: Nat) : Either (Equal n m) (Not (Equal n m))
Restricted_excluded_middle_eq n m = ?

To_reme (n: Nat) (m: Nat) (e: Equal n m) : Equal (Nat.equal n m) Bool.true
To_reme Nat.zero Nat.zero e         = Equal.refl
To_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) (Nat.succ m) e = To_reme n m (Succ_injective n m e)

From_reme (n: Nat) (m: Nat) (e: Equal (Nat.equal n m) Bool.true) : Equal n m
From_reme Nat.zero Nat.zero e         = Equal.refl
From_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) (Nat.succ m) e = Equal.apply (x => Nat.succ x) (From_reme n m e)
}

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão.

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão. Notavelmente, se houver uma prova no Kind de (Sigma a (x => (p x))), é possível exibir explicitamente um valor de x para o qual podemos provar p x - em outras palavras, toda prova de existência é necessariamente construtiva. Lógicas como a do Kind, que não assumem o princípio do terceiro excluído, são referidas como lógicas construtivas. Sistemas lógicos mais convencionais, como o ZFC, nos quais o princípio do terceiro excluído é válido para proposições arbitrárias, são referidos como clássicos.

O exemplo a seguir ilustra por que assumir o princípio do terceiro excluído pode levar a provas não construtivas:

Afirmação: Existem números irracionais a e b, tais que a^b é racional.

Prova: Não é difícil mostrar que a raiz quadrada de 2 é irracional. Se a raiz quadrada de 2 ^ raiz quadrada de 2 é racional, basta tomar a = b = raiz quadrada de 2 e estamos prontos. Caso contrário, se a raiz quadrada de 2 ^ raiz quadrada de 2 for irracional, podemos tomar a = raiz quadrada de 2 ^ raiz quadrada de 2 e b = raiz quadrada de 2, já que a ^ b = raiz quadrada de 2 ^ (raiz quadrada de 2 * raiz quadrada de 2) = raiz quadrada de 2 ^ 2 = 2.

Você percebeu o que aconteceu aqui? Usamos o princípio do terceiro excluído para considerar separadamente os casos em que a raiz quadrada de 2 ^ raiz quadrada de 2 é racional e onde não é, sem saber qual deles é verdadeiro! Por causa disso, sabemos que tais a e b existem, mas não podemos determinar quais são seus valores reais (pelo menos, usando essa linha de argumento).

Por útil que seja a lógica construtiva, ela tem suas limitações: há muitas declarações que podem ser facilmente provadas na lógica clássica, mas que têm provas construtivas muito mais complicadas, e há algumas que não se sabe ter prova construtiva alguma! Felizmente, assim como a extensão funcionalidade, o princípio do terceiro excluído é conhecido por ser compatível com a lógica do Kind, permitindo-nos adicioná-lo com segurança como um axioma. No entanto, não precisaremos fazer isso neste livro: os resultados que cobrimos podem ser desenvolvidos inteiramente dentro da lógica construtiva a um custo extra negligenciável.

Leva um pouco de prática para entender quais técnicas de prova devem ser evitadas no raciocínio construtivo, mas os argumentos por contradição, em particular, são infames por levar a provas não construtivas. Aqui está um exemplo típico: suponha que queremos mostrar que existe um x com alguma propriedade p, isto é, tal que p x. Começamos assumindo que nossa conclusão é falsa; isto é Not (Sigma a (x => (p x))). A partir desta premissa, não é difícil deduzir (x: a) -> Not (p x). Se conseguirmos mostrar que esse fato intermediário resulta em uma contradição, chegamos a uma prova de existência sem nunca exibir um valor de x para o qual p x seja verdadeiro!

A falha técnica aqui, do ponto de vista construtivo, é que afirmamos provar Sigma a (x => (p x)) usando uma prova de Not (Not (Sigma a (x =>(p x)))). Permitir-nos remover duplas negações de afirmações arbitrárias é equivalente a assumir o terceiro excluído, como mostrado em um dos exercícios abaixo. Assim, essa linha de raciocínio não pode ser codificada em Kind sem assumir axiomas adicionais.

Excluded_middle_irrefutable

A consistência do Kind com o axioma geral do terceiro excluído requer raciocínios complicados que não podem ser realizados dentro do próprio Kind. No entanto, o seguinte teorema implica que é sempre seguro assumir um axioma de decidibilidade (ou seja, uma instância do terceiro excluído) para qualquer tipo específico p. Por quê? Porque não podemos provar a negação de tal axioma; se pudéssemos, teríamos tanto Not (Either p (Not p)) quanto Not (Not (Either p (Not p))), o que é uma contradição.

#![allow(unused)]
fn main() {
Excluded_middle_irrefutable <p> : Not (Not (Either p (Not p)))
Excluded_middle_irrefutable p = ?
}

Not_exists_dist

É um teorema da lógica clássica que as seguintes duas afirmações são equivalentes:

#![allow(unused)]
fn main() {
Not (Sigma a (k => Not (p k))))
(x : a) -> p x
}

O teorema dist_not_exists acima prova um lado dessa equivalência. Curiosamente, a outra direção não pode ser provada na lógica construtiva. Sua tarefa é mostrar que ela é implicada pelo terceiro excluído.

#![allow(unused)]
fn main() {
Not_exists_dist <a> (p: a -> Type) (s: Not (Sigma a (k => Not (p k)))) : (x: a) -> p x
Not_exists_dist a p s = ?
}

sendo que

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
// Excluded_middle p = Confia 
}

Classical_axioms

Para aqueles que gostam de um desafio, aqui está um exercício retirado do livro Coq'Art de Bertot e Casteran (p. 123). Cada uma das seguintes quatro afirmações, juntamente com excluded_middle, pode ser considerada como caracterizando a lógica clássica. Não podemos provar nenhum deles em Kind, mas podemos adicionar consistentemente qualquer um deles como um axioma se quisermos trabalhar na lógica clássica.

Prove que todas as cinco proposições (essas quatro mais excluded_middle) são equivalentes.

#![allow(unused)]
fn main() {
Peirce <p> <q>(pq: (p -> q) -> p) : p

Double_negation_elimination <p> (np: Not (Not p)) : p

De_morgan_not_not <p> <q> (np: Pair (Not p) (Not q)) : Either p q

Implies_to_or <p> <q> (pq: p -> q) : Either (Not p) q
}

Lógica Clássica vs. Lógica Construtiva

Vimos que não é possível testar se uma proposição p é verdadeira ou não ao definir uma função Kind. Você pode se surpreender ao descobrir que uma restrição semelhante se aplica às provas! Em outras palavras, o seguinte princípio de raciocínio intuitivo não é derivável em Kind:

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
}

Para entender operacionalmente por que esse é o caso, lembre-se de que, para provar uma declaração da forma Either p q, usamos as correspondências de padrão Left e Right, que exigem saber qual lado da disjunção é verdadeiro. Mas a proposição p universalmente quantificada em Excluded_middle é uma proposição arbitrária, sobre a qual não sabemos nada. Não temos informações suficientes para escolher qual de Left ou Right aplicar, assim como Kind não tem informações suficientes para decidir mecanicamente se p é verdadeira ou não dentro de uma função.

No entanto, se soubermos que p é refletida em algum termo booleano b, saber se ela é verdadeira ou não é trivial: basta verificar o valor de b.

#![allow(unused)]
fn main() {
Restricted_excluded_middle <p> <q> (b: Bool)(e: Equivalence p (Equal b Bool.true)) : Either p (Not p) 
Restricted_excluded_middle p q Bool.true  (Equivalence.new pb bp) = Either.left (bp Equal.refl)
Restricted_excluded_middle p q Bool.false (Equivalence.new pb bp) = Either.right (Empty.absurd (Not_implies_our_not pb))
}

Em particular, o terceiro excluído é válido para equações n = m, entre números naturais n e m.

#![allow(unused)]
fn main() {
//TODO: Terminar aqui
Restricted_excluded_middle_eq (n: Nat) (m: Nat) : Either (Equal n m) (Not (Equal n m))
Restricted_excluded_middle_eq n m = ?

To_reme (n: Nat) (m: Nat) (e: Equal n m) : Equal (Nat.equal n m) Bool.true
To_reme Nat.zero Nat.zero e         = Equal.refl
To_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) (Nat.succ m) e = To_reme n m (Succ_injective n m e)

From_reme (n: Nat) (m: Nat) (e: Equal (Nat.equal n m) Bool.true) : Equal n m
From_reme Nat.zero Nat.zero e         = Equal.refl
From_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) (Nat.succ m) e = Equal.apply (x => Nat.succ x) (From_reme n m e)
}

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão.

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão. Notavelmente, se houver uma prova no Kind de (Sigma a (x => (p x))), é possível exibir explicitamente um valor de x para o qual podemos provar p x - em outras palavras, toda prova de existência é necessariamente construtiva. Lógicas como a do Kind, que não assumem o princípio do terceiro excluído, são referidas como lógicas construtivas. Sistemas lógicos mais convencionais, como o ZFC, nos quais o princípio do terceiro excluído é válido para proposições arbitrárias, são referidos como clássicos.

O exemplo a seguir ilustra por que assumir o princípio do terceiro excluído pode levar a provas não construtivas:

Afirmação: Existem números irracionais a e b, tais que a^b é racional.

Prova: Não é difícil mostrar que a raiz quadrada de 2 é irracional. Se a raiz quadrada de 2 ^ raiz quadrada de 2 é racional, basta tomar a = b = raiz quadrada de 2 e estamos prontos. Caso contrário, se a raiz quadrada de 2 ^ raiz quadrada de 2 for irracional, podemos tomar a = raiz quadrada de 2 ^ raiz quadrada de 2 e b = raiz quadrada de 2, já que a ^ b = raiz quadrada de 2 ^ (raiz quadrada de 2 * raiz quadrada de 2) = raiz quadrada de 2 ^ 2 = 2.

Você percebeu o que aconteceu aqui? Usamos o princípio do terceiro excluído para considerar separadamente os casos em que a raiz quadrada de 2 ^ raiz quadrada de 2 é racional e onde não é, sem saber qual deles é verdadeiro! Por causa disso, sabemos que tais a e b existem, mas não podemos determinar quais são seus valores reais (pelo menos, usando essa linha de argumento).

Por útil que seja a lógica construtiva, ela tem suas limitações: há muitas declarações que podem ser facilmente provadas na lógica clássica, mas que têm provas construtivas muito mais complicadas, e há algumas que não se sabe ter prova construtiva alguma! Felizmente, assim como a extensão funcionalidade, o princípio do terceiro excluído é conhecido por ser compatível com a lógica do Kind, permitindo-nos adicioná-lo com segurança como um axioma. No entanto, não precisaremos fazer isso neste livro: os resultados que cobrimos podem ser desenvolvidos inteiramente dentro da lógica construtiva a um custo extra negligenciável.

Leva um pouco de prática para entender quais técnicas de prova devem ser evitadas no raciocínio construtivo, mas os argumentos por contradição, em particular, são infames por levar a provas não construtivas. Aqui está um exemplo típico: suponha que queremos mostrar que existe um x com alguma propriedade p, isto é, tal que p x. Começamos assumindo que nossa conclusão é falsa; isto é Not (Sigma a (x => (p x))). A partir desta premissa, não é difícil deduzir (x: a) -> Not (p x). Se conseguirmos mostrar que esse fato intermediário resulta em uma contradição, chegamos a uma prova de existência sem nunca exibir um valor de x para o qual p x seja verdadeiro!

A falha técnica aqui, do ponto de vista construtivo, é que afirmamos provar Sigma a (x => (p x)) usando uma prova de Not (Not (Sigma a (x =>(p x)))). Permitir-nos remover duplas negações de afirmações arbitrárias é equivalente a assumir o terceiro excluído, como mostrado em um dos exercícios abaixo. Assim, essa linha de raciocínio não pode ser codificada em Kind sem assumir axiomas adicionais.

Excluded_middle_irrefutable

A consistência do Kind com o axioma geral do terceiro excluído requer raciocínios complicados que não podem ser realizados dentro do próprio Kind. No entanto, o seguinte teorema implica que é sempre seguro assumir um axioma de decidibilidade (ou seja, uma instância do terceiro excluído) para qualquer tipo específico p. Por quê? Porque não podemos provar a negação de tal axioma; se pudéssemos, teríamos tanto Not (Either p (Not p)) quanto Not (Not (Either p (Not p))), o que é uma contradição.

#![allow(unused)]
fn main() {
Excluded_middle_irrefutable <p> : Not (Not (Either p (Not p)))
Excluded_middle_irrefutable p = ?
}

Not_exists_dist

É um teorema da lógica clássica que as seguintes duas afirmações são equivalentes:

#![allow(unused)]
fn main() {
Not (Sigma a (k => Not (p k))))
(x : a) -> p x
}

O teorema dist_not_exists acima prova um lado dessa equivalência. Curiosamente, a outra direção não pode ser provada na lógica construtiva. Sua tarefa é mostrar que ela é implicada pelo terceiro excluído.

#![allow(unused)]
fn main() {
Not_exists_dist <a> (p: a -> Type) (s: Not (Sigma a (k => Not (p k)))) : (x: a) -> p x
Not_exists_dist a p s = ?
}

sendo que

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
// Excluded_middle p = Confia 
}

Classical_axioms

Para aqueles que gostam de um desafio, aqui está um exercício retirado do livro Coq'Art de Bertot e Casteran (p. 123). Cada uma das seguintes quatro afirmações, juntamente com excluded_middle, pode ser considerada como caracterizando a lógica clássica. Não podemos provar nenhum deles em Kind, mas podemos adicionar consistentemente qualquer um deles como um axioma se quisermos trabalhar na lógica clássica.

Prove que todas as cinco proposições (essas quatro mais excluded_middle) são equivalentes.

#![allow(unused)]
fn main() {
Peirce <p> <q>(pq: (p -> q) -> p) : p

Double_negation_elimination <p> (np: Not (Not p)) : p

De_morgan_not_not <p> <q> (np: Pair (Not p) (Not q)) : Either p q

Implies_to_or <p> <q> (pq: p -> q) : Either (Not p) q
}

Proposições Definidas Indutivamente

No capítulo de Lógica, examinamos várias maneiras de escrever proposições, incluindo conjunção, disjunção e quantificadores. Neste capítulo, adicionamos uma nova ferramenta à mistura: definições indutivas.

Lembre-se de que vimos duas maneiras de afirmar que um número n é par: podemos dizer (1) Evenb n = Bool.true ou (2) (k => Equal n (Nat.double k)). Outra possibilidade é dizer que n é par se pudermos estabelecer sua paridade a partir das seguintes regras:

• Regra Ev_0: O número 0 é par.
• Regra Ev_SS: Se n é par, então Nat.succ (Nat.succ n) é par.

Para ilustrar como essa definição de paridade funciona, vamos imaginar usá-la para mostrar que 4 é par. Pela regra Ev_SS, basta mostrar que 2 é par. Isso, por sua vez, é garantido novamente pela regra Ev_SS, desde que possamos mostrar que 0 é par. Mas esse último fato segue diretamente da regra Ev_0.

Veremos muitas definições como esta durante o restante do curso. Para fins de discussões informais, é útil ter uma notação leve que facilite a leitura e a escrita. Regras de inferência são uma dessas notações:

$$ \frac{ }{Ev\ \ 0} \ \ ev_0 $$

$$ \frac{\ \ \ \ ev\ \ \ \ \ }{Ev\ \ (Nat.succ \ (Nat.succ \ n))} \ \ ev_SS $$

Cada uma das regras textuais acima é reformatada aqui como uma regra de inferência; a leitura pretendida é que, se as premissas acima da linha forem todas válidas, então a conclusão abaixo da linha segue. Por exemplo, a regra ev_SS diz que, se n satisfaz ev, então Nat.succ (Nat.succ n) também satisfaz. Se uma regra não tiver premissas acima da linha, então sua conclusão é válida incondicionalmente.

Podemos representar uma prova usando essas regras combinando as aplicações de regras em uma árvore de prova. Aqui está como poderíamos transcrever a prova acima de que 4 é par:

$$ \frac{ }{Ev\ \ 0} \ \ ev_0 \ \ \ \ \frac{ }{Ev\ \ 2} \ \ ev_SS \ \ \ \ \frac{ }{Ev\ \ 4} \ \ ev_SS \ \ \ \ \frac{ }{Ev\ \ 6} \ \ ev_SS \ $$

type Ev ~ (n: Nat){
  ev_0 : Ev Nat.zero
  ev_ss <n : Nat> (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
}

Essa definição é diferente em um aspecto crucial em relação aos usos anteriores de dados: seu resultado não é um Tipo, mas sim uma função de Nat para Tipo - isto é, uma propriedade dos números. Note que já vimos outras definições indutivas que resultam em funções, como List, cujo tipo é Type -> Type. O que é novo aqui é que, como o argumento Nat de Ev não tem nome e aparece à direita dos dois pontos, é permitido que ele tome valores diferentes nos tipos de diferentes construtores: Nat.zero no tipo de ev_z e Nat.succ (Nat.succ n) no tipo de ev_ss.

Por outro lado, a definição deList nomeia o parâmetro x globalmente, forçando o resultado de Nil e Cons a ser o mesmo (List x). Se tivéssemos tentado omitir o tipo n : Nat ao definir ev_ss, teríamos visto um erro:

type Wrong_ev ~ (n: Nat){
  wrong_ev_0 : Ev Nat.zero
  wrong_ev_ss (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
}

Com o seguinte retorno:

   - ERROR  Cannot find the definition 'n'.

      ┌──[ev.kind2:9:25]
      │
    8 │      wrong_ev_z : Ev Nat.zero
    9 │      wrong_ev_ss (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
      │                            ┬                           ┬
      │                            │                           └Here!
      │                            └Here!
   10 │    

("Parâmetro" aqui é jargão do Kind para um argumento à esquerda dos dois pontos em uma definição indutiva; "índice" é usado para se referir a argumentos à direita dos dois pontos.)

Podemos pensar na definição de Ev como definindo uma propriedade do Kind Ev: Nat -> Type, juntamente com os teoremas ev_z: Ev 0 e ev_ss <n : Nat> (pred: Ev n) : Ev (Nat.succ (Nat.succ n)). Tais "teoremas construtores" têm o mesmo status que teoremas provados. Em particular, podemos aplicar nomes de regras como funções umas às outras para provar Ev para números específicos...

Ev_4 : Ev 4n
Ev_4 = Ev.ev_ss 2n (Ev.ev_ss 0n Ev.ev_z)

Também podemos provar teoremas que têm hipóteses envolvendo Ev.

Ev_plus5 (n: Nat) : Ev n -> Ev (Nat.add 4n n)
Ev_plus5 n = x => Ev.ev_ss (Ev.ev_ss x)

Mais geralmente, podemos mostrar que qualquer número multiplicado por 2 é par:

Ev_double

Ev_double (n: Nat) : Ev (Nat.double n)
Ev_double n = ?

Usando evidências em provas

Além de construir evidências de que os números são pares, também podemos raciocinar sobre tais evidências. Introduzir Ev com uma declaração de dados diz ao Kind não apenas que os construtores ev_z e ev_ss são formas válidas de construir evidências de que algum número é par, mas também que esses dois construtores são as únicas maneiras de construir evidências de que os números são pares (no sentido de Ev).

Em outras palavras, se alguém nos dá uma evidência e para a afirmação Ev n, então sabemos que e deve ter uma das duas formas:

• e é ev_z (e n é Nat.zero), ou
• e é ev_ss aplicando a indução com n e ele é igual ao sucessor do sucessor do n*.

Nota: Já usamos essa estratégia antes, relembre do exercícioProblems.t3* do capítulo de indução, aqui a diferença é que há apenas um "Nat.succ" a mais na nossa indução

Isso sugere que deve ser possível analisar uma hipótese da forma Ev n da mesma forma que fazemos com estruturas de dados definidas de forma indutiva; em particular, deve ser possível argumentar por indução e análise de casos sobre essa evidência. Vamos ver alguns exemplos para ver o que isso significa na prática.

Pattern Matching nas evidências

Suponha que estamos provando algum fato envolvendo um número n e nos é dada a hipótese Ev n. Já sabemos como realizar a análise de casos em n usando a tática de inversão, gerando submetas separadas para o caso em que n = Nat.zero e o caso em que n = Nat.succ n para algum n. Mas para algumas provas, podemos querer analisar diretamente a evidência de que Ev n é verdadeiro.

Pela definição de Ev, existem dois casos a considerar:

• Se a evidência for da forma ev_z, sabemos que n = Nat.zero.
• Caso contrário, a evidência deve ter a forma ev_ss n e, onde n = Nat.succ (Nat.succ n) e e é a evidência para Ev n.

Podemos realizar esse tipo de raciocínio em Kind, novamente usando o pattern matching. Além de permitir que raciocinemos sobre igualdades envolvendo construtores, a inversão fornece um princípio de análise de casos para proposições definidas de forma indutiva.

Ev_minus2 (n: Nat) (e: Ev n) : Ev (Nat.pred (Nat.pred n))
Ev_minus2 Nat.zero e = e
Ev_minus2 (Nat.succ Nat.zero) e = Ev.ev_z
Ev_minus2 (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = e

Em palavras, aqui está como o raciocínio de pattern matching funciona nesta prova:

• Se a evidência for da forma ev_z, sabemos que n = Nat.zero. Portanto, é suficiente mostrar que Ev (Nat.pred (Nat.pred Nat.zero)) é válido. Pela definição de Nat.pred, isso é equivalente a mostrar que Ev Z é válido, o que segue diretamente de ev_0.
• Caso contrário, a evidência deve ter a forma ev_ss n e, onde n = Nat.succ (Nat.succ n) e e é a evidência para Ev n. Devemos então mostrar que Ev (Nat.pred (Nat.pred (Nat.succ (Nat.succ n)))) é válido, o que, após simplificação, segue diretamente de e.

Suponha que quiséssemos provar a seguinte variação de Ev_minus2:

Evss_ev (n: Nat) (e: Ev (Nat.succ (Nat.succ n))) : Ev n

Intuitivamente, sabemos que a evidência para a hipótese não pode consistir apenas do construtor ev_z, uma vez que Nat.zero e Nat.succ são construtores diferentes do tipo Nat; portanto, ev_ss é o único caso que se aplica. Infelizmente, o pattern matching não é inteligente o suficiente para perceber isso e ainda gera duas submetas. Ainda pior, ao fazê-lo, mantém a meta final inalterada, deixando de fornecer qualquer informação útil para completar a prova.

A tática de inversão, por outro lado, pode detectar (1) que o primeiro caso não se aplica e (2) que o n que aparece no caso Ev_SS deve ser o mesmo que n. Isso nos permite concluir a prova.

Evss_ev n (Ev.ev_ss e) = e 

Usando o pattern matching dependente, também podemos aplicar o princípio da explosão a hipóteses "obviamente contraditórias" que envolvem propriedades indutivas. Por exemplo:

One_not_even : Not (Ev 1n)

Inversion_practice

Prove os seguintes resultados usando correspondência de padrões.

Ssssev__even (n: Data.Nat) (e: Ev (Data.Nat.succ (Data.Nat.succ (Data.Nat.succ (Data.Nat.succ n))))) : Ev n
Ssssev__even n e = ?

Even5_nonsense (e: Ev 5n) : Prop.Equal (Data.Nat.add 2n 2n) 9n
Even5_nonsense e = ?

A maneira como usamos a inversão aqui pode parecer um pouco misteriosa no início. Até agora, só usamos a inversão em proposições de igualdade para utilizar a injetividade dos construtores ou para discriminar entre diferentes construtores. Mas vemos aqui que a inversão também pode ser aplicada para analisar evidências de proposições definidas indutivamente.

Aqui está como a inversão funciona em geral. Suponha que o nome I se refere a uma suposição P no contexto atual, onde P foi definido por uma declaração Indutiva. Então, para cada um dos construtores de P, a inversão de I gera uma submeta em que I foi substituído pelas condições exatas e específicas sob as quais este construtor poderia ter sido usado para provar P. Alguns desses submetas serão auto contraditórios; a inversão descarta esses. Aqueles que são deixados representam os casos que devem ser provados para estabelecer a meta original. Para estes, a inversão adiciona todas as equações ao contexto de prova que devem ser verdadeiras para os argumentos fornecidos a P (por exemplo, Nat.succ (Nat.succ k) = n na prova de evSS_ev).

O exercício ev_double acima mostra que nossa nova noção de paridade é implicada pelas duas anteriores (uma vez que, por even_bool_prop no capítulo Lógica, já sabemos que elas são equivalentes entre si). Para mostrar que as três coincidem, nós apenas precisamos do seguinte lema:

Ev_even
  (n: Data.Nat)
  (e: Ev n) :
  (Data.Sigma Data.Nat(k => Prop.Equal n ( Data.Nat.double k)))
Ev_even n e = ?

Procedemos por análise de casos em Ev n. O primeiro caso pode ser resolvido trivialmente.

Ev_even Data.Nat.zero e = Data.Sigma.new 0n Prop.Equal.refl

                                                            <!-- mudar -->

Infelizmente, o segundo caso é mais difícil. Precisamos mostrar (k ** S (S n') = double k) Syntax sigma, mas a única suposição disponível é e', que afirma que Ev n' é verdadeiro. Uma vez que isso não é diretamente útil, parece que estamos presos e que a análise de casos em Ev nfoi uma perda de tempo.

Ev_even (Data.Nat.succ Data.Nat.zero) e = Data.Empty.absurd _ //todo

Se olharmos mais de perto para nosso segundo objetivo, no entanto, podemos ver que algo interessante aconteceu: ao realizar a análise de casos em Ev n, fomos capazes de reduzir o resultado original a um semelhante que envolve uma evidência diferente paraEv n: e'. Mais formalmente, podemos concluir nossa prova mostrando que

Ev_even (Data.Nat.succ (Data.Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)

o que é o mesmo que a declaração original, mas com n' em vez de n. Na verdade, não é difícil convencer o Kind de que esse resultado intermediário é suficiente.

Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)

Induction on Evidence

Se isso parece familiar, não é coincidência: encontramos problemas semelhantes no capítulo de Indução, ao tentar usar análise de casos para provar resultados que requeriam indução. E mais uma vez, a solução é... indução!

Vamos tentar nosso lema atual novamente:

Ev_even
  (n: Nat)
  (e: Ev n) :
  (Sigma Nat(k => Equal n ( Nat.double k)))
Ev_even Nat.zero e = Sigma.new 0n Equal.refl
Ev_even (Nat.succ Nat.zero) e = Empty.absurd _
Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)
// Ev_even (Nat.succ (Nat.succ n)) Ev.ev_z = Caso impossível

A equivalência entre as segunda e terceira definições de paridade agora segue.

Ev_even_equiv (n: Nat)  : Equivalence (Ev n) (Sigma Nat (k => Equal n (Nat.double k)))
Ev_even_equiv n         = Equivalence.new (x => Ev_even n x) (y => From_eee n y)

From_eee (n: Nat) (s: Sigma Nat (k => Equal n (Nat.double k))) : Ev n
From_eee n (Sigma.new a b fst snd) =
  Equal.rewrite (Equal.mirror (specialize b into #0 in snd)) (x =>(Ev x)) (Ev_double fst)

Ev_double (n: Nat)      : Ev (Nat.double n)
Ev_double Nat.zero      = Ev.ev_z
Ev_double (Nat.succ n)  = Ev.ev_ss (Ev_double n)

Como veremos nos próximos capítulos, a indução sobre evidências é uma técnica recorrente em várias áreas, especialmente na formalização da semântica de linguagens de programação, onde muitas propriedades de interesse são definidas indutivamente.

Os exercícios a seguir fornecem exemplos simples dessa técnica, para ajudá-lo a se familiarizar com ela.

Ev_sum

Ev_sum (n: Nat) (m: Nat) (e1: Ev n) (e2: Ev m) : Ev (Nat.add n m)
Ev_sum n m e1 e2 = ?

Ev_alternate

Em geral, pode haver várias maneiras de definir uma propriedade indutivamente. Por exemplo, aqui está uma definição alternativa (um pouco forçada) para Ev:

type Evn ~ (n: Nat){
  z : Evn Nat.zero
  d : Evn (Nat.succ (Nat.succ Nat.zero))
  sum <n : Nat> <m: Nat> (evn: Evn n) (evm: Evn m) : Evn (Nat.add n m)
} 

Prove que essa definição é logicamente equivalente à antiga. (Você pode querer olhar para o teorema anterior quando chegar à etapa de indução.)

Ev_evn (n: Nat): Equivalence (Ev n) (Evn n)
Ev_evn n = ?

Ev_ev__ev

Encontrar a coisa apropriada para fazer a indução é um pouco complicado aqui:

Ev_ev_ev (n: Nat) (m: Nat) (e: Ev (Nat.add n m)) (en: Ev n) : Ev m
Ev_ev_ev Nat.zero m e en = ?

Ev_plus_plus

Este exercício requer apenas a aplicação de lemas existentes. Nenhuma indução ou até mesmo análise de casos é necessária, embora algumas das reescritas possam ser tediosas.

Ev_pp 
  <n: Nat> 
  <m: Nat> 
  <p: Nat> 
  (e1: Ev (Nat.add n m))
  (e2: Ev (Nat.add n p))
  : Ev (Nat.add m p)
Ev_pp Nat.zero m p e1 e2 =
``

Inductive Relations

Uma proposição parametrizada por um número (como Ev) pode ser considerada como uma propriedade, ou seja, ela define um subconjunto de Nat, especificamente aqueles números para os quais a proposição é provável. Da mesma forma, uma proposição de dois argumentos pode ser considerada como uma relação, ou seja, ela define um conjunto de pares para os quais a proposição é provável.

Um exemplo útil é a relação "menor ou igual" entre números. A seguinte definição deve ser bastante intuitiva. Ela afirma que existem duas maneiras de fornecer evidências de que um número é menor ou igual a outro: observar que eles são o mesmo número ou fornecer evidências de que o primeiro é menor ou igual ao predecessor do segundo.

type Le (n: Nat) ~ (m: Nat) {
  n : Le n n
  S <m: Nat> (pred: (Le n m)) : (Le n (Nat.succ m)) 
}

Provas de fatos sobre Le usando os construtores n e S seguem os mesmos padrões que provas sobre propriedades, como Ev acima. Podemos aplicar os construtores para provar metas de Le (por exemplo, mostrar que Le 3n 3n ou Le 3n 6n) e podemos usar correspondência de padrões para extrair informações das hipóteses de Le no contexto (por exemplo, provar que (Le 2n 1n) -> (Equal (Plus 2n 2n) 5n)).

Aqui estão algumas verificações de sanidade sobre a definição. (Observe que, embora sejam do mesmo tipo de "testes simples" que demos para as funções de teste que escrevemos nas primeiras palestras, devemos construir suas provas explicitamente - Refl não faz o trabalho, porque as provas não são apenas uma questão de simplificar cálculos.)

Test_le1 : Le 3n 3n
Test_le1 = Le.n 3n

Test_le2 : Le 3n 6n
Test_le2 = Le.S (Le.S (Le.S Le.n))

Test_le3 (l: Le 2n 1n) : Equal (Nat.add 2n 2n) 5n
Test_le3 Le.n = Empty.absurd // TODO
Test_le3 (Le.S Le.n) = Empty.absurd // TODO
Test_le3 (Le.S (Le.S len)) = Empty.absurd // TODO

A relação "estritamente menor que" n < m agora pode ser definida em termos de Le.

Lt (n: Nat) (m: Nat) : Type
Lt n m = Le (Nat.succ n) m

Aqui estão algumas outras relações simples sobre números:

type Square_of ~ (n: Nat) (m: Nat) {
  sq <n: Nat> : Square_of n (Mult n n)
}

type Next_Nat ~ (n: Nat) (m: Nat) {
  Nn <n: Nat> : Next_Nat n (Nat.succ n)
}

type Next_even ~ (n: Nat) (m: Nat) {
  1 <n: Nat> (pred: Ev (Nat.succ n)) : Next_even n (Nat.succ n)
  2 <n: Nat> (pred: Ev (Nat.succ (Nat.succ n))) : Next_even n (Nat.succ (Nat.succ n))
}

Total_relation (Opcional)

Defina uma relação binária indutiva Total_relation que é válida para todos os pares de números naturais.

// TODO

Empty_relation (Opcional)

Defina uma relação binária indutiva Empty_relation (sobre números) que nunca é válida.

// TODO

Le_exercises (Opcional)

Aqui estão alguns fatos sobre as relações Le e Lt que vamos precisar mais adiante no curso. As provas são bons exercícios de prática.

Le.trans (n: Nat) (m: Nat) (o: Nat) (x: Le m n) (y: Le n o) : Le m o 
Le.trans n m o x y = ?

O_le_n (n: Nat) : Le Nat.zero n
O_le_n n = ?

N_le_m_sn_le_sm (n: Nat) (m: Nat) (l: Le n m) : Le (Nat.succ n) (Nat.succ m)
N_le_m_sn_le_sm n m l = ?

Sn_le_Sm_n_le_m (n: Nat) (m: Nat) (l: Le (Nat.succ n) (Nat.succ m)) : Le n m
Sn_le_Sm_n_le_m n m l = ?

Le_plus_l (a: Nat) (b: Nat) : Le a (Nat.add a b)
Le_plus_l a b = ?

Plus_lt (n1: Nat) (n2: Nat) (m: Nat) (lt: Lt (Nat.add n1 n2) m) : Pair (Lt n1 m) (Lt n2 m)
Plus_lt n1 n2 m lt = ?

Lt_S (n: Nat) (m: Nat) (l: Lt n m) : (Lt n (Nat.succ m))
Lt_S n m l = ?

Lte_complete (n: Nat) (m: Nat) (e: Equal (Nat.lte n m) Bool.true) :  (Le n m)
Lte_complete n m e = ? 

Dica: O próximo pode ser mais fácil de provar por indução em m.

Lte_correct (n: Nat) (m: Nat) (le: Le n m) : Equal Bool (Nat.lte n m) Bool.true
Lte_correct n m le = ?

Dica: Este teorema pode ser facilmente provado sem usar indução.

Lte_true_trans (n: Nat) (m: Nat) (o: Nat) 
  (l: Equal (Nat.lte n m) Bool.true) 
  (k: Equal (Nat.lte m o) Bool.true) 
  : Equal (Nat.lte n o) Bool.true
Lte_true_trans n m o l k = ?

lte_iff

Lte_iff (n: Nat) (m: Nat) : Iff (Equal (Nat.lte n m) Bool.true) (Le n m)
Lte_iff n m = ?

R_provability

We can define threeplace relations, four-place relations, etc., in just the same way as binary relations.

For example, consider the following three-place relation on numbers:

type R ~ (a: Nat) (b: Nat) (c: Nat) {
  C1 : R 0n 0n 0n
  C2 <m: Nat> <n: Nat> <o: Nat>
    (r: R m n o) 
  : R (Nat.succ m) n (Nat.succ o)
  C3 <m: Nat> <n: Nat> <o: Nat>
    (r: R m n o) 
  : R m (Nat.succ n) (Nat.succ o)
  C4 <m: Nat> <n: Nat> <o: Nat>
    (r: R (Nat.succ m) (Nat.succ n) (Nat.succ (Nat.succ o))) 
  C5 <m: Nat> <n: Nat> <o: Nat> 
   (r: R m n o) 
}

Which of the following propositions are provable?

• R 1n 1n 2n

// TODO

• R 2n 2n 6n

// TODO

• If we dropped constructor C5 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

// TODO

• If we dropped constructor C4 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

// TODO

R_fact (Optional)

The relation R above actually encodes a familiar function. Figure out which function; then state and prove this equivalence in Kind

F_R (m: Nat) (n: Nat) : Nat
F_R m n = ?

R_equiv_fR (m: Nat) (n: Nat) (o: Nat) : Iff (R m n o) (Equal (F_R m n) o)
R_equiv_fR m n o = ?

Subseq

Uma lista é uma subsequência de outra lista se todos os elementos da primeira lista ocorrem na mesma ordem na segunda lista, possivelmente com alguns elementos extras entre eles. Por exemplo, [1n,2n,3n] é uma subsequência de cada uma das listas [1n,2n,3n], [1n,1n,1n,2n,2n,3n], [1n,2n,7n,3n], [5n,6n,1n,9n,9n,2n,7n,3n,8n], mas não é uma subsequência de nenhuma das listas [1n,2n], [1n,3n], [5n,6n,2n,1n,7n,3n,8n].

• Defina um tipo indutivo Subseq em List Nat que capture o significado de ser uma subsequência. (Dica: Você precisará de três casos.)
• Prove subseq_refl, que a subsequência é reflexiva, ou seja, qualquer lista é uma subsequência de si mesma.
• Prove subseq_app, que para quaisquer listas l1, l2 e l3, se l1 é uma subsequência de l2, então l1 também é uma subsequência de (App l2 l3).
• (Opcional, mais difícil) Prove subseq_trans, que a subsequência é transitiva - ou seja, se l1 é uma subsequência de l2 e l2 é uma subsequência de l3, então l1 é uma subsequência de l3. Dica: escolha sua indução com cuidado!

R_provability

oli

R_provability2 (Opcional)

Suponha que demos a definição a seguir para o Kind:

type Rp ~ (n: Nat) (l: List Nat) {
  C1 
  : Rp 0n []
  C2 <n: Nat> <l: List Nat> 
  (r: Rp n l) 
  : Rp (Nat.succ n) (List.cons n l)
  C3 <n: Nat> <l: List Nat> 
  (r: Rp (Nat.succ n) l)
}

• Rp 2n [1n,0n]
• Rp 1n [1n,2n,1n,0n]
• Rp 6n [3n,2n,1n,0n]

Case Study: Regular Expressions

A propriedade Ev fornece um exemplo simples para ilustrar definições indutivas e as técnicas básicas para raciocinar sobre elas, mas não é muito empolgante - afinal, é equivalente às duas definições não indutivas de paridade que já vimos, e não parece oferecer nenhum benefício concreto sobre elas. Para dar uma melhor noção do poder das definições indutivas, vamos mostrar como usá-las para modelar um conceito clássico da ciência da computação: expressões regulares.

Expressões regulares são uma linguagem simples para descrever strings, definidas da seguinte forma:

type Regexp (t: Type) {
    emptyset                              
    emptystr                              
    chr   (h: t)                          
    app   (st1: Regexp t) (st2: Regexp t) 
    union (st1: Regexp t) (st2: Regexp t)
    star  (st1: Regexp t)                 
  }

Observe que essa definição é polimórfica: expressões regulares em Reg_exp t descrevem strings com caracteres extraídos de t - ou seja, listas de elementos de t.

(Nós nos afastamos um pouco da prática padrão ao não exigir que o tipo t seja finito. Isso resulta em uma teoria um pouco diferente de expressões regulares, mas a diferença não é significativa para nossos propósitos.)

Conectamos expressões regulares e strings por meio das seguintes regras, que definem quando uma expressão regular corresponde a alguma string:

• A expressão EmptySet não corresponde a nenhuma string. • A expressão EmptyStr corresponde à string vazia []. • A expressão Chr x corresponde à string de um caractere [x]. • Se re1 corresponde a s1 e re2 corresponde a s2, então (App re1 re2) corresponde a (App s1 s2). • Se pelo menos uma das expressões re1 e re2 corresponder a s, então Union re1 re2 corresponde a s. • Finalmente, se podemos escrever alguma string s como a concatenação de uma sequência de strings s = (App s_1 (App... s_k...)), e a expressão re corresponde a cada uma das strings s_i, então Star re corresponde a s.

Como caso especial, a sequência de strings pode estar vazia, então Star re sempre corresponde à string vazia [] independentemente de qual seja re.

Podemos facilmente traduzir essa definição informal em uma definição de dados da seguinte forma:

type Expmatch <t> ~(xs: Data.List t) (r: Regexp t) {
mempty              : Expmatch t []   Regexp.emptystr 
mchar (x: t)        : Expmatch t [x] (Regexp.chr x)
mapp 
  <s1: Data.List t>
  <s2: Data.List t>
  <re1: Regexp t>
  <re2: Regexp t>
  (e1: Expmatch t s1 re1)
  (e2: Expmatch t s2 re2)
  : Expmatch t (Data.List.concat t s1 s2) (Regexp.app re1 re2)
munionl <s1: Data.List t> (re1: Regexp t) (re2: Regexp t)
  (e1: Expmatch t s1 re1)
  : Expmatch t s1 (Regexp.union re1 re2)
munionr (re1: Regexp t) <s2: Data.List t> (re2: Regexp t)
  (e1: Expmatch t s2 re2)
  : Expmatch t s2 (Regexp.union re1 re2)
mstarz (r: Regexp t) : Expmatch t [] (Regexp.star r)  
mstarapp 
  <s1: Data.List t> 
  <s2: Data.List t>
  <r1: Regexp t>
  (e1: Expmatch s1 r1)
  (e2: Expmatch s2 (Regexp.star r1))
  : Expmatch t (Data.List.concat t s1 s2) (Regexp.star r1)
}

Vamos ilustrar essas regras com alguns exemplos.

Regexp_ex1 : Expmatch [1] (Regexp.chr 1)
Regexp_ex1 = Expmatch.mchar 1 

Regexp_ex2 : Expmatch [1, 2] (Regexp.app (Regexp.chr 1) (Regexp.chr 2))
Regexp_ex2 = Expmatch.mapp [1] (Regexp.chr 1) (Expmatch.mchar 1) [2] (Regexp.chr 2) (Expmatch.mchar 2)

Usando correspondência de padrões, também podemos mostrar que certas strings não correspondem a uma expressão regular:

Regexp_ex3 : Not (Expmatch [1, 2] (Regexp.chr 1))
Regexp_ex3 = Empty.absurd _

Podemos definir funções auxiliares para ajudar a escrever expressões regulares. A função reg_exp_of_list constrói uma expressão regular que corresponde exatamente à lista que recebe como argumento:

Regexp_of_list <t> (xs: List t)        : Regexp t
Regexp_of_list t List.nil              = Regexp.emptystr
Regexp_of_list t (List.cons xs.h xs.t) = Regexp.app (Regexp.chr xs.h) (Regexp_of_list t xs.t)

Regexp_ex4 : Expmatch [1, 2, 3] (Regexp_of_list [1, 2, 3])
Regexp_ex4 = 
  (Expmatch.mapp 
    [1] 
    (Regexp.chr 1) 
    (Expmatch.mchar 1) 
    [2, 3] 
    (Regexp_of_list [2, 3])
    (Expmatch.mapp
      [2]
      (Regexp.chr 2)
      (Expmatch.mchar 2) 
      [3]
      (Regexp_of_list [3])
      (Expmatch.mapp
        [3]
        (Regexp.chr 3)
        (Expmatch.mchar 3)
        []
        (Regexp_of_list [])
        (Expmatch.mempty)
      )
    )
  )

Também podemos provar fatos gerais sobre Exp_match. Por exemplo, o seguinte lema mostra que toda string s que corresponde a re também corresponde a Star re.

Mstar1 <t> <s: List t> <re: Regexp t> (e: Expmatch s re) : Expmatch s (Regexp.star re)  
Mstar1 t s re e = 
  let msz = Expmatch.mstarz re
  let mss = Expmatch.mstarapp s [] re e msz
  let lst = List_concat s
  let rwt = Equal.rewrite lst (x => (Expmatch t x (Regexp.star re))) mss
  rwt

(Obsere o uso de appendNilRightNeutral*** para alterar o objetivo do teorema para exatamente a mesma forma esperada por MStarApp.)

Exp_match_ex1

Os seguintes lemas mostram que as regras de correspondência informais fornecidas no início do capítulo podem ser obtidas a partir da definição indutiva formal.

  Munion 
  <t> 
  <s: List t> 
  <re1:  Regexp t> 
  <re2:  Regexp t> 
  (p: Pair (Expmatch s re1) (Expmatch s re2))
  : Expmatch s (Regexp.union re1 re2)
Munion t s re1 re2 (Pair.new fst snd) = 
  Expmatch.munionl t s [] re1 re2

O próximo lema é declarado em termos da função fold do capítulo Poly: Se ss: List (List t) representa uma sequência de strings s1, ..., sn, então fold (++) ss [] é o resultado da concatenação de todas elas.

Fold <x> <y> (f: x -> y -> y) (l: Data.List x) (b: y) : y
Fold x y f Data.List.nil b = b
Fold x y f (Data.List.cons xs.h xs.t) b = f xs.h (Fold f xs.t b) 

MStar_ <t>
  (ss : Data.List (Data.List t))
  (re : Regexp t)
  (construct_match : (s : Data.List t) -> (i : In s ss) -> Expmatch s re)
  : Expmatch (Concats ss) (Regexp.star re)
MStar_ ss re construct_match = ?

Reg_exp_of_list

Prove que reg_exp_of_list satisfaz a seguinte especificação:

Reg_exp_of_list_spec <t> (s1: Data.List t) (s2: Data.List t) : Iff (Expmatch s1 (Regexp_of_list s2)) (Prop.Equal s1 s2)
Reg_exp_of_list_spec s1 s2 = ?

Como a definição de Exp_match tem uma estrutura recursiva, é de se esperar que as provas envolvendo expressões regulares frequentemente exijam indução com base nas evidências. Por exemplo, suponha que quiséssemos provar o seguinte resultado intuitivo: se uma expressão regular re corresponde a alguma string s, então todos os elementos de s devem ocorrer em algum lugar de re. Para enunciar este teorema, primeiro definimos uma função re_chars que lista todos os caracteres que ocorrem em uma expressão regular:

Re_chars <t> (re: Regexp t) : Data.List t
Re_chars t Regexp.emptyset  = []
Re_chars t Regexp.emptystr  = []
Re_chars t (Regexp.chr x)   = [x]
Re_chars t (Regexp.app r0 r1) = Data.List.concat (Re_chars r0) (Re_chars r1)
Re_chars t (Regexp.union r0 r1) = Data.List.concat (Re_chars r0) (Re_chars r1)
Re_chars t (Regexp.star r0) = Re_chars r0

Re_star <t> (re: Regexp t) : Prop.Equal (Re_chars (Regexp.star re)) (Re_chars re)
Re_star e re = Prop.Equal.refl

Podemos então formular nosso teorema da seguinte forma:

Destruct <a> (x: a) (lx: Data.List a) (ly: Data.List a) (i: In x (Data.List.concat a lx ly)) : (Data.Either (In x lx) (In x ly))
Destruct a x lx ly i =  
  let Data.Pair.new fst snd = (In_app_iff x lx ly) 
  let f = (fst :: (_) -> (_)) i 
  f

Construct <a> (x: a) (lx: Regexp a) (ly: Regexp a) (e: Data.Either (In x (Re_chars lx)) (In x (Re_chars ly))) : In x (Data.List.concat (Re_chars lx) (Re_chars ly))
Construct a x lx ly e = (Data.Pair.snd ( In_app_iff x (Re_chars lx) (Re_chars ly)) :: (_) -> (_)) e

In_re_match <a> (x: a) (re: Regexp a) (s: Data.List a) (e: Expmatch s re) (i: In x s) : In x (Re_chars re)
In_re_match a x (Regexp.emptyset) Data.List.nil e i = i
In_re_match a x (Regexp.emptyset) (Data.List.cons head tail) e i = Data.Empty.absurd _ //todo
In_re_match a x (Regexp.emptystr) (Data.List.nil) Expmatch.mempty i = i
In_re_match a x (Regexp.chr u s)  (Data.List.cons t re (Data.List.nil _)) (Expmatch.mchar c) i = 
  let e0 = Prop.Equal.refl :: Prop.Equal c re
  let e1 = Prop.Equal.refl :: Prop.Equal s c
  let chn = Prop.Equal.chain e1 e0
  let rrt = Prop.Equal.rewrite (Prop.Equal.mirror chn) (y => (Data.Either (Prop.Equal _ x y) _)) i 
  rrt
In_re_match a x (Regexp.app t z y) (Data.List.concat u l1 l2) e i = 
  let e0 = Prop.Equal.refl :: Prop.Equal u a
  let l3 = l1 :: Data.List a
  let l4 = l2 :: Data.List a
  let e1 = Prop.Equal.refl :: Prop.Equal l1 l3
  let e2 = Prop.Equal.refl :: Prop.Equal l2 l4
  let e3 = Prop.Equal.refl :: Prop.Equal  (Data.List.concat u l1 l2) (Data.List.concat a l3 l4) 
  let i = i :: (In a x (Data.List.concat u l1 l2))
  let rrt = Prop.Equal.rewrite e3 ((k: (Data.List a))=> (In a x k)) i 
  let des = Destruct x l3 l4 rrt
  des
In_re_match a x re Data.List.nil (Expmatch.mstarz z) i = Data.Empty.absurd _ //todo

Re_not_empty

Escreva uma função recursiva re_not_empty que testa se uma expressão regular corresponde a alguma string. Prove que sua função está correta.

Re_not_empty <t> (re: Regexp t)   : Data.Bool
Re_not_empty t re = ?

Re_not_empty_correct <t> <re: Regexp t> 
: Equivalence (Data.Sigma (Data.List t) (s => Expmatch s re)) (Prop.Equal (Re_not_empty re) Data.Bool.true)
Re_not_empty_correct t re = ?

The remember Tactic

Reescrever a seção, o casamento de padrões dependentes resolve tudo isso.

Uma característica potencialmente confusa da tática de indução é que ela permite facilmente que você tente configurar uma indução sobre um termo que não é suficientemente geral. O efeito disso é perder informações (assim como destruct pode fazer) e deixá-lo incapaz de concluir a prova. Aqui está um exemplo:

Star_app  <a> (re: Regexp a) (s1: Data.List a) (s2: Data.List a) (exp0: Expmatch a s1 (Regexp.star re)) (exp1: Expmatch a s2 (Regexp.star re)) 
: (Expmatch (Data.List.concat s1 s2) (Regexp.star re))
Star_app a re (Data.List.nil _) s2 (Expmatch.mstarz e) exp1 = exp1
Star_app a re s1 s2 (Expmatch.mstarapp t r s r1 m ms) exp1 = 
  let e0 = Prop.Equal.refl :: Prop.Equal r1 re
  let e1 = Prop.Equal.refl :: Prop.Equal (Data.List.concat r s) s1
  let ind = Expmatch.mstarapp m (Star_app r1 s s2 ms exp1)
  let rrt = Prop.Equal.rewrite e0 (x => (Expmatch _ _ (Regexp.star _ x))) ind
  let aux = App_assoc r s s2
  let rrt = Prop.Equal.rewrite aux (x => (Expmatch _ (x) (_))) rrt
  let rrt = Prop.Equal.rewrite e1 (x => (Expmatch t (Data.List.concat _ x s2) (Regexp.star t re))) rrt
  rrt

Exp_match_ex2

MStar2 <t> (re: Regexp t) (s: Data.List t) (ss: Data.List (Data.List t)) (exp: Expmatch s (Regexp.star re)) 
: (Data.Pair (Prop.Equal s (Fold (x => y => Data.List.concat x y ) ss [])) ((s2: Data.List t) -> (In s2 ss) -> (Expmatch s2 re)))

O lema MStar'' abaixo (junto com o seu inverso, o exercício MStar' acima), mostra que a nossa definição de Exp_match para Star é equivalente àquela informalmente dada anteriormente.

pumping

Um dos primeiros teoremas realmente interessantes na teoria das expressões regulares é o chamado lema do bombeamento, que afirma, informalmente, que qualquer string suficientemente longa s que corresponde a uma expressão regular re pode ser "bombeada" repetindo alguma seção do meio de s um número arbitrário de vezes para produzir uma nova string também correspondente a re.

Para começar, precisamos definir o que significa "suficientemente longa". Uma vez que estamos trabalhando em uma lógica construtiva, na verdade precisamos ser capazes de calcular, para cada expressão regular re, o comprimento mínimo para as strings s garantirem a "bombeabilidade".

pumping_constant :

Em seguida, é útil definir uma função auxiliar que repete uma string (anexa a si mesma) um certo número de vezes.

napp :

Agora, o próprio lema do bombeamento afirma que, se s => re e se o comprimento de s for pelo menos a constante de bombeamento de re, então s pode ser dividida em três substrings s1 ++ s2 ++ s3 de tal forma que s2 pode ser repetida qualquer número de vezes e o resultado, quando combinado com s1 e s3, ainda corresponderá a re. Como s2 também está garantida a não ser a string vazia, isso nos dá uma maneira (construtiva!) de gerar strings correspondentes a re que são tão longas quanto desejarmos.

pumping :

Para agilizar a prova (que você deve preencher), a tática omega, que é habilitada pelo Require a seguir, é útil em vários lugares para completar automaticamente argumentos tediosos de baixo nível envolvendo igualdades ou desigualdades sobre números naturais. Voltaremos à tática omega em um capítulo posterior, mas sinta-se à vontade para experimentá-la agora, se quiser. O primeiro caso da indução dá um exemplo de como ela é usada.

pumping m le = ?pumping_rhs

Estudo de Caso: Melhorando a Reflexão

Vimos no capítulo de Lógica que frequentemente precisamos relacionar computações booleanos com declarações em Tipo. No entanto, realizar essa conversão da forma como fizemos lá pode resultar em scripts de prova tediosos. Considere a prova do seguinte teorema:

filter_not_empty_In : {n : Nat} -> Not (filter ((==) n) l = []) -> In n l //terminar

No segundo caso, aplicamos explicitamente o lema beq_nat_true à equação gerada ao fazer um dependent match em n == x, para converter a suposição n == x = True em n = m.

Podemos simplificar isso definindo uma proposição indutiva que fornece um melhor princípio de análise de casos para n == m. Em vez de gerar uma equação como n == m = True, que geralmente não é diretamente útil, esse princípio nos fornece imediatamente a suposição que realmente precisamos: n = m.

Na verdade, vamos definir algo um pouco mais geral, que pode ser usado com propriedades arbitrárias (e não apenas igualdades):

type Reflect  (p: Type) (b: Bool) { //TODO: corrigir
  ReflectT    (p: Type) (b= True) : Reflect p b
  ReflectF    (p: Type) (n: Not p) (b= False) : Reflect p b
}

A propriedade "reflect" recebe dois argumentos: uma proposição p e um booleano b. Intuitivamente, ela afirma que a propriedade p é refletida em (ou seja, equivalente a) o booleano b: p é verdadeira se e somente se b = True. Para entender isso, observe que, por definição, a única maneira de obtermos evidências de que "Reflect p True" é verdadeiro é mostrando que p é verdadeira e usando o construtor "ReflectT". Se invertermos essa afirmação, isso significa que deve ser possível extrair evidências para p a partir de uma prova de "Reflect p True". Da mesma forma, a única maneira de mostrar "Reflect p False" é combinando evidências de "Not p" com o construtor "ReflectF".

É fácil formalizar essa intuição e mostrar que as duas afirmações são de fato equivalentes:

Equiv_reflect <b: Bool> (e: Equiv p  (b = True)) : Reflect p b
Equiv_reflect Bool.false (pb, _) = ReflectF (uninhabited . pb) Equal.refl
Equiv_reflect Bool.true (_, bp)  = ReflectT (bp Refl) Equal.refl

Reflect_equiv

Reflect_equiv (r: Reflect p b) : Equivalence p  (Bool.equal b Bool.true)
Reflect_equiv x = ?

A vantagem do "Reflect" sobre o conectivo normal "se e somente se" é que, ao destruir uma hipótese ou lema da forma "Reflect p b", podemos realizar uma análise de casos em b ao mesmo tempo em que geramos hipóteses apropriadas nos dois ramos (p no primeiro subobjetivo e Not p no segundo).

Beq_natP <n: Nat> <m : Nat> :  Reflect (Equal n m) (Nat.equal n m)
Beq_natP {n} {m} = iff_reflect (iff_sym (beq_nat_true_iff n m))

A nova prova de filter_not_empty_In agora segue da seguinte maneira. Observe como as chamadas a destruct e apply são combinadas em uma única chamada a destruct.

(Para ver isso claramente, observe as duas provas de filter_not_empty_In com Kind e observe as diferenças no estado da prova no início do primeiro caso do destruct.)

Filter_not_empty_In_ <n : Nat> <n: Not (filter ((x => y => Nat.equal x y) n) l = []) : In n l

Beq_natP_practice

Use beq_natP, como mencionado acima, para provar o seguinte:

Count (n : Nat) : (l : List Nat) : Nat
Count n List.nil = 0n
Count n (List.cons xs.h xs.t) = Nat.add (Bool.if (Nat.equal n xs.h) 1n 0n)  (Count n xs.t)

Beq_natP_practice (e: Equal (count n l) Nat.zero) : Not (In n l)
Beq_natP_practice e = ? 

Essa técnica nos proporciona apenas uma pequena vantagem em conveniência para as provas que vimos aqui, mas usar o "Reflect" de forma consistente geralmente resulta em scripts de prova perceptivelmente mais curtos e claros à medida que as provas se tornam maiores. Veremos muitos outros exemplos nos próximos capítulos.

O uso da propriedade "reflect" foi popularizado pelo SSReflect, uma biblioteca Coq que tem sido utilizada para formalizar resultados importantes em matemática, incluindo o teorema das 4 cores e o teorema de Feit-Thompson. O nome SSReflect significa "small-scale reflection" (reflexão de pequena escala), ou seja, o uso generalizado da reflexão para simplificar pequenos passos de prova com computações booleanas.

Exercícios adicionais

Nostutter

Formular definições indutivas de propriedades é uma habilidade importante que você precisará neste curso. Tente resolver este exercício sem qualquer ajuda.

Dizemos que uma lista "gagueja" se ela repete o mesmo elemento consecutivamente. A propriedade "Nostutter minha_lista" significa que minha_lista não gagueja. Formule uma definição indutiva para Nostutter. (Isso é diferente da propriedade NoDup no exercício abaixo; a sequência [1,4,1] se repete, mas não gagueja).

type Nostutter <t> (l: List t) {
  RemoveMe : Nostutter []
}

Certifique-se de que cada um desses testes seja bem-sucedido, mas sinta-se à vontade para alterar a prova sugerida (em comentários) se ela não funcionar para você. Sua definição pode ser diferente da nossa e ainda estar correta, nesse caso, os exemplos podem precisar de uma prova diferente. (Você vai perceber que as provas sugeridas usam várias táticas sobre as quais não falamos, para torná-las mais robustas em relação às diferentes formas possíveis de definir Nostutter. Provavelmente, você pode apenas descomentá-las e usá-las como estão, mas também pode provar cada exemplo com táticas mais básicas.)

Test_nostutter_1 : Nostutter [3n,1n,4n,1n,5n,6n]
Test_nostutter_1 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_2 : Nostutter []
Test_nostutter_2 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_3 : Nostutter [5n]
Test_nostutter_3 = ?
// Prova. repita o construtor; aplique beq_nat_false; auto. Qed.

Test_nostutter_4 : Not (Nostutter [3n,1n,1n,4n])
Test_nostutter_4 = ?
// Prova. intro.
// repetir correspondência de metas com
// h: nostutter _ |- _ => inversão h; limpar h; subst
// end.
// contradição H1; auto.

Filter_challenge

Vamos provar que nossa definição de filter do capítulo Poly corresponde a uma especificação abstrata. Aqui está a especificação, escrita informalmente em inglês:

Uma lista l é uma "mescla em ordem" de l1 e l2 se ela contém todos os mesmos elementos de l1 e l2, na mesma ordem de l1 e l2, mas possivelmente intercalados. Por exemplo,

[1n,4n,6n,2n,3n]

é uma mescla em ordem de

[1n,6n,2n]

e

[4n,3n].

Agora, suponha que temos um conjunto t, uma função test: t -> Bool e uma lista l do tipo List t. Suponha ainda que l é uma mescla em ordem de duas listas, l1 e l2, de modo que cada item em l1 satisfaça test e nenhum item em l2 satisfaça test. Então, filter test l = l1.

Traduza esta especificação em um teorema em Kind e prove-o. (Você precisará começar definindo o que significa uma lista ser uma mescla de outras duas. Faça isso com um tipo de dados indutivo, não uma função.)

Filter_challenge_2

Uma maneira diferente de caracterizar o comportamento do filter é a seguinte: Entre todas as subsequências de l com a propriedade de que test avalia como Verdadeiro para todos os seus elementos, o filter test l é o mais longo. Formalize essa afirmação e prove-a.

Palindromes

Um palíndromo é uma sequência que é lida da mesma forma de trás para frente.

• Defina uma proposição indutiva Pal sobre List t que capture o que significa ser um palíndromo. (Dica: você precisará de três casos. Sua definição deve ser baseada na estrutura da lista; ter apenas um único construtor como

  C <t> (l : List t)  (rev: Equal l (Rev l)) : Pal l
  

  pode parecer óbvio, mas não funcionará muito bem.)

• Prove (pal_app_rev) que

  (l : List t) : Pal (List.concat l (Rev l))

• Prove (pal_rev) que

    (l : List t) (p: Pal l) : Equal l (Rev l)

Palindrome_converse

Novamente, a direção contrária é significativamente mais difícil, devido à falta de evidência. Usando sua definição de Pal do exercício anterior, prove que

(l : List t) ( Equal l (Rev l)) Pal l

NoDup

Lembre-se da definição da propriedade In do capítulo Lógica, que afirma que um valor x aparece pelo menos uma vez em uma lista l:

In <t> (x : t) (l : List t) : Type
In x List.nil = Empty
In x (List.concat xs.h xs.t) = Either (Equal x xs.h)  (In x xs)

Sua primeira tarefa é usar In para definir uma proposição Disjoint <t> l1 l2, que deve ser comprovável exatamente quando l1 e l2 são listas (com elementos do tipo t) que não têm elementos em comum.

Em seguida, use In para definir uma proposição indutiva NoDup <t> l, que deve ser comprovável exatamente quando l é uma lista (com elementos do tipo t) em que cada membro é diferente de todos os outros. Por exemplo, NoDup U60 [1,2,3,4] e NoDup Bool [] devem ser comprováveis, enquanto NoDup Nat [1,2,1] e NoDup Bool [True,True] não devem ser.

Por fim, declare e prove um ou mais teoremas interessantes que relacionam Disjoint, NoDup e List.

Pigeonhole principle

O princípio da gaiola de pombos afirma um fato básico sobre contagem: se distribuirmos mais do que n itens em n gaiolas de pombos, alguma gaiola de pombos deve conter pelo menos dois itens. Como frequentemente acontece, esse fato aparentemente trivial sobre números requer uma máquina não trivial para provar, mas agora temos o suficiente... Primeiro, prove um lema fácil e útil.

In_split 
  <t> 
  <x: t> 
  <l: List t> 
  (i: In x l) 
  : ([l1] -> [l2] -> ((Equal l (List.concat l1  (List.cons x  l2)))))
In_split i = ?

Agora defina uma propriedade Repeats de forma que Repeats <t> l afirme que l contém pelo menos um elemento repetido (do tipo t).

type  Repeats <t> (l: List t) {
  -- PREENCHA AQUI
  RemoveMe' : Repeats [] -- necessário para verificação de tipo, os dados não devem estar vazios
}

Essa prova é muito mais fácil se você usar a hipótese excluded_middle para mostrar que In é decidível, ou seja, Either (In x l) (Not (In x l)). No entanto, também é possível fazer a prova sem assumir que In é decidível; se você conseguir fazer isso, não precisará da hipótese excluded_middle.

Aqui está uma maneira de formalizar o princípio da gaiola de pombos. Suponha que a lista l2 represente uma lista de rótulos de gaiolas de pombos, e a lista l1 represente os rótulos atribuídos a uma lista de itens. Se houver mais itens do que rótulos, pelo menos dois itens devem ter o mesmo rótulo - ou seja, a lista l1 deve conter repetições.

Pigeonhole_principle <t> (x: t) 
	(l1: Data.List t) 
	(l2: Data.List t) 
	(i1: In x l1) 
	(i2: In x l2) 
	(lt: Lt (Data.List.length l1) (Data.List.length l2)) 
	: Repeats l1
Pigeonhole_principle t x l1 l2 i2 i2 lt = ?

Excluded_middle : (p : Type) : Either p (Not p)

Contribuidores

• NaoEhSavio
• Bonatto