From 2b505dd4bc46fba7ecc3455a91b345a42bf4df3d Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 17 Mar 2020 16:52:25 +0100
Subject: [PATCH] introduction of unification hints

---
 README.md               |  2 +-
 encodings/cert_f.lp     |  2 ++
 prelude/cert_f/logic.lp | 14 +++++++-------
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index 1390244..6fa3d64 100644
--- a/README.md
+++ b/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
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index ae93b3c..6be9e6c 100644
--- a/encodings/cert_f.lp
+++ b/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)
diff --git a/prelude/cert_f/logic.lp b/prelude/cert_f/logic.lp
index 3247a3f..18ee520 100644
--- a/prelude/cert_f/logic.lp
+++ b/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
-- 
GitLab