A Hands-on Introduction to Coq
Nov 22, 2020 21:00 · 3262 words · 16 minute read
Introduction
I have been doing quite a bit of functional programming in haskell for the past few months as a part of my university study. That’s why I am delighted to see a relevant challenge come up in this year’s DragonCTF.
The challenge involves proving a few mathematical theorems using Coq, a functional programming language / interactive theorem prover. I have heard of Coq before but have never got the time to learn it. This challenge became the perfect opportunity for me to get to know it and write a hands-on introduction about it :)
Warmup
The challenge starts out with a few easy proofs for us to first get a hang of Coq.
Theorem problem0: forall A B, A \/ B -> B \/ A.
1 subgoal (ID 3)
============================
forall A B : Prop, A \/ B -> B \/ A
In this proof, we are asked to prove that for two propositions, (A or B) is the same as (B or A) which is quite trivial.
We can try it first in our local environment using the Coq interactive session coqtop in the terminal:
$ coqtop
Welcome to Coq 8.12.1 (November 2020)
Coq < Theorem problem0: forall A B, A \/ B -> B \/ A.
1 subgoal
============================
forall A B : Prop, A \/ B -> B \/ A
problem0 <
As you can see we are greeted with a list of subgoals that we need to validate once we input the theorem that we are trying to prove.
We can first introduce A, B and move them into our context using the intros command:
problem0 < intros A B.
1 subgoal
A, B : Prop
============================
A \/ B -> B \/ A
What this does is effectively give a name to A and B and add that to the context. We can certainly use other names for the two propositions as well. Another point to note is that all coq commands need to end with a . just like how every line in C needs to end with ;.
The next step would be to again introduce our hypothesis that A \/ B:
problem0 < intros H.
1 subgoal
A, B : Prop
H : A \/ B
============================
B \/ A
Now with our named propositions A and B and hypothesis H, we can start proving our goal that B \/ A.
We can use the destruct keyword or tactic as it’s commonly called in Coq. What it does is that it breaks down hypothesis H : A \/ B into two cases: one with H: A and one with H : B and we can prove those two separately as two subgoals:
problem0 < destruct H.
2 subgoals
A, B : Prop
H : A
============================
B \/ A
subgoal 2 is:
B \/ A
problem0 <
Next, we use right to suggest that we want to prove that the right-hand side of B \/ A is true. Because it is an OR statement, we only need to show that one of the two is true, not both. Similarly, left is another valid tactic as well.
problem0 < right.
2 subgoals
A, B : Prop
H : A
============================
A
subgoal 2 is:
B \/ A
Now, we can see that our hypothesis H matches the statement we are trying to prove exactly. We can use exact H to finish this sub-proof:
problem0 < exact H.
1 subgoal
A, B : Prop
H : B
============================
B \/ A
Now, we only have 1 subgoal left which is when H: B. As you can already tell, this is very similar to our last case. To not repeat ourselves, we can use the auto tactic to solve this case automatically:
problem0 < auto.
No more subgoals.
Just like that, we finished our first proof in Coq! 🎉🎉🎉
The next few proofs are similar in difficulty:
Coq < Theorem problem0: forall A B, ((((A -> B) -> A) -> A) -> B) -> B.
1 subgoal
============================
forall A B : Type, ((((A -> B) -> A) -> A) -> B) -> B
problem0 < intros A B.
1 subgoal
A : Type
B : Type
============================
((((A -> B) -> A) -> A) -> B) -> B
problem0 < auto.
No more subgoals.
This proof is so simple that
autocan just handle it by itself.
Coq < Theorem problem0: forall (m n: nat), m + n = n + m.
1 subgoal
============================
forall m n : nat, m + n = n + m
problem0 < intros m n.
1 subgoal
m, n : nat
============================
m + n = n + m
problem0 < induction m.
2 subgoals
n : nat
============================
0 + n = n + 0
subgoal 2 is:
S m + n = n + S m
problem0 < simpl.
2 subgoals
n : nat
============================
n = n + 0
subgoal 2 is:
S m + n = n + S m
problem0 < trivial.
1 subgoal
m, n : nat
IHm : m + n = n + m
============================
S m + n = n + S m
problem0 < simpl.
1 subgoal
m, n : nat
IHm : m + n = n + m
============================
S (m + n) = n + S m
problem0 < rewrite IHm.
1 subgoal
m, n : nat
IHm : m + n = n + m
============================
S (n + m) = n + S m
problem0 < trivial.
No more subgoals.
problem0 <
This proof of the commutativity of addition is a bit more involved. We used the
inductiontactic onmand later rewrote(m+n)as(n+m)in the inductive case utilizing the inductive hypothesis.
Coq < Theorem problem0: forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D.
1 subgoal
============================
forall A B C D : Prop, (A -> B) /\ (C -> D) /\ A /\ C -> B /\ D
problem0 < intros A B C D.
1 subgoal
A, B, C, D : Prop
============================
(A -> B) /\ (C -> D) /\ A /\ C -> B /\ D
problem0 < intros H.
1 subgoal
A, B, C, D : Prop
H : (A -> B) /\ (C -> D) /\ A /\ C
============================
B /\ D
problem0 < destruct H.
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : (C -> D) /\ A /\ C
============================
B /\ D
problem0 < destruct H0.
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : A /\ C
============================
B /\ D
problem0 < destruct H1.
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : A
H2 : C
============================
B /\ D
problem0 < apply H in H1. apply H0 in H2.
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : B
H2 : C
============================
B /\ D
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : B
H2 : D
============================
B /\ D
problem0 < split.
2 subgoals
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : B
H2 : D
============================
B
subgoal 2 is:
D
problem0 < assumption.
1 subgoal
A, B, C, D : Prop
H : A -> B
H0 : C -> D
H1 : B
H2 : D
============================
D
problem0 < auto.
No more subgoals.
Few noteworthy points in this proof include:
- We can use the
assumptiontactic in place ofexact ???when the thing we are trying to prove is already in our context- When we have
A And B, we can usesplitto break it into two cases of provingAand provingB.- Just like how equality can be used to rewrite statements using
rewrite, implications can be applied to statements usingapply- The
inkeyword allows us to manipulate hypotheses rather than our goal.
Coq < Theorem problem0: forall (C:Prop) (T:Set) (B: T -> Prop), (exists x : T, C -> B x) -> C -> exists x : T, B x.
1 subgoal
============================
forall (C : Prop) (T : Set) (B : T -> Prop),
(exists x : T, C -> B x) -> C -> exists x : T, B x
problem0 < intros C T B H.
1 subgoal
C : Prop
T : Set
B : T -> Prop
H : exists x : T, C -> B x
============================
C -> exists x : T, B x
problem0 < destruct H.
1 subgoal
C : Prop
T : Set
B : T -> Prop
x : T
H : C -> B x
============================
C -> exists x0 : T, B x0
problem0 < exists x.
1 subgoal
C : Prop
T : Set
B : T -> Prop
x : T
H : C -> B x
H0 : C
============================
B x
problem0 < apply H in H0.
1 subgoal
C : Prop
T : Set
B : T -> Prop
x : T
H : C -> B x
H0 : B x
============================
B x
problem0 < exact H0.
No more subgoals.
Most of the tactics in the proof are introduced before with the exception of
existswhich simply states that a variable in our context satisfies the goal that we are trying to prove.
Coq < Theorem problem0: forall b1 b2, negb (b1 && b2) = orb (negb b1) (negb b2).
1 subgoal
============================
forall b1 b2 : bool, negb (b1 && b2) = (negb b1 || negb b2)%bool
problem0 < intros b1 b2.
1 subgoal
b1, b2 : bool
============================
negb (b1 && b2) = (negb b1 || negb b2)%bool
problem0 < destruct b1.
2 subgoals
b2 : bool
============================
negb (true && b2) = (negb true || negb b2)%bool
subgoal 2 is:
negb (false && b2) = (negb false || negb b2)%bool
problem0 < simpl.
2 subgoals
b2 : bool
============================
negb b2 = negb b2
subgoal 2 is:
negb (false && b2) = (negb false || negb b2)%bool
problem0 < trivial.
1 subgoal
b2 : bool
============================
negb (false && b2) = (negb false || negb b2)%bool
problem0 < simpl.
1 subgoal
b2 : bool
============================
true = true
problem0 < trivial.
No more subgoals.
This last one is also quite easy to prove. We have two boolean values which only lead to four cases. Using
destruct, we can divide-and-conquer each of the cases.
Fun with Math
With the easy ones out of the way, we face a slightly more challenging question:
Coq < Require Import Arith.Mult.
Theorem math_problem: forall m n, (n + m) * (n + m) = n * n + 2 * n * m + m * m.
Coq < 1 subgoal
============================
forall m n : nat, (n + m) * (n + m) = n * n + 2 * n * m + m * m
Here we can see that Arith.Mult. has been imported suggesting that we might need to use some of its properties.
Again, we start with introducing the variables:
math_problem < intros m n.
1 subgoal
m, n : nat
============================
(n + m) * (n + m) = n * n + 2 * n * m + m * m
Then we can use the distributivity of multiplication in Arith.Mult. and a few other properties on addition to simplify our expression.
math_problem < rewrite mult_plus_distr_r.
1 subgoal
m, n : nat
============================
n * (n + m) + m * (n + m) = n * n + 2 * n * m + m * m
math_problem < rewrite mult_plus_distr_l.
1 subgoal
m, n : nat
============================
n * n + n * m + m * (n + m) = n * n + 2 * n * m + m * m
math_problem < rewrite mult_plus_distr_l.
1 subgoal
m, n : nat
============================
n * n + n * m + (m * n + m * m) = n * n + 2 * n * m + m * m
math_problem < simpl.
1 subgoal
m, n : nat
============================
n * n + n * m + (m * n + m * m) = n * n + (n + (n + 0)) * m + m * m
math_problem < rewrite plus_0_r.
1 subgoal
m, n : nat
============================
n * n + n * m + (m * n + m * m) = n * n + (n + n) * m + m * m
math_problem < rewrite mult_plus_distr_r.
1 subgoal
m, n : nat
============================
n * n + n * m + (m * n + m * m) = n * n + (n * m + n * m) + m * m
math_problem < rewrite plus_assoc.
1 subgoal
m, n : nat
============================
n * n + n * m + m * n + m * m = n * n + (n * m + n * m) + m * m
math_problem < rewrite plus_assoc.
1 subgoal
m, n : nat
============================
n * n + n * m + m * n + m * m = n * n + n * m + n * m + m * m
At this point, what we really need to prove is that n * m is the same as m * n. We can use cut to state that as a hypothesis and prove it later:
math_problem < cut (n*m=m*n).
2 subgoals
m, n : nat
============================
n * m = m * n ->
n * n + n * m + m * n + m * m = n * n + n * m + n * m + m * m
subgoal 2 is:
n * m = m * n
math_problem < intros H.
2 subgoals
m, n : nat
H : n * m = m * n
============================
n * n + n * m + m * n + m * m = n * n + n * m + n * m + m * m
subgoal 2 is:
n * m = m * n
math_problem < rewrite H.
2 subgoals
m, n : nat
H : n * m = m * n
============================
n * n + m * n + m * n + m * m = n * n + m * n + m * n + m * m
subgoal 2 is:
n * m = m * n
math_problem < trivial.
1 subgoal
m, n : nat
============================
n * m = m * n
math_problem < apply mult_comm.
No more subgoals.
Proof on Lists
As the last question, we are asked to write a proof about lists:
Require Import Le.
Section last_stage.
Variable A : Type.
Inductive list : Type :=
| nil : list
| cons : A -> list -> list.
Fixpoint nth (l : list) (n : nat) : option A :=
match n,l with
| 0, cons x xs => Some x
| S n, cons _ xs => nth xs n
| _, _ => None
end.
Fixpoint length (l:list) : nat :=
match l with
| nil => 0
| cons _ xs => 1 + length xs
end.
Theorem nth_in: forall (n:nat) (l:list), n < length l -> exists a: A, nth l n = Some a.
I struggled a lot with this proof and solved it in the end by referencing a similar proof on the standard list type in coq.
Here is my attempt at it:
unfold lt. intro n.
induction n as [| n hn].
simpl. intro l.
destruct l.
simpl. intro H. apply le_Sn_O in H. contradiction.
simpl. exists a. trivial.
simpl. destruct l.
simpl. intros H. apply le_Sn_O in H. contradiction.
simpl. intros H. apply le_S_n in H. apply hn in H. exact H.
The basic idea is to do a nested induction on both the index n as well as the list l. However, you need to be careful with the order in which you introduce things otherwise Coq will generate inductive hypotheses not strong enough to prove the theorem.
Summary
I really enjoyed getting to know Coq this weekend and managed to catch a glimpse of the full power of Coq as an interactive theorem prover. I really hope this blog post can inspire more people to try Coq and have some fun with it.
Here are some resources that aided me in the process of learning Coq:
- Coq cheat sheet: A great introduction to all the tactics available in Coq and a clear breakdown of when to use what
- Theorem proving with Coq: A wonderful example-based introduction the language that shows the full process of proving things
- Coq Tactics Index: A more in-depth look at the various tactics with some small tricks mixed in
Exploit + Flag
If you care about my exploit script and want to see the flag, here you go:
from pwn import *
context.log_level = 'debug'
sh = remote('babykok.hackable.software', 1337)
solves = {
'forall A B : Type, ((((A -> B) -> A) -> A) -> B) -> B': '''
intros A B.
auto.
''',
'forall A B : Prop, A \\/ B -> B \\/ A': '''
intros A B.
intros H.
destruct H.
right.
exact H.
auto.
''',
'forall A B C D: Prop,(A->B)/\\(C->D)/\\A/\\C -> B/\\D.': '''
intros A B C D.
intros H.
destruct H.
destruct H0.
destruct H1.
split.
apply H.
exact H1.
auto.
''',
'forall (C:Prop) (T:Set) (B: T -> Prop), (exists x : T, C -> B x) -> C -> exists x : T, B x.': '''
intros C T B.
intros H.
destruct H.
exists x.
apply H.
exact H0.
''',
'forall (m n: nat), m + n = n + m.': '''
intros m n.
induction m.
simpl.
trivial.
simpl.
rewrite IHm.
trivial.
''',
'forall b1 b2, negb (b1 && b2) = orb (negb b1) (negb b2).': '''
intros b1 b2.
destruct b1.
simpl.
trivial.
simpl.
trivial.
''',
'forall m n, (n + m) * (n + m) = n * n + 2 * n * m + m * m.': '''
intros M N.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
rewrite mult_plus_distr_l.
rewrite plus_assoc.
cut (2*N*M=N*M+M*N).
intros H.
rewrite H.
rewrite plus_assoc.
trivial.
simpl.
rewrite plus_0_r.
rewrite mult_plus_distr_r.
cut (M * N = N * M).
intros H1.
rewrite H1.
trivial.
apply mult_comm.
''',
'forall (n:nat) (l:list), n < length l -> exists a: A, nth l n = Some a.': '''
unfold lt.
intro n.
induction n as [| n hn].
simpl.
intro l.
destruct l.
simpl.
intro H.
apply le_Sn_O in H.
contradiction.
simpl.
exists a.
trivial.
simpl.
destruct l.
simpl.
intros H.
apply le_Sn_O in H.
contradiction.
simpl.
intros H.
apply le_S_n in H.
apply hn in H.
exact H.
''',
}
while True:
question = sh.recvuntil('\n> ')
print question
for ques in solves:
ans = solves[ques]
if ques in question:
ans = map(lambda x: x.strip(), ans.strip().split('\n'))
sh.sendline(ans[0])
for line in ans[1:]:
sh.sendlineafter('\n> ', line)
break
else:
print question
sh.interactive()
flag: DrgnS{xxxx_my_c0q_for_4_flag_17bcbc34b7c565a766e335}