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 =
``