Some fixes

- renamed subtype to subtype_poly
- pi function does not have implicit arguments anymore
- changed a rewrite rule into an axiom
- added wip tuples

encodings/ad_hoc.lp

-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.subtype
-
-// A possible encoding of ad-hoc polymorphism.
-// Should be made prenex.
-set declared "∀ah"
-constant symbol ∀ah: Set → (Set → Set) → Set
-rule η (∀ah $a $b) ↪ Π(c: Set) (h: ε (c ~ $a)) (x: η c),
-                     ε (π {$a} (eqcast h (↑ x))) → η ($b c)
-// TODO: work on implicitness of argument of π

encodings/subtype.lp → encodings/subtype_poly.lp

+/// Sub-type polymorphism
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.bool_hol
+require open personoj.encodings.tuple
+require open personoj.encodings.prenex
 
 set declared "μ"
 set declared "μ₀"
@@ -16,23 +19,27 @@ with μ (tuple_t $T $U) ↪ tuple_t (μ $T) (μ $U)
 with μ (arrd $b) ↪ arrd (λx, μ ($b x))
 with μ (μ $T) ↪ μ $T // FIXME: can be proved
 
-symbol π {T: Set}: η (μ T) → Bool
+symbol π (T: Set): η (μ T) → Bool
 
 // Casting from/to maximal supertype
 constant symbol maxcast {t: Set}: η t → η (μ t)
-constant symbol downcast {t: Set} (x: η (μ t)): ε (π {μ t} x) → η t
+constant symbol downcast {t: Set} (x: η (μ t)): ε (π (μ t) x) → η t
 definition ↑ {t} ≔ maxcast {t}
 definition ↓ {t} ≔ downcast {t}
 
-rule π {$t ~> $u} ↪ λx: η $t → η (μ $u), ∀ (λy, π {$u} (x y))
-with π {tuple_t $t $u}
-   ↪ λx: η (tuple_t (μ $t) (μ $u)), π {$t} (p1 x) ∧ (λ_, π {$u} (p2 x))
-with π {psub {$t} $a}
-   ↪ λx: η (μ $t), (π {μ $t} x) ∧ (λy: ε (π {μ $t} x), $a (↓ x y))
-with π {arrd $b}
-   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π {μ ($b y)} (x y))
+rule π ($t ~> $u) ↪ λx: η $t → η (μ $u), ∀ (λy, π $u (x y))
+with π (tuple_t $t $u)
+   ↪ λx: η (tuple_t (μ $t) (μ $u)), π $t (p1 x) ∧ (λ_, π $u (p2 x))
+with π (psub {$t} $a)
+   ↪ λx: η (μ $t), (π (μ $t) x) ∧ (λy: ε (π (μ $t) x), $a (↓ x y))
+with π (arrd $b)
+   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π (μ ($b y)) (x y))
 
-rule ε (π (maxcast _)) ↪ ε true // FIXME: to  be justified
+/// A term ‘x’ that has been cast up still verifies the properties to be of its
+/// former type.
+symbol cstr_maxcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (maxcast x))))
+// or as a rewrite-rule:
+// rule ε (π _ (maxcast _)) ↪ ε true
 
 private constant symbol max_eq: Set → Set → Bool
 set infix 6 "≃" ≔ max_eq
@@ -44,7 +51,7 @@ set infix 6 "~" ≔ compatible
 
 // The one true cast
 symbol cast {fr_t: Set} (to_t: Set) (comp: ε (fr_t ~ to_t)) (m: η fr_t):
-  ε (π {to_t} (eqcast comp (maxcast m))) → η to_t
+  ε (π to_t (eqcast comp (maxcast m))) → η to_t
 
 /// Proof irrelevance
 protected symbol _cast {fr_t: Set} (to_t: Set): η fr_t → η to_t
@@ -55,28 +62,28 @@ theorem comp_same_cstr_cast
         (fr to: Set)
         (comp: ε (μ fr ≃ μ to))
         (_: ε (eq {μ fr ~> bool}
-                  (π {fr})
-                  (λx, π {to} (eqcast comp x))))
+                  (π fr)
+                  (λx, π to (eqcast comp x))))
         (x: η fr)
