philzook58/z3_tut.v

## z3_tut.v
(*|

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. 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 a cross country slog.

There are a number of factors 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 automatically 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 that are just the water that Coq users 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. 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.

Still, 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 Componenets stuff makes you buy in on ssreflect style and some hardcore math topics, which are nuts I have not cracked. Also, all of them are really long and initimidating.

This was also a nice opportunity to take Alectryon out for a spin https://github.com/cpitclaudel/alectryon allowing you to see the proof state on hover over in your browser. It's a super important part of the Coq


|*)


(*|
-----------
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].

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, this may be a valid approach, use external tools to produce solutions and just manually place them into Coq.

|*)

Require Import Lia.
Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
     exists 7, 0. 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 7, 0. 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.
   do 2 eexists. eauto with arith. Show Proof. Defined.


(* A fairly manual version for comparison. Could be even worse. *)
Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
   exists 7, 0. split.
     - unfold ">". Locate "<". unfold "<". Print le. do 4 apply
              le_S. apply le_n.
     - split.
       + do 9 apply le_S. apply le_n.
       + simpl. 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. intros. assumption. Qed.

(* Even shorter proof *)
Goal forall P, 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). unfold not. intros. apply H. 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.

Goal exists x : R, x^3 + 3 * x^2 + 4 * x + 2 = 0.
  exists (- 1). 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. intros.
   nra. Qed.

(* A slightly more manual proof involving completing the square.*)
Goal forall x, x ^ 2 + 2 * x + 2 > 0.
   intros.
   assert (x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1) as H by ring.
   rewrite H. Search (0 <= _ ^ 2).
   pose (pow2_ge_0 (x + 1)).
   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.
  intros.
  assert ((x^3 + 3 * x^2 + 4 * x + 2) =
         ((x + 1) * (x ^ 2 + 2 * x + 2 ))) as H0 by ring.
  rewrite H0. pose (pos_poly x). nra. Qed.

(* A slightly more manual proof *)
Goal forall x, x + 1 <> 0 -> (x^3 + 3 * x^2 + 4 * x + 2) <> 0.
  intros.
  assert ((x^3 + 3 * x^2 + 4 * x + 2) =
         ((x + 1) * (x ^ 2 + 2 * x + 2 ))) by ring.
  rewrite H0. pose (pos_poly x). Search (_ * _ = 0).
  apply Rmult_integral_contrapositive_currified.
  assumption. 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].

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].

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 9. exists 5. exists 6. exists 7.
   exists 1. exists 0. exists 8. exists 2.
   cbv. 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.
  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].

  (* 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.

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. intros; ring. Qed.
Goal forall x y z : R, (x + y) + z = x + (y + z). intros; ring. Qed.
Goal forall x : R, x > 0 \/ x = 0 \/ x < 0. intros. lra. Qed.
Goal forall x : R, x ^ 2 >= 0. intros. 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.
   intros. destruct u, v, w. cbv. f_equal; ring. Qed.

Theorem vadd_comm : forall u v, vadd u v = vadd v u.
   intros. destruct u, v. cbv. 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).
   v2_tac. Qed.

Require Import Psatz.
Theorem cauchy_schwartz_v2 : forall u v, (dot u v) ^ 2 <= (dot v v) * (dot u u).
   intros. destruct u, v. unfold dot. simpl. 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).
   intros. destruct m, v. cbv. 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).
   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)). intros.
   induction n. reflexivity. simpl. 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') ).
         intros x y. unfold two_sort.
         destruct (le_dec x y). auto. 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.
|*)
	(*\|

	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. 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 a cross country slog.

	There are a number of factors 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 automatically 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 that are just the water that Coq users 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. 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.

	Still, 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 Componenets stuff makes you buy in on ssreflect style and some hardcore math topics, which are nuts I have not cracked. Also, all of them are really long and initimidating.

	This was also a nice opportunity to take Alectryon out for a spin https://github.com/cpitclaudel/alectryon allowing you to see the proof state on hover over in your browser. It's a super important part of the Coq


	\|*)




	(*\|
	-----------
	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].

	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, this may be a valid approach, use external tools to produce solutions and just manually place them into Coq.

	\|*)

	Require Import Lia.
	Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
	exists 7, 0. 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 7, 0. 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.
	do 2 eexists. eauto with arith. Show Proof. Defined.


	(* A fairly manual version for comparison. Could be even worse. *)
	Goal exists x y, x > 2 /\ y < 10 /\ x + 2 * y = 7.
	exists 7, 0. split.
	- unfold ">". Locate "<". unfold "<". Print le. do 4 apply
	le_S. apply le_n.
	- split.
	+ do 9 apply le_S. apply le_n.
	+ simpl. 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. intros. assumption. Qed.

	(* Even shorter proof *)
	Goal forall P, 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). unfold not. intros. apply H. exact I. Qed.

	(*\|
	The first exercise:
	Get a root of the polynomial x*3 + 3x*2 + 4x + 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.

	Goal exists x : R, x^3 + 3 * x^2 + 4 * x + 2 = 0.
	exists (- 1). 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. intros.
	nra. Qed.

	(* A slightly more manual proof involving completing the square.*)
	Goal forall x, x ^ 2 + 2 * x + 2 > 0.
	intros.
	assert (x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1) as H by ring.
	rewrite H. Search (0 <= _ ^ 2).
	pose (pow2_ge_0 (x + 1)).
	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.
	intros.
	assert ((x^3 + 3 * x^2 + 4 * x + 2) =
	((x + 1) * (x ^ 2 + 2 * x + 2 ))) as H0 by ring.
	rewrite H0. pose (pos_poly x). nra. Qed.

	(* A slightly more manual proof *)
	Goal forall x, x + 1 <> 0 -> (x^3 + 3 * x^2 + 4 * x + 2) <> 0.
	intros.
	assert ((x^3 + 3 * x^2 + 4 * x + 2) =
	((x + 1) * (x ^ 2 + 2 * x + 2 ))) by ring.
	rewrite H0. pose (pos_poly x). Search (_ * _ = 0).
	apply Rmult_integral_contrapositive_currified.
	assumption. 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].

	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].

	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 9. exists 5. exists 6. exists 7.
	exists 1. exists 0. exists 8. exists 2.
	cbv. 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.
	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].

	(* 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.

	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. intros; ring. Qed.
	Goal forall x y z : R, (x + y) + z = x + (y + z). intros; ring. Qed.
	Goal forall x : R, x > 0 \/ x = 0 \/ x < 0. intros. lra. Qed.
	Goal forall x : R, x ^ 2 >= 0. intros. 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.
	intros. destruct u, v, w. cbv. f_equal; ring. Qed.

	Theorem vadd_comm : forall u v, vadd u v = vadd v u.
	intros. destruct u, v. cbv. 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).
	v2_tac. Qed.

	Require Import Psatz.
	Theorem cauchy_schwartz_v2 : forall u v, (dot u v) ^ 2 <= (dot v v) * (dot u u).
	intros. destruct u, v. unfold dot. simpl. 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).
	intros. destruct m, v. cbv. 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).
	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)). intros.
	induction n. reflexivity. simpl. 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') ).
	intros x y. unfold two_sort.
	destruct (le_dec x y). auto. 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.
	\|*)