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.