changed notations

.dir-locals.el

@@ -4,5 +4,6 @@
 ((lambdapi-mode
   (eval set-local-abbrevs
         '(("subtype" "⊑" nil)
-          ("upcast" "↑" nil)))
+          ("upcast" "↑" nil)
+          ("downcast" "↓" nil)))
   (eval abbrev-mode)))

adlib/cert_f/subtype.lp

@@ -8,14 +8,14 @@ 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 refl eA: Term (eA ⊑ eA)
-symbol restr eA P: Term (ePsub eA P ⊑ eA)
+symbol refl T: Term (T ⊑ T)
+symbol restr T P: Term (Psub T P ⊑ T)
 
-symbol trans (eA eB eC: Term uType):
-  Term (eA ⊑ eB) ⇒ Term (eB ⊑ eC) ⇒ Term (eA ⊑ eC)
+symbol trans (T U V: Term uType):
+  Term (T ⊑ U) ⇒ Term (U ⊑ V) ⇒ Term (T ⊑ V)
 
-symbol sub {eT eS: Term uType}
-  (P: Term eT ⇒ Term bool) (Q: Term eS ⇒ Term bool)
-  (psubt: Term (eT ⊑ eS)): // Proof of eT ⊑ eS
-  Term (forall (λx, imp (P x) (Q (↑ eS psubt x)))) ⇒
-  Term (ePsub eT P ⊑ ePsub eS Q)
+symbol sub {T S: Term uType}
+  (P: Term T ⇒ Term bool) (Q: Term S ⇒ Term bool)
+  (psubt: Term (T ⊑ S)): // Proof of eT ⊑ eS
+  Term (forall (λx, imp (P x) (Q (↑ S psubt x)))) ⇒
+  Term (Psub T P ⊑ Psub S Q)

encodings/cert_f.lp

@@ -37,45 +37,51 @@ rule Term (@prod &s1 &s2 &A &B) → ∀ x : @Term &s1 &A, @Term &s2 (&B x)
 // can be seen as a dependant pair type with
 // - first element is a term of some type [A] and
 // - second is a predicate on [A] verified by the first element.
-symbol ePsub (A : Term uType) : (Term A ⇒ Term uProp) ⇒ Term uType
+symbol Psub (T : Term uType) : (Term T ⇒ Term uProp) ⇒ Term uType
 
-// Γ ⊢ M : { v : T | U }
+// Γ ⊢ M : { v : T | P }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-symbol fst {T : Univ Type} (U : Term T ⇒ Univ Prop): Term (ePsub T U) ⇒ Term T
+symbol fst {T: Univ Type} (P: Term T ⇒ Univ Prop): Term (Psub T P) ⇒ Term T
 
-//  Γ ⊢ M : { v : T | U }
+//  Γ ⊢ M : { v : T | P }
 // ——————————————————————————PROJr
-// Γ ⊢ snd(M) : U[v ≔ fst(M)]
-constant symbol snd {T: Univ Type} (U: Term T ⇒ Univ Prop)
-  (M: Term (ePsub T U)):
-  Term (U (fst U M))
+// Γ ⊢ snd(M) : P[v ≔ fst(M)]
+constant symbol snd {T: Univ Type} (P: Term T ⇒ Univ Prop)
+  (M: Term (Psub T P)):
+  Term (P (fst P M))
 
 // An inhabitant of a predicate subtype, that is, a pair of
 // an element and the proof that it satisfies the predicate
-// Γ ⊢ M : T    Γ ⊢ N : U[v ≔ M]    Γ ⊢ { v : T | U }
+// Γ ⊢ M : T    Γ ⊢ N : P[v ≔ M]    Γ ⊢ { v : T | P }
 // ——————————————————————————————————————————————————PAIR
-//           Γ ⊢ ⟨M, N⟩ : {v : T | U}
-symbol pair {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term T):
-  Term (U M) ⇒ Term (ePsub T U)
+//           Γ ⊢ ⟨M, N⟩ : {v : T | P}
+symbol pair {T: Univ Type} (P: Term T ⇒ Univ Prop) (M: Term T):
+  Term (P M) ⇒ Term (Psub T P)
 
-rule fst &U (pair &U &M _) → &M
+// FIXME: unification should allow to remove non linearity
+rule fst &P (pair &P &M _) → &M
 
 // opair is a pair forgetting its snd argument
-protected symbol opair (T: Univ Type) (U: Term T ⇒ Univ Prop) (M: Term T):
-  Term (ePsub T U)
+protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
+  Term (Psub T P)
 
 // Two pairs are convertible if their first element is
-rule pair {&T} &U &M _ → opair &T &U &M
+rule pair {&T} &P &M _ → opair &T &P &M
 
 // The subtype relation
 symbol subtype: Term uType ⇒ Term uType ⇒ Term uProp
 set infix left 6 "⊑" ≔ subtype
 
-// [cast eA eB p t] casts element [t] from type [eA] to type [eB] given
-// the proof [p] that [eA] is a subtype of [eB]
-symbol cast {eA: Term uType} (eB: Term uType):
-  Term (eA ⊑ eB) ⇒ Term eA ⇒ Term eB
+// [↑ {T} U p t] casts element [t] from type [T] to type [U] given
+// the proof [p] that [T] is a subtype of [U]
 set declared "↑"
