From 1d9884391cbd5c2d506232a47fb45770178c0602 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 12 Mar 2020 14:23:05 +0100
Subject: [PATCH] fixes

---
 encodings/cert_f.lp         |  1 -
 prelude/cert_f/functions.lp | 32 +++++++++++++++-----------------
 prelude/cert_f/numbers.lp   | 10 ++++++++++
 3 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 082c2ff..ae93b3c 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -90,7 +90,6 @@ definition ↓ {T} ≔ pair {T}
 
 definition arrow {sA} {sB} (A: Univ sA) (B: Univ sB) ≔ prod A (λ_, B)
 set infix left 5 "~>" ≔ arrow
-
 // Builtins
 definition T ≔ Term {Type}
 set builtin "T" ≔ T
diff --git a/prelude/cert_f/functions.lp b/prelude/cert_f/functions.lp
index 4cdd088..5d25812 100644
--- a/prelude/cert_f/functions.lp
+++ b/prelude/cert_f/functions.lp
@@ -1,46 +1,44 @@
 require open encodings.cert_f
-adlib.cert_f.booleans
+adlib.cert_f.bootstrap
 prelude.cert_f.logic
 require adlib.cert_f.subtype as S
 
-definition arrow (D R: Term uType) ≔ prod D (λ_, R)
-
 //
 // functions [D, R: TYPE]
 //
 
-definition {|injective?|} {D} {R} (f: Term (arrow D R))
+definition {|injective?|} {D} {R} (f: Term (D ~> R))
   ≔ forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
 
-definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (arrow D R))
+definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R))
   ≔ forall (λy, ∃ (λx, (f x) = y))
 
-definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (arrow D R))
+definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R))
   ≔ ({|injective?|} f) ∧ ({|surjective?|} f)
 
-theorem bij_is_inj (D R: Term uType):
-  Term (Psub {arrow D R} {|bijective?|} ⊑ Psub {arrow D R} {|injective?|})
+theorem bij_is_inj {D: Term uType} {R: Term uType}:
+  Term (Psub {D ~> R} {|bijective?|} ⊑ Psub {D ~> R} {|injective?|})
 proof
 admit
 
-theorem bij_is_surj (D R: Term uType):
-  Term (Psub {arrow D R} {|bijective?|} ⊑ Psub {arrow D R} {|surjective?|})
+theorem bij_is_surj {D: Term uType} {R: Term uType}:
+  Term (Psub {D ~> R} {|bijective?|} ⊑ Psub {D ~> R} {|surjective?|})
 proof
 admit
 
-symbol domain {D: Term uType} {R: Term uType} (f: Term (arrow D R)): Term uType
+symbol domain {D: Term uType} {R: Term uType} (f: Term (D ~> R)): Term uType
 rule domain {&D} {_} _ → &D
 
 //
 // restrict[T: TYPE, S: TYPE FROM T, R: TYPE]
 //
 symbol restrict {T: Term uType} (S: Term uType) {R: Term uType}
-  (f: Term (arrow T R)) (_: Term (S ⊑ T)) (s: Term S)
+  (f: Term (T ~> R)) (_: Term (S ⊑ T)) (s: Term S)
   : Term R
 rule restrict {&T} _ {_} &f &pr &s → &f (↑ &T &pr &s)
 
-theorem injective_restrict {T} {R} (f: Term (arrow T R))
-  (S: Term uType) (pr: Term (S ⊑ T))
+theorem injective_restrict {T} S {R} (f: Term (T ~> R))
+  (pr: Term (S ⊑ T))
   : Term ({|injective?|} f) ⇒ Term ({|injective?|} (restrict S f pr))
 proof
 admit
@@ -49,8 +47,8 @@ admit
 // restrict_props[T: TYPE, R: TYPE]
 //
 
-theorem restrict_full {T: Term uType} {R: Term uType} (f: Term (arrow T R))
-  : Term (eq {arrow T R} (restrict {T} T {R} f (S.refl T)) f)
+theorem restrict_full {T: Term uType} {R: Term uType} (f: Term (T ~> R))
+  : Term (eq {T ~> R} (restrict {T} T {R} f (S.refl T)) f)
 proof
 admit
 
@@ -61,7 +59,7 @@ admit
 definition extend {T: Term uType}
   (s_pred: Term (pred T))
   {R: Term uType} (d: Term R)
-  (f: Term (arrow (Psub s_pred) R))
+  (f: Term (Psub s_pred ~> R))
   (t: Term T)
   (pr: Term (s_pred t))
   ≔ if (s_pred t) (f (↓ s_pred t pr)) d
diff --git a/prelude/cert_f/numbers.lp b/prelude/cert_f/numbers.lp
index 8fccf42..42ba6f7 100644
--- a/prelude/cert_f/numbers.lp
+++ b/prelude/cert_f/numbers.lp
@@ -22,6 +22,13 @@ set infix left 6 "+" ≔ {|+|}
 symbol {|-|}: Term numfield ⇒ Term numfield ⇒ Term numfield
 set infix left 6 "-" ≔ {|-|}
 
+// Other way to extend type of functions,
+symbol ty_plus: Term uType ⇒ Term uType ⇒ Term uType
+symbol polyplus {T: Term uType} {U: Term uType}
+: Term T ⇒ Term U ⇒ Term (ty_plus T U)
+// plus is defined on numfield
+rule ty_plus numfield numfield → numfield
+
 symbol commutativ_add (x y: Term numfield): Term ((x + y) = (y + x))
 symbol associative_add (x y z: Term numfield): Term (x + (y + z) = (x + y) + z)
 // FIXME add a cast on zero?
@@ -51,6 +58,8 @@ symbol closed_plus_real: ∀(x y: Term real),
   let ynf ≔ ↑ numfield pr y in
   Term (real_pred (xnf + ynf))
 
+// With polymorphic plus
+rule ty_plus real real → real
 
 symbol lt (x y: Term real): Term bool
 set infix 6 "<" ≔ lt
@@ -95,6 +104,7 @@ symbol closed_plus_rat (x y: Term rat):
   let ynf ≔ ↑ numfield (S.restr numfield real_pred) yreal in
   let sum ≔ xnf + ynf in
   Term (rational_pred (↓ real_pred sum (closed_plus_real xreal yreal)))
+rule ty_plus rat rat → rat
 
 definition nonneg_rat_pred (x: Term rational) ≔ (↑ real rat_is_real x) >= zero
 definition nonneg_rat ≔ Psub nonneg_rat_pred
-- 
GitLab