-      : ε (π {to} (eqcast comp (maxcast x)))
+      : ε (π to (eqcast comp (maxcast x)))
 proof
   assume fr to comp eq_cstr x
   refine eq_cstr (λf, f (maxcast x)) _
-  refine λx: ε false, x
+  refine cstr_maxcast_idem fr x
 qed
 
 rule ε ($t ≃ $t) ↪ ε true
 rule ε (($t1 ~> $u1) ≃ ($t2 ~> $u2))
    ↪ ε ((μ $t1 ≃ μ $t2)
         ∧ (λh,
-           (eq {μ $t1 ~> bool} (π {$t1}) (λx: η (μ $t1), π {$t2} (eqcast h x)))
+           (eq {μ $t1 ~> bool} (π $t1) (λx: η (μ $t1), π $t2 (eqcast h x)))
            ∧ (λ_, $u1 ≃ $u2)))
 rule ε (tuple_t $t1 $u1 ≃ tuple_t $t2 $u2)
    ↪ ε ($t1 ≃ $t2 ∧ (λ_, $u1 ≃ $u2))
 with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
    ↪ ε ((μ $t1 ≃ μ $t2)
         ∧ (λh,
-           (eq {μ $t1 ~> bool} (π {$t1}) (λx, π {$t2} (eqcast h x)))
+           (eq {μ $t1 ~> bool} (π $t1) (λx, π $t2 (eqcast h x)))
            ∧ (λh', ∀
                (λx: η $t1,
                 ($u1 x) ≃ ($u2 (cast {$t1} $t2 h x

encodings/tuple.lp

+/// WIP
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+// Non dependent tuples
+constant symbol tuple_t: Set → Set → Set
+constant symbol tuple {t} {u}: η t → η u → η (tuple_t t u)
+symbol p1 {t} {u}: η (tuple_t t u) → η t
+symbol p2 {t} {u}: η (tuple_t t u) → η u
+rule p1 (tuple $m _) ↪ $m
+rule p2 (tuple _ $n) ↪ $n
+
+constant symbol set_t: Set
+constant symbol set_nil: η set_t
+constant symbol set_cons: Set → η set_t → η set_t
+// TODO rewrite rules that transform (t, u, v) ~> w in t ~> u ~> v ~> w
+
+constant symbol TypeList: TYPE
+constant symbol type_nil: TypeList
+constant symbol type_cons: Set → TypeList → TypeList
+symbol type_cdr: TypeList → TypeList
+rule type_cdr (type_cons _ $tl) ↪ $tl
+symbol type_car: TypeList → Set
+rule type_car (type_cons $hd _) ↪ $hd
+
+constant symbol Tuple: TypeList → TYPE
+constant symbol tuple_nil: Tuple type_nil
+constant symbol tuple_cons (t: Set) (_: η t) (tl: TypeList) (_: Tuple tl):
+  Tuple (type_cons t tl)
+
+symbol tuple_car (tl: TypeList): Tuple tl → η (type_car tl)
+rule tuple_car (type_cons $t _) (tuple_cons $t $x _) ↪ $x
+symbol tuple_cdr (tl: TypeList): Tuple tl → Tuple (type_cdr tl)
+rule tuple_cdr _ (tuple_cons _ _ _ $tup) ↪ $tup

prelude/numbers.lp

@@ -4,7 +4,7 @@ require open personoj.encodings.bool_hol
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
 require open personoj.encodings.builtins
-require open personoj.encodings.subtype
+require open personoj.encodings.subtype_poly
 
 //
 // Theory numbers

tests/tuple.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.deptype
+require open personoj.encodings.prenex
+require open personoj.encodings.tuple
+
+constant symbol nat: Set
+constant symbol rat: Set
+
+
+set verbose 3
+constant symbol zn: η nat
+constant symbol zq: η rat
+definition tuple_zz ≔ tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)
+// assert tuple_car (type_cons nat _) (tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)) ≡ zn