equality of root, builtins

adlib/cert_f/booleans.lp

@@ -21,3 +21,10 @@ set infix 7 "⇔" ≔ biff
 
 definition when (P Q: Term uProp) ≔ imp Q P
 // FIXME explicitness?
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "imp" ≔ imp
+set builtin "and" ≔ band
+set builtin "or" ≔ bor
+set builtin "not" ≔ bnot

adlib/cert_f/subtype.lp

@@ -8,10 +8,13 @@ set flag "print_implicits" on
 //    Term (&P x) ⇒ Term (&Q (↑ &B pr x))
 // FIXME 'File "src/basics.ml", line 116 character 36-42: Assertion failed'
 
-symbol root: Term uType ⇒ Term uType
-rule root (Psub &T _) → root &T
-// TODO the [sub] rule needs to check that the two types have the same root,
-// so the [eq] symbol must be loaded
+// [eqroot T U] reduces to [true] if [T] and [U] have the same root
+symbol eqroot: Term uType ⇒ Term uType ⇒ Term uProp
+rule eqroot &X &X → true // NOTE: non linear
+ and eqroot (Psub &T _) &U → eqroot &T &U
+ and eqroot &T (Psub &U _) → eqroot &T &U
+
+symbol eqtype: Term uType ⇒ Term uType ⇒ Term uProp
 
 symbol refl T: Term (T ⊑ T)
 symbol restr T P: Term (Psub T P ⊑ T)
@@ -19,11 +22,14 @@ symbol restr T P: Term (Psub T P ⊑ T)
 symbol trans (T U V: Term uType):
   Term (T ⊑ U) ⇒ Term (U ⊑ V) ⇒ Term (T ⊑ V)
 
-// [sub {U} P T π ρ] proves that, given type [U], predicate from [U],
-// type [T], proof [π] that [T] is a sub-type of [U] and proof [ρ] that
-// any element of [T] verifies [P], [T] is a sub-type of [{x: U | P}].
+// [sub {U} P T μ π ρ] proves that, given type [U], [P] predicate from [U],
+// type [T],
+// - proof [μ] that [T] has the same root as [U];
+// - proof [π] that [T] is a sub-type of [U];
+// - proof [ρ] that // any element of [T] verifies [P];
+// [T] is a sub-type of [{x: U | P}].
 symbol sub {U: Term uType} (P: Term U ⇒ Term bool) (T: Term uType)
-  (pr: Term (T ⊑ U)):
+  (_: Term (eqroot T U)) (pr: Term (T ⊑ U)):
   Term (forall (λx: Term T, P (↑ U pr x))) ⇒ Term (T ⊑ Psub U P)
 
 // symbol sub {T S: Term uType}

encodings/cert_f.lp

@@ -85,3 +85,10 @@ set declared "↓"
 // proof [π] that [t] verifies predicate [P].
 definition ↓ {T} ≔ pair {T}
 // NOTE: we can only down-cast from a type to its direct sub-type
+
+// Builtins
+definition T ≔ Term {Type}
+set builtin "T" ≔ T
+
+definition P ≔ Term {Prop}
+set builtin "P" ≔ P

prelude/cert_f/logic.lp

@@ -110,6 +110,13 @@ admit
 
 symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
 
+// FIXME: carrying builtins over import?
+set builtin "T" ≔ T
+set builtin "P" ≔ P
+// FIXME: could builtins be more flexible?
+// set builtin "eq" ≔ eq
+// set builtin "refl" ≔ reflexivity_of_equal
+
 symbol transitivity_of_equal T (x y z: Term T) :
   Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
 

prelude/cert_f/numbers.lp

@@ -121,22 +121,14 @@ admit
 theorem posrat_is_nzrat: Term (posrat ⊑ nzrat)
 proof
   // FIXME explicitness behaves strangely
-  refine @S.sub rational nonzero_rational_pred posrat ?P1 ?Fa
+  refine @S.sub rational nonzero_rational_pred posrat ?R ?P1 ?Fa
+  refine λx, x // Trivial proof that rational and posrat have the same root
   refine S.trans posrat nonneg_rat rat ?R1 ?R2
   apply S.restr nonneg_rat posrat_pred
   apply S.restr rational nonneg_rat_pred
   assume x
   // TODO finish this proof
 admit
-// With old version of S-Sub rule
-// proof
-//   // FIXME explicitness behaves strangely
-//   refine @S.sub nonneg_rat rational
-//     posrat_pred nonzero_rational_pred ?Carrier ?Imp
-//   apply S.restr rational nonneg_rat_pred
-//   assume x Pxgz Pxez
-//   // Some work needed on casts
-//   admit
 type λ (r: Term real) (q: Term posrat), r /
   (↑ nzreal _ (↑ nzrat posrat_is_nzrat q))
 ///