Czy jest minimalny kompletny zestaw taktyk w Coq?

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.

Źródło

2015-09-20 tinlyx

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". –

Dowód w Coq jest tylko terminem właściwego typu. Taktyki pomagają budować ten termin, łącząc mniejsze sub-terms w bardziej złożone. Dlatego minimalny zestaw podstawowych taktyk zawierałby tylko taktykę exact, jak wspomniał Konstantin.

Taktyka refine pozwala bezpośrednio podać warunki dowodowe, ale z dziurami, które wygenerują podcele. Zasadniczo każda taktyka jest tylko przykładem taktyki refine.

Jednakże, jeśli chcesz najpierw rozważyć jedynie minimalny zestaw taktyk, uważam, existsintro{s}, reflexivity, symmetry, apply, rewrite, revert, destruct i induction. inversion może się przydać dość szybko.

Źródło

2015-09-21 09:28:37 Vinz

'reflexivity' to po prostu' apply eq_refl', jeśli nie używasz setoids, a symetria również jest aplikacją; istnieje "konstruktor", który z kolei jest po prostu "zastosować". Czy często używasz 'revert'? Z drugiej strony, 'przepisać' i' simpl' będą prawdopodobnie miłymi dodatkami do tej listy. –

Można powiedzieć, że mówienie o "przepisaniu", to po prostu zastosowanie lematu o prawidłowym kształcie. Jak już mówiłem, wszystko zaczęło się "dopracowywać" (bezpośrednio pisząc dowód). Ale przyznaję, że "przepisać" powinien znajdować się na liście. Często używam odwrotu, ponieważ wykonuję wiele indukcji z zależnymi typami, gdzie bardzo pomaga. – Vinz

Ah, typy zależne użyłyby dużo 'revert'ing, w rzeczy samej :)' rewrite' jest rzeczywiście często tylko aplikacją zasady indukcyjnej, ale praktycznie nigdy jej nie używam. –

Czy jest minimalny kompletny zestaw taktyk w Coq?

Odpowiedz

Powiązane problemy