Translating My Z3 Tutorial to Coq

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. It was a fantastic tutorial (maybe the best I've seen?), but it was tough love. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on an uphill mountaineering slog.

There are a number of factors to lead to this:

• I could use Z3’s python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
• Z3 can actually be used to declaratively state problems and pushbutton calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
• Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are totally bizarre. But Coq users, this is just the water they swim in. For example, defining an inductive predicate as a datatype is still a bizarre notion to me, but it is Coq 101. I say this to Coq users and they look at me like I’m nuts. “What could even be the problem?”

Anyway, a fun exercise for me was to take the examples from my tutorial and try to translate them into Coq. For the most part I think it isn't that hard and rather educational.

It's interesting the things that show up. Because the Z3 tutorial was designed for automation, the more automated tactics in MicroOmega and Ring are super useful.

https://coq.inria.fr/refman/addendum/micromega.html

The thing is that the sort of proofs that show up here are fine and all, but they aren't going to teach you to fish for yourself. When you step out of this super automatable fragment you're sunk if you don't know other techniques, like the ones Cody was teaching. There may be a better balance of fun and education to be found.

I think there is a hole in the educational content out there on Coq. Software Foundations focuses on the rudiments, CPDT and FRAP kind of takes it a little hardcore, and the Mathematical Components stuff makes you buy in on ssreflect style and some hardcore math topics, both of which are nuts I have not cracked. Also, all of them are really long and initimidating. Seems like there should be something a little more breezy, a little more automatic. It is demoralizing as a beginner to either not know how to prove obvious trivial facts, or even to struggle to do so at great length.

This was also a nice opportunity to take Alectryon by Clément Pit-Claudel out for a spin https://github.com/cpitclaudel/alectryon Alectryon allows you to see the proof state on hover over in your browser. It's a super important part of the Coq. It was pretty easy to put in my blog. Just copy and paste the gnarly html output into a Jekyll post and make sure to link in the CSS files in an assets folder, because they are where the magic happens.

The gist for this post is here https://gist.github.com/philzook58/acd204b4895c41f9e85618f0f6b30a58

Intro Stuff

The very first problem in the tutorial was

(** python
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
*)

which Z3 returns the solution [y = 0, x = 7].

It isn't so obvious how to get coq to find this solution in a low effort way. However, it is easy to get Coq to confirm the validity of this solution given that you know about the [lia] tactic. Otherwise it may be kind of annoying. In general, it may be a good approach to use external tools to produce solutions and just manually place the solutions into Coq. Validating a solution is often easier than producing it.

Require Import Lia.
Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7
     exists 7, 0.
7 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 7 lia. Qed.

A different automated version. Giving the appropriate hint database can matter a lot. https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#hint-databases-defined-in-the-coq-standard-library

Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7
     exists 7, 0.
7 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 7 eauto with arith. Qed.

It turns out, surprisingly to me, that stock eauto is sufficient to actually solve the problem without supplying the solutions. They are discovered via unification and a prolog like search. This found the different solution x = 3, y = 2

Definition solution : exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7
   do 2 eexists. eauto with arith. Show Proof.
(ex_intro
   (fun x : nat =>
    exists y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7)
   3
   (ex_intro
      (fun y : nat => 3 > 2 /\ y < 10 /\ 3 + 2 * y = 7)
      2
      (conj (Gt.gt_Sn_n 2)
         (conj
            (Lt.lt_n_S 1 9
               (Lt.lt_n_S 0 8
                  (PeanoNat.Nat.lt_0_succ 7))) eq_refl)))) Defined.


(* A fairly manual version for comparison. Could be even worse. *)
Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7
   exists 7, 0.
7 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 7 split.
7 > 2
0 < 10 /\ 7 + 2 * 0 = 7 
     -
7 > 2 unfold ">".
2 < 7 Locate "<".
Notation
"x <= y < z" := and (le x y) (lt y z) : nat_scope
(default interpretation)
"x < y <= z" := and (lt x y) (le y z) : nat_scope
(default interpretation)
"x < y < z" := and (lt x y) (lt y z) : nat_scope
(default interpretation)
"x < y" := lt x y : nat_scope (default interpretation)
2 < 7 unfold "<".
3 <= 7 Print le.
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n
  | le_S : forall m : nat, n <= m -> n <= S m

Arguments le (_ _)%nat_scope
Arguments le_n _%nat_scope
Arguments le_S (_ _)%nat_scope
3 <= 7 do 4 apply 
              le_S.
3 <= 3 apply le_n.
     -
0 < 10 /\ 7 + 2 * 0 = 7 split.
0 < 10
7 + 2 * 0 = 7
       +
0 < 10 do 9 apply le_S.
1 <= 1 apply le_n.
       +
7 + 2 * 0 = 7 simpl.
7 = 7 reflexivity.
Qed. 

The next thing is the simplest possible tautology

(**python
p = Bool("p")
my_true_thm = Implies(p, p)
prove(my_true_thm)
*)

This is not a challenge in Coq.

Goal forall P, P -> P.
forall P : Type, P -> P intros.
P:Type
X:P
P assumption. Qed.

(* Even shorter proof *)
Goal forall P, P -> P.
forall P : Type, P -> P auto. Qed.

A valid counterexample found by Z3. Here we prove the counterexample.

(**python
q = Bool("q")
my_false_thm = Implies(q, p)
prove(my_false_thm)

# counterexample
# [p = False, q = True]

*)

Goal not (True -> False).
~ (True -> False) unfold not.
(True -> False) -> False intros.
H:True -> False
False apply H.
H:True -> False
True exact I. Qed.

The first exercise: Get a root of the polynomial x**3 + 3*x**2 + 4*x + 2 == 0 using z3. Can you use z3 to show this is the only solution?

Here we open up the reals. It is easy enough to confirm that the solution of x=-1 is a zero using the [ring] tactic.

Require Import Reals.
Open Scope R_scope.
Print Scope R_scope.
Scope R_scope
Delimiting key is R
Bound to class R
"r ²" := Rsqr r
"x ^ y" := pow x y
"x >= y" := Rge x y
"x > y" := Rgt x y
"x <= y <= z" := and (Rle x y) (Rle y z)
"x <= y < z" := and (Rle x y) (Rlt y z)
"x <= y" := Rle x y
"x < y <= z" := and (Rlt x y) (Rle y z)
"x < y < z" := and (Rlt x y) (Rlt y z)
"x < y" := Rlt x y
"x / y" := Rdiv x y
"x - y" := Rminus x y
"x + y" := Rplus x y
"x * y" := Rmult x y
"/ x" := RinvImpl.Rinv x
"- x" := Ropp x


Goal exists x : R, x^3 + 3 * x^2 + 4 * x + 2 = 0.
exists x : R, x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = 0
  exists (- 1).
(-1) ^ 3 + 3 * (-1) ^ 2 + 4 * -1 + 2 = 0 ring. Qed.

Proving there is no other solution is a bit trickier. A important lemma about a polynomial factor of x^3 + 3 * x^2 + 4 * x + 2

Require Import Lra.
Lemma pos_poly : forall x, x ^ 2 + 2 * x + 2 > 0.
forall x : R, x ^ 2 + 2 * x + 2 > 0 intros.
x:R
x ^ 2 + 2 * x + 2 > 0
   nra. Qed.

(* A slightly more manual proof involving completing the square.*)
Goal forall x, x ^ 2 + 2 * x + 2 > 0.
forall x : R, x ^ 2 + 2 * x + 2 > 0 
   intros.
x:R
x ^ 2 + 2 * x + 2 > 0
   assert (x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1) as H by ring.
x:R
H:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1
x ^ 2 + 2 * x + 2 > 0
   rewrite H.
x:R
H:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1
(x + 1) ^ 2 + 1 > 0 Search (0 <= _ ^ 2).
pow2_ge_0: forall x : R, 0 <= x ^ 2
x:R
H:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1
(x + 1) ^ 2 + 1 > 0
   pose (pow2_ge_0 (x + 1)).
x:R
H:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1
r:=pow2_ge_0 (x + 1):0 <= (x + 1) ^ 2
(x + 1) ^ 2 + 1 > 0
   lra. Qed.



(* I'm actually a little suprised [nra] sufficed here and not psatz. *)

Goal forall x, x + 1 <> 0 -> (x^3 + 3 * x^2 + 4 * x + 2) <> 0.
forall x : R,
x + 1 <> 0 -> x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  intros.
x:R
H:x + 1 <> 0
x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  assert ((x^3 + 3 * x^2 + 4 * x + 2) = 
         ((x + 1) * (x ^ 2 + 2 * x + 2 ))) as H0 by ring.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  rewrite H0.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
(x + 1) * (x ^ 2 + 2 * x + 2) <> 0 pose (pos_poly x).
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
(x + 1) * (x ^ 2 + 2 * x + 2) <> 0 nra. Qed.

(* A slightly more manual proof *)
Goal forall x, x + 1 <> 0 -> (x^3 + 3 * x^2 + 4 * x + 2) <> 0.
forall x : R,
x + 1 <> 0 -> x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  intros.
x:R
H:x + 1 <> 0
x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  assert ((x^3 + 3 * x^2 + 4 * x + 2) = 
         ((x + 1) * (x ^ 2 + 2 * x + 2 ))) by ring.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0
  rewrite H0.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
(x + 1) * (x ^ 2 + 2 * x + 2) <> 0 pose (pos_poly x).
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
(x + 1) * (x ^ 2 + 2 * x + 2) <> 0 Search (_ * _ = 0).
Rmult_0_l: forall r : R, 0 * r = 0
Rmult_0_r: forall r : R, r * 0 = 0
Rmult_eq_0_compat_l:
  forall r1 r2 : R, r2 = 0 -> r1 * r2 = 0
Rmult_eq_0_compat_r:
  forall r1 r2 : R, r1 = 0 -> r1 * r2 = 0
Rmult_eq_0_compat:
  forall r1 r2 : R, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0
Rmult_integral:
  forall r1 r2 : R, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0
Rmult_integral_contrapositive_currified:
  forall r1 r2 : R, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0
Rmult_neq_0_reg:
  forall r1 r2 : R, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0
Rmult_integral_contrapositive:
  forall r1 r2 : R, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0
sqrt3_2_neq_0: 2 * sqrt 3 <> 0
powerRZ_mult_distr:
  forall (m : Z) (x y : R),
  (0 <= m)%Z \/ x * y <> 0 ->
  powerRZ (x * y) m = powerRZ x m * powerRZ y m
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
(x + 1) * (x ^ 2 + 2 * x + 2) <> 0
  apply Rmult_integral_contrapositive_currified.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
x + 1 <> 0
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
x ^ 2 + 2 * x + 2 <> 0
  assumption.
x:R
H:x + 1 <> 0
H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 =
(x + 1) * (x ^ 2 + 2 * x + 2)
r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0
x ^ 2 + 2 * x + 2 <> 0 lra. Qed.

Close Scope R_scope.

The send + more = money Puzzle

There is an assignment of unique digits to letters such that the equation send + more = money holds. Find an assignment of the digits to make this true.

Here is a Z3 version:

(**python
digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits

send = Sum([10**(3-i) * d for i,d in enumerate([s,e,n,d])]) # convert digits of number to number
more = Sum([10**(3-i) * d for i,d in enumerate([m,o,r,e])])
money = Sum([10**(4-i) * d for i,d in enumerate([m,o,n,e,y])])
solver = Solver()
solver.add([s > 0, m > 0]) # first digits are nonzero

# Constrain all digits constrained to be 0 through 9
solver.add([  And( 0 <= d, d <= 9 )   for d in digits])

# Constrain all digits to be unique (Hint: Look at the 8-Queens constraints. Anything useful?)
solver.add(Distinct(digits))

# Constrain send + more == money
solver.add(send + more == money)

solver.check()
solver.model()
*)

Again we can compute in Z3 and just verify in Coq.

I basically always want lists and list notation and can never remember where to find them. I think they should be on by default.

From Coq Require Import List.
Import ListNotations.

(* Convert list of digits to number *)
Definition decimal_list l :=
   let fix decimal_list_aux acc l := match l with
         | h :: t => acc * h + decimal_list_aux (10 * acc) t
         | [] => 0
         end 
   in 
   decimal_list_aux 1 (List.rev l).
Compute decimal_list [1;2;3].
= 123
: nat

Fixpoint all_different (l : list nat) : Prop := match l with
   | h :: t => List.fold_left (fun acc x => (h <> x)  /\ acc ) t   (all_different t)
   | [] => True
   end.
Eval simpl in all_different [1 ; 2 ; 3].
= 1 <> 3 /\ 1 <> 2 /\ 2 <> 3 /\ True
: Prop

Theorem send_more_money : exists s e n d m o r y,
   let digits := [s ;e ;n ;d; m; o; r; y] in
   let send := decimal_list [s ;e; n; d] in
   let more := decimal_list [m ;o; r; e] in
   let money := decimal_list [m ; o ; n ; e; y] in
   s > 0 /\ m > 0 /\ Refl.make_conj (fun x => x <= 9) digits /\
   all_different digits
   /\ send + more = money.
exists s e n d m o r y : nat,
  let digits := [s; e; n; d; m; o; r; y] in
  let send := decimal_list [s; e; n; d] in
  let more := decimal_list [m; o; r; e] in
  let money := decimal_list [m; o; n; e; y] in
  s > 0 /\
  m > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money
   exists 9.
exists e n d m o r y : nat,
  let digits := [9; e; n; d; m; o; r; y] in
  let send := decimal_list [9; e; n; d] in
  let more := decimal_list [m; o; r; e] in
  let money := decimal_list [m; o; n; e; y] in
  9 > 0 /\
  m > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 5.
exists n d m o r y : nat,
  let digits := [9; 5; n; d; m; o; r; y] in
  let send := decimal_list [9; 5; n; d] in
  let more := decimal_list [m; o; r; 5] in
  let money := decimal_list [m; o; n; 5; y] in
  9 > 0 /\
  m > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 6.
exists d m o r y : nat,
  let digits := [9; 5; 6; d; m; o; r; y] in
  let send := decimal_list [9; 5; 6; d] in
  let more := decimal_list [m; o; r; 5] in
  let money := decimal_list [m; o; 6; 5; y] in
  9 > 0 /\
  m > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 7.
exists m o r y : nat,
  let digits := [9; 5; 6; 7; m; o; r; y] in
  let send := decimal_list [9; 5; 6; 7] in
  let more := decimal_list [m; o; r; 5] in
  let money := decimal_list [m; o; 6; 5; y] in
  9 > 0 /\
  m > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money 
   exists 1.
exists o r y : nat,
  let digits := [9; 5; 6; 7; 1; o; r; y] in
  let send := decimal_list [9; 5; 6; 7] in
  let more := decimal_list [1; o; r; 5] in
  let money := decimal_list [1; o; 6; 5; y] in
  9 > 0 /\
  1 > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 0.
exists r y : nat,
  let digits := [9; 5; 6; 7; 1; 0; r; y] in
  let send := decimal_list [9; 5; 6; 7] in
  let more := decimal_list [1; 0; r; 5] in
  let money := decimal_list [1; 0; 6; 5; y] in
  9 > 0 /\
  1 > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 8.
exists y : nat,
  let digits := [9; 5; 6; 7; 1; 0; 8; y] in
  let send := decimal_list [9; 5; 6; 7] in
  let more := decimal_list [1; 0; 8; 5] in
  let money := decimal_list [1; 0; 6; 5; y] in
  9 > 0 /\
  1 > 0 /\
  Refl.make_conj (fun x : nat => x <= 9) digits /\
  all_different digits /\ send + more = money exists 2.
let digits := [9; 5; 6; 7; 1; 0; 8; 2] in
let send := decimal_list [9; 5; 6; 7] in
let more := decimal_list [1; 0; 8; 5] in
let money := decimal_list [1; 0; 6; 5; 2] in
9 > 0 /\
1 > 0 /\
Refl.make_conj (fun x : nat => x <= 9) digits /\
all_different digits /\ send + more = money
   cbv.
1 <= 9 /\
1 <= 1 /\
(9 <= 9 /\
 5 <= 9 /\
 6 <= 9 /\
 7 <= 9 /\ 1 <= 9 /\ 0 <= 9 /\ 8 <= 9 /\ 2 <= 9) /\
((9 = 2 -> False) /\
 (9 = 8 -> False) /\
 (9 = 0 -> False) /\
 (9 = 1 -> False) /\
 (9 = 7 -> False) /\
 (9 = 6 -> False) /\
 (9 = 5 -> False) /\
 (5 = 2 -> False) /\
 (5 = 8 -> False) /\
 (5 = 0 -> False) /\
 (5 = 1 -> False) /\
 (5 = 7 -> False) /\
 (5 = 6 -> False) /\
 (6 = 2 -> False) /\
 (6 = 8 -> False) /\
 (6 = 0 -> False) /\
 (6 = 1 -> False) /\
 (6 = 7 -> False) /\
 (7 = 2 -> False) /\
 (... -> False) /\ (...) /\ ... /\ ...) /\
10652 = 10652 lia. Qed.

But if we want to try solving the problem in coq, here is an approach. This is a send more money solver translated fairly verbatim from Haskell. https://blog.plover.com/prog/haskell/monad-search.html It turned out that using Int63 was much much faster than using peano nat (0.5s vs 20mins), probably because of checking the addition send + more == money

This solver isn't verified, but it does give you a way of computing the puzzle without leaving coq. Interesting question: How do make a efficient toolbox of verified finite domain solvers?

Section find_money.
  Require Import Int63.
Use of “Require” inside a section is fragile. It is
not recommended to use this functionality in finished
proof scripts. [require-in-section,fragile]
  Open Scope int63_scope.
  (* Convert list of digits to number *)
  Definition to_number l := 
     let fix decimal_list_aux acc l := match l with
              | h :: t => acc * h + decimal_list_aux (10 * acc) t
              | [] => 0
              end 
     in
     decimal_list_aux 1 (List.rev l).

  Definition remove d l := filter (fun x => negb (existsb (eqb x) d)) l.
  Compute remove [1;2] [1;2;3;4;5].
= [3; 4; 5]
: list int

  (* Some cute do noation syntax for lists *)
  Notation "x <- c1 ;; c2" := (@flat_map _ _ (fun x => c2) c1)
  (at level 61, c1 at next level, right associativity).

  Definition find_solution :=
     let digits := [0;1;2;3;4;5;6;7;8;9] in
     s <- remove [0] digits;;
     e <- remove [s] digits;;
     n <- remove [s;e] digits;;
     d <- remove [s;e;n] digits;;
     let send := to_number [s;e;n;d] in
     m <- remove [0;s;e;n;d] digits;;
     o <- remove [s;e;n;d;m] digits;;
     r <- remove [s;e;n;d;m;o] digits;;
     let more := to_number [m;o;r;e] in
     y <- remove [s;e;n;d;m;o;r] digits;;
     let money := to_number [m;o;n;e;y] in
     if ((send + more) == money) then [(s,e,n,d,m,o,r,y)] else [].

  (* native_compute is the fastest evaluation method *)
  Eval native_compute in find_solution.
native_compute disabled at configure time; falling
back to vm_compute.
[native-compute-disabled,native-compiler]
= [(9, 5, 6, 7, 1, 0, 8, 2)]
: list
    (int * int * int * int * int * int * int *
     int)

End find_money.

Simple Properties of the Reals

A Z3 version:

(**python
x,y,z = Reals("x y z")
prove( x + y == y + x)
prove( (x + y) + z == x + (y + z))s
prove( x*x >= 0 )
*)


Open Scope R_scope.
Goal forall x y : R, x + y = y + x.
forall x y : R, x + y = y + x intros; ring. Qed.
Goal forall x y z : R, (x + y) + z = x + (y + z).
forall x y z : R, x + y + z = x + (y + z) intros; ring. Qed.
Goal forall x : R, x > 0 \/ x = 0 \/ x < 0.
forall x : R, x > 0 \/ x = 0 \/ x < 0 intros.
x:R
x > 0 \/ x = 0 \/ x < 0 lra. Qed. 
Goal forall x : R, x ^ 2 >= 0.
forall x : R, x ^ 2 >= 0 intros.
x:R
x ^ 2 >= 0 nra. Qed.

Simple Properties of 2D Vectors

Record V2 := {
   x : R;
   y : R
}.

(* vector addition *)
Definition vadd v w := {| 
   x := v.(x) + w.(x);
   y := v.(y) + w.(y) 
   |}.

(* scalar multiplication *)
Definition smul s v := {| x := s * v.(x) ;
 y := s * v.(y)   |}.

(* dot product *)
Definition dot v w := v.(x) * w.(x) + v.(y) * w.(y).


Theorem vadd_assoc : forall u v w, vadd u (vadd v w) = vadd (vadd u v) w.
forall u v w : V2,
vadd u (vadd v w) = vadd (vadd u v) w
   intros.
u, v, w:V2
vadd u (vadd v w) = vadd (vadd u v) w destruct u, v, w.
x0, y0, x1, y1, x2, y2:R
vadd {| x := x0; y := y0 |}
  (vadd {| x := x1; y := y1 |} {| x := x2; y := y2 |}) =
vadd
  (vadd {| x := x0; y := y0 |} {| x := x1; y := y1 |})
  {| x := x2; y := y2 |} cbv.
x0, y0, x1, y1, x2, y2:R
{| x := x0 + (x1 + x2); y := y0 + (y1 + y2) |} =
{| x := x0 + x1 + x2; y := y0 + y1 + y2 |} f_equal; ring. Qed.

Theorem vadd_comm : forall u v, vadd u v = vadd v u.
forall u v : V2, vadd u v = vadd v u
   intros.
u, v:V2
vadd u v = vadd v u destruct u, v.
x0, y0, x1, y1:R
vadd {| x := x0; y := y0 |} {| x := x1; y := y1 |} =
vadd {| x := x1; y := y1 |} {| x := x0; y := y0 |} cbv.
x0, y0, x1, y1:R
{| x := x0 + x1; y := y0 + y1 |} =
{| x := x1 + x0; y := y1 + y0 |} f_equal; ring. Qed.

(* We can notice a pattern in the proofs here that we can abstract *)

Ltac v2_tac :=
   intros;
   repeat match goal with
   | [ u : V2 |- _ ] => destruct u
   end;
   cbv ; f_equal; ring.

Theorem v2_distrib : forall s u v, smul s (vadd u v) = vadd (smul s u) (smul s v).
forall (s : R) (u v : V2),
smul s (vadd u v) = vadd (smul s u) (smul s v)
   v2_tac. Qed.

Require Import Psatz.
Theorem cauchy_schwartz_v2 : forall u v, (dot u v) ^ 2 <= (dot v v) * (dot u u).
forall u v : V2, dot u v ^ 2 <= dot v v * dot u u
   intros.
u, v:V2
dot u v ^ 2 <= dot v v * dot u u destruct u, v.
x0, y0, x1, y1:R
dot {| x := x0; y := y0 |} {| x := x1; y := y1 |} ^ 2 <=
dot {| x := x1; y := y1 |} {| x := x1; y := y1 |} *
dot {| x := x0; y := y0 |} {| x := x0; y := y0 |} unfold dot.
x0, y0, x1, y1:R
(x {| x := x0; y := y0 |} * x {| x := x1; y := y1 |} +
 y {| x := x0; y := y0 |} * y {| x := x1; y := y1 |})
^ 2 <=
(x {| x := x1; y := y1 |} * x {| x := x1; y := y1 |} +
 y {| x := x1; y := y1 |} * y {| x := x1; y := y1 |}) *
(x {| x := x0; y := y0 |} * x {| x := x0; y := y0 |} +
 y {| x := x0; y := y0 |} * y {| x := x0; y := y0 |}) simpl.
x0, y0, x1, y1:R
(x0 * x1 + y0 * y1) * ((x0 * x1 + y0 * y1) * 1) <=
(x1 * x1 + y1 * y1) * (x0 * x0 + y0 * y0) Abort. (* psatz R. Qed. *) (* Alectryon doesn't like this one for some reason, but it passes when run manually. *)

(* We can define matrix multiplication *)
Record M2 := {
   a : R; b : R;
   c : R; d : R
}.


Definition mmul m v :=
   {|
   x := m.(a) * v.(x) + m.(b) * v.(y);
   y := m.(c) * v.(x) + m.(d) * v.(y)  
   |}.

Theorem mat_scalar_mul_comm : forall m s v, mmul m (smul s v) = smul s (mmul m v).
forall (m : M2) (s : R) (v : V2),
mmul m (smul s v) = smul s (mmul m v)
   intros.
m:M2
s:R
v:V2
mmul m (smul s v) = smul s (mmul m v) destruct m, v.
a0, b0, c0, d0, s, x0, y0:R
mmul {| a := a0; b := b0; c := c0; d := d0 |}
  (smul s {| x := x0; y := y0 |}) =
smul s
  (mmul {| a := a0; b := b0; c := c0; d := d0 |}
     {| x := x0; y := y0 |}) cbv.
a0, b0, c0, d0, s, x0, y0:R
{|
x := a0 * (s * x0) + b0 * (s * y0);
y := c0 * (s * x0) + d0 * (s * y0) |} =
{|
x := s * (a0 * x0 + b0 * y0);
y := s * (c0 * x0 + d0 * y0) |} f_equal; ring. Qed.

(* Update our tactic slightly to destruct the matrices also. *)

Ltac m2_tac :=
   intros;
   repeat match goal with
   | [ u : V2 |- _ ] => destruct u
   | [ m : M2 |- _ ] => destruct m
   end;
   cbv ; f_equal; ring.

Goal forall m u v, mmul m (vadd u v) = vadd (mmul m u) (mmul m v).
forall (m : M2) (u v : V2),
mmul m (vadd u v) = vadd (mmul m u) (mmul m v)
   m2_tac. Qed.

Close Scope R_scope.

Summing N

Proving a closed form of the sum of 1 to n.

Fixpoint sumn n := match n with
 | O => O
 | S n' => n + sumn n'
end.

Goal forall n, 2 * sumn n = (n * (n + 1)).
forall n : nat, 2 * sumn n = n * (n + 1) intros.
n:nat
2 * sumn n = n * (n + 1)
   induction n.
2 * sumn 0 = 0 * (0 + 1)
n:nat
IHn:2 * sumn n = n * (n + 1)
2 * sumn (S n) = S n * (S n + 1) reflexivity.
n:nat
IHn:2 * sumn n = n * (n + 1)
2 * sumn (S n) = S n * (S n + 1) simpl.
n:nat
IHn:2 * sumn n = n * (n + 1)
S (n + sumn n + S (n + sumn n + 0)) =
S (n + 1 + n * S (n + 1)) ring [IHn]. Qed.

Two Sort

I like two_sort as an example. It's a sorting function that does not require induction, so for a beginner, I feel like its a nice pedagogical thing to talk about. You can find more complicated sorts proved in Vol 3 of Software Foundations https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html

Definition two_sort x y :=
   if (le_dec x y) then (x, y) else (y, x).

Goal forall x y, let (x', y') := two_sort x y in
         x' <= y' /\  
         ( (x = x' /\ y = y') \/ (y = x' /\ x = y') ).
forall x y : nat,
let (x', y') := two_sort x y in
x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y')
         intros x y.
x, y:nat
let (x', y') := two_sort x y in
x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y') unfold two_sort.
x, y:nat
let (x', y') :=
  if le_dec x y then (x, y) else (y, x) in
x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y')
         destruct (le_dec x y).
x, y:nat
l:x <= y
x <= y /\ (x = x /\ y = y \/ y = x /\ x = y)
x, y:nat
n:~ x <= y
y <= x /\ (x = y /\ y = x \/ y = y /\ x = x) auto.
x, y:nat
n:~ x <= y
y <= x /\ (x = y /\ y = x \/ y = y /\ x = x) lia. Qed.

There Ya Go

So you see that it isn't that much harder if you lean on automation to do these problems in Coq rather than Z3. However, having said that, I did not do the most impressive tasks from the tutorial. Verifying a neural network or a sorting network are worthy blogposts in their own right. Anton Trunov on twitter makes a good point: "In addition to the automatic tactics covered in the post, you might want to check things like field, congruence (EUF solver), intuition, firstorder, and some powerful combinations like 'firstorder congruence'. And also, CoqHammer's sauto and hammer, see <https://github.com/lukaszcz/coqhammer>" By no means are the techniques shown here the end of the road. I have not even covered all the low hanging fruit. If you liked this, you may also enjoy the programming flavored tutorial I wrote on Learn X in Y minutes <https://learnxinyminutes.com/docs/coq/>