Widziałem wiele taktyk Coq, które nakładają się na siebie w funkcji.Czy jest minimalny kompletny zestaw taktyk w Coq?
Na przykład, kiedy trzeba dokładnie wniosku w tej hipotezy, można użyć assumption
, apply
, exact
, trivial
, a może inni. Inne przykłady obejmują destruct
i induction
dla typów nieindukcyjnych (??).
Moje pytanie brzmi:
Czy istnieje minimalny zestaw podstawowych taktyki (która wyklucza auto
i jej podobne), które są kompletne, w tym sensie, że zestaw ten może być użyty do udowodnienia jakiegokolwiek Coq - udokumentowane twierdzenia o funkcjach liczb naturalnych?
Taktyka w tym minimalnym kompletnym zestawie byłaby idealnie podstawowa, tak aby każda z nich wykonywała tylko jedną (lub dwie) funkcje i można łatwo zrozumieć, co robi.
Z powodu izomorfizmu Curry-Howarda każdy dowód, który można zbudować za pomocą taktyki, odpowiada pewnemu terminowi. Tak więc "dokładna" taktyka jest wystarczająca do udowodnienia jakiegokolwiek celu. Jeśli nie chcesz budować całego terminu za jednym razem, możesz zamiast tego użyć polecenia "sprecyzuj". –