From 66cfe53282010d36eccb2a3994a8decd6d29b5e8 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 24 Mar 2020 09:42:48 +0100
Subject: [PATCH] a proof on even numbers

---
 sandbox/nat.lp | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/sandbox/nat.lp b/sandbox/nat.lp
index 5141595..d600d58 100644
--- a/sandbox/nat.lp
+++ b/sandbox/nat.lp
@@ -24,7 +24,7 @@ rule (succ &n) *       &m  → &n * &m + &m
  and       &n  * (succ &m) → &n * &m + &n
  and        _  * 0         → 0
 
-symbol prod_comm (x y: Term Nat): Term (eq (times x y) (times y x))
+symbol prod_comm (x y: Term Nat): Term ((x * y) = (y * x))
 
 
 //
@@ -45,3 +45,16 @@ symbol one_not_zero: Term (not_zero 1)
 
 symbol induction (P: Term Nat ⇒ Term bool):
   ∀n, Term (P 0) ⇒ Term (P (n + 1)) ⇒ ∀m, Term (P m)
+
+// Divisions
+definition div (x y: Term Nat) ≔ ∃ (λk, x * k = y)
+definition even (x: Term Nat) ≔ div 2 x
+definition Even ≔ Psub even
+
+theorem even_stable_double: ∀x: Term Even, Term (even (2 * (fst x)))
+proof
+    assume x h
+    refine (h (fst x) _)
+    simpl
+    refine reflexivity_of_equal _ ((fst x) + (fst x))
+qed
-- 
GitLab