ประเภทที่ขึ้นต่อกันเป็นอาร์กิวเมนต์ของฟังก์ชันใน Coq

นี่คือการแปลฟังก์ชันของคุณใน Coq โดยตรง:

From Coq Require Import Arith.

Definition add_two_even (n : {n : nat | Nat.even n = true}) : nat :=
  proj1_sig n + 1.

โปรดทราบว่าคุณต้องใช้ฟังก์ชัน proj1_sig เพื่อแยก n จากประเภทย่อย {n : nat | Nat.even n = true} หากต้องการใช้ add_two_even คุณต้องดำเนินการอีกทางหนึ่ง: เปลี่ยนจากตัวเลขไปเป็นองค์ประกอบของ {n | Nat.even n = true} ใน Coq สิ่งนี้ต้องมีการพิสูจน์ด้วยตนเอง สำหรับค่าคอนกรีต n สามารถทำได้ง่าย:

(* 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).

ตัวสร้าง exist ล้อมค่า x ด้วยการพิสูจน์ P x ทำให้เกิดองค์ประกอบประเภทเซ็ตย่อย {x | P x} คำว่า eq_refl เป็นการพิสูจน์ x = x สำหรับค่าใดๆ ของ x เมื่อ n เป็นจำนวนเฉพาะ Coq สามารถประเมิน Nat.even n และค้นหาว่า eq_refl เป็นข้อพิสูจน์ที่ถูกต้องของ Nat.even n = true หรือไม่ เมื่อ n เป็น 1, Nat.even n = false และการตรวจสอบล้มเหลว นำไปสู่ข้อความแสดงข้อผิดพลาดแรก เมื่อ n เป็น 4 การตรวจสอบจะสำเร็จ

สิ่งต่างๆ จะซับซ้อนมากขึ้นเมื่อ n ไม่ใช่ค่าคงที่ แต่เป็นนิพจน์ที่กำหนดเอง การพิสูจน์ว่า Nat.even n = true อาจต้องการการให้เหตุผลโดยละเอียดซึ่งผู้ใช้ต้องได้รับคำแนะนำ ตัวอย่างเช่น เรารู้ว่า Nat.even (n + n) = true สำหรับค่าใดๆ ที่เป็น n แต่ Coq ไม่ทราบ ดังนั้น หากต้องการเรียก add_two_even บางอย่างในรูปแบบ n + n เราจำเป็นต้องแสดงบทแทรก

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)).

มีเครื่องมือบางอย่างที่ช่วยอำนวยความสะดวกในการเขียนโปรแกรมรูปแบบนี้ เช่น ปลั๊กอินสมการ แต่เครื่องมือทั่วไป ภูมิปัญญาในชุมชน Coq คือคุณควรหลีกเลี่ยงประเภทย่อยสำหรับฟังก์ชันเช่น add_two_even ซึ่งข้อจำกัดไม่ได้ทำให้คุณสมบัติเกี่ยวกับฟังก์ชันง่ายขึ้นอย่างมาก

คุณจะพบตัวอย่างการใช้งานประเภทเซ็ตย่อยที่ดีได้มากมายในไลบรารี Mathematical Components ตัวอย่างเช่น ไลบรารีใช้ประเภทเซ็ตย่อยเพื่อกำหนดประเภท n.-tuple T ของรายการที่มีความยาว n และประเภท 'I_n ของจำนวนเต็มที่ล้อมรอบด้วย n สิ่งนี้ช่วยให้เราสามารถกำหนดฟังก์ชันตัวเข้าถึงทั้งหมด tnth (t : n.-tuple T) (i : 'I_n) : T ที่แยกองค์ประกอบ ith ของรายการ t หากเรากำหนดตัวเข้าถึงนี้สำหรับรายการและจำนวนเต็มที่กำหนดเอง เราจำเป็นต้องส่งค่าเริ่มต้นไปยังฟังก์ชันเพื่อส่งคืนเมื่อดัชนีอยู่นอกขอบเขต หรือเปลี่ยนลายเซ็นของฟังก์ชันเพื่อให้ส่งคืนค่าประเภท option T แทน ซึ่งบ่งชี้ว่า ฟังก์ชั่นไม่สามารถส่งกลับค่าได้ การเปลี่ยนแปลงนี้ทำให้คุณสมบัติของฟังก์ชัน accessor ระบุได้ยากขึ้น ตัวอย่างเช่น ลองพิจารณาบทแทรก eq_from_tnth ซึ่งระบุว่าสองรายการเท่ากันหากองค์ประกอบทั้งหมดเท่ากัน:

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

บทแทรกนี้สำหรับรายการตามอำเภอใจมีความซับซ้อนมากขึ้น เนื่องจากเราต้องการสมมติฐานเพิ่มเติมว่าทั้งสองรายการมีขนาดเท่ากัน (ในที่นี้ x0 คือค่าเริ่มต้น)

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