證明輔助工具coq簡(jiǎn)介-預(yù)覽頁(yè)
【正文】 明構(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 歸納謂詞 ? 問(wèn)題：證明 EqNat 0 0 ? ? 寫(xiě)出類型為 EqNat 0 0的證明構(gòu)造 ? 答案： OEq Lemma LEqNat1 : EqNat O O. Proof OEq. Definition LEqNat1 : EqNat O O := OEq. 歸納謂詞 ? 問(wèn)題：證明 EqNat 1 1 ? ? 寫(xiě)出類型為 EqNat 1 1的證明構(gòu)造 Lemma LEqNat1 : EqNat 1 1. Proof (SEq 0 0 LEqNat0). Definition LEqNat1 : EqNat O O := (SEq 0 0 LEqNat0).. Inductive EqNat : nat nat Prop := | OEq : EqNat O O | SEq : forall m n : nat, EqNat m n EqNat (S m) (S n). 歸納謂詞 ? 練習(xí)：證明 EqNat 2 2 ? Inductive EqNat : nat nat Prop := | OEq : EqNat O O | SEq : forall m n : nat, EqNat m n EqNat (S m) (S n). 歸納謂詞 ? 問(wèn)題：證明 forall n, EqNat n n ? Definition LEqNatn : forall n, EqNat n n := ? Inductive EqNat : nat nat Prop := | OEq : EqNat O O | SEq : forall m n : nat, EqNat m n EqNat (S m) (S n). 歸納謂詞 ? 問(wèn)題：證明 forall n, EqNat n n ? ? 答案：遞歸函數(shù) Fixpoint LEqNatn (n : nat) : EqNat n n := match n return (EqNat n n) with | O = OEq | S n39。證明輔助工具 Coq簡(jiǎn)介 郭宇 20220720 中科大 耶魯高可信軟件聯(lián)合研究中心 課程主頁(yè) 問(wèn)題 ? 如何表示數(shù)學(xué)證明？ ?Miracles often occur… 費(fèi)馬大定理 (1673) ? Xn = Yn + Zn ?當(dāng) n2時(shí)無(wú)整數(shù)解 ? A. Wiles ? 1993 ? 證明 ? ?超過(guò)一百頁(yè) ?世界上能看懂的人屈指可數(shù) ?原始證明有錯(cuò)，一年多以后更正 四色定理 ? K. Appel amp。) = evenb n39。 (LEqNatn n
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1