Jak mogę przeczytać definicję ex_intro?

Question

Czytam Mike Nahas's introductory Coq tutorial, który mówi:

argumenty, aby "ex_intro" są:

• orzecznik
• świadek
• dowodem opiera nazywany ze świadkiem

Spojrzałem na the definition:

Inductive ex (A:Type) (P:A -> Prop) : Prop := 
    ex_intro : forall x:A, P x -> ex (A:=A) P. 

i mam problem z analizą. Które części wyrażenia forall x:A, P x -> ex (A:=A) P odpowiadają tym trzem argumentom (predykatom, świadectwu i dowodowi)?

Answer 1

Aby zrozumieć, co Mike oznaczało, że lepiej, aby uruchomić interpreter Coq i kwerendy dla typu ex_intro:

Check ex_intro. 

Następnie należy zobaczyć:

ex_intro 
    : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x 

Ten mówi, że ex_intro nie bierze tylko 3, ale 4 argumenty:

• rodzaj thi ng you're quantification over, A;
• predykat P : A -> Prop;
• świadek x : A; i
• dowód P x, potwierdzający, że x jest ważnym świadkiem.

Jeśli połączysz wszystkie te rzeczy, otrzymasz dowód na exists x : A, P x. Na przykład: @ex_intro nat (fun n => n = 3) 3 eq_refl jest dowodem exists n, n = 3.

Zatem różnica pomiędzy rzeczywistą typu ex_intro i jednego można przeczytać na definicji jest to, że były zawiera wszystkie parametry, które są podane w nagłówku - w tym przypadku, A i P.

Answer 2

Tak, te definicje typów indukcyjnych mogą być trudne do odczytania.

Pierwsza część to:

Inductive ex (A:Type) (P:A -> Prop) : Prop := 

To, co jest związane z samego typu. Więc za każdym razem, gdy zobaczysz ex, będzie on miał A, a P i ex będzie miał typ Prop. Pomijając obecnie A, skupmy się na P, która jest predykatem. Tak więc, jeśli użyjemy naszego przykładu "istnieje liczba naturalna, która jest pierwsza", P może być is_prime, gdzie is_prime przyjmuje nat (liczba naturalna) jako argument i może istnieć dowód na to, że nat jest liczbą pierwszą.

W tym przykładzie A będzie nat. W samouczku A nie jest wymieniony, ponieważ Coq zawsze może go wnioskować. Biorąc pod uwagę predykat, Coq może uzyskać typ A, patrząc na typ argumentu predykatu.

Podsumowując, w naszym przykładzie typem będzie ex nat is_prime. To mówi, że istnieje nat, który jest pierwszorzędny, ale nie mówi, który nat. Kiedy skonstruujemy ex nat is_prime, będziemy musieli powiedzieć, który z nich - będziemy potrzebować "świadka". A to prowadzi nas do definicji konstruktora:

ex_intro : forall x:A, P x -> ex (A:=A) P. 

Konstruktor nazywa ex_intro. Trudność polega na tym, że konstruktor ma wszystkie parametry tego typu. Tak więc, zanim przejdziemy do tych wymienionych po ex_intro, musimy uwzględnić te dla typu: A i P.

Po te parametry są te wymienione po ex_intro: x, który jest świadkiem, a P x, co jest dowodem na to, że orzeczenie odnosi się do świadka. Przy użyciu naszego przykładu, x może być 2, a P x będzie dowodem (is_prime 2).

Konstruktor musi określić parametry dla konstruktora typu ex. Tak dzieje się po strzale (->). Nie muszą one odpowiadać parametrom użytym do wywołania konstruktora, ale zazwyczaj tak. Aby to osiągnąć, argument jest następujący: jest on przekazywany jawnie. (A:=A) mówi, że parametr A w ex powinien być równy A w wywołaniu do konstruktora. Podobnie parametry P z ustawia się na P od wywołania do konstruktora.

Tak więc, jeśli mieliśmy proof_that_2_is_prime z rodzaju (prime 2), możemy wywołać ex_intro is_prime 2 proof_that_2_is_prime i byłoby to rodzaj ex nat is_prime. Który jest naszym dowodem, że istnieje liczba naturalna, która jest pierwsza.

---

Aby odpowiedzieć na to pytanie wprost: W wyrażeniu forall x:A, P x -> ex (A:=A), x:A jest świadkiem i P x jest dowód, że świadectwo jest prawdziwe. Wyrażenie nie zawiera predykatu, ponieważ jest to część parametrów typu, które należy przekazać do konstruktora ex_intro. Lista parametrów tutoriala nie zawiera A, ponieważ została wywnioskowana przez Coq.

Mam nadzieję, że rozumiesz, dlaczego uważam, że ta dyskusja była zbyt szczegółowa dla mojego tutoriala! Dzięki za pytanie.