Notes

quando estudamos provas por indução se faz uma analise de casa para a ultima regra utilizada

então vamos trabalhar com tantos casos quantos regras tivermos para deduzir uma determinada regra

a tatica inversion sobre uma hipotese indutiva, ela faz uma analise de caso para cada regra, note que ao encontrar algo impossivel, ele dira que temos algo equivalente a False, aka, _|_ (bottom)

note que o uso do inversion, gera um monte de igualdade, e o uso do substion que vai trocar os argumentos das hipoteses pelas igualdades existente,

podemos definir um tatica a ser aplicada a varias subgoals, gerados ao aplicar uma tatica a conclusao
podemos aplicar uma mesma tatica a todas, uma diferente a cada uma, porem neste caso é necessário saber exatamente quantos casos serão gerados

podemos definir uma tatica try t que tem exatamente semantica de t, porem se t da erro, try t não

constructor e uma tatica que vai descobrir qual hipotese pode ser aplicada a usara ela, se houver mais de uma, ele aplica a primeira

tativa clear h remove a hipotese h das hipoteses conhecidas, usada pra remover hipoteses certamente inuteis em provas automaticas

tatica congruence encontra hipoteses contraditorias

intuiton resolve tautologias da logica proposicional e algumas da logica de predicados

omega resolve formulas que envolvem os conectivos, variaveis, inteiros, adicao, subtracao

a tatica repet fica repetindo uma tatica ate provar, dar falha ou entra em loop infinito

auto, prova qualquer conclusao que use somente assumptiom, intros e apply ate uma certa profundidade (default = 5)
: podemos configurar o que a tatica auto vai usar, por exemplo um teorema que foi provado, fazemos isso adicionando -o ao hint database
- hint resolver:
- hint constructor: coloca todos os construtores do teorema no hint database
- hint unfold: ao usar em uma definicao dizemos que a auto pode expandir a definicao

e permitido definir suas proprias taticas