證明輔助工具coq簡介(編輯修改稿)
2024-08-28 14:08 本頁面
【文章內容簡介】 | true = fun (b : bool) = b | false = fun (b : bool) = false end. Coq Check (andb). Coq Check (andb true). 示例一：布爾值計算 Coq Definition double (f : bool bool) : bool bool := fun (a : bool) = f (f a). Coq Eval pute in (double negb true). 示例二：自然數 Coq Inductive nat : Set := O : nat | S : nat nat. nat is defined nat_rect is defined nat_ind is defined nat_rec is defined 偶數判定 Fixpoint evenb (n:nat) : bool := match n with | O = true | S O = false | S (S n39。) = evenb n39。 end. 加法 ?原始遞歸函數（ Primitive Recursion） ?保證函數的終止性 Fixpoint plus (n : nat) (m : nat) {struct n}: nat := match n with | O = m | S n’ = S (plus n’ m) end. 基本邏輯推理 原子命題定義 Variables A B C : Prop. 定理證明演示 Theorem T1 : A A. 證明構造的編程 打印證明 Theorem T1 : A A. Coq Print T1. T1 = fun H : A = H : A A ? CurryHoward 同構 ?類型形如 A B 的證明是一個函數 ?以命題 A的證明為參數，返回 B的證明 程序即證明 Definition T1’ := fun (H : A) = H. Check T1’. 程序即證明 Definition T1’’:= fun (H : A) = T1 H. Check T1’’. ? 證明的構造方式并不唯一 ? 構造 —— Construction Definition T1’ := fun (H : A) = H. Check T1’. 練習 Theorem T2 : A B A. Proof ? 答案 Theorem T2 : A B A. Proof fun (H : A) = fun (H2 : B) = H. ? T2是定理 AB A 的 “ 構造 ” 合取連接詞 Theorem T3 : A /\ B A. Proof fun (H : A /\ B) = (proj1 H). Theorem T4 : A /\ B B. Proof fun (H : A /\ B) = (proj2 H). 析取連接詞 Theorem T6 : A /\ B A \/ B. Proof ? Theorem T5 : A A \/
環(huán)評公示相關推薦
鄂ICP備17016276號-1