From f6bd1bbfb869aa7087c3e729eba7a289702937e4 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 14 Apr 2020 16:32:00 +0200
Subject: [PATCH] fixed rat

---
 paper/rat.lp | 41 +++++++++++++++++++----------------------
 1 file changed, 19 insertions(+), 22 deletions(-)

diff --git a/paper/rat.lp b/paper/rat.lp
index 4cdb5ec..2596d33 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -29,15 +29,14 @@ rule Z * _ → Z
  and _ * Z → Z
  and (S &m) * &n → &n + (&m * &n)
 
-symbol nat_induction
-     : ∀P: η ℕ ⇒ Bool, ε (P 0) ⇒ (∀n, ε (P n) ⇒ ε (P (S n))) ⇒ ∀n, ε (P n)
+symbol nat_induction: ∀P: η ℕ ⇒ Bool, ε (P 0) ⇒ (∀n, ε (P n) ⇒ ε (P (S n))) ⇒ ∀n, ε (P n)
 
 symbol ¬: Bool ⇒ Bool
 rule ε (¬ &x) → ε &x ⇒ ∀(z: Bool), ε z
 symbol eqnat: η (ℕ ~> ℕ ~> bool)
 set infix left 3 "=ℕ" ≔ eqnat
 
-symbol s_not_z : ∀x: η ℕ, ε (¬ (Z =ℕ (S x)))
+symbol s_not_z: ∀x: η ℕ, ε (¬ (Z =ℕ (S x)))
 
 theorem times_comm: ε (forall (λa, forall (λb, (a * b) =ℕ (b * a))))
 proof
@@ -49,8 +48,8 @@ definition ℕ* ≔ psub {|nznat?|}
 definition Onz ≔ pair {ℕ} {{|nznat?|}} (S Z) (s_not_z Z) // One not zero
 
 symbol Snz: η ℕ* ⇒ η ℕ* // Successor not zero
-symbol nznat_induction
-: ∀P: η ℕ* ⇒ Bool, ε (P Onz) ⇒ (∀n, ε (P n) ⇒ ε (P (Snz n))) ⇒ ∀n, ε (P n)
+symbol nznat_induction:
+  ∀P: η ℕ* ⇒ Bool, ε (P Onz) ⇒ (∀n, ε (P n) ⇒ ε (P (Snz n))) ⇒ ∀n, ε (P n)
 
 symbol div: η (ℕ ~> ℕ* ~> ℚ+)
 set infix left 6 "/" ≔ div
@@ -60,18 +59,18 @@ set infix left 7 "=ℚ" ≔ eqrat
 rule (&a / &b) =ℚ (&c / &d) → (&a * (fst &d)) =ℕ ((fst &b) * &c)
 
 definition imp P Q ≔ impd {P} (λ_, Q)
+set infix left 6 "⊃" ≔ imp
 definition false ≔ forall {bool} (λx, x)
 
-theorem nzprod
-: ε (forall
-     {â„•*}
-     (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
+theorem nzprod: ε (forall
+                     {â„•*}
+                     (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
 proof
   refine nznat_induction
-         (λx, forall (λy: η ℕ*, imp (Z =ℕ (fst x * fst y)) false)) ?xOnz ?xSnz
+         (λx, forall (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
   // x = 1
   refine nznat_induction
-         (λy, imp (Z =ℕ (fst Onz * fst y)) false) ?yOnz ?ySnz
+         (λy, (Z =ℕ (fst Onz * fst y)) ⊃ false) ?yOnz ?ySnz
   simpl
   apply s_not_z Z
   // x = S n
@@ -80,24 +79,22 @@ proof
   refine snd (Snz n)
   assume n Hn
   refine nznat_induction
-         (λz, imp (Z =ℕ (fst (Snz n) * (fst z))) false) ?zOnz[n,Hn] ?zSnz[n,Hn]
+         (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n,Hn] ?zSnz[n,Hn]
   simpl
   refine snd (Snz n)
   assume m Hm
 admit
 
-definition nat_of_nznat ≔ fst {ℕ} {{|nznat?|}}
-
 symbol times_rat: η (ℚ+ ~> ℚ+ ~> ℚ+)
 rule times_rat (&a / &b) (&c / &d) →
-     let denom ≔ fst &b * (fst &d) in
-     let prf ≔ nzprod &b &d in
-     (&a * &c) / (pair denom prf)
-
-theorem right_cancel
-: ε (forall
-     (λa, forall
-          (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
+  let denom ≔ fst &b * (fst &d) in
+  let prf ≔ nzprod &b &d in
+  (&a * &c) / (pair denom prf)
+
+theorem right_cancel:
+  ε (forall
+       (λa, forall
+              (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
 proof
   assume x y
   simpl
-- 
GitLab