matching operator for tuples

personoj/proj.lp

@@ -2,11 +2,11 @@ require open personoj.lhol personoj.nat personoj.tuple personoj.sum;
 
 /// [Proj n l t] returns the element at index [n] of tuple [t] of length [l].
 symbol Proj : Nat → Nat → Π (a: Set), El a → TYPE;
-rule Proj 0 0 $a _ ↪ El $a with
-    Proj 0 (succ _) (Σ $a _) _ ↪ El $a with
-    Proj 0 (succ _) (σ $a _) _ ↪ El $a with
-    Proj (succ $n) (succ $l) (Σ _ $u) $x ↪ Proj $n $l ($u (card $x)) (cdrd $x) with
-    Proj (succ $n) (succ $l) (σ _ $u) $x ↪ Proj $n $l $u (cdr $x);
+rule Proj 0 0 $a _ ↪ El $a
+with Proj 0 (succ _) (Σ $a _) _ ↪ El $a
+with Proj 0 (succ _) (σ $a _) _ ↪ El $a
+with Proj (succ $n) (succ $l) (Σ _ $u) $x ↪ Proj $n $l ($u (card $x)) (cdrd $x)
+with Proj (succ $n) (succ $l) (σ _ $u) $x ↪ Proj $n $l $u (cdr $x);
 
 assert (T: Set) (U: Set) (x: El T) (y: El U) ⊢ Proj 1 1 (σ T U) (cons x y) ≡ El U;
 assert (T: Set) (U: El T → Set) (x: El T) (y: El (U x)) ⊢ Proj 1 1 (Σ T U) (consd x y) ≡ El (U x);
@@ -19,13 +19,13 @@ assert (T: Set) (U: Set) (V: Set) (x1: El T) (x2: El U) (x3: El V) ⊢
 /// of type [T] of length [l], where [length (σ _ B) = 1 + length B] and [length
 /// t = 0] if [t] is not a pair.
 symbol proj {a: Set} (n: Nat) (l: Nat) (x: El a): Proj n l a x;
-rule @proj (σ _ _) 0 (succ _) (cons $x _) ↪ $x with
-    @proj (Σ _ _) 0 (succ _) (consd $x _) ↪ $x with
-    @proj (σ _ _) 1 1 (cons _ $y) ↪ $y with
-    @proj (Σ _ _) 1 1 (consd _ $y) ↪ $y with
-    @proj (σ _ $b) (succ $n) (succ (succ $m)) (cons _ $y) ↪
-     @proj $b $n (succ $m) $y with
-    @proj (Σ _ $b) (succ $n) (succ (succ $m)) (consd $x $y) ↪
+rule @proj (σ _ _) 0 (succ _) (cons $x _) ↪ $x
+with @proj (Σ _ _) 0 (succ _) (consd $x _) ↪ $x
+with @proj (σ _ _) 1 1 (cons _ $y) ↪ $y
+with @proj (Σ _ _) 1 1 (consd _ $y) ↪ $y
+with @proj (σ _ $b) (succ $n) (succ (succ $m)) (cons _ $y) ↪
+     @proj $b $n (succ $m) $y
+with @proj (Σ _ $b) (succ $n) (succ (succ $m)) (consd $x $y) ↪
      @proj ($b $x) $n (succ $m) $y ;
 
 assert (T: Set) (e: El T) (e': El T) ⊢ proj {σ T T} 1 1 (cons e e') ≡ e';
@@ -38,3 +38,16 @@ assert (T: Set) (U: Set) (V: Set) (et: El T) (eu: El U) (ev: El V) ⊢
   proj 1 2 (cons et (cons eu ev)) ≡ eu;
 assert (T: Set) (U: Set) (V: Set) (et: El T) (eu: El U) (ev: El V) ⊢
   proj 0 2 (cons et (cons eu ev)) ≡ et;
+
+require personoj.extra.arity-tools as A;
+symbol σ->arr: A.N → Set → Set → Set;
+rule σ->arr (A.s A.z) $dom $ret ↪ $dom ~> $ret
+with σ->arr (A.s $n) (σ $x $y) $ret ↪ $x ~> (σ->arr $n $y $ret)
+with σ->arr (A.s $n) (Σ $x $y) $ret ↪ arrd $x (λ e: El $x, σ->arr $n ($y e) $ret);
+symbol match {dom: Set} {ret: Set} (n: A.N):
+  El dom → El (σ->arr n dom ret) → El ret;
+rule @match  _ _ (A.s A.z) $x $f ↪ $f $x
+with @match  (σ _ _) $ret (A.s $n) (cons $x $y) $f ↪ @match _ $ret $n $y ($f $x);
+
+assert (X: Set) (R: Set) ⊢ σ->arr A.three (σ X (σ X X)) R ≡ X ~> X ~> X ~> R;
+assert (X: Set) (x1 x2 x3: El X) ⊢ match (A.& 3) (cons x1 (cons x2 x3)) (λ x1 x2 x3, x2) ≡ x2;