no unif hints

README.md

@@ -13,7 +13,7 @@ library, also known as _Prelude_. The prelude is available
 
 
 ## Requirements
-- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `unif_hint`
+- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `heavy-let`
   branch
 
 ## Structure

encodings/cert_f.lp

@@ -26,8 +26,6 @@ injective symbol Term {s: Sort}: Univ s ⇒ TYPE
 rule Term uProp → Univ Prop
  and Term uType → Univ Type
 
-hint Term &x ≡ Univ Prop → &x ≡ uProp
-
 // [prod s1 s2 A B] encodes [Π x : (A: s1). (B: s2)]
 symbol prod {sA: Sort} {sB: Sort} (A: Univ sA):
   (Term A ⇒ Univ sB) ⇒ Univ (Rule sA sB)
@@ -68,6 +66,8 @@ protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
 rule pair {&T} &P &M _ → opair &T &P &M
 
 rule fst (opair _ _ &M) → &M
+// and opair _ &P (fst {_} {&P} &X) → &X // Surjective pairing
+//NOTE: can we remove non linearity?
 
 // The subtype relation
 symbol subtype: Term uType ⇒ Term uType ⇒ Term uProp

prelude/functions.lp

@@ -7,6 +7,10 @@ require personoj.adlib.subtype as S
 // functions [D, R: TYPE]
 //
 
+// symbol
+// extensionality_postulate (D R: Term uType) (f g: Term (D ~> R))
+// : Term (biff (forall (λx: Term D, f x = g ) (f = g)))
+
 definition {|injective?|} {D} {R} (f: Term (D ~> R))
   ≔ forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
 

prelude/logic.lp

@@ -28,8 +28,9 @@ symbol if {T: Term uType}: Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
 //
 // boolean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: Term (neq false true)
-constant symbol bool_inclusive A: Term ((eq A false) ∨ (eq A true))
+constant symbol bool_exclusive: Term (neq {bool} false true)
+constant symbol
+bool_inclusive A: Term ((eq {bool} A false) ∨ (eq {bool} A true))
 
 theorem excluded_middle (A: Term bool): Term (A ∨ ¬ A)
 proof
@@ -45,16 +46,16 @@ qed
 //
 // xor_def
 //
-definition xor (a b: Term bool) ≔ neq a b
+definition xor (a b: Term bool) ≔ neq {bool} a b
 
 theorem xor_def (a b: Term bool):
-  Term (eq (xor a b) (if a (bnot b) b))
+  Term (eq {bool} (xor a b) (if {bool} a (bnot b) b))
 proof
 refine I.disjunction
-  (λa: Term bool, forall (λb, eq (xor a b) (if a (bnot b) b)))
+  (λa: Term bool, forall {bool} (λb, eq {bool} (xor a b) (if {bool} a (bnot b) b)))
   ?Cf ?Ct
 refine I.disjunction
-  (λ b, eq (xor false b) (if false (bnot b) b))
+  (λ b, eq {bool} (xor false b) (if {bool} false (bnot b) b))
   ?Ccf ?Cct
 admit
 
@@ -122,6 +123,6 @@ print
 admit
 
 theorem lift_if2 (S: Term uType) (a b c: Term bool) (x y: Term S):
-  Term ((if (if a b c) x y) = (if a (if b x y) (if c x y)))
+  Term ((if (if {bool} a b c) x y) = (if a (if b x y) (if c x y)))
 proof
 admit

prelude/numbers.lp

@@ -57,7 +57,7 @@ symbol closed_plus_real: ∀(x y: Term real),
   let ynf ≔ ↑ numfield pr y in
   Term (real_pred (xnf + ynf))
 
-hint Term &x ≡ Univ Type → &x ≡ uType
+// hint Term &x ≡ Univ Type → &x ≡ uType
 
 // With polymorphic plus
 rule ty_plus real real → real
@@ -93,7 +93,7 @@ proof
   refine S.restr real rational_pred
 qed
 
-hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
+// hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
 theorem rat_is_real_auto: Term (rational ⊑ real)
 proof
   apply S.restr _ _