From 992797591bcd9e429548702f43dcc45bb8d42d8c Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Sat, 6 Jan 2024 20:28:08 +1100
Subject: [PATCH] Add a little example about Fibonacci to examples/misc

---
 examples/misc/Holmakefile       |  2 +-
 examples/misc/fibmod3Script.sml | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 examples/misc/fibmod3Script.sml

diff --git a/examples/misc/Holmakefile b/examples/misc/Holmakefile
index fe26561233..d421aec1d6 100644
--- a/examples/misc/Holmakefile
+++ b/examples/misc/Holmakefile
@@ -1,4 +1,4 @@
-INCLUDES = $(dprot $(HOLDIR)/src/real) $(dprot $(HOLDIR)/src/real/analysis) $(dprot $(HOLDIR)/src/bag)
+INCLUDES = $(dprot $(HOLDIR)/src/real) $(dprot $(HOLDIR)/src/real/analysis) $(dprot $(HOLDIR)/src/bag) $(dprot $(HOLDIR)/src/integer)
 
 all: $(DEFAULT_TARGETS) euclid-OK
 .PHONY: all
diff --git a/examples/misc/fibmod3Script.sml b/examples/misc/fibmod3Script.sml
new file mode 100644
index 0000000000..e3cd80c40b
--- /dev/null
+++ b/examples/misc/fibmod3Script.sml
@@ -0,0 +1,19 @@
+open HolKernel Parse boolLib bossLib;
+
+val _ = new_theory "fibmod3";
+
+Definition fib_def:
+  fib n = if n = 0n then 1n else if n = 1 then 1 else fib (n-1) + fib (n - 2)
+End
+
+Theorem fibmod:
+  ∀n. EVEN (fib n) ⇔ n MOD 3 = 2
+Proof
+  recInduct fib_ind >> rw[] >>
+  ONCE_REWRITE_TAC [fib_def] >> rw[] >>
+  gs[arithmeticTheory.EVEN_ADD] >>
+  intLib.ARITH_TAC
+QED
+
+
+val _ = export_theory();