proof(solo-core): multiplicative product (X) (TTensor + let-pair) — F1.4 phase 3b

Completes the product redesign: adds the genuine multiplicative
product `TTensor` (a (X) b) alongside the additive `TWith` (a & b)
from phase 3a.

Where `&` shares usage and projects one component, `(X)` SPLITS usage
at introduction (both halves paid for separately) and its eliminator
`LetPair` (let (x,y) = e1 in e2) delivers BOTH components: the body
binds two variables (x:a at de Bruijn index 1, y:b at index 0), each
used linearly.

  * Syntax.v    TTensor type; Tensor / LetPair terms; shift & subst_at
                cases (LetPair body cutoff/index += 2); new `subst2`
                two-variable substitution (subst0 . subst0, correct for
                the closed values the reduction rule plugs in).
  * Typing.v    T_Tensor (uadd D1 D2, split); T_LetPair (body in
                TSnoc (TSnoc G a) b under USnoc (USnoc D2 One) One).
  * Soundness.v VTensor value; S_Tensor1/2 congruence; S_LetPair
                computation (-> subst2 v1 v2 body); S_LetPair1
                congruence; canon_tensor; the four existing canonical
                forms extended to the new 7th value constructor;
                progress Tensor + LetPair cases.

Verification: full chain compiles under Coq 8.18; `progress` over the
full 15-constructor term language remains "Closed under the global
context" (zero axioms, zero admits).

NOTE: Idris twin + Rust checker still to gain the &/(X) split (phases
5 / future). `subst2`'s general (open-term) form is a phase-4 concern;
the operational rule only ever substitutes closed values.

Author: claude

proofs/verification/coq/solo-core/Soundness.v

@@ -40,7 +40,9 @@ Inductive value : tm -> Prop :=
   | VInr  : forall a t, value t -> value (Inr a t)
   (* an echo with a fully-evaluated residue is a value; [Weaken] is
      not (it is the elimination that drives the linear->affine step) *)
-  | VEcho : forall m a b t, value t -> value (MkEcho m a b t).
+  | VEcho : forall m a b t, value t -> value (MkEcho m a b t)
+  (* a multiplicative pair is a value once both components are *)
+  | VTensor : forall t1 t2, value t1 -> value t2 -> value (Tensor t1 t2).
 
 (** * Small-step reduction — call-by-value, left-to-right (F1.1).
 
@@ -63,6 +65,9 @@ Inductive step : tm -> tm -> Prop :=
       value v -> step (Case (Inr a v) tL tR) (subst0 v tR)
   | S_Let   : forall q v t2,
       value v -> step (Let q v t2) (subst0 v t2)
+  | S_LetPair : forall v1 v2 body,
+      value v1 -> value v2 ->
+      step (LetPair (Tensor v1 v2) body) (subst2 v1 v2 body)
   (* --- congruence (left-to-right, CBV) --- *)
   | S_App1  : forall t1 t1' t2,
       step t1 t1' -> step (App t1 t2) (App t1' t2)
@@ -84,6 +89,12 @@ Inductive step : tm -> tm -> Prop :=
       step t t' -> step (Case t tL tR) (Case t' tL tR)
   | S_Let1  : forall q t1 t1' t2,
       step t1 t1' -> step (Let q t1 t2) (Let q t1' t2)
+  | S_Tensor1 : forall t1 t1' t2,
+      step t1 t1' -> step (Tensor t1 t2) (Tensor t1' t2)
+  | S_Tensor2 : forall v1 t2 t2',
+      value v1 -> step t2 t2' -> step (Tensor v1 t2) (Tensor v1 t2')
+  | S_LetPair1 : forall t1 t1' t2,
+      step t1 t1' -> step (LetPair t1 t2) (LetPair t1' t2)
   (* echo residue: evaluate inside, and the one-way linear->affine
      weakening fires once the residue is a value (EchoLinear.weaken). *)
   | S_Echo1   : forall m a b t t',
@@ -155,13 +166,14 @@ Lemma canon_arr : forall q a b v,
 Proof.
   intros q a b v Hv Ht.
   destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
-                 | m0 ae be ue Hue ].
+                 | m0 ae be ue Hue | w1 w2 Hw1 Hw2 ].
   - inversion Ht.
   - exists q0, a0, tb. reflexivity.
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
+  - inversion Ht.
 Qed.
 
 Lemma canon_with : forall a b v,
@@ -170,13 +182,14 @@ Lemma canon_with : forall a b v,
 Proof.
   intros a b v Hv Ht.
   destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
-                 | m0 ae be ue Hue ].
+                 | m0 ae be ue Hue | w1 w2 Hw1 Hw2 ].
   - inversion Ht.
   - inversion Ht.
   - exists u1, u2. split; [reflexivity | split; assumption].
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
+  - inversion Ht.
 Qed.
 
 Lemma canon_sum : forall a b v,
