Add a little example about Fibonacci to examples/misc

HOL-Theorem-Prover · Jan 6, 2024 · 9927975 · 9927975
1 parent ba2cfb3
commit 9927975
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 1 deletion.
diff --git 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
@@ -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();