證明輔助工具coq簡介-文庫吧資料
2025-08-07 14:08本頁面
【正文】 唯一 ? 構(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 \/ B. Proof fun (H : A) = or_intro1 H. 析取連接詞 Theorem T6 : A /\ B A \/ B. Proof fun (H : A /\ B) = T5 (T3 H). Theorem T5 : A A \/ B. Theorem T3 : A /\ B A. 全稱量詞 Theorem T7 : forall A : Prop, A A. ? CurryHoward 同構(gòu) ?類型形如 forall x :A, B 的證明仍然是一個函數(shù) ?以 x 為參數(shù)，返回 B的證明 全稱量詞 Theorem T7 : forall A : Prop, A A. Proof fun (A : Prop) = fun (x : A) = x. 【 思考 】 下面證明構(gòu)造的含義： Definition T4 := T3 (forall A : Prop, A) 全稱量詞 Theorem T7 : forall A : Prop, A A. 【 思考 】 下面證明構(gòu)造的含義： Definition T8 := T7 (forall A : Prop, A) T8 : False False 練習(xí) Theorem T9 : forall A B C: Prop, (A B) (B C) (A C). Proof ?. 函數(shù)復(fù)合 歸納 歸納謂詞 Inductive EqNat : nat nat Prop := | OEq : EqNat O O | SEq : forall m n : nat, EqNat m n EqNat (S m) (S n). P (m, n) iff m = n 歸納謂詞 ? 問題：證明 EqNat 0 0 ? ? 寫出類型為 EqNat 0 0的證明構(gòu)造 ? 答案： OEq Lemma LEqNat1 : EqNat O O. Proof OEq. Definition LEqNat1 : EqNat O O := OEq. 歸納謂詞 ? 問題：證明 EqNat 1 1 ? ? 寫出類型為 EqNat 1 1的證明構(gòu)造 Lemma LEqNat1 : EqNat 1 1. Proof (SEq 0 0 LEqNat0). Definition LEqNat1 : EqNat O O := (SEq 0
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1