@@ -186,13 +199,14 @@ Lemma canon_sum : forall a b v,
 Proof.
   intros a b v Hv Ht.
   destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
-                 | m0 ae be ue Hue ].
+                 | m0 ae be ue Hue | w1 w2 Hw1 Hw2 ].
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
   - left.  exists b0, u0. split; [reflexivity | assumption].
   - right. exists a0, u0. split; [reflexivity | assumption].
   - inversion Ht.
+  - inversion Ht.
 Qed.
 
 (** Canonical form for echoes: a closed value of echo type is an
@@ -204,13 +218,33 @@ Lemma canon_echo : forall m a b v,
 Proof.
   intros m a b v Hv Ht.
   destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
-                 | m0 ae be ue Hue ].
+                 | m0 ae be ue Hue | w1 w2 Hw1 Hw2 ].
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
   - inversion Ht.
   - inversion Ht; subst. exists ue. split; [reflexivity | assumption].
+  - inversion Ht.
+Qed.
+
+(** Canonical form for tensors: a closed value of multiplicative-product
+    type is a [Tensor] of two values. Drives the [LetPair] case of
+    progress. *)
+Lemma canon_tensor : forall a b v,
+  value v -> has_type TEmpty UEmpty v (TTensor a b) ->
+  exists v1 v2, v = Tensor v1 v2 /\ value v1 /\ value v2.
+Proof.
+  intros a b v Hv Ht.
+  destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
+                 | m0 ae be ue Hue | w1 w2 Hw1 Hw2 ].
+  - inversion Ht.
+  - inversion Ht.
+  - inversion Ht.
+  - inversion Ht.
+  - inversion Ht.
+  - inversion Ht.
+  - exists w1, w2. split; [reflexivity | split; assumption].
 Qed.
 
 (** ** Progress. *)
@@ -226,6 +260,8 @@ Proof.
     | t1 IHt1 t2 IHt2 (* With *)
     | t1 IHt1         (* Fst  *)
     | t1 IHt1         (* Snd  *)
+    | t1 IHt1 t2 IHt2 (* Tensor  *)
+    | t1 IHt1 t2 IHt2 (* LetPair *)
     | bAnn t1 IHt1    (* Inl  *)
     | aAnn t1 IHt1    (* Inr  *)
     | t1 IHt1 tL IHtL tR IHtR  (* Case *)
