rat.lp

require open
    personoj.encodings.cert_f
    personoj.adlib.bootstrap
    personoj.prelude.logic

require personoj.sandbox.nat as N

set builtin "0" ≔ N.zero
set builtin "+1" ≔ N.succ

constant symbol Rat : Term uType
constant symbol zero : Term Rat

symbol rat : Term N.Nat ⇒ Term N.Nznat ⇒ Term Rat
set infix 8 "/" ≔ rat

symbol times : Term Rat ⇒ Term Rat ⇒ Term Rat

rule times (rat &a &b) (rat &c &d) →
  let bv ≔ fst &b in
  let dv ≔ fst &d in
  rat
   (N.times &a &c)
   (N.nznat
    (N.times bv dv)
    (N.prod_not_zero bv dv
     (snd &b)
     (snd &d)))

symbol rateq : Term Rat ⇒ Term Rat ⇒ Term bool
rule rateq (&a / &b) (&c / &d) →
  let nzval x ≔ fst x in
  (N.times &a (nzval &d)) = (N.times (nzval &b) &c)

definition onz : Term N.Nznat ≔ N.nznat 1 N.one_not_zero

// NOTE: we use this rewriting rule because in the proof below, calling simpl
// causes protected [opair] to appear, and we cannot use refl since it requires
// the user to input the protected opair, which is forbidden.
// Perhaps using [hints] could help, using [refl Nat _] and the unification
// engine would instantiate _ accordingly, but it is not likely since it is
// based on non linearity, and hints are linear.
// We rather reduce the proof to the trivial proof
rule &x = &x → true
theorem right_cancellation (a: Term N.Nat) (b: Term N.Nznat):
    Term (rateq (times (a / b) ((fst b) / onz)) (a / onz))
proof
    assume a b
    simpl
    refine N.prod_comm a (fst b)
qed