-definition ↑ {eA: Term uType} ≔ cast {eA}
-rule cast {&eA} &eA _ &x → &x
+symbol ↑ {T: Term uType} (U: Term uType):
+  Term (T ⊑ U) ⇒ Term T ⇒ Term U
+rule ↑ {&T} &T _ &x → &x // Identity cast
+// NOTE: a cast from a type [{x: A | P}] to type [A] is a [fst],
+// and a "downcast" is the pair constructor
+set declared "↓"
+symbol ↓ {T: Term uType} (P: Term T ⇒ Term uProp) (x: Term T):
+  Term (P x) ⇒ Term (Psub T P)
+// NOTE: we can only down-cast from a type to its direct sub-type

prelude/cert_f/logic.lp

@@ -11,6 +11,7 @@ require adlib.cert_f.subtype as S
 // Equalities
 //
 symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp
+set infix 5 "=" ≔ eq
 
 // NOTE not in the prelude
 constant symbol cast_trans (A B C: Term uType) (prab: Term (A ⊑ B)) (prbc: Term (B ⊑ C))

prelude/cert_f/numbers.lp

 require adlib.cert_f.subtype as S
 require open encodings.cert_f
 adlib.cert_f.booleans
+adlib.cert_f.numerals
 prelude.cert_f.logic
 
 //
@@ -12,16 +13,26 @@ constant symbol number: Term uType
 // Theory number_fields
 //
 symbol field_pred: Term number ⇒ Univ Prop
-definition number_field ≔ ePsub number field_pred
+definition number_field ≔ Psub number field_pred
 // number_field is an uninterpreted subtype
 definition numfield ≔ number_field
 
+symbol {|+|}: Term numfield ⇒ Term numfield ⇒ Term numfield
+set infix left 6 "+" ≔ {|+|}
+symbol {|-|}: Term numfield ⇒ Term numfield ⇒ Term numfield
+set infix left 6 "-" ≔ {|-|}
+
+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?
+// symbol identity_add (x: Term numfield): Term (x + zero = x)
+
 
 //
 // reals
 //
 symbol real_pred: Term (pred numfield)
-definition real ≔ ePsub numfield real_pred
+definition real ≔ Psub numfield real_pred
 theorem real_not_empty: Term (∃ real_pred)
 proof admit
 
@@ -29,7 +40,7 @@ constant symbol zero : Term real
 // Built in the PVS typechecker
 
 definition nonzero_real_pred ≔ neq zero
-definition nonzero_real ≔ ePsub real nonzero_real_pred
+definition nonzero_real ≔ Psub real nonzero_real_pred
 theorem nonzero_real_not_empty: Term (∃ nonzero_real_pred)
 proof admit
 definition nzreal ≔ nonzero_real
@@ -55,7 +66,7 @@ set infix 7 ">=" ≔ geq
 // rationals
 //
 symbol rational_pred: Term (pred real)
-definition rational ≔ ePsub real rational_pred
+definition rational ≔ Psub real rational_pred
 theorem rational_not_empty: Term (∃ rational_pred)
 proof admit
 
@@ -67,12 +78,12 @@ qed
 
 definition nonzero_rational_pred (x: Term rational): Term bool ≔
   neq zero (↑ real rat_is_real x)
-definition nonzero_rational ≔ ePsub rational nonzero_rational_pred
+definition nonzero_rational ≔ Psub rational nonzero_rational_pred
 definition nzrat ≔ nonzero_rational
 
 
 definition nonneg_rat_pred (x: Term rational) ≔ (↑ real rat_is_real x) >= zero
-definition nonneg_rat ≔ ePsub rational nonneg_rat_pred
+definition nonneg_rat ≔ Psub rational nonneg_rat_pred
 
 theorem nonneg_rat_is_real: Term (nonneg_rat ⊑ real)
 proof
@@ -83,7 +94,7 @@ proof
 qed
 
 definition posrat_pred (x: Term nonneg_rat) ≔ (↑ real nonneg_rat_is_real x) > zero
-definition posrat ≔ ePsub nonneg_rat posrat_pred
+definition posrat ≔ Psub nonneg_rat posrat_pred
 
 symbol div: Term real ⇒ Term nonzero_real ⇒ Term real
 set infix left 8 "/" ≔ div
@@ -112,7 +123,7 @@ type λ (r: Term real) (q: Term posrat), r /
 // integers
 //
 symbol integer_pred: Term (pred rational)
-definition integer ≔ ePsub rational integer_pred
+definition integer ≔ Psub rational integer_pred
 // Proof of existence because NONEMPTY_TYPE
 theorem integer_not_empty: Term (∃ integer_pred)
 proof
@@ -121,5 +132,8 @@ definition int ≔ integer
 
 symbol natz : Term int
 
-definition nonzero_integer ≔ ePsub int (neq natz)
+definition nonzero_integer ≔ Psub int (neq natz)
 definition nzint ≔ nonzero_integer
+
+// symbol closed_plus (i j: Term int):
+//   Term (integer_pred ((↑ real _ i) + (↑ real _ j)))