Software Foundations

•

[ 교재 ]

New volumes : Vol 1. Logical Foundations, Vol 2. Programming Language Foundations
- https://softwarefoundations.cis.upenn.edu/

[ 강의 로드맵 ]

[ Coq 프로그래밍 환경 ]
- https://coq.inria.fr/

[ 보조 자료]

[ 전술 목록 :  Ch. More Basic Tactics in Volume 1 ]

  • 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
  • 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
  • inversion: reason by injectivity and distinctness of constructors
  • 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

[전술 목록 : Ch.3 from Coq in a Hurry ]