Skip to content

Latest commit

 

History

History
67 lines (52 loc) · 2.99 KB

README.md

File metadata and controls

67 lines (52 loc) · 2.99 KB
Raw

coq_learn

this project is created in order to learn coq.

coq library about nat.

https://coq.inria.fr/library/Coq.Init.Nat.html

some exercise:

https://github.com/jam231/Software-Foundations https://github.com/atungare/coq-software-foundations

reference:

https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

notes

  1. 等号两边消除，保持格式一致

  2. 将格式类似的作为lemma

  3. destruct 也可以用在 (let (x, y) := h in let (lx, ly) := split t in (x :: lx, y :: ly)) = (l1, l2) 这样复杂式子中的解耦合。 具体为依次destruct h. destruct (split t). 也可以用于context中的命题为False.还可以用在exists 中，如H:exists x : nat,m = n +x. destruct H as [x H]。就可以把x分离。

    import library:

    From Coq Require Import Nat . https://www.coder.work/article/6672855 https://stackoverflow.com/questions/36621752/how-to-import-the-library-coq-arith-peanonat-in-coq

一些个人规范

  1. assert的sub global 用{}作为bullet
  2. induction 和 deduction的bullet等级不要超过2 层。如果一定要超过，考虑lemma。
  3. 命名规范
  4. 尽可能使用assert，而不是replace.
  5. 新的函数definition 或者fixpoint 之后，要加上example 方便阅读。
  6. 证明之前先search.
  7. 不同抽象等级的变量分别intros.

tactics:

  • intros: move hypotheses/variables from goal to context
  • reflexivity: finish the proof (when the goal looks like e = e)
  • apply: prove goal using a hypothesis, lemma, or constructor
  • apply... in H: apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)
  • apply... with...: explicitly specify values for variables that cannot be determined by pattern matching
  • simpl: simplify computations in the goal
  • simpl in H: ... or a hypothesis
  • rewrite: use an equality hypothesis (or lemma) to rewrite the goal
  • rewrite ... in H: ... or a hypothesis
  • symmetry: changes a goal of the form t=u into u=t
  • symmetry in H: changes a hypothesis of the form t=u into u=t
  • transitivity y: prove a goal x=z by proving two new subgoals, x=y and y=z
  • unfold: replace a defined constant by its right-hand side in the goal
  • unfold... in H: ... or a hypothesis
  • destruct... as...: case analysis on values of inductively defined types
  • destruct... eqn:...: specify the name of an equation to be added to the context, recording the result of the case analysis
  • induction... as...: induction on values of inductively defined types
  • injection... as...: reason by injectivity on equalities between values of inductively defined types
  • discriminate: reason by disjointness of constructors on equalities between values of inductively defined types
  • assert (H: e) (or assert (e) as H): introduce a "local lemma" e and call it H
  • generalize dependent x: move the variable x (and anything else that depends on it) from the context back to an
  • explicit hypothesis in the goal formula
  • f_equal: change a goal of the form f x = f y into x = y