Berikut ini terjemahan langsung dari fungsi Anda di Coq:
From Coq Require Import Arith.
Definition add_two_even (n : {n : nat | Nat.even n = true}) : nat :=
proj1_sig n + 1.
Perhatikan bahwa Anda memerlukan fungsi proj1_sig untuk mengekstrak n dari subset tipe {n : nat | Nat.even n = true}. Untuk menggunakan add_two_even, Anda juga perlu melakukan sebaliknya: beralih dari angka ke elemen {n | Nat.even n = true}. Di Coq, ini memerlukan pembuktian manual. Untuk nilai konkrit n, caranya mudah:
(* The next command fails with a type checking error *)
Fail Compute add_two_even (exist _ 1 eq_refl).
(* The next command succeeds *)
Compute add_two_even (exist _ 4 eq_refl).
Konstruktor exist membungkus nilai x dengan bukti P x, menghasilkan elemen bertipe subset {x | P x}. Suku eq_refl adalah bukti dari x = x untuk setiap nilai x. Jika n adalah bilangan konkrit, Coq dapat mengevaluasi Nat.even n dan mencari tahu apakah eq_refl merupakan bukti valid dari Nat.even n = true. Ketika n adalah 1, Nat.even n = false, dan pemeriksaan gagal, menyebabkan pesan kesalahan pertama. Ketika n adalah 4, pengecekan berhasil.
Segalanya menjadi lebih rumit ketika n bukan sebuah konstanta, melainkan ekspresi arbitrer. Sebuah bukti bahwa Nat.even n = true memerlukan alasan terperinci yang harus dipandu oleh pengguna. Misalnya, kita mengetahui bahwa Nat.even (n + n) = true untuk nilai n apa pun, tetapi Coq tidak. Jadi, untuk memanggil add_two_even pada sesuatu yang berbentuk n + n, kita perlu menunjukkan sebuah lemma.
Lemma add_n_n_even n : Nat.even (n + n) = true.
Proof.
induction n as [|n IH]; trivial.
now simpl; rewrite <- plus_n_Sm, IH.
Qed.
Definition foo (n : nat) :=
add_two_even (exist _ (n + n) (add_n_n_even n)).
Ada beberapa alat untuk memfasilitasi gaya pemrograman ini, seperti plugin persamaan, namun yang umum kebijaksanaan dalam komunitas Coq adalah Anda harus menghindari tipe subset untuk fungsi seperti add_two_even, yang batasannya tidak menyederhanakan properti fungsi secara substansial.
Anda dapat menemukan banyak contoh penggunaan tipe subset yang baik di pustaka Komponen Matematika. Misalnya, perpustakaan menggunakan tipe subset untuk mendefinisikan tipe n.-tuple T dari daftar dengan panjang n, dan tipe 'I_n dari bilangan bulat yang dibatasi oleh n. Hal ini memungkinkan kita untuk mendefinisikan fungsi pengakses total tnth (t : n.-tuple T) (i : 'I_n) : T yang mengekstrak elemen ke i dari daftar t. Jika kita mendefinisikan pengakses ini untuk daftar dan bilangan bulat arbitrer, kita perlu meneruskan nilai default ke fungsi untuk dikembalikan ketika indeks berada di luar batas, atau mengubah tanda tangan fungsi sehingga mengembalikan nilai bertipe option T, yang menunjukkan bahwa fungsi bisa gagal mengembalikan nilai. Perubahan ini membuat properti fungsi pengakses lebih sulit untuk dinyatakan. Misalnya, perhatikan lemma eq_from_tnth, yang menyatakan bahwa dua daftar adalah sama jika semua elemennya sama:
eq_from_tnth:
forall (n : nat) (T : Type) (t1 t2 : n.-tuple T),
(forall i : 'I_n, tnth t1 i = tnth t2 i) -> t1 = t2
Pernyataan lemma untuk daftar arbitrer ini menjadi lebih rumit, karena memerlukan asumsi tambahan yang mengatakan bahwa kedua daftar tersebut berukuran sama. (Di sini, x0 adalah nilai default.)
eq_from_nth:
forall (T : Type) (x0 : T) (s1 s2 : list T),
size s1 = size s2 ->
(forall i : nat, i < size s1 -> nth x0 s1 i = nth x0 s2 i) -> s1 = s2
person
Arthur Azevedo De Amorim
schedule
14.11.2019
