From 6a97438b4d78e5dfabf35587ac60056ec1a5db12 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 31 Jan 2020 13:29:05 +0100
Subject: [PATCH] rat & nat

---
 adlib/cert_f/nat.lp   | 15 +++++++++++++++
 sandbox/cert_f/rat.lp | 20 ++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 adlib/cert_f/nat.lp
 create mode 100644 sandbox/cert_f/rat.lp

diff --git a/adlib/cert_f/nat.lp b/adlib/cert_f/nat.lp
new file mode 100644
index 0000000..53cd195
--- /dev/null
+++ b/adlib/cert_f/nat.lp
@@ -0,0 +1,15 @@
+require open encodings.cert_f prelude.cert_f.booleans
+prelude.cert_f.equalities prelude.cert_f.notequal
+prelude.cert_f.naturalnumbers
+
+definition not_zero ≔ neq 0
+definition nznat ≔ psub nat not_zero
+
+symbol times : Term nat ⇒ Term nat ⇒ Term nat
+
+symbol prod_not_zero (x y: Term nat):
+  Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
+
+// Constructor of nznat
+definition nznatc (x: Term nat) (h: Term (not_zero x)) ≔
+  pair not_zero x h
diff --git a/sandbox/cert_f/rat.lp b/sandbox/cert_f/rat.lp
new file mode 100644
index 0000000..c48a322
--- /dev/null
+++ b/sandbox/cert_f/rat.lp
@@ -0,0 +1,20 @@
+require open encodings.cert_f prelude.cert_f.booleans
+prelude.cert_f.equalities prelude.cert_f.notequal
+prelude.cert_f.naturalnumbers prelude.cert_f.int
+require adlib.cert_f.nat as N
+
+constant symbol rat : Univ Type
+constant symbol zero : Term rat
+
+symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
+
+symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
+
+rule times (frac &a &b) (frac &c &d) →
+  let bv ≔ @fst nat N.not_zero &b in
+  let bpr ≔ @snd nat N.not_zero &b in
+  let dv ≔ @fst nat N.not_zero &d in
+  let dpr ≔ @snd nat N.not_zero &d in
+  frac
+   (N.times &a &c)
+   (N.nznatc (N.times bv dv) (N.prod_not_zero bv dv bpr dpr))
-- 
GitLab