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