introduction of unification 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 `local-let`
+- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `unif_hint`
   branch
 
 ## Structure

encodings/cert_f.lp

@@ -26,6 +26,8 @@ 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)

prelude/cert_f/logic.lp

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