fine tuning of tuples

surjective pairing
projections

personoj/coercions.lp

+// FIXME: implicit arguments must be avoided in the definition of coercions
+// because they are not type checked properly.
 require open personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical personoj.sum;
 
-// coercion "set-pred" (t: Set) ⊢ (λ _: El t, true) : El t → El prop on 1;
-// coercion "pred-set" (t: Set) (p: El (t ~> prop)) ⊢ @psub t p : Set on 2;
+coercion "set-pred" (t: Set) ⊢ (λ _: El t, true) : El t → El prop on 1;
+coercion "pred-set" (t: Set) (p: El (t ~> prop)) ⊢ @psub t p : Set on 2;
 
 coercion "psub-fst"
   (t: Set) (p: El t → Prop) (m: El (@psub t p)) ⊢ @fst t p m : El t
@@ -31,9 +33,17 @@ with c : El t → El u;
 //  with d: El b → El b';
 
 require personoj.extra.arity-tools as A;
+// The following coercion is redundant with 'tup-cons'
+coercion "2-uple"
+  (a a' b b': Set) (arg: El (σ {A.two} (a && b))) ⊢
+  @^^ a' b' $c[@head A.two (a && b) arg] $d[@head A.one (@& A.z b &nil) (@tail A.one (a && b) arg)]:
+  El (σ {A.two} (a' && b'))
+  on 5
+  with c: El a → El a'
+  with d: El b → El b';
 coercion "tup-cons"
   (a a': Set) (n: A.N) (v v': SVec n) (arg: El (@σ (A.s n) (@& n a v))) ⊢
-  @^ n a' v' $c[@head (A.s n) a arg] $d[@tail n v arg]:
+  @^ n a' v' $c[@head (A.s n) (@& n a v) arg] $d[@tail n (@& n a v) arg]:
   El (@σ (A.s n) (@& n a' v'))
  on 6
  with c: El a → El a'

personoj/examples/transitivity.lp

@@ -34,6 +34,6 @@ symbol foox : Π x: El real*, Prf (foo x)
 begin admit; end;
 
 // With a tuple
-symbol bar: El (σ (numfield & numfield* & &nil)) → Prop;
-symbol barx : Π x: El real, Π y: El real*, Prf (bar (x ^ y ^ ^nil))
+symbol bar: El (σ (numfield && numfield*)) → Prop;
+symbol barx : Π x: El real, Π y: El real*, Prf (bar (x ^^ y))
 begin admit; end;

personoj/extra/arity-tools.lp

@@ -21,6 +21,6 @@ symbol six ≔ s five;
 
 require personoj.nat as Pn;
 /// A constructor from PVS nat
-injective symbol & : Pn.Nat → N;
-rule & (Pn.succ $n) ↪ s (& $n)
-with & Pn.zero ↪ z;
+injective symbol pure : Pn.Nat → N;
+rule pure (Pn.succ $n) ↪ s (pure $n)
+with pure Pn.zero ↪ z;

personoj/tuple.lp

@@ -4,14 +4,14 @@ require open personoj.lhol;
 require open personoj.extra.arity-tools;
 
 constant symbol SVec : N → TYPE;
-constant symbol & {n: N}: Set → SVec n → SVec (s n);
+injective symbol & {n: N}: Set → SVec n → SVec (s n);
 constant symbol &nil : SVec z;
 notation & infix right 10;
 
 constant symbol σ {n: N}: SVec n → Set;
 
 symbol SVmap {n: N}: (Set → Set) → SVec n → SVec n;
-rule SVmap $f &nil ↪ &nil
+rule SVmap _ &nil ↪ &nil
 with SVmap $f ($x & $y) ↪ ($f $x) & (SVmap $f $y);
 
 /* [mkarr tele ret] creates the type [tele₀ ~> tele₁ ~> ... ~> ret]. */
@@ -19,24 +19,28 @@ injective symbol mkarr {n: N}: SVec n → Set → Set;
 rule mkarr &nil $Ret ↪ $Ret
 with mkarr ($X & $Q) $Ret ↪ arr $X (mkarr $Q $Ret);
 
