學一些coq指令

f_equal用法,消去等號兩邊函式的相同部分

舉例：

goal : x + (y + (-y)) + z = x + z

goal : x + (y + (-y)) = x

eg: rewrite !plus_sn_m 相當於 repeat rewrite plus_sn_m

progress (tac)

如果tac生效就繼續，不成功就失敗

eg： repeat progess (try rewrite lemmax).

rename

將變數重新命名

eg: rename n into m.

change 將假設的自由變元改一下

eg: change (forall b, p b) in h0.

searchabout x 搜所有關於x的命題

eg: searchabout plus.

specialize (h a)對h裡的forall x，將變數x例項化為a

p->q的證明 實際上就是 p的證明到q的證明的乙個函式

goal : forall p, ~ ~ p.

proof.

intros.

exact (fun h0: ~ p => h0 h).

如果編譯不通過，可以將上乙個.v的**寫成下面這個形式貼上過來

module x.

...end x.
end x.
import x

class group : type := .

(*將group的元素轉化為乙個型別*)
coersion a : group >-> sortclass.
theorem fact1 : forall (g: group) (x: g) x + (- x) = 0.

同時歸納定義兩種型別

inductive a : type :=

| a1 : a
| a2 : b -> a
with b : type :=
| b1 : b
| b2 : a -> b -> b.

Linux一些指令

date 檢視日曆 cal 輸出 檢視命令 顯示輸入的內容 echo 顯示文字檔案內容 cat 翻頁顯示檔案內容 只能向下翻頁 more 翻頁顯示檔案內容 帶上下翻頁 less 顯示檔案的頭幾行 預設10行 head n 指定顯示的行數 顯示檔案的末尾幾行 預設10行 tail n f追蹤顯示檔案更...

docker 一些指令

docker run it tomcat 7.0.68 jre8 bin bash 進入容器 root iz25ljx2ojuz command cat create.sh bin bash docker create v logs logs v dockertmp skywalker api sk...

一些轉移指令

轉移指令 8086cpu的轉移指令分為以下幾類 無條件轉移指令 如 jmp 條件轉移指令 迴圈指令 如 loop 過程 相當於函式 中斷 操作符offset在組合語言中是由編譯器處理的符號，它的功能是取得標號的偏移位址 a.無條件轉移 jmp為無條件轉移，可以只改變ip,也可以同時修改cs和ip j...