sf
Working Software Foundations
Proof General (Emacs plugin) tips:
- C-c C-RET
- C-c C-p : for displaying goals
- C-c C-l : Refreshes goals
- C-c C-a C-a : Run SearchAbout
- C-c C-; : Paste SearchAbout response into buffer
- C-/ : Go to the proof end (Very handy!)
Useful functions:
- coq-Print : View the definition of particular function
Notes:
Things which aren't in the book and learned from seeing other's code.
- You can
rewrite
like this:
rewrite <- plus_comm with (n := n' * m) (m := m + m) at 1.
See different styles here.
apply tactic
Example 1
Theorem f_equal : forall (A B : Type) (f: A -> B) (x y: A),
x = y -> f x = f y.
Current goals:
H : ....
============================
S n = S m'
apply f_equal.
Current goals:
H : ....
============================
n = m'
Example 2
n' : nat
IHn' : forall m : nat, n' + n' = m + m -> n' = m
m' : nat
H1 : n' + n' = m' + m'
============================
S n' = S m'
apply IHn' with (m := m') in H1.
n' : nat
IHn' : forall m : nat, n' + n' = m + m -> n' = m
m' : nat
H1 : n' = m
============================
S n' = S m'
destruct tactic
Example 1
H : P \/ Q
=============
S n' = S m'
destruct H as [H1 | H2].
H1 : P
========
S n' = S m'
Example 2
H2 : exists x : A, f x = y /\ In x l'
============================
exists x : A, f x = y /\ (x' = x \/ In x l')
destruct H2
x : A
H : f x = y /\ In x l'
============================
exists x0 : A, f x0 = y /\ (x' = x0 \/ In x0 l')
Example 3
H : f x = y /\ In x l
============================
In y (map f l)
destruct H as [H1 H2].
H1 : f x = y
H2 : In x l
============================
In y (map f l)
References:
- Coq Modules: Very useful for understanding.