證明輔助工具coq簡介(編輯修改稿)
2025-08-28 14:08 本頁面
【文章內(nèi)容簡介】 | true = fun (b : bool) = b | false = fun (b : bool) = false end. Coq Check (andb). Coq Check (andb true). 示例一：布爾值計(jì)算 Coq Definition double (f : bool bool) : bool bool := fun (a : bool) = f (f a). Coq Eval pute in (double negb true). 示例二：自然數(shù) Coq Inductive nat : Set := O : nat | S : nat nat. nat is defined nat_rect is defined nat_ind is defined nat_rec is defined 偶數(shù)判定 Fixpoint evenb (n:nat) : bool := match n with | O = true | S O = false | S (S n39。) = evenb n39。 end. 加法 ?原始遞歸函數(shù)（ Primitive Recursion） ?保證函數(shù)的終止性 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. 證明構(gòu)造的編程 打印證明 Theorem T1 : A A. Coq Print T1. T1 = fun H : A = H : A A ? CurryHoward 同構(gòu) ?類型形如 A B 的證明是一個(gè)函數(shù) ?以命題 A的證明為參數(shù)，返回 B的證明 程序即證明 Definition T1’ := fun (H : A) = H. Check T1’. 程序即證明 Definition T1’’:= fun (H : A) = T1 H. Check T1’’. ? 證明的構(gòu)造方式并不唯一 ? 構(gòu)造 —— Construction Definition T1’ := fun (H : A) = H. Check T1’. 練習(xí) Theorem T2 : A B A. Proof ? 答案 Theorem T2 : A B A. Proof fun (H : A) = fun (H2 : B) = H. ? T2是定理 AB A 的 “ 構(gòu)造 ” 合取連接詞 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)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1