rat & nat

adlib/cert_f/nat.lp

+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

sandbox/cert_f/rat.lp

+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))