-constant symbol ^ {n: N} {a: Set} {v: SVec n}:
+/* [mkarr* v] creates the product type [El v₀ → El v₁ → ... → Set]. */
+symbol mkarr* {n: N}: SVec n → TYPE;
+rule mkarr* &nil ↪ Set
+with mkarr* ($x & $y) ↪ El $x → mkarr* $y;
+
+injective symbol ^ {n: N} {a: Set} {v: SVec n}:
   El a → El (σ v) → El (σ (a & v));
 constant symbol ^nil : El (σ &nil);
 notation ^ infix right 10;
 
-symbol match {l: N} {v: SVec l} (ret: Set) (arg: El (σ v)):
+symbol match {l: N} {v: SVec l} {ret: Set} (arg: El (σ v)):
   El (mkarr v ret) → El ret;
-rule match {z} {&nil} _ ^nil $e ↪ $e
-with match $Ret ($x ^ $y) $f ↪ match $Ret $y ($f $x);
+rule match {z} {&nil} ^nil $e ↪ $e
+with @match _ _ $Ret ($x ^ $y) $f ↪ @match _ _ $Ret $y ($f $x);
 
-/// Accessors
+/* [match* t f] applied function [f] that yields a type to the components of
+   [t]. */
+symbol match* {l: N} {v: SVec l} (arg: El (σ v)): mkarr* v → Set;
+rule match* ^nil $e ↪ $e
+with match* ($x ^ $y) $f ↪ match* $y ($f $x);
 
-/* [nth n v arg] returns the [n]th element of vector [v].
-   NOTE: the argument [arg] is not used in the computation, but we need it to
-   have the same interface as telescopes. */
-symbol nth {n: N} (_: N) (v: SVec n) (_: El (σ v)): Set;
-rule nth z ($x & _) _ ↪ $x
-with nth (s $n) (_ & $tl) (_ ^ $y) ↪ nth $n $tl $y;
+/// Standard accessors
 
 symbol car {n: N}: SVec n → Set;
 rule car ($x & _) ↪ $x;
@@ -44,13 +48,39 @@ symbol cdr {n: N}: SVec (s n) → SVec n;
 rule cdr (_ & $x) ↪ $x;
 symbol cadr {n: N} (v: SVec (s n)): Set ≔ car (cdr v);
 
-symbol argn {l: N} {v: SVec l} (n: N) (arg: El (σ v)): El (nth n v arg);
-rule argn z ($x ^ _) ↪ $x
-with argn (s $n) (_ ^ $Y) ↪ argn $n $Y;
-
-/// Low level accessors
+// Surjective pairing for SetVec
+rule (car $x) & (cdr $x) ↪ $x;
 
 symbol head {l: N} {v: SVec l} (arg: El (σ v)): El (car v);
 rule head ($x ^ _) ↪ $x;
 symbol tail {l: N} {v: SVec (s l)}: El (σ v) → El (σ (cdr v));
 rule tail (_ ^ $y) ↪ $y;
+
+// Surjective pairing for tuples
+rule (head $x) ^ (tail $x) ↪ $x;
+
+/// Accessors
+
+/* [nth n v arg] returns the [n]th element of vector [v].
+   NOTE: the argument [arg] is not used in the computation, but we need it to
+   have the same interface as telescopes. */
+symbol nth {l: N} (_: N) (v: SVec l) (_: El (σ v)): Set;
+rule nth z ($x & _) _ ↪ $x
+with nth (s $n) (_ & $tl) $x ↪ nth $n $tl (tail $x);
+// NOTE we must take care to be able to reduce even if the argument is a
+// variable.
+
+symbol proj {l: N} {v: SVec l} (n: N) (arg: El (σ v)): El (nth n v arg);
+rule proj z ($x ^ _) ↪ $x
+with proj (s $n) (_ ^ $Y) ↪ proj $n $Y;
+
+/// Convenience
+
+/* [a && b] creates the telescope of two (independant) codes. */
+symbol && (a b: Set) ≔ a & b & &nil;
+notation && infix 11;
+assert (X: Set) ⊢ X & X && X ≡ X & (X && X);
+
+/* [x ^^ y] creates a tuple of two elements with [x] and [y]. */
+symbol ^^ {a: Set} {b: Set} (x: El a) (y: El b) ≔ x ^ y ^ ^nil;
+notation ^^ infix 11;