nat & rat

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
+require open encodings.cert_f adlib.cert_f.booleans
+prelude.cert_f.logic
+
+constant symbol nat: Term uType
+injective symbol succ: Term nat ⇒ Term nat
+constant symbol zero: Term nat
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
 
 symbol times : Term nat ⇒ Term nat ⇒ Term nat
 symbol plus : Term nat ⇒ Term nat ⇒ Term nat
@@ -25,14 +30,16 @@ symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
 //
 
 definition not_zero ≔ neq 0
-type not_zero
 symbol prod_not_zero (x y: Term nat):
   Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
 
-definition nznat ≔ psub nat not_zero
+definition nznat ≔ ePsub nat not_zero
 
 // Constructor of nznat
 definition nznatc (x: Term nat) (h: Term (not_zero x)) : Term nznat ≔
   pair not_zero x h
 
 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)

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 open encodings.cert_f adlib.cert_f.booleans
+prelude.cert_f.logic
 require adlib.cert_f.nat as N
 
+set builtin "0" ≔ N.zero
+set builtin "+1" ≔ N.succ
+
 constant symbol rat : Univ Type
 constant symbol zero : Term rat
 
-symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
+symbol frac : Term N.nat ⇒ Term N.nznat ⇒ Term rat
 set infix 8 "/" ≔ frac
 
-symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
+symbol times : Term rat ⇒ Term rat ⇒ Term rat
 
 rule times (frac &a &b) (frac &c &d) →
   let bv ≔ fst N.not_zero &b in
@@ -29,22 +31,24 @@ rule rateq (&a / &b) (&c / &d) →
 
 definition onz : Term N.nznat ≔ N.nznatc 1 N.one_not_zero
 
-theorem rrefl (a: Term nat) (b: Term N.nznat):
+theorem rrefl (a: Term N.nat) (b: Term N.nznat):
   Term (rateq (a / b) (a / b))
 proof
 assume a b
 apply N.prod_comm a (fst N.not_zero b)
 qed
 
-theorem one_neutral (a: Term nat) (b: Term N.nznat):
-  Term (rateq (times (a / b) (1 / onz)) (1 / onz))
-proof
-assume a b
-refine N.prod_comm ?p1[a,b] ?p2[a,b]
-qed
-// theorem right_cancellation (a: Term nat) (b: Term N.nznat):
-//   Term (rateq (times (a / b) ((fst N.not_zero b) / onz)) (a / onz))
+// theorem one_neutral (a: Term N.nat) (b: Term N.nznat):
+//   Term (rateq (times (a / b) (1 / onz)) (1 / onz))
 // proof
-// assume a b
-// refine Term
 // qed
+type Term (N.nznat ⊑ N.nat)
+type λ(b: Term N.nznat) (pr: Term (N.nznat ⊑ N.nat)),
+  @↑ N.nznat N.nat pr b
+// FIXME explicitness required
+theorem right_cancellation (a: Term N.nat) (b: Term N.nznat)
+  (pr: Term (N.nznat ⊑ N.nat)):
+  Term (rateq (times (a / b) ((@↑ N.nznat N.nat pr b) / onz)) (a / onz))
+proof
+qed
+// Should generate a TCC to provide [pr]