@@ -288,6 +324,27 @@ Proof.
       | right; exists (Snd t1'); apply S_Snd1; exact Hs ]
     end.
 
+  - (* Tensor t1 t2 : multiplicative pair — a value once both components are *)
+    inversion Ht; subst; empty_uvec.
+    match goal with HT1 : has_type TEmpty UEmpty t1 _ |- _ =>
+      match goal with HT2 : has_type TEmpty UEmpty t2 _ |- _ =>
+        destruct (IHt1 _ HT1) as [Hv1 | [t1' Hs1]];
+        [ destruct (IHt2 _ HT2) as [Hv2 | [t2' Hs2]];
+          [ left; apply VTensor; assumption
+          | right; exists (Tensor t1 t2'); apply S_Tensor2; [exact Hv1 | exact Hs2] ]
+        | right; exists (Tensor t1' t2); apply S_Tensor1; exact Hs1 ]
+      end
+    end.
+
+  - (* LetPair t1 t2 : steps once the scrutinee is a Tensor value *)
+    inversion Ht; subst; empty_uvec.
+    match goal with HT : has_type TEmpty UEmpty t1 (TTensor _ _) |- _ =>
+      destruct (IHt1 _ HT) as [Hv | [t1' Hs]];
+      [ destruct (canon_tensor _ _ _ Hv HT) as [v1 [v2 [Heqv [Hv1 Hv2]]]]; subst t1;
+        right; exists (subst2 v1 v2 t2); apply S_LetPair; [exact Hv1 | exact Hv2]
+      | right; exists (LetPair t1' t2); apply S_LetPair1; exact Hs ]
+    end.
+
   - (* Inl bAnn t1 *)
     inversion Ht; subst; empty_uvec.
     match goal with HT : has_type TEmpty UEmpty t1 _ |- _ =>

proofs/verification/coq/solo-core/Syntax.v

@@ -17,10 +17,10 @@ Require Import EchoMode.
 
 Inductive ty : Type :=
   | TUnit : ty
-  | TWith : ty -> ty -> ty          (* additive product  a & b  (shared usage,
-                                       projected by Fst/Snd). The multiplicative
-                                       product  a (X) b  is deferred to a
-                                       follow-up (TTensor + let-pair). *)
+  | TWith   : ty -> ty -> ty        (* additive product  a & b
+                                       (shared usage, projected by Fst/Snd) *)
+  | TTensor : ty -> ty -> ty        (* multiplicative product  a (X) b
+                                       (split usage, eliminated by let-pair) *)
   | TSum  : ty -> ty -> ty
   | TArr  : Q -> ty -> ty -> ty     (* (q x : a) -> b *)
   | TEcho : Mode -> ty -> ty -> ty. (* echo residue: [m] Echo<a => b> *)
@@ -35,6 +35,8 @@ Inductive tm : Type :=
   | With  : tm -> tm -> tm    (* additive pair  <t1, t2> : a & b *)
   | Fst   : tm -> tm
   | Snd   : tm -> tm
+  | Tensor  : tm -> tm -> tm  (* multiplicative pair  (t1, t2) : a (X) b *)
+  | LetPair : tm -> tm -> tm  (* let (x, y) = e1 in e2  (e2 binds 2 vars) *)
   | Inl   : ty -> tm -> tm    (* annotation = the other summand *)
   | Inr   : ty -> tm -> tm
   | Case  : tm -> tm -> tm -> tm   (* scrutinee, left (binds 1), right (binds 1) *)
@@ -71,6 +73,8 @@ Fixpoint shift (c : nat) (t : tm) : tm :=
   | With t1 t2   => With (shift c t1) (shift c t2)
   | Fst t1       => Fst (shift c t1)
   | Snd t1       => Snd (shift c t1)
+  | Tensor t1 t2  => Tensor (shift c t1) (shift c t2)
+  | LetPair t1 t2 => LetPair (shift c t1) (shift (S (S c)) t2)
   | Inl b t1     => Inl b (shift c t1)
   | Inr a t1     => Inr a (shift c t1)
   | Case t1 tL tR => Case (shift c t1) (shift (S c) tL) (shift (S c) tR)
@@ -97,6 +101,9 @@ Fixpoint subst_at (j : nat) (u : tm) (t : tm) : tm :=
   | With t1 t2   => With (subst_at j u t1) (subst_at j u t2)
   | Fst t1       => Fst (subst_at j u t1)
   | Snd t1       => Snd (subst_at j u t1)
+  | Tensor t1 t2  => Tensor (subst_at j u t1) (subst_at j u t2)
+  | LetPair t1 t2 =>
+      LetPair (subst_at j u t1) (subst_at (S (S j)) (shift 0 (shift 0 u)) t2)
   | Inl b t1     => Inl b (subst_at j u t1)
   | Inr a t1     => Inr a (subst_at j u t1)
   | Case t1 tL tR =>
@@ -111,3 +118,10 @@ Fixpoint subst_at (j : nat) (u : tm) (t : tm) : tm :=
 (** Single-variable substitution for index 0 — the [(\x.t) v -> t[v/x]]
     workhorse of the reduction rules. *)
 Definition subst0 (u : tm) (t : tm) : tm := subst_at 0 u t.
+
+(** Two-variable substitution for the let-pair eliminator: replace de
+    Bruijn index 1 by [u1] and index 0 by [u2]. For CLOSED [u1] [u2]
+    (the operational use — both are values), the two sequential single
+    substitutions suffice: substituting index 0 first collapses the
+    former index 1 down to index 0 for the second pass. *)
+Definition subst2 (u1 u2 : tm) (t : tm) : tm := subst0 u1 (subst0 u2 t).

proofs/verification/coq/solo-core/Typing.v

@@ -83,6 +83,23 @@ Inductive has_type : tctx -> uvec -> tm -> ty -> Prop :=
       has_type G D t (TWith a b) ->
       has_type G D (Snd t) b
 
+  (* Multiplicative product  a (X) b  (the genuine tensor). Introduction
+     SPLITS usage (uadd D1 D2): both halves are paid for separately,
+     because elimination delivers BOTH components. Eliminated by LetPair
+     (let (x,y) = e1 in e2): the body e2 binds two variables — x:a at de
+     Bruijn index 1, y:b at index 0 — each used linearly (One). *)
+  | T_Tensor : forall G D D1 D2 a b t1 t2,
+      has_type G D1 t1 a ->
+      has_type G D2 t2 b ->
+      uadd D1 D2 = Some D ->
+      has_type G D (Tensor t1 t2) (TTensor a b)
+
+  | T_LetPair : forall G D D1 D2 a b c t1 t2,
+      has_type G D1 t1 (TTensor a b) ->
+      has_type (TSnoc (TSnoc G a) b) (USnoc (USnoc D2 One) One) t2 c ->
+      uadd D1 D2 = Some D ->
+      has_type G D (LetPair t1 t2) c
+
   | T_Inl : forall G D a b t,
       has_type G D t a ->
       has_type G D (Inl b t) (TSum a b)