From 197082c54f9994ebadc4ebdd0c186b3afc8224fa Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Sat, 14 Feb 2026 16:02:00 +0000
Subject: [PATCH 01/11] Start on the metatheory.Syntax, env, subst, numerics
 mostly done.

---
 spectec/metatheory/Makefile             |   5 +
 spectec/metatheory/dune-project         |  12 ++
 spectec/metatheory/metatheory.opam      |  23 +++
 spectec/metatheory/theories/dune        |   7 +
 spectec/metatheory/theories/env.v       |  37 +++++
 spectec/metatheory/theories/numerics.v  | 157 ++++++++++++++++++
 spectec/metatheory/theories/reduction.v |  85 ++++++++++
 spectec/metatheory/theories/subst.v     | 204 ++++++++++++++++++++++++
 spectec/metatheory/theories/syntax.v    | 191 ++++++++++++++++++++++
 spectec/metatheory/theories/typing.v    |  96 +++++++++++
 10 files changed, 817 insertions(+)
 create mode 100644 spectec/metatheory/Makefile
 create mode 100644 spectec/metatheory/dune-project
 create mode 100644 spectec/metatheory/metatheory.opam
 create mode 100644 spectec/metatheory/theories/dune
 create mode 100644 spectec/metatheory/theories/env.v
 create mode 100644 spectec/metatheory/theories/numerics.v
 create mode 100644 spectec/metatheory/theories/reduction.v
 create mode 100644 spectec/metatheory/theories/subst.v
 create mode 100644 spectec/metatheory/theories/syntax.v
 create mode 100644 spectec/metatheory/theories/typing.v

diff --git a/spectec/metatheory/Makefile b/spectec/metatheory/Makefile
new file mode 100644
index 0000000000..bc7a5adf4b
--- /dev/null
+++ b/spectec/metatheory/Makefile
@@ -0,0 +1,5 @@
+default:
+	opam install .
+
+clean:
+	dune clean
\ No newline at end of file
diff --git a/spectec/metatheory/dune-project b/spectec/metatheory/dune-project
new file mode 100644
index 0000000000..97a3db3c01
--- /dev/null
+++ b/spectec/metatheory/dune-project
@@ -0,0 +1,12 @@
+(lang dune 3.11)
+(using coq 0.8)
+(generate_opam_files true)
+
+(package
+  (name metatheory)
+  (synopsis "Spectec Wasm formalisation in Rocq")
+  (depends
+    (coq (>= 9.0))
+    (coq-mathcomp-ssreflect (and (>= 2.0.0) (<= 2.4.0)))
+  )
+)
\ No newline at end of file
diff --git a/spectec/metatheory/metatheory.opam b/spectec/metatheory/metatheory.opam
new file mode 100644
index 0000000000..57f04b41df
--- /dev/null
+++ b/spectec/metatheory/metatheory.opam
@@ -0,0 +1,23 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Spectec Wasm formalisation in Rocq"
+depends: [
+  "dune" {>= "3.11"}
+  "coq" {>= "9.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0.0" & <= "2.4.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
diff --git a/spectec/metatheory/theories/dune b/spectec/metatheory/theories/dune
new file mode 100644
index 0000000000..7ef1f0c5d3
--- /dev/null
+++ b/spectec/metatheory/theories/dune
@@ -0,0 +1,7 @@
+(coq.theory
+  (name MetaSpectec)
+  (theories Stdlib mathcomp HB elpi elpi_elpi)
+  (package metatheory)
+  (flags -w -notation-overridden -w -abstract-large-number -w -ambiguous-paths
+         -w -unused-pattern-matching-variable -w -non-recursive
+         ))
\ No newline at end of file
diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
new file mode 100644
index 0000000000..d811ffbe5c
--- /dev/null
+++ b/spectec/metatheory/theories/env.v
@@ -0,0 +1,37 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+Require Import Stdlib.FSets.FMapAVL.
+Require Import Stdlib.Structures.OrderedTypeEx.
+From MetaSpectec Require Import syntax.
+
+Module StringMap := FMapAVL.Make(String_as_OT).
+
+(* TYPING *)
+
+Definition var_def : Type := il_typ.
+Definition typ_def : Type := list il_param * list il_inst.
+Definition rel_def : Type := mixop * il_typ * list il_rule.
+Definition definition_def : Type := list il_param * il_typ * list il_clause.
+
+(* Typing context *)
+
+Record il_env := {
+  VARS : StringMap.t var_def;
+  TYPS : StringMap.t typ_def;
+  DEFS : StringMap.t definition_def;
+  RELS : StringMap.t rel_def
+}.
+
+Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20).
+Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20).
+Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20).
+Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20).
+
+Record store := {
+  S_TYPS : StringMap.t typ_def;
+  S_DEFS : StringMap.t definition_def;
+  S_RELS : StringMap.t rel_def
+}.
+
+Definition store_to_env (s : store) : il_env :=
+  {| VARS := StringMap.empty var_def; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/numerics.v b/spectec/metatheory/theories/numerics.v
new file mode 100644
index 0000000000..32c7705ce0
--- /dev/null
+++ b/spectec/metatheory/theories/numerics.v
@@ -0,0 +1,157 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import all_ssreflect all_algebra ssrnat ssrint.
+Import GRing.Theory.
+From MetaSpectec Require Import syntax.
+
+Coercion absz : int >-> nat.
+
+Coercion ratz: int >-> rat.
+
+(* Booleans *)
+
+Definition boolun (op : boolunop) (b : bool) : bool :=
+  match op with
+  | NotOp => negb b
+  end
+.
+
+Definition boolbin (op : boolbinop) (b1 b2 : bool) : bool :=
+  match op with
+  | AndOp => b1 && b2
+  | OrOp => b1 || b2
+  | ImplOp => b1 ==> b2
+  | EquivOp => b1 ==> b2 && b2 ==> b1
+  end
+.
+
+Definition iszero(x : il_num) : bool := 
+  match x with
+  | NatE n => n == 0%nat
+  | IntE i => i == 0%R
+  | RatE r => r == 0%R
+  | RealE r => r == 0%R
+  end
+.
+
+Definition isone(x : il_num) : bool := 
+  match x with
+  | NatE n => n == 1%nat
+  | IntE i => i == 1%R
+  | RatE r => r == 1%R 
+  | RealE r => r == 1%R
+  end
+.
+
+Definition option_map {α β : Type} (f : α -> β) (x : option α) : option β :=
+	match x with
+  | Some x => Some (f x)
+  | _ => None
+	end.
+
+Definition option_join {α : Type} (x : option (option α)) : option α :=
+  match x with
+  | Some None => None
+  | None => None
+  | Some (Some x') => Some x'
+  end.
+
+(* Numerics *)
+
+Definition rat_to_int (x : rat) : option int :=
+  if isone (IntE (denq x)) then Some (numq x) else None
+.
+
+Definition int_to_nat_num (x : int) : option il_num :=
+  if (x >= 0)%R then Some (NatE x) else None.
+
+Definition to_nat (x : R) : nat :=
+  (Num.floor x).
+
+Definition rat_to_R (q : rat) : R :=
+  ((numq q)%:~R / (denq q)%:~R)%R.
+
+(* TODO finish some of the conversions - especially for reals *)
+Definition numcvt (nt : numtyp) (val : il_num) : option il_num :=
+  match nt, val with
+  | NatT, NatE n => Some (NatE n)
+  | NatT, IntE i => int_to_nat_num i
+  | NatT, RatE r => let opt := rat_to_int r in
+    option_join (option_map (fun i => int_to_nat_num i) opt)
+  | NatT, RealE r => Some (NatE (to_nat r))
+  | IntT, NatE n => Some (IntE n)
+  | IntT, IntE i => Some (IntE i)
+  | IntT, RatE r => if isone (IntE (denq r)) then Some (IntE (numq r)) else None
+  | IntT, RealE r => Some (IntE (Num.floor r))
+  | RatT, NatE n => Some (RatE (n%:Q))
+  | RatT, IntE i => Some (RatE (i%:Q))
+  | RatT, RatE r => Some (RatE r)
+  (* TODO think of a better way to cvt real to rational *)
+  | RatT, RealE r => Some (RatE (Num.floor r)%:Q)
+  | RealT, NatE n => Some (RealE (n%:R))
+  | RealT, IntE i => Some (RealE (i%:R))
+  | RealT, RatE r => Some (RealE (rat_to_R r))
+  | RealT, RealE r => Some (RealE r)
+  end
+.
+
+Definition numun (op : numunop) (val : il_num) : option il_num :=
+  match op, val with
+  | PlusOp, n => Some n
+  | MinusOp, NatE n => Some (IntE (0 - n%:R)%R) 
+  | MinusOp, IntE i => Some (IntE (0 - i)%R)
+  | MinusOp, RatE r => Some (RatE (0 - r)%R)
+  | MinusOp, RealE r => Some (RealE (0 - r)%R)
+  end
+.
+
+Definition numbin (op : numbinop) (val1 val2 : il_num) : option il_num :=
+  match op, val1, val2 with
+  | AddOp, NatE n1, NatE n2 => Some (NatE (n1 + n2)%nat)
+  | AddOp, IntE i1, IntE i2 => Some (IntE (i1 + i2)%R)
+  | AddOp, RatE r1, RatE r2 => Some (RatE (r1 + r2)%R)
+  | AddOp, RealE r1, RealE r2 => Some (RealE (r1 + r2)%R)
+  | SubOp, NatE n1, NatE n2 => if (n1 >= n2)%nat then Some (NatE (n1 - n2)%nat) else None
+  | SubOp, IntE i1, IntE i2 => Some (IntE (i1 - i2)%R)
+  | SubOp, RatE r1, RatE r2 => Some (RatE (r1 - r2)%R)
+  | SubOp, RealE r1, RealE r2 => Some (RealE (r1 - r2)%R)
+  | MulOp, NatE n1, NatE n2 => Some (NatE (n1 * n2)%nat)
+  | MulOp, IntE i1, IntE i2 => Some (IntE (i1 * i2)%R)
+  | MulOp, RatE r1, RatE r2 => Some (RatE (r1 * r2)%R)
+  | MulOp, RealE r1, RealE r2 => Some (RealE (r1 * r2)%R)
+  | DivOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.div n1 n2)) else None
+  | DivOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (IntE (divz i1 i2)) else None
+  | DivOp, RatE r1, RatE r2 => if negb (iszero val2) then Some (RatE (r1 / r2)%R) else None
+  | DivOp, RealE r1, RealE r2 => if negb (iszero val2) then Some (RealE (r1 / r2)%R) else None
+  | ModOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.modulo n1 n2)) else None
+  | ModOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (NatE (modz i1 i2)) else None
+  | PowOp, NatE n1, NatE n2 => Some (NatE (n1^n2))
+  | PowOp, IntE i1, IntE i2 => if (i2 >= 0)%R then Some (IntE (i1^i2)) else None 
+  | PowOp, RatE r1, RatE r2 => if isone (IntE (denq r2)) then Some (RatE (r1^(numq r2))) else None 
+  (* TODO - don't know how this is supposed to work: 
+  | PowOp, RealE r1, RealE r2 => RealE (r1^r2) *)
+  | _, _, _ => None
+  end
+.
+
+
+Definition numcmp (op : numcmpop) (val1 val2 : il_num) : option bool :=
+  match op, val1, val2 with
+  | LtOp, NatE n1, NatE n2 => Some ((n1 < n2)%nat)
+  | LtOp, IntE i1, IntE i2 => Some ((i1 < i2)%R)
+  | LtOp, RatE r1, RatE r2 => Some ((r1 < r2)%R)
+  | LtOp, RealE r1, RealE r2 => Some ((r1 < r2)%R)
+  | GtOp, NatE n1, NatE n2 => Some ((n1 > n2)%nat)
+  | GtOp, IntE i1, IntE i2 => Some ((i1 > i2)%R)
+  | GtOp, RatE r1, RatE r2 => Some ((r1 > r2)%R)
+  | GtOp, RealE r1, RealE r2 => Some ((r1 > r2)%R)
+  | LeOp, NatE n1, NatE n2 => Some ((n1 <= n2)%nat)
+  | LeOp, IntE i1, IntE i2 => Some ((i1 <= i2)%R)
+  | LeOp, RatE r1, RatE r2 => Some ((r1 <= r2)%R)
+  | LeOp, RealE r1, RealE r2 => Some ((r1 <= r2)%R)
+  | GeOp, NatE n1, NatE n2 => Some ((n1 >= n2)%nat)
+  | GeOp, IntE i1, IntE i2 => Some ((i1 >= i2)%R)
+  | GeOp, RatE r1, RatE r2 => Some ((r1 >= r2)%R)
+  | GeOp, RealE r1, RealE r2 => Some ((r1 >= r2)%R)
+  | _, _, _ => None
+  end
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
new file mode 100644
index 0000000000..efcef70672
--- /dev/null
+++ b/spectec/metatheory/theories/reduction.v
@@ -0,0 +1,85 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+From MetaSpectec Require Import syntax subst env numerics.
+Import ListNotations.
+
+Definition option_to_list {T: Type} (arg : option T) : seq T :=
+	match arg with
+		| None => nil
+		| Some a => a :: nil
+	end.
+
+Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
+  (* UnE Rules *)
+  | se_unop_ctx : forall s op e1 e2,
+    step_exp s e1 e2 ->
+    step_exp s (UnE op e1) (UnE op e2)
+  | se_unop_bool : forall s boolop b,
+    step_exp s (UnE (BoolUnop boolop) (BoolE b)) (BoolE (boolun boolop b))
+  | se_unop_num : forall s numop n n',
+    (numun numop n) = Some n' ->
+    step_exp s (UnE (NumUnop numop) (NumE n)) (NumE n')
+  (* BinE Rules *)
+  | se_bin_ctxl : forall s op e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (BinE op e1 e2) (BinE op e1' e2)
+  | se_bin_ctxr : forall s op e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (BinE op e1 e2) (BinE op e1 e2')
+  | se_bin_bool : forall s boolop b1 b2,
+    step_exp s (BinE (BoolBinop boolop) (BoolE b1) (BoolE b2)) (BoolE (boolbin boolop b1 b2))
+  | se_bin_num : forall s numop n1 n2 n3,
+    (numbin numop n1 n2) = Some n3 ->
+    step_exp s (BinE (NumBinop numop) (NumE n1) (NumE n2)) (NumE n3)
+  (* CmpE Rules *)
+  | se_cmp_ctxl : forall s op e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (CmpE op e1 e2) (CmpE op e1' e2)
+  | se_cmp_ctxr : forall s op e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (CmpE op e1 e2) (CmpE op e1 e2')
+  | se_cmp_eq_true : forall s e1 e2,
+    e1 = e2 ->
+    step_exp s (CmpE (BoolCmpop EqOp) e1 e2) (BoolE true)
+  | se_cmp_ne_false : forall s e1 e2,
+    e1 = e2 ->
+    step_exp s (CmpE (BoolCmpop NeqOp) e1 e2) (BoolE false)
+  | se_cmp_num : forall s numcmpop n1 n2 b,
+    (numcmp numcmpop n1 n2) = Some b ->
+    step_exp s (CmpE (NumCmpop numcmpop) (NumE n1) (NumE n2)) (BoolE b)
+  | se_cmp_opt_ctx : forall s opt_e e e',
+    opt_e = Some e ->
+    step_exp s e e' ->
+    step_exp s (OptE opt_e) (OptE (Some e'))
+  (* ListE rules *)
+  | se_list_ctx : forall s es es',
+    List.Forall2 (fun e e' => step_exp s e e') es es' ->
+    step_exp s (ListE es) (ListE es')
+  (* TupE rules *)
+  | se_tup_ctx : forall s es es',
+    List.Forall2 (fun e e' => step_exp s e e') es es' ->
+    step_exp s (TupE es) (TupE es')
+  (* StrE rules *)
+  | se_str_ctx : forall s fields fields',
+    List.Forall2 (fun f f' => step_exp s (snd f) (snd f')) fields fields' ->
+    step_exp s (StrE fields) (StrE fields')
+  (* CasE rules *)
+  | se_case_ctx : forall s m e e',
+    step_exp s e e' ->
+    step_exp s (CaseE m e) (CaseE m e')
+  (* LiftE rules *)
+  | se_lift_ctx : forall s e e',
+    step_exp s e e' ->
+    step_exp s (LiftE e) (LiftE e')
+  | se_lift_none : forall s, step_exp s (LiftE (OptE None)) (ListE [])
+  | se_list_some : forall s e , step_exp s (LiftE (OptE (Some e))) (ListE [e])
+  (* ProjE rules *)
+.
+
+Inductive reduce_exp : store -> il_exp -> il_exp -> Prop :=
+  | re_refl : forall s e, reduce_exp s e e
+  | re_step : forall s e1 e2 e3, 
+    reduce_exp s e2 e3 ->
+    reduce_exp s e1 e3
+.
+
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
new file mode 100644
index 0000000000..213bf5db60
--- /dev/null
+++ b/spectec/metatheory/theories/subst.v
@@ -0,0 +1,204 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+From MetaSpectec Require Import syntax env.
+Require Import Stdlib.FSets.FMapAVL.
+Require Import Stdlib.Structures.OrderedTypeEx.
+Import ListNotations.
+
+Module StringMap := FMapAVL.Make(String_as_OT).
+
+Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
+  StringMap.add k v (StringMap.empty A).
+
+Record il_subst : Type := 
+  {
+  S_EXP : StringMap.t il_exp;
+  S_TYP : StringMap.t il_typ;
+  S_FUN : StringMap.t il_id;
+  }
+.
+
+Definition empty_exp : StringMap.t il_exp := StringMap.empty il_exp.
+Definition empty_typ : StringMap.t il_typ := StringMap.empty il_typ.
+Definition empty_id : StringMap.t il_id := StringMap.empty il_id.
+Definition subst_empty : il_subst := {| S_EXP := empty_exp; S_TYP := empty_typ; S_FUN := empty_id |}.
+
+Definition union {A}
+  (m1 m2 : StringMap.t A) : StringMap.t A :=
+  StringMap.fold (fun k v => StringMap.add k v) m1 m2.
+
+Definition append_subst (s1 s2 : il_subst) : il_subst :=
+  {|
+  S_EXP := union s1.(S_EXP) s2.(S_EXP);
+  S_TYP := union s1.(S_TYP) s2.(S_TYP);
+  S_FUN := union s1.(S_FUN) s2.(S_FUN) 
+  |}.
+
+Record dom : Type :=
+  {
+  D_EXP : list il_id;
+  D_TYP : list il_id;
+  D_FUN : list il_id 
+  }
+.
+
+Definition append_dom (d1 d2 : dom) : dom :=
+  {|
+  D_EXP := d1.(D_EXP) ++ d2.(D_EXP);
+  D_TYP := d1.(D_TYP) ++ d2.(D_TYP);
+  D_FUN := d1.(D_FUN) ++ d2.(D_FUN)
+  |}
+.
+
+Definition get_keys {A : Type} (s : StringMap.t A) : list string :=
+  List.map fst (StringMap.elements s).
+
+Definition dom_subst (s : il_subst) : dom :=
+  {| D_EXP := get_keys s.(S_EXP); D_TYP := get_keys s.(S_TYP); D_FUN := get_keys s.(S_FUN) |}.
+
+Definition bound_param (p : il_param) : dom :=
+  match p with
+  | ExpP il_id _ => {| D_EXP := [il_id]; D_TYP := []; D_FUN := [] |}
+  | TypP il_id => {| D_EXP := []; D_TYP := [il_id]; D_FUN := [] |}
+  | DefP il_id _ _ => {| D_EXP := []; D_TYP := []; D_FUN := [il_id]|}
+  end
+.
+
+Fixpoint bound_params (ps : list il_param) : dom :=
+  match ps with
+  | [] => {| D_EXP := []; D_TYP := []; D_FUN := [] |}
+  | p :: ps => append_dom (bound_param p) (bound_params ps)
+  end
+.
+
+Definition subst_fun (s : il_subst) (x : il_id) : il_id :=
+  match StringMap.find x s.(S_FUN) with
+  | Some y => y
+  | None => x
+  end
+.
+
+Definition subst_iter (s : il_subst) (i : iter) : iter :=
+  match i with
+  | I_SUP x e => I_SUP x e
+  | _ => i
+  end
+.
+
+Fixpoint subst_typ (s : il_subst) (t : il_typ) : il_typ :=
+  match t with
+  | VarT x args => 
+    match StringMap.find x s.(S_TYP) with
+    | Some t' => t'
+    | None => VarT x (List.map (subst_arg s) args)
+    end
+  | TupT xts => TupT (List.map (fun p => (fst p, subst_typ s (snd p))) xts)
+  | IterT t' it => IterT (subst_typ s t') (subst_iter s it)
+  | _ => t
+  end
+
+with
+
+subst_exp (s : il_subst) (e : il_exp) : il_exp :=
+  match e with
+  | VarE x => 
+    match StringMap.find x s.(S_EXP) with
+    | Some e' => e'
+    | _ => e
+    end
+  | UnE unop e1 => UnE unop (subst_exp s e1)
+  | BinE bop e1 e2 => BinE bop (subst_exp s e1) (subst_exp s e2)
+  | CmpE cmop e1 e2 => CmpE cmop (subst_exp s e1) (subst_exp s e2)
+  | TupE exps => TupE (List.map (subst_exp s) exps)
+  | CaseE m e' => CaseE m (subst_exp s e')
+  | OptE (Some e') => OptE (Some (subst_exp s e'))
+  | TheE e' => TheE (subst_exp s e')
+  | ListE exps => ListE (List.map (subst_exp s) exps)
+  | LiftE e' => LiftE (subst_exp s e')
+  | StrE efields => StrE (List.map (fun p => (fst p, subst_exp s (snd p)))efields)
+  | ProjE e' n => ProjE (subst_exp s e') n
+  | LenE e' => LenE (subst_exp s e')
+  | MemE e1 e2 => MemE (subst_exp s e1) (subst_exp s e2)
+  | CatE e1 e2 => CatE (subst_exp s e1) (subst_exp s e2)
+  | CompE e1 e2 => CompE (subst_exp s e1) (subst_exp s e2)
+  | IdxE e1 e2 => IdxE (subst_exp s e1) (subst_exp s e2)
+  | SliceE e1 e2 e3 => SliceE (subst_exp s e1) (subst_exp s e2) (subst_exp s e3)
+  | UpdE e1 p e2 => UpdE (subst_exp s e1) p (subst_exp s e2)
+  | ExtE e1 p e2 => ExtE (subst_exp s e1) p (subst_exp s e2)
+  | CallE x args => CallE x (List.map (subst_arg s) args)
+  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun p => (fst p, subst_exp s (snd p))) xexps)
+  | CvtE e' nt1 nt2 => CvtE (subst_exp s e') nt1 nt2
+  | SubE e' t1 t2 => SubE (subst_exp s e') (subst_typ s t1) (subst_typ s t2)
+  | _ => e
+  end
+
+with
+
+subst_path (s : il_subst) (p : il_path) : il_path :=
+  match p with
+  | RootP => RootP
+  | IdxP p' e' => IdxP (subst_path s p') (subst_exp s e')
+  | SliceP p' e1 e2 => SliceP (subst_path s p') (subst_exp s e1) (subst_exp s e2)
+  | DotP p' a => DotP (subst_path s p') a
+  end
+
+with 
+
+subst_arg (s : il_subst) (a : il_arg) : il_arg :=
+  match a with
+  | ExpA e => ExpA (subst_exp s e)
+  | TypA t => TypA (subst_typ s t)
+  | DefA x => DefA (subst_fun s x)
+  end
+.
+
+Fixpoint subst_param (s : il_subst) (p : il_param) : il_param :=
+  match p with
+  | ExpP x t => ExpP x (subst_typ s t)
+  | TypP x => TypP x
+  | DefP x ps t => DefP x (List.map (subst_param s) ps) (subst_typ s t)
+  end
+.
+
+Definition subst_quant (s : il_subst) (p : il_quant) : il_quant := subst_param s p.
+
+Fixpoint subst_prem (s : il_subst) (p : il_prem) : il_prem :=
+  match p with
+  | RulePr x args e => RulePr x (List.map (subst_arg s) args) (subst_exp s e)
+  | IfPr e => IfPr (subst_exp s e)
+  | ElsePr => ElsePr
+  | LetPr e1 e2 => LetPr (subst_exp s e1) (subst_exp s e2)
+  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun p'' => (fst p'', subst_exp s (snd p''))) xexps)
+  | NegPr p' => NegPr (subst_prem s p')
+  end.
+
+Definition arg_for_param (a : il_arg) (p : il_param) : il_subst :=
+  match a, p with
+  | ExpA e, ExpP x _ => {| S_EXP := singleton x e; S_TYP := empty_typ; S_FUN := empty_id |}
+  | TypA t, TypP x => {| S_EXP := empty_exp; S_TYP := singleton x t; S_FUN := empty_id |}
+  | DefA y, DefP x _ _ => {| S_EXP := empty_exp; S_TYP := empty_typ; S_FUN := singleton x y |} 
+  | _, _ => subst_empty
+  end
+.
+
+Fixpoint args_for_params (ags : list il_arg) (ps : list il_param) : il_subst :=
+  match ags, ps with
+  | [], [] => subst_empty
+  | _, [] => subst_empty
+  | [], _ => subst_empty
+  | a :: ags', p :: ps' => append_subst (arg_for_param a p) (args_for_params ags' ps')
+  end
+.
+
+Definition param_to_arg (p : il_param) : il_arg :=
+  match p with
+  | ExpP x _ => ExpA (VarE x)
+  | TypP x => TypA (VarT x [])
+  | DefP x _ _ => DefA x
+  end
+.
+
+Inductive ok_subst : il_env -> il_subst -> list il_quant -> Prop := 
+  | Subst_OK : forall E s q_lst,
+    ok_subst E s q_lst.
+     
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
new file mode 100644
index 0000000000..23527648dd
--- /dev/null
+++ b/spectec/metatheory/theories/syntax.v
@@ -0,0 +1,191 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import all_ssreflect all_algebra.
+Import GRing.Theory.
+
+Parameter R : archiNumDomainType.
+
+(* SYNTAX *)
+
+Definition atom : Type := string.
+Definition mixop : Type := list (list atom).
+Definition il_id : Type := string.
+Definition text : Type := string.
+
+Inductive optyp : Type :=
+  | BoolOp
+  | NumOp
+.
+
+Inductive numunop : Type :=
+  | PlusOp
+  | MinusOp
+.
+
+Inductive boolunop : Type :=
+  | NotOp
+.
+
+Inductive unop : Type :=
+  | NumUnop : numunop -> unop
+  | BoolUnop : boolunop -> unop
+.
+
+Inductive numbinop : Type :=
+  | AddOp
+  | SubOp
+  | MulOp
+  | DivOp
+  | ModOp
+  | PowOp
+.
+
+Inductive boolbinop : Type :=
+  | AndOp
+  | OrOp
+  | ImplOp
+  | EquivOp
+.
+
+Inductive binop : Type :=
+  | NumBinop : numbinop -> binop
+  | BoolBinop : boolbinop -> binop
+.
+
+Inductive numcmpop : Type :=
+  | LtOp
+  | LeOp
+  | GtOp
+  | GeOp
+.
+
+Inductive boolcmpop : Type :=
+  | EqOp
+  | NeqOp
+.
+
+Inductive cmpop : Type :=
+  | NumCmpop : numcmpop -> cmpop
+  | BoolCmpop : boolcmpop -> cmpop
+.
+
+Inductive numtyp : Type :=
+  | NatT
+  | IntT
+  | RatT
+  | RealT
+.
+
+Inductive il_num : Type :=
+  | NatE : nat -> il_num
+  | IntE : int -> il_num
+  | RatE : rat -> il_num
+  | RealE : R -> il_num
+.
+
+Inductive il_typ : Type :=
+  | VarT : il_id -> list il_arg -> il_typ
+  | BoolT
+  | TextT
+  | NumT : numtyp -> il_typ
+  | TupT : list (il_id * il_typ) -> il_typ
+  | IterT : il_typ -> iter -> il_typ
+
+with
+
+il_exp : Type :=
+  | VarE : il_id -> il_exp
+  | BoolE : bool -> il_exp
+  | NumE : il_num -> il_exp
+  | TextE : text -> il_exp
+  | UnE : unop -> il_exp -> il_exp
+  | BinE : binop -> il_exp -> il_exp -> il_exp
+  | CmpE : cmpop -> il_exp -> il_exp -> il_exp
+  | TupE : list il_exp -> il_exp
+  | ProjE : il_exp -> nat -> il_exp
+  | CaseE : mixop -> il_exp -> il_exp
+  | UncaseE : il_exp -> mixop -> il_exp
+  | OptE : option il_exp -> il_exp
+  | TheE : il_exp -> il_exp
+  | StrE : list (atom * il_exp) -> il_exp
+  | DotE : il_exp * atom -> il_exp
+  | CompE : il_exp -> il_exp -> il_exp
+  | ListE : list il_exp -> il_exp
+  | LiftE : il_exp -> il_exp
+  | MemE : il_exp -> il_exp -> il_exp
+  | LenE : il_exp -> il_exp
+  | CatE : il_exp -> il_exp -> il_exp
+  | IdxE : il_exp -> il_exp -> il_exp
+  | SliceE : il_exp -> il_exp -> il_exp -> il_exp
+  | UpdE : il_exp -> il_path -> il_exp -> il_exp
+  | ExtE : il_exp -> il_path -> il_exp -> il_exp
+  | CallE : il_id -> list il_arg -> il_exp
+  | IterE : il_exp -> iter -> list (il_id * il_exp) -> il_exp
+  | CvtE : il_exp -> numtyp -> numtyp -> il_exp
+  | SubE : il_exp -> il_typ -> il_typ -> il_exp
+  | IfE : il_exp -> il_exp -> il_exp -> il_exp
+
+with
+
+il_path : Type :=
+  | RootP
+  | IdxP : il_path -> il_exp -> il_path
+  | SliceP : il_path -> il_exp -> il_exp -> il_path
+  | DotP : il_path -> atom -> il_path
+
+with
+
+il_arg : Type := 
+  | ExpA : il_exp -> il_arg
+  | TypA : il_typ -> il_arg
+  | DefA : il_id -> il_arg
+
+with
+
+iter : Type :=
+  | I_STAR
+  | I_OPT
+  | I_PLUS
+  | I_SUP : option il_id -> il_exp -> iter
+.
+
+
+Inductive il_param : Type :=
+  | ExpP : il_id -> il_typ -> il_param
+  | TypP : il_id -> il_param
+  | DefP : il_id -> list il_param -> il_typ -> il_param
+.
+
+Definition il_quant : Type := il_param.
+
+Inductive il_prem : Type :=
+  | RulePr : il_id -> list il_arg -> il_exp -> il_prem
+  | IfPr : il_exp -> il_prem
+  | ElsePr
+  | LetPr : il_exp -> il_exp -> il_prem
+  | IterPr : il_prem -> iter -> list (il_id * il_exp) -> il_prem
+  | NegPr : il_prem -> il_prem
+.
+
+Definition typfield : Type := atom * (list il_quant * il_typ * list il_prem).
+Definition typcase : Type := mixop * (list il_quant * il_typ * list il_prem).
+
+Inductive il_deftyp : Type :=
+  | AliasT : il_typ -> il_deftyp
+  | StructT : list typfield -> il_deftyp
+  | VariantT : list typcase -> il_deftyp
+.
+
+Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
+
+Definition il_rule : Type := il_id * list il_quant * mixop * il_exp * list il_prem.
+
+Definition il_clause : Type := list il_quant * list il_arg * il_exp * list il_prem.
+
+Inductive il_def : Type :=
+  | TypD : il_id -> list il_param -> list il_inst -> il_def
+  | RelD : il_id -> mixop -> il_typ -> list il_rule -> il_def
+  | DecD : il_id -> list il_param -> il_typ -> list il_clause -> il_def
+  | RecD : list il_def -> il_def
+.
+
+Definition script : Type := list il_def.
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
new file mode 100644
index 0000000000..08510f8d33
--- /dev/null
+++ b/spectec/metatheory/theories/typing.v
@@ -0,0 +1,96 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+From MetaSpectec Require Import syntax env.
+
+
+ 
+(* Inductive valid_unop : unop -> optyp -> il_typ -> il_typ -> Prop :=
+  | NotOp_ok : valid_unop NotOp BoolOp BoolT BoolT
+  | Minus_ok : valid_unop MinusOp NumOp (NumT NatT) (NumT NatT)
+  | Plus_ok : valid_unop PlusOp NumOp (NumT NatT) (NumT NatT)
+. *)
+(*
+Inductive valid_binop : binop -> optyp -> il_typ -> il_typ -> il_typ -> Prop :=
+  | AndOp_ok : valid_binop AndOp BoolOp BoolT BoolT BoolT
+  | OrOp_ok : valid_binop OrOp BoolOp BoolT BoolT BoolT
+  | ImplOp_ok : valid_binop ImplOp BoolOp BoolT BoolT BoolT
+  | EquivOp_ok : valid_binop EquivOp BoolOp BoolT BoolT BoolT
+  | AddOp_ok : valid_binop AddOp NumOp NatT NatT NatT
+  | SubOp_ok : valid_binop AddOp NumOp NatT NatT NatT
+  | MulOp_ok : valid_binop MulOp NumOp NatT NatT NatT
+  | DivOp_ok : valid_binop DivOp NumOp NatT NatT NatT
+  | ModOp_ok : valid_binop ModOp NumOp NatT NatT NatT
+  | PowOp_ok : valid_binop PowOp NumOp NatT NatT NatT
+.
+
+Inductive valid_cmpop : cmpop -> optyp -> il_typ -> il_typ -> il_typ -> Prop :=
+  | EqOp_ok : forall t, valid_cmpop EqOp BoolOp t t BoolT
+  | NeqOp_ok : forall t, valid_cmpop NeqOp BoolOp t t BoolT
+  | LtOp_ok : valid_cmpop LtOp NumOp NatT NatT BoolT
+  | LeOp_ok : valid_cmpop LeOp NumOp NatT NatT BoolT
+  | GtOp_ok : valid_cmpop GtOp NumOp NatT NatT BoolT
+  | GeOp_ok : valid_cmpop GeOp NumOp NatT NatT BoolT
+.
+
+Inductive valid_typ : il_env -> il_typ -> Prop :=
+  | VarT_ok : forall env il_id args params insts, 
+    env[il_id]t = (params, insts) ->
+    List.Forall2 (fun a p => valid_arg env a p) args params ->
+    valid_typ env (VarT il_id args)
+  | BoolT_ok : forall env, valid_typ env BoolT
+  | NatT_ok : forall env, valid_typ env NatT
+  | TextT_ok : forall env, valid_typ env TextT
+  | IterT_ok : forall env iter t, 
+    valid_typ env t -> valid_typ env (IterT iter t)
+  | TupT_ok : forall env typbinds,
+    List.Forall (fun p => valid_typ env (snd p)) typbinds ->
+    valid_typ env (TupT typbinds)  
+
+with
+
+valid_exp : il_env -> side -> il_exp -> il_typ -> Prop :=
+  | VarE_hole_ok : forall env t, valid_exp env LHS (VarE "_") t 
+  | VarE_ok : forall env il_id s t,
+    env[il_id]v = t ->
+    valid_exp env s (VarE il_id) t
+  | BoolE_ok : forall env s b, valid_exp env s (BoolE b) BoolT
+  | NatE_ok : forall env s n, valid_exp env s (NatE n) NatT
+  | TextE_ok : forall env s str, valid_exp env s (TextE str) TextT
+  | UnE_ok : forall env s unop op e t,
+    valid_unop unop op t t ->
+    valid_exp env s e t ->
+    valid_exp env s (UnE unop op e) t
+  | BinE_ok : forall env s binop op e1 e2 t,
+    valid_binop binop op t t t ->
+    valid_exp env s e1 t ->
+    valid_exp env s e2 t ->
+    valid_exp env s (BinE binop op e1 e2) t
+  | CmpE_ok : forall env s cmpop op e1 e2 t,
+    valid_cmpop cmpop op t t BoolT ->
+    valid_exp env s e1 t ->
+    valid_exp env s e2 t ->
+    valid_exp env s (CmpE cmpop op e1 e2) BoolT
+  | IdxE_ok : forall env s e1 e2 t,
+    valid_exp env s e1 (IterT I_STAR t) ->
+    valid_exp env s e2 NatT ->
+    valid_exp env s (IdxE e1 e2) t
+    | I_SUP : option il_ild -> il_exp -> iter
+  | SliceE_ok : forall env s e1 e2 e3 t,
+    valid_exp env s e1 t ->
+    valid_exp env s e2 NatT ->
+    valid_exp env s e3 NatT ->
+    valid_exp env s (SliceE e1 e2 e3) t
+
+with
+
+valid_arg : il_env -> il_arg -> il_param -> Prop :=
+  | ExpA_ok : forall env e il_id t, 
+    valid_exp env LHS e t ->
+    valid_arg env (ExpA e) (ExpP il_id t)
+  | TypA_ok : forall env t il_id,
+    valid_typ env t ->
+    valid_arg env (TypA t) (TypP il_id)
+  | DefA_ok : forall env il_id ps t clauses, 
+    env[il_id]d = (ps, t, clauses) ->
+    valid_arg env (DefA il_id) (DefP il_id ps t)
+. *)

From 9c96777025abbd3949b3e177577f0430b8219663 Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Tue, 17 Feb 2026 14:46:55 +0000
Subject: [PATCH 02/11] Mostly finished defining reduction rules, only
 iteration left.

---
 spectec/metatheory/theories/reduction.v | 287 +++++++++++++++++++++++-
 spectec/metatheory/theories/subst.v     |  30 ++-
 spectec/metatheory/theories/syntax.v    |   9 +-
 3 files changed, 308 insertions(+), 18 deletions(-)

diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index efcef70672..9bf8b86e70 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -3,12 +3,57 @@ From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssri
 From MetaSpectec Require Import syntax subst env numerics.
 Import ListNotations.
 
-Definition option_to_list {T: Type} (arg : option T) : seq T :=
+Definition option_forall {T : Type} (f : T -> Prop) (arg : option T) : Prop :=
 	match arg with
-		| None => nil
-		| Some a => a :: nil
+		| None => True
+		| Some a => f a
 	end.
 
+Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
+	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
+
+Definition slice {A : Type} (i j : nat) (l : list A) : list A :=
+  firstn (j - i) (skipn i l).
+
+(* PRE: i < size l *)
+Definition update {A : Type} (l : list A) (i : nat) (x : A) : list A :=
+  set_nth x l i x.
+
+Definition update_slice {A : Type} (l : list A) (i : nat) (j : nat) (xs : list A) : list A :=
+  let idx_lst := iota i (j - i) in
+  foldl (fun acc '(idx, x) => update acc idx x) l (zip idx_lst xs)
+.
+
+Definition is_plaintyp (t : il_typ) : bool :=
+  match t with
+  | VarT _ _ => false
+  | _ => true
+  end
+.
+
+Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> il_subst -> Prop :=
+  | ma_rule : forall s ags qs ags' sbst,
+    ok_subst (store_to_env s) (sbst) qs ->
+    ags = List.map (subst_arg sbst) ags' ->
+    match_args s ags qs ags' sbst
+.
+
+Inductive expand_typ : store -> il_typ -> il_deftyp -> Prop :=
+  | et_plain : forall s t,
+    is_plaintyp t ->
+    expand_typ s t (AliasT t)
+  | et_alias : forall s x ags t dt,
+    expand_typ s (VarT x ags) (AliasT t) ->
+    expand_typ s t dt ->
+    expand_typ s (VarT x ags) dt
+  | et_step : forall s e x ags ags' dt ps insts n qs sbst,
+    store_to_env s = e ->
+    StringMap.find x (TYPS e) = Some (ps, insts) ->
+    List.nth_error insts n = Some (qs, ags', dt) ->
+    match_args s ags qs ags' sbst ->
+    expand_typ s (VarT x ags) (subst_deftyp sbst dt)
+.
+
 Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   (* UnE Rules *)
   | se_unop_ctx : forall s op e1 e2,
@@ -63,7 +108,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_str_ctx : forall s fields fields',
     List.Forall2 (fun f f' => step_exp s (snd f) (snd f')) fields fields' ->
     step_exp s (StrE fields) (StrE fields')
-  (* CasE rules *)
+  (* CaseE rules *)
   | se_case_ctx : forall s m e e',
     step_exp s e e' ->
     step_exp s (CaseE m e) (CaseE m e')
@@ -74,12 +119,240 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_lift_none : forall s, step_exp s (LiftE (OptE None)) (ListE [])
   | se_list_some : forall s e , step_exp s (LiftE (OptE (Some e))) (ListE [e])
   (* ProjE rules *)
-.
+  | se_proj_ctx : forall s e e' n,
+    step_exp s e e' ->
+    step_exp s (ProjE e n) (ProjE e' n)
+  | se_proj_tup : forall s es e_n n,
+    List.nth_error es n = Some e_n ->
+    step_exp s (ProjE (TupE es) n) e_n 
+  (* LenE rules *)
+  | se_len_ctx : forall s e e',
+    step_exp s e e' ->
+    step_exp s (LenE e) (LenE e')
+  | se_len_list : forall s es,
+    step_exp s (LenE (ListE es)) (NumE (NatE (List.length es)))
+  (* MemE rules *)
+  | se_mem_ctxl : forall s e1 e2 e1',
+    step_exp s e1 e1' ->
+    step_exp s (MemE e1 e2) (MemE e1' e2)
+  | se_mem_ctxr : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (MemE e1 e2) (MemE e1 e2')
+  | se_mem_opt_true : forall s e1 e2,
+    e1 = e2 ->
+    step_exp s (MemE e1 (OptE (Some e2))) (BoolE true)
+  | se_mem_opt_false : forall s e1 e2_opt,
+    option_forall (fun e2 => e1 <> e2) e2_opt ->
+    step_exp s (MemE e1 (OptE e2_opt)) (BoolE false)
+  | se_mem_list_true : forall s e1 e2s,
+    List.In e1 e2s ->
+    step_exp s (MemE e1 (ListE e2s)) (BoolE true)
+  | se_mem_list_false : forall s e1 e2s,
+    List.Forall (fun e2 => e1 <> e2) e2s ->
+    step_exp s (MemE e1 (ListE e2s)) (BoolE false)
+  (* CatE rules *)
+  | se_cat_ctxl : forall s e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (CatE e1 e2) (CatE e1' e2)
+  | se_cat_ctxr : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (CatE e1 e2) (CatE e1 e2')
+  | se_cat_opt1 : forall s e1,
+    step_exp s (CatE (OptE (Some e1)) (OptE None)) (OptE (Some e1))
+  | se_cat_opt2 : forall s e2,
+    step_exp s (CatE (OptE None) (OptE (Some e2))) (OptE (Some e2))
+  | se_cat_list : forall s es1 es2,
+    step_exp s (CatE (ListE es1) (ListE es2)) (ListE (es1 ++ es2))
+  | se_cat_str : forall s fields1 fields2,
+    List.Forall2 (fun '(a, _) '(a', _) => a = a') fields1 fields2 ->
+    step_exp s (CatE (StrE fields1) (StrE fields2)) (StrE (list_zipWith (fun x y => (fst x, CatE (snd x) (snd y))) fields1 fields2))
+  (* AccE rules *)
+  | se_acc_ctxexp : forall s e e' p,
+    step_exp s e e' ->
+    step_exp s (AccE e p) (AccE e' p)
+  (* TODO: what does step path mean? *)
+  | se_acc_root : forall s e,
+    step_exp s (AccE e RootP) e
+  | se_acc_the : forall s e e' p,
+    step_exp s (AccE e p) (OptE (Some e')) ->
+    step_exp s (AccE e (TheP p)) e'
+  | se_acc_idx : forall s e e_lst' e_n' p n,
+    step_exp s (AccE e p) (ListE e_lst') ->
+    n < List.length e_lst' ->
+    List.nth_error e_lst' n = Some e_n' ->
+    step_exp s (AccE e (IdxP p (NumE (NatE n)))) e_n'
+  | se_acc_slice : forall s e p n m e'_lst e''_lst,
+    step_exp s (AccE e p) (ListE e'_lst) ->
+    n <= m ->
+    n < List.length e'_lst /\ (n + m) < List.length e'_lst ->
+    e''_lst = slice n m e'_lst ->
+    step_exp s (AccE e (SliceP p (NumE (NatE n)) (NumE (NatE n)))) (ListE e''_lst)
+  | se_acc_dot : forall s e p a e_n' fields n,
+    step_exp s (AccE e p) (StrE fields) ->
+    List.nth_error fields n = Some (a, e_n') ->
+    step_exp s (AccE e (DotP p a)) e_n'
+  | se_acc_uncase : forall s e p m e',
+    step_exp s (AccE e p) (CaseE m e') ->
+    step_exp s (AccE e (UncaseP p m)) e'
+  (* UpdE rules *)
+  | se_upd_ctxl : forall s e1 e1' p e2,
+    step_exp s e1 e1' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1' p e2)
+  | se_upd_ctxr : forall s e1 p e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1 p e2')
+  | se_upd_root : forall s e1 e2,
+    step_exp s (UpdE e1 RootP e2) e2
+  | se_upd_the : forall s e1 p e2 e',
+    step_exp s (AccE e1 p) (OptE (Some e')) ->
+    step_exp s (UpdE e1 (TheP p) e2) (UpdE e1 p (OptE (Some e2)))
+  | se_upd_idx : forall s e1 p n e2 e_lst',
+    step_exp s (AccE e1 p) (ListE e_lst') ->
+    n < size e_lst' ->
+    step_exp s (UpdE e1 (IdxP p (NumE (NatE n))) e2) (UpdE e1 p (ListE (update e_lst' n e2)))
+  | se_upd_slice : forall s e1 p n m e2_lst e_lst',
+    step_exp s (AccE e1 p) (ListE e_lst') ->
+    n <= m ->
+    n < size e_lst' ->
+    (n + m) < size e_lst' ->
+    step_exp s (UpdE e1 (SliceP p (NumE (NatE n)) (NumE (NatE m))) (ListE e2_lst)) (UpdE e1 p (ListE (update_slice e_lst' n m e2_lst)))
+  | se_upd_dot : forall s e1 p e2 fields a e' n,
+    step_exp s (AccE e1 p) (StrE fields) ->
+    List.nth_error fields n = Some (a, e') ->
+    step_exp s (UpdE e1 (DotP p a) e2) (UpdE e1 p (StrE (update fields n (a, e2))))
+  | se_upd_uncase : forall s e1 p m e2 e', 
+    step_exp s (AccE e1 p) (CaseE m e') ->
+    step_exp s (UpdE e1 (UncaseP p m) e2) (UpdE e1 p (CaseE m e2))
+  (* ExtE rule *)
+  | se_ext : forall s e1 p e2,
+    step_exp s (ExtE e1 p e2) (UpdE e1 p (CatE (AccE e1 p) e2))
+  (* IterE rules *)
+  | se_iter_ctx1 : forall s e it ep_lst e',
+    step_exp s e e' ->
+    step_exp s (IterE e it ep_lst) (IterE e' it ep_lst)
+  (* TODO ctx on iter and exppull? *)
+  (* | se_iter_quest : forall s e ep_lst, *)
+  (* TODO other iter rules *)
+    (* CallE rules *)
+  | se_call_ctx : forall s x ags n a a',
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_exp s (CallE x ags) (CallE x (update ags n a'))
+  | se_call_app : forall s x ags ags' ps qs t cs e prems sbst n,
+    StringMap.find x (DEFS (store_to_env s)) = Some (ps, t, cs) ->
+    List.nth_error cs n = Some (qs, ags', e, prems) ->
+    match_args s ags qs ags' sbst ->
+    reduce_prems s (List.map (subst_prem sbst) prems) [] ->
+    step_exp s (CallE x ags) (subst_exp sbst e)
+  (* CvtE rules *)
+  | se_cvt_ctx : forall s e nt1 nt2 e',
+    step_exp s e e' ->
+    step_exp s (CvtE e nt1 nt2) (CvtE e' nt1 nt2)
+  | se_cvt_num : forall s num nt1 nt2 e,
+    numcvt nt2 num = Some e ->
+    step_exp s (CvtE (NumE num) nt1 nt2) (NumE e)
+  (* SubE rules *)
+  | se_sub_ctx1 : forall s e t1 t2 e',
+    step_exp s e e' ->
+    step_exp s (SubE e t1 t2) (SubE e' t1 t2)
+  | se_sub_ctx2 : forall s e t1 t1' t2,
+    step_typ s t1 t1' ->
+    step_exp s (SubE e t1 t2) (SubE e t1' t2)
+  | se_sub_ctx3 : forall s e t1 t2 t2',
+    step_typ s t2 t2' ->
+    step_exp s (SubE e t1 t2) (SubE e t1 t2')
+  | se_sub_sub : forall s e' t1' t2' t1 t2,
+    step_exp s (SubE (SubE e' t1' t2') t1 t2) (SubE e' t1' t2)
+  | se_sub_tup : forall s es tups tups',
+    size es = size tups ->
+    size tups = size tups' ->
+    step_exp s (SubE (TupE es) (TupT tups) (TupT tups')) 
+    (TupE (List.map (fun '(e, ((_, t1), (_, t2))) => SubE e t1 t2) (zip es (zip tups tups'))))
+  (* TODO sub x's *)
+with
+
+step_arg : store -> il_arg -> il_arg -> Prop :=
+  | sa_exp : forall s e e',
+    step_exp s e e' ->
+    step_arg s (ExpA e) (ExpA e')
+  | sa_typ : forall s t t',
+    step_typ s t t' ->
+    step_arg s (TypA t) (TypA t')
+with
+
+step_typ : store -> il_typ -> il_typ -> Prop :=
+  | st_var_ctx : forall s x ags n a a',
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_typ s (VarT x ags) (VarT x (update ags n a'))
+  | st_var_app : forall s x ags t, 
+    expand_typ s (VarT x ags) (AliasT t) ->
+    step_typ s (VarT x ags) t
+  | st_tup_ctx : forall s tups n x t,
+    List.nth_error tups n = Some (x, t) ->
+    step_typ s (TupT tups) (TupT (update tups n (x, t)))
+  | st_iter_ctx : forall s t t' it,
+    step_typ s t t' ->
+    step_typ s (IterT t it) (IterT t' it)
 
-Inductive reduce_exp : store -> il_exp -> il_exp -> Prop :=
+with
+
+step_prems : store -> list il_prem -> list il_prem -> Prop :=
+  | sp_ctx : forall s p ps p' ps',
+    step_prems s [p] p' ->
+    step_prems s (p :: ps) (p' ++ ps')
+  (* IfPr rules *)
+  | sp_if_ctx : forall s e e',
+    step_exp s e e' ->
+    step_prems s [IfPr e] [IfPr e']
+  | sp_if_true : forall s,
+    step_prems s [IfPr (BoolE true)] []
+  (* LetPr rules *)
+  | sp_let_ctx : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_prems s [LetPr e1 e2] [LetPr e1 e2']
+  | sp_let : forall s e1 e2 e1' e2',
+    reduce_exp s e1 e1' ->
+    reduce_exp s e2 e2' ->
+    e1' = e2' ->
+    step_prems s [LetPr e1 e2] []
+  (* IterPr rules *)
+  | sp_iter_ctxl : forall s p it eps p',
+    step_prems s [p] [p'] ->
+    step_prems s [IterPr p it eps] [IterPr p' it eps]
+  (* TODO ctx for iter and exppull? *)
+  (* TODO other iter rules *)
+with
+
+reduce_exp : store -> il_exp -> il_exp -> Prop :=
   | re_refl : forall s e, reduce_exp s e e
-  | re_step : forall s e1 e2 e3, 
+  | re_step : forall s e1 e2 e3,
+    step_exp s e1 e3 ->
     reduce_exp s e2 e3 ->
     reduce_exp s e1 e3
+
+with
+
+reduce_prems : store -> list il_prem -> list il_prem -> Prop :=
+  | rp_refl : forall s p, reduce_prems s p p
+  | rp_step : forall s p1 p2 p3,
+    step_prems s p1 p2 ->
+    reduce_prems s p2 p3 ->
+    reduce_prems s p1 p3
+.
+
+Inductive reduce_arg : store -> il_arg -> il_arg -> Prop :=
+  | ra_refl : forall s a, reduce_arg s a a
+  | ra_step : forall s a1 a2 a3,
+    step_arg s a1 a2 ->
+    reduce_arg s a2 a3 ->
+    reduce_arg s a1 a3
 .
 
+Inductive reduce_typ : store -> il_typ -> il_typ -> Prop :=
+  | rt_refl : forall s t, reduce_typ s t t
+  | rt_step : forall s t1 t2 t3,
+    step_typ s t1 t2 ->
+    reduce_typ s t2 t3 ->
+    reduce_typ s t1 t3
+.
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index 213bf5db60..a7ce492bad 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -71,6 +71,8 @@ Fixpoint bound_params (ps : list il_param) : dom :=
   end
 .
 
+(* TODO handle capture avoidance *)
+
 Definition subst_fun (s : il_subst) (x : il_id) : il_id :=
   match StringMap.find x s.(S_FUN) with
   | Some y => y
@@ -92,7 +94,7 @@ Fixpoint subst_typ (s : il_subst) (t : il_typ) : il_typ :=
     | Some t' => t'
     | None => VarT x (List.map (subst_arg s) args)
     end
-  | TupT xts => TupT (List.map (fun p => (fst p, subst_typ s (snd p))) xts)
+  | TupT xts => TupT (List.map (fun '(x, t) => (x, subst_typ s t)) xts)
   | IterT t' it => IterT (subst_typ s t') (subst_iter s it)
   | _ => t
   end
@@ -112,10 +114,9 @@ subst_exp (s : il_subst) (e : il_exp) : il_exp :=
   | TupE exps => TupE (List.map (subst_exp s) exps)
   | CaseE m e' => CaseE m (subst_exp s e')
   | OptE (Some e') => OptE (Some (subst_exp s e'))
-  | TheE e' => TheE (subst_exp s e')
   | ListE exps => ListE (List.map (subst_exp s) exps)
   | LiftE e' => LiftE (subst_exp s e')
-  | StrE efields => StrE (List.map (fun p => (fst p, subst_exp s (snd p)))efields)
+  | StrE efields => StrE (List.map (fun '(a, e) => (a, subst_exp s e))efields)
   | ProjE e' n => ProjE (subst_exp s e') n
   | LenE e' => LenE (subst_exp s e')
   | MemE e1 e2 => MemE (subst_exp s e1) (subst_exp s e2)
@@ -123,10 +124,11 @@ subst_exp (s : il_subst) (e : il_exp) : il_exp :=
   | CompE e1 e2 => CompE (subst_exp s e1) (subst_exp s e2)
   | IdxE e1 e2 => IdxE (subst_exp s e1) (subst_exp s e2)
   | SliceE e1 e2 e3 => SliceE (subst_exp s e1) (subst_exp s e2) (subst_exp s e3)
-  | UpdE e1 p e2 => UpdE (subst_exp s e1) p (subst_exp s e2)
-  | ExtE e1 p e2 => ExtE (subst_exp s e1) p (subst_exp s e2)
+  | AccE e' p => AccE (subst_exp s e') (subst_path s p)
+  | UpdE e1 p e2 => UpdE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
+  | ExtE e1 p e2 => ExtE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
   | CallE x args => CallE x (List.map (subst_arg s) args)
-  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun p => (fst p, subst_exp s (snd p))) xexps)
+  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun '(x, e) => (x, subst_exp s e)) xexps)
   | CvtE e' nt1 nt2 => CvtE (subst_exp s e') nt1 nt2
   | SubE e' t1 t2 => SubE (subst_exp s e') (subst_typ s t1) (subst_typ s t2)
   | _ => e
@@ -140,6 +142,8 @@ subst_path (s : il_subst) (p : il_path) : il_path :=
   | IdxP p' e' => IdxP (subst_path s p') (subst_exp s e')
   | SliceP p' e1 e2 => SliceP (subst_path s p') (subst_exp s e1) (subst_exp s e2)
   | DotP p' a => DotP (subst_path s p') a
+  | TheP p' => TheP (subst_path s p')
+  | UncaseP p' m => UncaseP (subst_path s p') m 
   end
 
 with 
@@ -168,7 +172,7 @@ Fixpoint subst_prem (s : il_subst) (p : il_prem) : il_prem :=
   | IfPr e => IfPr (subst_exp s e)
   | ElsePr => ElsePr
   | LetPr e1 e2 => LetPr (subst_exp s e1) (subst_exp s e2)
-  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun p'' => (fst p'', subst_exp s (snd p''))) xexps)
+  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun '(x, e) => (x, subst_exp s e)) xexps)
   | NegPr p' => NegPr (subst_prem s p')
   end.
 
@@ -190,6 +194,18 @@ Fixpoint args_for_params (ags : list il_arg) (ps : list il_param) : il_subst :=
   end
 .
 
+Definition subst_deftyp (s : il_subst) (dt : il_deftyp) : il_deftyp :=
+  match dt with
+  | AliasT t => AliasT (subst_typ s t)
+  | StructT typfields => StructT (List.map (fun '(a, qs, t, prems) =>
+    (a, List.map (subst_quant s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typfields)
+  | VariantT typcases => VariantT (List.map (fun '(m, qs, t, prems) =>
+    (m, List.map (subst_quant s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typcases)
+  end
+.
+
 Definition param_to_arg (p : il_param) : il_arg :=
   match p with
   | ExpP x _ => ExpA (VarE x)
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 23527648dd..93fac65297 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -103,9 +103,7 @@ il_exp : Type :=
   | TupE : list il_exp -> il_exp
   | ProjE : il_exp -> nat -> il_exp
   | CaseE : mixop -> il_exp -> il_exp
-  | UncaseE : il_exp -> mixop -> il_exp
   | OptE : option il_exp -> il_exp
-  | TheE : il_exp -> il_exp
   | StrE : list (atom * il_exp) -> il_exp
   | DotE : il_exp * atom -> il_exp
   | CompE : il_exp -> il_exp -> il_exp
@@ -116,6 +114,7 @@ il_exp : Type :=
   | CatE : il_exp -> il_exp -> il_exp
   | IdxE : il_exp -> il_exp -> il_exp
   | SliceE : il_exp -> il_exp -> il_exp -> il_exp
+  | AccE : il_exp -> il_path -> il_exp
   | UpdE : il_exp -> il_path -> il_exp -> il_exp
   | ExtE : il_exp -> il_path -> il_exp -> il_exp
   | CallE : il_id -> list il_arg -> il_exp
@@ -129,6 +128,8 @@ with
 il_path : Type :=
   | RootP
   | IdxP : il_path -> il_exp -> il_path
+  | TheP : il_path -> il_path
+  | UncaseP : il_path -> mixop -> il_path 
   | SliceP : il_path -> il_exp -> il_exp -> il_path
   | DotP : il_path -> atom -> il_path
 
@@ -166,8 +167,8 @@ Inductive il_prem : Type :=
   | NegPr : il_prem -> il_prem
 .
 
-Definition typfield : Type := atom * (list il_quant * il_typ * list il_prem).
-Definition typcase : Type := mixop * (list il_quant * il_typ * list il_prem).
+Definition typfield : Type := atom * list il_quant * il_typ * list il_prem.
+Definition typcase : Type := mixop * list il_quant * il_typ * list il_prem.
 
 Inductive il_deftyp : Type :=
   | AliasT : il_typ -> il_deftyp

From b1e54c6dcfe6def2bf26b85ec507f6d048dc8e3f Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Tue, 17 Feb 2026 14:53:54 +0000
Subject: [PATCH 03/11] Additional rules for Negpr and IfE

---
 spectec/metatheory/theories/reduction.v | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 9bf8b86e70..9a24ea21b4 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -233,7 +233,8 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   (* TODO ctx on iter and exppull? *)
   (* | se_iter_quest : forall s e ep_lst, *)
   (* TODO other iter rules *)
-    (* CallE rules *)
+
+  (* CallE rules *)
   | se_call_ctx : forall s x ags n a a',
     List.nth_error ags n = Some a ->
     step_arg s a a' ->
@@ -269,6 +270,21 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     step_exp s (SubE (TupE es) (TupT tups) (TupT tups')) 
     (TupE (List.map (fun '(e, ((_, t1), (_, t2))) => SubE e t1 t2) (zip es (zip tups tups'))))
   (* TODO sub x's *)
+  
+  (* IfE rules *)
+  | se_ife_ctx1 : forall s e1 e2 e3 e1',
+    step_exp s e1 e1' ->
+    step_exp s (IfE e1 e2 e3) (IfE e1' e2 e3)
+  | se_ife_ctx2 : forall s e1 e2 e3 e2',
+    step_exp s e2 e2' ->
+    step_exp s (IfE e1 e2 e3) (IfE e1 e2' e3)
+  | se_ife_ctx3 : forall s e1 e2 e3 e3',
+    step_exp s e3 e3' -> 
+    step_exp s (IfE e1 e2 e3) (IfE e1 e2 e3')
+  | se_ife_true : forall s e2 e3,
+    step_exp s (IfE (BoolE true) e2 e3) e2
+  | se_ife_false : forall s e2 e3,
+    step_exp s (IfE (BoolE false) e2 e3) e3 
 with
 
 step_arg : store -> il_arg -> il_arg -> Prop :=
@@ -322,6 +338,12 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     step_prems s [IterPr p it eps] [IterPr p' it eps]
   (* TODO ctx for iter and exppull? *)
   (* TODO other iter rules *)
+  (* NegPr rules *)
+  | sp_neg_ctx : forall s p p',
+    step_prems s [p] [p'] ->
+    step_prems s [NegPr p] [NegPr p']
+  | sp_neg_bool: forall s b,
+    step_prems s [NegPr (IfPr (BoolE b))] [IfPr (BoolE (negb b))]
 with
 
 reduce_exp : store -> il_exp -> il_exp -> Prop :=

From a2305934484426368bbdeee70e514caf880d8f64 Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Tue, 17 Feb 2026 19:34:15 +0000
Subject: [PATCH 04/11] Start on typing rules

---
 spectec/metatheory/theories/env.v       |  30 +++-
 spectec/metatheory/theories/reduction.v |  11 +-
 spectec/metatheory/theories/subst.v     |  16 +-
 spectec/metatheory/theories/typing.v    | 210 ++++++++++++++----------
 4 files changed, 166 insertions(+), 101 deletions(-)

diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
index d811ffbe5c..79be6ce5e6 100644
--- a/spectec/metatheory/theories/env.v
+++ b/spectec/metatheory/theories/env.v
@@ -6,6 +6,13 @@ From MetaSpectec Require Import syntax.
 
 Module StringMap := FMapAVL.Make(String_as_OT).
 
+Definition union {A}
+  (m1 m2 : StringMap.t A) : StringMap.t A :=
+  StringMap.fold (fun k v => StringMap.add k v) m1 m2.
+
+Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
+  StringMap.add k v (StringMap.empty A).
+
 (* TYPING *)
 
 Definition var_def : Type := il_typ.
@@ -22,6 +29,24 @@ Record il_env := {
   RELS : StringMap.t rel_def
 }.
 
+Definition empty_vars : StringMap.t var_def := StringMap.empty var_def.
+Definition empty_typs : StringMap.t typ_def := StringMap.empty typ_def.
+Definition empty_defs : StringMap.t definition_def := StringMap.empty definition_def.
+Definition empty_rels : StringMap.t rel_def := StringMap.empty rel_def.
+
+Definition env_empty : il_env := {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition append_env (e1 e2 : il_env) : il_env :=
+{|
+  VARS := union e1.(VARS) e2.(VARS);
+  TYPS := union e1.(TYPS) e2.(TYPS);
+  DEFS := union e1.(DEFS) e2.(DEFS);
+  RELS := union e1.(RELS) e2.(RELS) 
+|}.
+
+Definition single_var (x : il_id) (t : il_typ) : il_env :=
+  {| VARS := singleton x t; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
 Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20).
 Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20).
 Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20).
@@ -34,4 +59,7 @@ Record store := {
 }.
 
 Definition store_to_env (s : store) : il_env :=
-  {| VARS := StringMap.empty var_def; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
\ No newline at end of file
+  {| VARS := empty_vars; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
+
+Definition env_to_store (e : il_env) : store :=
+  {| S_TYPS := e.(TYPS); S_DEFS := e.(DEFS); S_RELS := e.(RELS) |}.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 9a24ea21b4..cfd19fe378 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -3,11 +3,12 @@ From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssri
 From MetaSpectec Require Import syntax subst env numerics.
 Import ListNotations.
 
-Definition option_forall {T : Type} (f : T -> Prop) (arg : option T) : Prop :=
-	match arg with
-		| None => True
-		| Some a => f a
-	end.
+Inductive option_forall {T : Type} (P : (T -> Prop)) : option T -> Prop :=
+	| opt_none : option_forall P None
+  | opt_some : forall x,
+    P x ->
+    option_forall P (Some x)
+.
 
 Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
 	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index a7ce492bad..974084bf2a 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -5,11 +5,6 @@ Require Import Stdlib.FSets.FMapAVL.
 Require Import Stdlib.Structures.OrderedTypeEx.
 Import ListNotations.
 
-Module StringMap := FMapAVL.Make(String_as_OT).
-
-Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
-  StringMap.add k v (StringMap.empty A).
-
 Record il_subst : Type := 
   {
   S_EXP : StringMap.t il_exp;
@@ -23,10 +18,6 @@ Definition empty_typ : StringMap.t il_typ := StringMap.empty il_typ.
 Definition empty_id : StringMap.t il_id := StringMap.empty il_id.
 Definition subst_empty : il_subst := {| S_EXP := empty_exp; S_TYP := empty_typ; S_FUN := empty_id |}.
 
-Definition union {A}
-  (m1 m2 : StringMap.t A) : StringMap.t A :=
-  StringMap.fold (fun k v => StringMap.add k v) m1 m2.
-
 Definition append_subst (s1 s2 : il_subst) : il_subst :=
   {|
   S_EXP := union s1.(S_EXP) s2.(S_EXP);
@@ -34,6 +25,13 @@ Definition append_subst (s1 s2 : il_subst) : il_subst :=
   S_FUN := union s1.(S_FUN) s2.(S_FUN) 
   |}.
 
+Definition subst_svar (x : il_id) (e : il_exp) : il_subst :=
+  {|
+  S_EXP := singleton x e;
+  S_TYP := empty_typ;
+  S_FUN := empty_id
+  |}.
+
 Record dom : Type :=
   {
   D_EXP : list il_id;
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index 08510f8d33..ad949deaf1 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -1,96 +1,134 @@
 From Stdlib Require Import List String Reals.
 From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
-From MetaSpectec Require Import syntax env.
+From MetaSpectec Require Import syntax env reduction subst.
+Import ListNotations.
 
-
- 
-(* Inductive valid_unop : unop -> optyp -> il_typ -> il_typ -> Prop :=
-  | NotOp_ok : valid_unop NotOp BoolOp BoolT BoolT
-  | Minus_ok : valid_unop MinusOp NumOp (NumT NatT) (NumT NatT)
-  | Plus_ok : valid_unop PlusOp NumOp (NumT NatT) (NumT NatT)
-. *)
-(*
-Inductive valid_binop : binop -> optyp -> il_typ -> il_typ -> il_typ -> Prop :=
-  | AndOp_ok : valid_binop AndOp BoolOp BoolT BoolT BoolT
-  | OrOp_ok : valid_binop OrOp BoolOp BoolT BoolT BoolT
-  | ImplOp_ok : valid_binop ImplOp BoolOp BoolT BoolT BoolT
-  | EquivOp_ok : valid_binop EquivOp BoolOp BoolT BoolT BoolT
-  | AddOp_ok : valid_binop AddOp NumOp NatT NatT NatT
-  | SubOp_ok : valid_binop AddOp NumOp NatT NatT NatT
-  | MulOp_ok : valid_binop MulOp NumOp NatT NatT NatT
-  | DivOp_ok : valid_binop DivOp NumOp NatT NatT NatT
-  | ModOp_ok : valid_binop ModOp NumOp NatT NatT NatT
-  | PowOp_ok : valid_binop PowOp NumOp NatT NatT NatT
+Inductive composable_typ : il_env -> il_typ -> Prop :=
+  | ct_iter : forall env t t' it,
+    expand_typ (env_to_store env) t (AliasT (IterT t' it)) ->
+    composable_typ env t
+  | ct_struct : forall env t typfields,
+    expand_typ (env_to_store env) t (StructT typfields) ->
+    List.Forall (fun p => composable_typ env (snd (fst p))) typfields ->
+    composable_typ env t
 .
 
-Inductive valid_cmpop : cmpop -> optyp -> il_typ -> il_typ -> il_typ -> Prop :=
-  | EqOp_ok : forall t, valid_cmpop EqOp BoolOp t t BoolT
-  | NeqOp_ok : forall t, valid_cmpop NeqOp BoolOp t t BoolT
-  | LtOp_ok : valid_cmpop LtOp NumOp NatT NatT BoolT
-  | LeOp_ok : valid_cmpop LeOp NumOp NatT NatT BoolT
-  | GtOp_ok : valid_cmpop GtOp NumOp NatT NatT BoolT
-  | GeOp_ok : valid_cmpop GeOp NumOp NatT NatT BoolT
+Inductive sub_numtyp : numtyp -> numtyp -> Prop :=
+  | sn_nat : sub_numtyp NatT IntT
+  | sn_int : sub_numtyp IntT RatT
+  | sn_rat : sub_numtyp RatT RealT
+  | sn_rfl : forall nt, sub_numtyp nt nt
+  | sn_trans : forall nt1 nt2 nt,
+    sub_numtyp nt1 nt ->
+    sub_numtyp nt nt2 ->
+    sub_numtyp nt1 nt2
 .
 
-Inductive valid_typ : il_env -> il_typ -> Prop :=
-  | VarT_ok : forall env il_id args params insts, 
-    env[il_id]t = (params, insts) ->
-    List.Forall2 (fun a p => valid_arg env a p) args params ->
-    valid_typ env (VarT il_id args)
-  | BoolT_ok : forall env, valid_typ env BoolT
-  | NatT_ok : forall env, valid_typ env NatT
-  | TextT_ok : forall env, valid_typ env TextT
-  | IterT_ok : forall env iter t, 
-    valid_typ env t -> valid_typ env (IterT iter t)
-  | TupT_ok : forall env typbinds,
-    List.Forall (fun p => valid_typ env (snd p)) typbinds ->
-    valid_typ env (TupT typbinds)  
-
-with
+Inductive sub_typ : il_env -> il_typ -> il_typ -> Prop :=
+  | st_tup : forall env x1 t1 x2 t2 tups tups',
+    let env' := (single_var x1 t1) in
+    let sbst := (subst_svar x2 (VarE x1)) in
+    sub_typ env t1 t2 ->
+    sub_typ (append_env env env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
+    sub_typ env (TupT ((x1, t1) :: tups)) (TupT ((x2, t2) :: tups'))
+  | st_struct : forall env t1 t2 tfs1 tfs2,
+    expand_typ (env_to_store env) t1 (StructT tfs1) ->
+    expand_typ (env_to_store env) t2 (StructT tfs2) -> 
+    sub_typ env t1 t2
+.
 
-valid_exp : il_env -> side -> il_exp -> il_typ -> Prop :=
-  | VarE_hole_ok : forall env t, valid_exp env LHS (VarE "_") t 
-  | VarE_ok : forall env il_id s t,
-    env[il_id]v = t ->
-    valid_exp env s (VarE il_id) t
-  | BoolE_ok : forall env s b, valid_exp env s (BoolE b) BoolT
-  | NatE_ok : forall env s n, valid_exp env s (NatE n) NatT
-  | TextE_ok : forall env s str, valid_exp env s (TextE str) TextT
-  | UnE_ok : forall env s unop op e t,
-    valid_unop unop op t t ->
-    valid_exp env s e t ->
-    valid_exp env s (UnE unop op e) t
-  | BinE_ok : forall env s binop op e1 e2 t,
-    valid_binop binop op t t t ->
-    valid_exp env s e1 t ->
-    valid_exp env s e2 t ->
-    valid_exp env s (BinE binop op e1 e2) t
-  | CmpE_ok : forall env s cmpop op e1 e2 t,
-    valid_cmpop cmpop op t t BoolT ->
-    valid_exp env s e1 t ->
-    valid_exp env s e2 t ->
-    valid_exp env s (CmpE cmpop op e1 e2) BoolT
-  | IdxE_ok : forall env s e1 e2 t,
-    valid_exp env s e1 (IterT I_STAR t) ->
-    valid_exp env s e2 NatT ->
-    valid_exp env s (IdxE e1 e2) t
-    | I_SUP : option il_ild -> il_exp -> iter
-  | SliceE_ok : forall env s e1 e2 e3 t,
-    valid_exp env s e1 t ->
-    valid_exp env s e2 NatT ->
-    valid_exp env s e3 NatT ->
-    valid_exp env s (SliceE e1 e2 e3) t
+Inductive ok_numunop : numunop -> numtyp -> numtyp -> Prop :=
+  | ok_unop_sign : forall numop nt,
+    sub_numtyp IntT nt ->
+    ok_numunop numop nt nt
+.
 
-with
+Inductive ok_numbinop : numbinop -> numtyp -> numtyp -> numtyp -> Prop :=
+  | ok_binop_add : forall nt, ok_numbinop AddOp nt nt nt
+  | ok_binop_sub : forall nt nt',
+    sub_numtyp IntT nt' ->
+    ok_numbinop SubOp nt nt nt'
+  | ok_binop_mul : forall nt, ok_numbinop MulOp nt nt nt
+  | ok_binop_div : forall nt nt',
+    sub_numtyp RatT nt' ->
+    ok_numbinop DivOp nt nt nt'
+  | ok_binop_mod : forall nt,
+    sub_numtyp nt IntT ->
+    ok_numbinop ModOp nt nt nt
+  | ok_binop_pownat : forall nt, ok_numbinop PowOp nt NatT nt
+  | ok_binop_powint : forall nt,
+    sub_numtyp nt RatT ->
+    ok_numbinop PowOp nt IntT nt
+.
 
-valid_arg : il_env -> il_arg -> il_param -> Prop :=
-  | ExpA_ok : forall env e il_id t, 
-    valid_exp env LHS e t ->
-    valid_arg env (ExpA e) (ExpP il_id t)
-  | TypA_ok : forall env t il_id,
-    valid_typ env t ->
-    valid_arg env (TypA t) (TypP il_id)
-  | DefA_ok : forall env il_id ps t clauses, 
-    env[il_id]d = (ps, t, clauses) ->
-    valid_arg env (DefA il_id) (DefP il_id ps t)
-. *)
+Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
+  | oke_bool : forall env b, ok_exp env (BoolE b) BoolT
+  | oke_nat : forall env n, ok_exp env (NumE (NatE n)) (NumT NatT)
+  | oke_int : forall env i, ok_exp env (NumE (IntE i)) (NumT IntT)
+  | oke_rat : forall env q, ok_exp env (NumE (RatE q)) (NumT RatT)
+  | oke_real : forall env r, ok_exp env (NumE (RealE r)) (NumT RealT)
+  | oke_text : forall env t, ok_exp env (TextE t) TextT
+  | oke_unop_bool : forall env bop e,
+    ok_exp env e BoolT ->
+    ok_exp env (UnE (BoolUnop bop) e) BoolT
+  | oke_unop_num : forall env numop e nt nt',
+    ok_exp env e (NumT nt) ->
+    ok_numunop numop nt nt' ->
+    ok_exp env (UnE (NumUnop numop) e) (NumT nt')
+  | oke_binop_bool : forall env bop e1 e2,
+    ok_exp env e1 BoolT ->
+    ok_exp env e2 BoolT ->
+    ok_exp env (BinE (BoolBinop bop) e1 e2) BoolT
+  | oke_binop_num : forall env numop e1 e2 nt1 nt2 nt,
+    ok_exp env e1 (NumT nt1) ->
+    ok_exp env e2 (NumT nt2) ->
+    ok_numbinop numop nt1 nt2 nt ->
+    ok_exp env (BinE (NumBinop numop) e1 e2) (NumT nt)
+  | oke_cmp_bool : forall env bop e1 e2 t,
+    ok_exp env e1 t ->
+    ok_exp env e2 t ->
+    ok_exp env (CmpE (BoolCmpop bop) e1 e2) BoolT
+  | oke_cmp_num : forall env numop e1 e2 nt,
+    ok_exp env e1 (NumT nt) ->
+    ok_exp env e2 (NumT nt) ->
+    ok_exp env (CmpE (NumCmpop numop) e1 e2) BoolT
+  | oke_tup_eps : forall env, ok_exp env (TupE []) (TupT [])
+  | oke_tup_cons : forall env e1 es x1 t1 tups,
+    let sbst := (subst_svar x1 e1) in
+    ok_exp env e1 t1 ->
+    ok_exp env (TupE es) (subst_typ sbst (TupT tups)) ->
+    ok_exp env (TupE (e1 :: es)) (TupT ((x1, t1) :: tups))
+  | oke_opt : forall env e_opt t,
+    option_forall (fun e => ok_exp env e t) e_opt ->
+    ok_exp env (OptE e_opt) (IterT t I_OPT)
+  | oke_list : forall env es t,
+    List.Forall (fun e => ok_exp env e t) es ->
+    ok_exp env (ListE es) (IterT t I_STAR)
+  | oke_lift : forall env e t,
+    ok_exp env e (IterT t I_OPT) ->
+    ok_exp env e (IterT t I_STAR)
+  | oke_case : forall env m e x ags tcs n t qs ps,
+    expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
+    List.nth_error tcs n = Some (m, qs, t, ps) ->
+    ok_exp env e t ->
+    ok_exp env (CaseE m e) (VarT x ags)
+  | oke_str : forall env a e x ags tfs fs n t qs ps,
+    expand_typ (env_to_store env) (VarT x ags) (StructT tfs) ->
+    size tfs = size fs ->
+    List.nth_error tfs n = Some (a, qs, t, ps) ->
+    List.nth_error fs n = Some (a, e) ->
+    ok_exp env e t ->
+    ok_exp env (StrE fs) (VarT x ags)
+  (* TODO rule for ProjE *)
+  | oke_len : forall env e t,
+    ok_exp env e (IterT t I_STAR) ->
+    ok_exp env (LenE e) (NumT NatT)
+  | oke_mem : forall env e1 e2 t1,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 (IterT t1 I_STAR) ->
+    ok_exp env (MemE e1 e2) BoolT
+  | oke_cat : forall env e1 e2 t,
+    ok_exp env e1 (IterT t I_STAR) ->
+    ok_exp env e2 (IterT t I_STAR) ->
+    ok_exp env (CatE e1 e2) (IterT t I_STAR)
+.
\ No newline at end of file

From 6e77d3ab99135d555b66deacb1641ae3b4dc8d6c Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Mon, 23 Feb 2026 15:37:43 +0000
Subject: [PATCH 05/11] Added more contextual reduction rules.

---
 spectec/metatheory/theories/reduction.v | 47 ++++++++++++++++++++++++-
 spectec/metatheory/theories/syntax.v    |  1 +
 2 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index cfd19fe378..806f0561a2 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -171,6 +171,9 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_acc_ctxexp : forall s e e' p,
     step_exp s e e' ->
     step_exp s (AccE e p) (AccE e' p)
+  | se_acc_ctxpath : forall s e p p',
+    step_path s p p' ->
+    step_exp s (AccE e p) (AccE e p')
   (* TODO: what does step path mean? *)
   | se_acc_root : forall s e,
     step_exp s (AccE e RootP) e
@@ -199,6 +202,9 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_upd_ctxl : forall s e1 e1' p e2,
     step_exp s e1 e1' ->
     step_exp s (UpdE e1 p e2) (UpdE e1' p e2)
+  | se_upd_ctxm : forall s e1 p p' e2,
+    step_path s p p' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1 p' e2)
   | se_upd_ctxr : forall s e1 p e2 e2',
     step_exp s e2 e2' ->
     step_exp s (UpdE e1 p e2) (UpdE e1 p e2')
@@ -231,7 +237,10 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_iter_ctx1 : forall s e it ep_lst e',
     step_exp s e e' ->
     step_exp s (IterE e it ep_lst) (IterE e' it ep_lst)
-  (* TODO ctx on iter and exppull? *)
+  | se_iter_ctx2 : forall s e it it' ep_lst,
+    step_iter s it it' ->
+    step_exp s (IterE e it ep_lst) (IterE e it' ep_lst)
+  (* TODO ctx on exppull? *)
   (* | se_iter_quest : forall s e ep_lst, *)
   (* TODO other iter rules *)
 
@@ -314,6 +323,34 @@ step_typ : store -> il_typ -> il_typ -> Prop :=
 
 with
 
+step_path : store -> il_path -> il_path -> Prop :=
+  | sp_idx_ctxl : forall s p p' e,
+    step_path s p p' ->
+    step_path s (IdxP p e) (IdxP p' e)
+  | sp_idx_ctxr : forall s p e e',
+    step_exp s e e' ->
+    step_path s (IdxP p e) (IdxP p e')
+  | sp_the_ctx : forall s p p',
+    step_path s p p' ->
+    step_path s (TheP p) (TheP p')
+  | sp_uncase_ctx : forall s m p p',
+    step_path s p p' ->
+    step_path s (UncaseP p m) (UncaseP p' m)
+  | sp_slice_ctx1 : forall s p p' e1 e2,
+    step_path s p p' ->
+    step_path s (SliceP p e1 e2) (SliceP p' e1 e2)
+  | sp_slice_ctx2 : forall s p e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_path s (SliceP p e1 e2) (SliceP p e1' e2)
+  | sp_slice_ctx3 : forall s p e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_path s (SliceP p e1 e2) (SliceP p e1 e2')
+  | sp_dot_ctx : forall s p p' a, 
+    step_path s p p' ->
+    step_path s (DotP p a) (DotP p' a) 
+
+with 
+
 step_prems : store -> list il_prem -> list il_prem -> Prop :=
   | sp_ctx : forall s p ps p' ps',
     step_prems s [p] p' ->
@@ -345,8 +382,16 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     step_prems s [NegPr p] [NegPr p']
   | sp_neg_bool: forall s b,
     step_prems s [NegPr (IfPr (BoolE b))] [IfPr (BoolE (negb b))]
+
 with
 
+step_iter : store -> iter -> iter -> Prop :=
+  | si_ctx : forall s x e e',
+    step_exp s e e' ->
+    step_iter s (I_SUP x e) (I_SUP x e')
+
+with 
+
 reduce_exp : store -> il_exp -> il_exp -> Prop :=
   | re_refl : forall s e, reduce_exp s e e
   | re_step : forall s e1 e2 e3,
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 93fac65297..60fa7ace69 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -149,6 +149,7 @@ iter : Type :=
   | I_SUP : option il_id -> il_exp -> iter
 .
 
+Definition exppull : Type := (il_id * il_exp).
 
 Inductive il_param : Type :=
   | ExpP : il_id -> il_typ -> il_param

From e6beb1aa363fefe34864999c02328432b76fb28a Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Mon, 23 Feb 2026 16:13:24 +0000
Subject: [PATCH 06/11] Some more typing rules.

---
 spectec/metatheory/theories/reduction.v |  8 +++
 spectec/metatheory/theories/typing.v    | 94 +++++++++++++++++++++++--
 2 files changed, 97 insertions(+), 5 deletions(-)

diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 806f0561a2..ed1855526c 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -424,3 +424,11 @@ Inductive reduce_typ : store -> il_typ -> il_typ -> Prop :=
     reduce_typ s t2 t3 ->
     reduce_typ s t1 t3
 .
+
+Inductive eq_typ : store -> il_typ -> il_typ -> Prop :=
+  | eq_typ_rule : forall s t1 t2 t1' t2',
+    reduce_typ s t1 t1' ->
+    reduce_typ s t2 t2' ->
+    t1' = t2' ->
+    eq_typ s t1 t2
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index ad949deaf1..b3647864a5 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -107,16 +107,16 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
   | oke_lift : forall env e t,
     ok_exp env e (IterT t I_OPT) ->
     ok_exp env e (IterT t I_STAR)
-  | oke_case : forall env m e x ags tcs n t qs ps,
+  | oke_case : forall env m e x ags tcs t qs ps,
     expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
-    List.nth_error tcs n = Some (m, qs, t, ps) ->
+    List.In (m, qs, t, ps) tcs ->
     ok_exp env e t ->
     ok_exp env (CaseE m e) (VarT x ags)
-  | oke_str : forall env a e x ags tfs fs n t qs ps,
+  | oke_str : forall env a e x ags tfs fs t qs ps,
     expand_typ (env_to_store env) (VarT x ags) (StructT tfs) ->
     size tfs = size fs ->
-    List.nth_error tfs n = Some (a, qs, t, ps) ->
-    List.nth_error fs n = Some (a, e) ->
+    List.In (a, qs, t, ps) tfs ->
+    List.In (a, e) fs ->
     ok_exp env e t ->
     ok_exp env (StrE fs) (VarT x ags)
   (* TODO rule for ProjE *)
@@ -131,4 +131,88 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
     ok_exp env e1 (IterT t I_STAR) ->
     ok_exp env e2 (IterT t I_STAR) ->
     ok_exp env (CatE e1 e2) (IterT t I_STAR)
+  | oke_comp : forall env e1 e2 t,
+    ok_exp env e1 t ->
+    ok_exp env e2 t ->
+    composable_typ env t ->
+    ok_exp env (CompE e1 e2) t
+  | oke_acc : forall env e p t t',
+    ok_exp env e t ->
+    ok_path env p t t' ->
+    ok_exp env (AccE e p) t'
+  | oke_upd : forall env e1 p e2 t1 t2,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 t2 ->
+    ok_path env p t1 t2 ->
+    ok_exp env (UpdE e1 p e2) t1
+  | oke_ext : forall env e1 p e2 t1 t2,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 (IterT t2 I_STAR) ->
+    ok_path env p t1 (IterT t2 I_STAR) ->
+    ok_exp env (ExtE e1 p e2) t1
+  | oke_call : forall env x ags ps sbst rt clauses,
+    StringMap.find x (DEFS env) = Some (ps, rt, clauses) ->
+    (* TODO - ok_args *)
+    ok_exp env (CallE x ags) (subst_typ sbst rt)
+  (* TODO iterE valid *)
+  | oke_cvt : forall env e nt1 nt2,
+    ok_exp env e (NumT nt1) ->
+    ok_exp env (CvtE e nt1 nt2) (NumT nt2)
+  (* TODO subE valid *)
+  | ok_exp_conv : forall env e t t',
+    ok_exp env e t' ->
+    eq_typ (env_to_store env) t t' ->
+    ok_exp env e t
+with
+
+ok_path : il_env -> il_path -> il_typ -> il_typ -> Prop :=
+  | okp_root : forall env t,
+    ok_typ env t ->
+    ok_path env RootP t t
+  | okp_the : forall env p t t',
+    ok_path env p t (IterT t' I_OPT) ->
+    ok_path env (TheP p) t t'
+  | okp_idx : forall env p e t t',
+    ok_path env p t (IterT t' I_STAR) ->
+    ok_exp env e (NumT NatT) ->
+    ok_path env (IdxP p e) t t'
+  | okp_slice : forall env p e1 e2 t t',
+    ok_path env p t (IterT t' I_STAR) ->
+    ok_exp env e1 (NumT NatT) ->
+    ok_exp env e2 (NumT NatT) ->
+    ok_path env (SliceP p e1 e2) t t'
+  | okp_dot : forall env p a x ags t t' tfs qs prems,
+    ok_path env p t (VarT x ags) -> 
+    expand_typ (env_to_store env) (VarT x ags) (StructT tfs) ->
+    List.In (a, qs, t', prems) tfs ->
+    ok_path env (DotP p a) t t'
+  | okp_uncase : forall env p m t t' x ags qs prems tcs,
+    ok_path env p t (VarT x ags) ->
+    expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
+    List.In (m, qs, t', prems) tcs ->
+    ok_path env (UncaseP p m) t t'
+  | okp_conv : forall env p t t' t'',
+    ok_path env p t'' t' ->
+    eq_typ (env_to_store env) t t'' ->
+    ok_path env p t t'
+
+with
+
+ok_typ : il_env -> il_typ -> Prop :=
+  | okt_bool : forall env, ok_typ env BoolT
+  | okt_num : forall env nt, ok_typ env (NumT nt)
+  | okt_text : forall env, ok_typ env TextT
+  | okt_tupemp : forall env, ok_typ env (TupT [])
+  | okt_tup : forall env x1 t1 tups,
+    let env' := single_var x1 t1 in
+    ok_typ env t1 ->
+    ok_typ (append_env env env') (TupT tups) ->
+    ok_typ env (TupT ((x1, t1) :: tups))
+  | okt_iter : forall env t it,
+    ok_typ env t ->
+    (it = I_STAR) \/ (it = I_OPT) ->
+    ok_typ env (IterT t it)
+  | okt_var : forall env x ags ps insts,
+    (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
+    ok_typ env (VarT x ags)
 .
\ No newline at end of file

From dbb0123304d547195c123d242254abd59eb29944 Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Wed, 25 Feb 2026 10:12:17 +0000
Subject: [PATCH 07/11] Ported almost all of the typing rules.

---
 spectec/metatheory/theories/env.v       |  46 ++++-
 spectec/metatheory/theories/reduction.v |  32 +---
 spectec/metatheory/theories/subst.v     |  14 ++
 spectec/metatheory/theories/syntax.v    |   6 +-
 spectec/metatheory/theories/typing.v    | 242 +++++++++++++++++++++++-
 spectec/metatheory/theories/utils.v     |  66 +++++++
 6 files changed, 359 insertions(+), 47 deletions(-)
 create mode 100644 spectec/metatheory/theories/utils.v

diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
index 79be6ce5e6..39514ba493 100644
--- a/spectec/metatheory/theories/env.v
+++ b/spectec/metatheory/theories/env.v
@@ -3,7 +3,9 @@ From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssri
 Require Import Stdlib.FSets.FMapAVL.
 Require Import Stdlib.Structures.OrderedTypeEx.
 From MetaSpectec Require Import syntax.
+Import ListNotations.
 
+Declare Scope env_scope.
 Module StringMap := FMapAVL.Make(String_as_OT).
 
 Definition union {A}
@@ -17,7 +19,7 @@ Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
 
 Definition var_def : Type := il_typ.
 Definition typ_def : Type := list il_param * list il_inst.
-Definition rel_def : Type := mixop * il_typ * list il_rule.
+Definition rel_def : Type := list il_param * il_typ * list il_rule.
 Definition definition_def : Type := list il_param * il_typ * list il_clause.
 
 (* Typing context *)
@@ -47,10 +49,19 @@ Definition append_env (e1 e2 : il_env) : il_env :=
 Definition single_var (x : il_id) (t : il_typ) : il_env :=
   {| VARS := singleton x t; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
 
-Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20).
-Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20).
-Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20).
-Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20).
+Definition single_envtyp (x : il_id) (ps : list il_param) (insts : list il_inst) : il_env :=
+  {| VARS := empty_vars; TYPS := singleton x (ps, insts); DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition single_def (x : il_id) (ps : list il_param) (rt : il_typ) (clauses : list il_clause) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := singleton x (ps, rt, clauses); RELS := empty_rels |}.
+
+Definition single_rel (x : il_id) (ps : list il_param) (t : il_typ) (rules : list il_rule) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := singleton x (ps, t, rules) |}.
+
+Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20) : env_scope.
 
 Record store := {
   S_TYPS : StringMap.t typ_def;
@@ -62,4 +73,27 @@ Definition store_to_env (s : store) : il_env :=
   {| VARS := empty_vars; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
 
 Definition env_to_store (e : il_env) : store :=
-  {| S_TYPS := e.(TYPS); S_DEFS := e.(DEFS); S_RELS := e.(RELS) |}.
\ No newline at end of file
+  {| S_TYPS := e.(TYPS); S_DEFS := e.(DEFS); S_RELS := e.(RELS) |}.
+
+Fixpoint composeenvs (envs : list il_env) : il_env :=
+  match envs with
+  | [] => env_empty
+  | e1 :: es => append_env e1 (composeenvs es)
+  end
+.
+
+Definition tupenv (t : il_typ) : il_env :=
+  match t with
+  | TupT tups => composeenvs (List.map (fun '(x, t) => single_var x t) tups)
+  | _ => env_empty
+  end
+.
+
+Fixpoint paramenv (ps : list il_param) : il_env :=
+  match ps with
+  | [] => env_empty
+  | ExpP x t :: ps' => append_env (single_var x t) (paramenv ps')
+  | TypP x :: ps' => append_env (single_envtyp x [] []) (paramenv ps')
+  | DefP x ps' rt :: ps'' => append_env (single_def x ps' rt []) (paramenv ps'')
+  end
+. 
\ No newline at end of file
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index ed1855526c..79c011ee81 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -1,40 +1,10 @@
 From Stdlib Require Import List String Reals.
 From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
-From MetaSpectec Require Import syntax subst env numerics.
+From MetaSpectec Require Import syntax subst env numerics utils.
 Import ListNotations.
 
-Inductive option_forall {T : Type} (P : (T -> Prop)) : option T -> Prop :=
-	| opt_none : option_forall P None
-  | opt_some : forall x,
-    P x ->
-    option_forall P (Some x)
-.
-
-Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
-	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
-
-Definition slice {A : Type} (i j : nat) (l : list A) : list A :=
-  firstn (j - i) (skipn i l).
-
-(* PRE: i < size l *)
-Definition update {A : Type} (l : list A) (i : nat) (x : A) : list A :=
-  set_nth x l i x.
-
-Definition update_slice {A : Type} (l : list A) (i : nat) (j : nat) (xs : list A) : list A :=
-  let idx_lst := iota i (j - i) in
-  foldl (fun acc '(idx, x) => update acc idx x) l (zip idx_lst xs)
-.
-
-Definition is_plaintyp (t : il_typ) : bool :=
-  match t with
-  | VarT _ _ => false
-  | _ => true
-  end
-.
-
 Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> il_subst -> Prop :=
   | ma_rule : forall s ags qs ags' sbst,
-    ok_subst (store_to_env s) (sbst) qs ->
     ags = List.map (subst_arg sbst) ags' ->
     match_args s ags qs ags' sbst
 .
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index 974084bf2a..e6b03e8d9f 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -32,6 +32,20 @@ Definition subst_svar (x : il_id) (e : il_exp) : il_subst :=
   S_FUN := empty_id
   |}.
 
+Definition subst_styp (x : il_id) (t : il_typ) : il_subst :=
+  {|
+  S_EXP := empty_exp;
+  S_TYP := singleton x t;
+  S_FUN := empty_id
+  |}.
+
+Definition subst_sfun (x : il_id) (y : il_id) : il_subst :=
+  {|
+  S_EXP := empty_exp;
+  S_TYP := empty_typ;
+  S_FUN := singleton x y
+  |}.
+
 Record dom : Type :=
   {
   D_EXP : list il_id;
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 60fa7ace69..913fbcc7c6 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -1,5 +1,5 @@
 From Stdlib Require Import List String.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect all_algebra. 
 Import GRing.Theory.
 
 Parameter R : archiNumDomainType.
@@ -179,13 +179,13 @@ Inductive il_deftyp : Type :=
 
 Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
 
-Definition il_rule : Type := il_id * list il_quant * mixop * il_exp * list il_prem.
+Definition il_rule : Type := list il_quant * il_exp * list il_prem.
 
 Definition il_clause : Type := list il_quant * list il_arg * il_exp * list il_prem.
 
 Inductive il_def : Type :=
   | TypD : il_id -> list il_param -> list il_inst -> il_def
-  | RelD : il_id -> mixop -> il_typ -> list il_rule -> il_def
+  | RelD : il_id -> list il_param -> il_typ -> list il_rule -> il_def
   | DecD : il_id -> list il_param -> il_typ -> list il_clause -> il_def
   | RecD : list il_def -> il_def
 .
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index b3647864a5..dcf136fe56 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -1,7 +1,15 @@
 From Stdlib Require Import List String Reals.
-From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
-From MetaSpectec Require Import syntax env reduction subst.
+From mathcomp Require Import all_ssreflect all_algebra.
+From MetaSpectec Require Import syntax env reduction subst utils.
 Import ListNotations.
+Open Scope env_scope.
+
+Fixpoint disjoint {X : eqType} (xs : list X) : bool :=
+  match xs with
+  | [] => true
+  | x :: xs => negb (x \in xs) && disjoint xs
+  end
+.
 
 Inductive composable_typ : il_env -> il_typ -> Prop :=
   | ct_iter : forall env t t' it,
@@ -35,6 +43,36 @@ Inductive sub_typ : il_env -> il_typ -> il_typ -> Prop :=
     expand_typ (env_to_store env) t1 (StructT tfs1) ->
     expand_typ (env_to_store env) t2 (StructT tfs2) -> 
     sub_typ env t1 t2
+  | st_iter : forall env t1 t2 it,
+    sub_typ env t1 t2 ->
+    sub_typ env (IterT t1 it) (IterT t2 it) 
+  | st_refl : forall env t, sub_typ env t t
+  | st_trans : forall env t1 t2 t',
+    sub_typ env t1 t' ->
+    sub_typ env t' t2 ->
+    sub_typ env t1 t2
+.
+
+Inductive sub_param : il_env -> il_param -> il_param -> il_subst -> Prop :=
+  | sp_exp : forall env x1 t1 x2 t2,
+    sub_typ env t1 t2 ->
+    sub_param env (ExpP x1 t1) (ExpP x2 t2) (subst_svar x2 (VarE x1))
+  | sp_typ : forall env x1 x2,
+    sub_param env (TypP x1) (TypP x2) (subst_styp x2 (VarT x1 []))
+  | sp_fun : forall env x1 ps1 t1 x2 ps2 t2 sbst,
+    let penv2 := paramenv ps2 in
+    sub_params env ps2 ps1 sbst ->
+    sub_typ (append_env env penv2) (subst_typ sbst t1) t2 ->
+    sub_param env (DefP x1 ps1 t1) (DefP x2 ps2 t2) (subst_sfun x2 x1)
+
+with
+
+sub_params : il_env -> list il_param -> list il_param -> il_subst -> Prop :=
+  | sps_emp : forall env, sub_params env [] [] subst_empty
+  | sps_cons : forall env p1 p1s p2 p2s sbst sbst',
+    sub_param env p1 p2 sbst ->
+    sub_params env p1s (List.map (subst_param sbst) p2s) sbst' ->
+    sub_params env (p1 :: p1s) (p2 :: p2s) (append_subst sbst sbst')
 .
 
 Inductive ok_numunop : numunop -> numtyp -> numtyp -> Prop :=
@@ -106,7 +144,7 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
     ok_exp env (ListE es) (IterT t I_STAR)
   | oke_lift : forall env e t,
     ok_exp env e (IterT t I_OPT) ->
-    ok_exp env e (IterT t I_STAR)
+    ok_exp env (LiftE e) (IterT t I_STAR)
   | oke_case : forall env m e x ags tcs t qs ps,
     expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
     List.In (m, qs, t, ps) tcs ->
@@ -152,17 +190,21 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
     ok_exp env (ExtE e1 p e2) t1
   | oke_call : forall env x ags ps sbst rt clauses,
     StringMap.find x (DEFS env) = Some (ps, rt, clauses) ->
-    (* TODO - ok_args *)
+    ok_args env ags ps sbst ->
     ok_exp env (CallE x ags) (subst_typ sbst rt)
   (* TODO iterE valid *)
   | oke_cvt : forall env e nt1 nt2,
     ok_exp env e (NumT nt1) ->
     ok_exp env (CvtE e nt1 nt2) (NumT nt2)
-  (* TODO subE valid *)
+  | oke_sub : forall env e t1 t2, 
+    ok_exp env e t1 ->
+    sub_typ env t1 t2 ->
+    ok_exp env (SubE e t1 t2) t2
   | ok_exp_conv : forall env e t t',
     ok_exp env e t' ->
     eq_typ (env_to_store env) t t' ->
     ok_exp env e t
+
 with
 
 ok_path : il_env -> il_path -> il_typ -> il_typ -> Prop :=
@@ -212,7 +254,193 @@ ok_typ : il_env -> il_typ -> Prop :=
     ok_typ env t ->
     (it = I_STAR) \/ (it = I_OPT) ->
     ok_typ env (IterT t it)
-  | okt_var : forall env x ags ps insts,
+  | okt_var : forall env x ags ps insts sbst,
     (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
+    ok_args env ags ps sbst ->
     ok_typ env (VarT x ags)
-.
\ No newline at end of file
+
+with
+
+ok_iter : il_env -> iter -> iter -> il_env -> Prop :=
+  | oki_quest : forall env, ok_iter env I_OPT I_OPT env_empty 
+  | oki_star : forall env, ok_iter env I_STAR I_STAR env_empty
+  | oki_plus : forall env, ok_iter env I_PLUS I_STAR env_empty
+  | oki_sup_none : forall env e,
+    ok_exp env e (NumT NatT) ->
+    ok_iter env (I_SUP None e) I_STAR env_empty
+  | oki_sup_some : forall env e x,
+    ok_exp env e (NumT NatT) ->
+    ok_iter env (I_SUP (Some x) e) I_STAR (single_var x (NumT NatT))
+
+with
+
+ok_prem : il_env -> il_prem -> Prop :=
+  | okp_rule : forall env x ags sbst e ps t rules,
+    StringMap.find x (RELS env) = Some (ps, t, rules) ->
+    ok_args env ags ps sbst ->
+    ok_exp env e (subst_typ sbst t) ->
+    ok_prem env (RulePr x ags e)
+  | okp_if : forall env e,
+    ok_exp env e BoolT ->
+    ok_prem env (IfPr e)
+  | okp_else : forall env, ok_prem env ElsePr
+  (* TODO think about let semantics *)
+  | okp_let : forall env e1 e2 t,
+    ok_exp env e1 t ->
+    ok_exp env e2 t ->
+    ok_prem env (LetPr e1 e2)
+  (* | okp_iter : forall env pr it it' env'' expps,
+    let env' := single_var x  
+    ok_iter env it it' env' -> *)
+  | okp_neg : forall env p,
+    ok_prem env p ->
+    ok_prem env (NegPr p)
+
+with
+
+ok_arg : il_env -> il_arg -> il_param -> il_subst -> Prop :=
+  | oka_exp : forall env e x t,
+    ok_exp env e t ->
+    ok_arg env (ExpA e) (ExpP x t) (subst_svar x e)
+  | oka_typ : forall env t x,
+    ok_typ env t ->
+    ok_arg env (TypA t) (TypP x) (subst_styp x t)
+  (* TODO fun arg *)
+  | oka_fun : forall env y x ps rt ps' rt' clauses sbst,
+    StringMap.find y (DEFS env) = Some (ps', rt', clauses) ->
+    sub_params env ps ps' sbst ->
+    sub_typ env (subst_typ sbst rt') rt ->
+    ok_arg env (DefA y) (DefP x ps rt) (subst_sfun x y)
+
+with
+
+ok_args : il_env -> list il_arg -> list il_param -> il_subst -> Prop :=
+  | okas_emp : forall env, ok_args env [] [] subst_empty
+  | okas_cons : forall env a1 p1 sbst sbst1 ags ps,
+    ok_arg env a1 p1 sbst1 ->
+    ok_args env ags (List.map (subst_param sbst) ps) sbst ->
+    ok_args env (a1 :: ags) (p1 :: ps) (append_subst sbst1 sbst)
+
+with
+
+ok_param : il_env -> il_param -> Prop :=
+  | okpa_exp : forall env x t,
+    ok_typ env t ->
+    ok_param env (ExpP x t) 
+  | okpa_typ : forall env x, ok_param env (TypP x)
+  | okpa_fun : forall env x ps t, 
+    let penv := paramenv ps in
+    ok_params env ps ->
+    ok_typ (append_env env penv) t ->
+    ok_param env (DefP x ps t)
+
+with
+
+ok_params : il_env -> list il_param -> Prop :=
+  | okpas_emp : forall env, ok_params env []
+  | okpas_cons : forall env p1 ps,
+    ok_param env p1 ->
+    ok_params (append_env env (paramenv [p1])) ps
+.
+
+Inductive ok_typfield : il_env -> typfield -> Prop :=
+  | oktypfield : forall env a t qs prems,
+    let tenv := tupenv t in
+    let qsenv := paramenv qs in
+    ok_typ env t ->
+    ok_params (append_env env tenv) qs ->
+    List.Forall (fun p => ok_prem (append_env env (append_env tenv qsenv)) p) prems ->
+    ok_typfield env (a, qs, t, prems)
+.
+
+Inductive ok_typcase : il_env -> typcase -> Prop :=
+  | oktypcase : forall env m t qs prems,
+    let tenv := tupenv t in
+    let qsenv := paramenv qs in
+    ok_typ env t ->
+    ok_params (append_env env tenv) qs ->
+    List.Forall (fun p => ok_prem (append_env env (append_env tenv qsenv)) p) prems ->
+    ok_typcase env (m, qs, t, prems)
+.
+
+Inductive ok_deftyp : il_env -> il_deftyp -> Prop :=
+  | okd_alias : forall env t,
+    ok_typ env t ->
+    ok_deftyp env (AliasT t)
+  | okd_struct : forall env tfs,
+    let atoms := List.map (fun '(a, qs, t, prems) => a) tfs in
+    List.Forall (fun tf => ok_typfield env tf) tfs ->
+    disjoint atoms ->
+    ok_deftyp env (StructT tfs)
+  | okd_variant : forall env tcs,
+    let mixops := List.map (fun '(m, qs, t, prems) => m) tcs in
+    List.Forall (fun tc => ok_typcase env tc) tcs ->
+    disjoint mixops ->
+    ok_deftyp env (VariantT tcs)
+.
+ 
+
+Inductive ok_inst : il_env -> il_inst -> list il_param -> Prop :=
+  | oki_inst : forall env qs ags dt ps sbst,
+    ok_params env qs ->
+    ok_args (append_env env (paramenv qs)) ags ps sbst ->
+    ok_deftyp (append_env env (paramenv qs)) dt ->
+    ok_inst env (qs, ags, dt) ps
+.
+
+Inductive ok_rule : il_env -> il_rule -> il_typ -> Prop :=
+  | okr_rule : forall env qs e prems t,
+    ok_params env qs ->
+    ok_exp (append_env env (paramenv qs)) e t ->
+    List.Forall (fun p => ok_prem (append_env env (paramenv qs)) p) prems ->
+    ok_rule env (qs, e, prems) t
+.
+
+Inductive ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
+  | okc_clause : forall env qs ags e prems ps t sbst,
+    let qsenv := paramenv qs in
+    ok_params env qs ->
+    ok_args (append_env env qsenv) ags ps sbst ->
+    ok_exp (append_env env qsenv) e t ->
+    List.Forall (fun p => ok_prem (append_env env qsenv) p) prems ->
+    ok_clause env (qs, ags, e, prems) ps t
+.
+
+Inductive ok_def : il_env -> il_def -> il_env -> Prop :=
+  | okd_typ : forall env x ps insts,
+    let env' := single_envtyp x ps insts in
+    ok_params env ps ->
+    List.Forall (fun inst => ok_inst env inst ps) insts ->
+    ok_def env (TypD x ps insts) (append_env env env')
+  | okd_rel : forall env x ps t rules,
+    let env' := single_rel x ps t rules in
+    let penv := paramenv ps in
+    ok_params env ps ->
+    List.Forall (fun rule => ok_rule (append_env env penv) rule t) rules ->
+    ok_def env (RelD x ps t rules) (append_env env env')
+  | okd_fun : forall env x ps t clauses,
+    let env' := single_def x ps t clauses in
+    let penv := paramenv ps in
+    ok_params env ps ->
+    List.Forall (fun clause => ok_clause (append_env env penv) clause ps t) clauses ->
+    ok_def env (DecD x ps t clauses) (append_env env env')
+  (* TODO recs doesn't make much sense *)
+  | okd_rec : forall env env' defs,
+    ok_defs (append_env env env') defs env' ->
+    ok_def env (RecD defs) env'
+  
+with
+
+ok_defs : il_env -> list il_def -> il_env -> Prop :=
+  | okdefs_emp : forall env, ok_defs env [] env_empty
+  | okdefs_cons : forall env d1 defs env' env'', 
+    ok_def env d1 env' ->
+    ok_defs env' defs env'' ->
+    ok_defs env (d1 :: defs) env''
+.
+
+Inductive ok_script : script -> Prop :=
+  | okscript : forall defs env,
+    ok_defs env_empty defs env ->
+    ok_script defs
+.
diff --git a/spectec/metatheory/theories/utils.v b/spectec/metatheory/theories/utils.v
new file mode 100644
index 0000000000..c41c31dd62
--- /dev/null
+++ b/spectec/metatheory/theories/utils.v
@@ -0,0 +1,66 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+Import ListNotations.
+From MetaSpectec Require Import syntax.
+From HB Require Import structures.
+
+Inductive option_forall {T : Type} (P : (T -> Prop)) : option T -> Prop :=
+	| opt_none : option_forall P None
+  | opt_some : forall x,
+    P x ->
+    option_forall P (Some x)
+.
+
+Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
+	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
+
+Definition slice {A : Type} (i j : nat) (l : list A) : list A :=
+  firstn (j - i) (skipn i l).
+
+(* PRE: i < size l *)
+Definition update {A : Type} (l : list A) (i : nat) (x : A) : list A :=
+  set_nth x l i x.
+
+Definition update_slice {A : Type} (l : list A) (i : nat) (j : nat) (xs : list A) : list A :=
+  let idx_lst := iota i (j - i) in
+  foldl (fun acc '(idx, x) => update acc idx x) l (zip idx_lst xs)
+.
+
+Definition is_plaintyp (t : il_typ) : bool :=
+  match t with
+  | VarT _ _ => false
+  | _ => true
+  end
+.
+
+Lemma eq_dec_Equality_axiom :
+  forall (T : Type) (eq_dec : forall (x y : T), decidable (x = y)),
+  let eqb v1 v2 := is_left (eq_dec v1 v2) in Equality.axiom eqb.
+Proof.
+  move=> T eq_dec eqb x y. rewrite /eqb.
+  case: (eq_dec x y); by [apply: ReflectT | apply: ReflectF].
+Qed.
+
+Definition atom_eq_dec : forall (v1 v2 : atom),
+  {v1 = v2} + {v1 <> v2}.
+Proof. do ? decide equality. Defined.
+
+Definition atom_eqb (v1 v2 : atom) : bool :=
+	is_left(atom_eq_dec v1 v2).
+Definition eqatomP : Equality.axiom (atom_eqb) :=
+	eq_dec_Equality_axiom (atom) (atom_eq_dec).
+
+HB.instance Definition _ := hasDecEq.Build (atom) (eqatomP).
+
+Definition mixop_eq_dec : forall (v1 v2 : mixop),
+  {v1 = v2} + {v1 <> v2}.
+Proof. do ? decide equality. Defined.
+
+Definition mixop_eqb (v1 v2 : mixop) : bool :=
+	is_left(mixop_eq_dec v1 v2).
+Definition eqmixopP : Equality.axiom (mixop_eqb) :=
+	eq_dec_Equality_axiom (mixop) (mixop_eq_dec).
+
+HB.instance Definition _ := hasDecEq.Build (mixop) (eqmixopP).
+
+

From e47fd2f740857074a10982956ba890fccb4b5cda Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Wed, 25 Feb 2026 17:10:04 +0000
Subject: [PATCH 08/11] Added Iter and Sub reduction rules.

---
 spectec/metatheory/theories/env.v       |   1 +
 spectec/metatheory/theories/reduction.v | 153 ++++++++++++++++++++----
 spectec/metatheory/theories/subst.v     |   7 ++
 spectec/metatheory/theories/syntax.v    |   2 +-
 spectec/metatheory/theories/typing.v    |  51 ++++----
 spectec/metatheory/theories/utils.v     |  89 ++++++++++++++
 6 files changed, 252 insertions(+), 51 deletions(-)

diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
index 39514ba493..30c31e646d 100644
--- a/spectec/metatheory/theories/env.v
+++ b/spectec/metatheory/theories/env.v
@@ -62,6 +62,7 @@ Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20) :
 Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20) : env_scope.
 Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20) : env_scope.
 Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20) : env_scope.
+Notation "x @@ y" := (append_env x y) (at level 20) : env_scope.
 
 Record store := {
   S_TYPS : StringMap.t typ_def;
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 79c011ee81..0595db29d5 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -35,6 +35,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_unop_num : forall s numop n n',
     (numun numop n) = Some n' ->
     step_exp s (UnE (NumUnop numop) (NumE n)) (NumE n')
+
   (* BinE Rules *)
   | se_bin_ctxl : forall s op e1 e1' e2,
     step_exp s e1 e1' ->
@@ -47,6 +48,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_bin_num : forall s numop n1 n2 n3,
     (numbin numop n1 n2) = Some n3 ->
     step_exp s (BinE (NumBinop numop) (NumE n1) (NumE n2)) (NumE n3)
+
   (* CmpE Rules *)
   | se_cmp_ctxl : forall s op e1 e1' e2,
     step_exp s e1 e1' ->
@@ -67,28 +69,34 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     opt_e = Some e ->
     step_exp s e e' ->
     step_exp s (OptE opt_e) (OptE (Some e'))
+
   (* ListE rules *)
   | se_list_ctx : forall s es es',
     List.Forall2 (fun e e' => step_exp s e e') es es' ->
     step_exp s (ListE es) (ListE es')
+
   (* TupE rules *)
   | se_tup_ctx : forall s es es',
     List.Forall2 (fun e e' => step_exp s e e') es es' ->
     step_exp s (TupE es) (TupE es')
+
   (* StrE rules *)
   | se_str_ctx : forall s fields fields',
     List.Forall2 (fun f f' => step_exp s (snd f) (snd f')) fields fields' ->
     step_exp s (StrE fields) (StrE fields')
+
   (* CaseE rules *)
   | se_case_ctx : forall s m e e',
     step_exp s e e' ->
     step_exp s (CaseE m e) (CaseE m e')
+
   (* LiftE rules *)
   | se_lift_ctx : forall s e e',
     step_exp s e e' ->
     step_exp s (LiftE e) (LiftE e')
   | se_lift_none : forall s, step_exp s (LiftE (OptE None)) (ListE [])
-  | se_list_some : forall s e , step_exp s (LiftE (OptE (Some e))) (ListE [e])
+  | se_lift_some : forall s e , step_exp s (LiftE (OptE (Some e))) (ListE [e])
+
   (* ProjE rules *)
   | se_proj_ctx : forall s e e' n,
     step_exp s e e' ->
@@ -96,12 +104,14 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_proj_tup : forall s es e_n n,
     List.nth_error es n = Some e_n ->
     step_exp s (ProjE (TupE es) n) e_n 
+
   (* LenE rules *)
   | se_len_ctx : forall s e e',
     step_exp s e e' ->
     step_exp s (LenE e) (LenE e')
   | se_len_list : forall s es,
     step_exp s (LenE (ListE es)) (NumE (NatE (List.length es)))
+
   (* MemE rules *)
   | se_mem_ctxl : forall s e1 e2 e1',
     step_exp s e1 e1' ->
@@ -121,6 +131,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_mem_list_false : forall s e1 e2s,
     List.Forall (fun e2 => e1 <> e2) e2s ->
     step_exp s (MemE e1 (ListE e2s)) (BoolE false)
+
   (* CatE rules *)
   | se_cat_ctxl : forall s e1 e1' e2,
     step_exp s e1 e1' ->
@@ -137,6 +148,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_cat_str : forall s fields1 fields2,
     List.Forall2 (fun '(a, _) '(a', _) => a = a') fields1 fields2 ->
     step_exp s (CatE (StrE fields1) (StrE fields2)) (StrE (list_zipWith (fun x y => (fst x, CatE (snd x) (snd y))) fields1 fields2))
+  
   (* AccE rules *)
   | se_acc_ctxexp : forall s e e' p,
     step_exp s e e' ->
@@ -144,7 +156,6 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_acc_ctxpath : forall s e p p',
     step_path s p p' ->
     step_exp s (AccE e p) (AccE e p')
-  (* TODO: what does step path mean? *)
   | se_acc_root : forall s e,
     step_exp s (AccE e RootP) e
   | se_acc_the : forall s e e' p,
@@ -168,6 +179,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_acc_uncase : forall s e p m e',
     step_exp s (AccE e p) (CaseE m e') ->
     step_exp s (AccE e (UncaseP p m)) e'
+
   (* UpdE rules *)
   | se_upd_ctxl : forall s e1 e1' p e2,
     step_exp s e1 e1' ->
@@ -200,19 +212,54 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_upd_uncase : forall s e1 p m e2 e', 
     step_exp s (AccE e1 p) (CaseE m e') ->
     step_exp s (UpdE e1 (UncaseP p m) e2) (UpdE e1 p (CaseE m e2))
+
   (* ExtE rule *)
   | se_ext : forall s e1 p e2,
     step_exp s (ExtE e1 p e2) (UpdE e1 p (CatE (AccE e1 p) e2))
+
   (* IterE rules *)
-  | se_iter_ctx1 : forall s e it ep_lst e',
+  | se_iter_ctx1 : forall s e it eps e',
     step_exp s e e' ->
-    step_exp s (IterE e it ep_lst) (IterE e' it ep_lst)
-  | se_iter_ctx2 : forall s e it it' ep_lst,
+    step_exp s (IterE e it eps) (IterE e' it eps)
+  | se_iter_ctx2 : forall s e it it' eps,
     step_iter s it it' ->
-    step_exp s (IterE e it ep_lst) (IterE e it' ep_lst)
-  (* TODO ctx on exppull? *)
-  (* | se_iter_quest : forall s e ep_lst, *)
-  (* TODO other iter rules *)
+    step_exp s (IterE e it eps) (IterE e it' eps)
+  | se_iter_ctx3 : forall s e it eps n ep ep',
+    List.nth_error eps n = Some ep ->
+    step_exppull s ep ep' ->
+    step_exp s (IterE e it eps) (IterE e it (update eps n ep'))
+  | se_iter_quest : forall s e xs es,
+    let es' := List.map opt_to_lst es in
+    let es'' := transpose es' in
+    let es''' := lst_to_opt es'' in
+    same_size es' ->
+    size xs = size es ->
+    size es'' <= 1 ->
+    step_exp s (IterE e I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es))
+    (OptE (option_map (fun ess => subst_exp (many_svars (zip xs ess)) e) es'''))
+  | se_iter_plus : forall s e xs ess,
+    same_size ess ->
+    seq.all (fun es => size es >= 1) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_exp s (IterE e I_PLUS res_ess) (IterE e I_STAR res_ess)
+  | se_iter_star : forall s e xs ess n,
+    seq.all (fun es => size es == n) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_exp s (IterE e I_STAR res_ess) (IterE e (I_SUP None (NumE (NatE n))) res_ess)
+  | se_iter_sup_eps : forall s e eps e_n y,
+    (* TODO y needs to not clash with any other variable *)
+    step_exp s (IterE e (I_SUP None e_n) eps) (IterE e (I_SUP y e_n) eps)
+  | se_iter_sup : forall s e x_i n xs ess,
+    seq.all (fun es => size es == n) ess ->
+    size xs = size ess -> 
+    let ess' := transpose ess in
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    let res_ess' := (list_mapi (fun i es => 
+      let sbst := subst_svar x_i (NumE (NatE i)) in
+      let sbst' := many_svars (zip xs es) in
+      subst_exp (append_subst sbst sbst') e 
+    ) ess') in
+    step_exp s (IterE e (I_SUP (Some x_i) (NumE (NatE n))) res_ess) (ListE res_ess')
 
   (* CallE rules *)
   | se_call_ctx : forall s x ags n a a',
@@ -225,6 +272,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     match_args s ags qs ags' sbst ->
     reduce_prems s (List.map (subst_prem sbst) prems) [] ->
     step_exp s (CallE x ags) (subst_exp sbst e)
+
   (* CvtE rules *)
   | se_cvt_ctx : forall s e nt1 nt2 e',
     step_exp s e e' ->
@@ -232,6 +280,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_cvt_num : forall s num nt1 nt2 e,
     numcvt nt2 num = Some e ->
     step_exp s (CvtE (NumE num) nt1 nt2) (NumE e)
+
   (* SubE rules *)
   | se_sub_ctx1 : forall s e t1 t2 e',
     step_exp s e e' ->
@@ -247,24 +296,39 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_sub_tup : forall s es tups tups',
     size es = size tups ->
     size tups = size tups' ->
+    let sbst1 := many_svars (list_zipWith (fun e '(x1, _) => (x1, e)) es tups) in
+    let sbst2 := many_svars (list_zipWith (fun e '(x2, _) => (x2, e)) es tups') in
     step_exp s (SubE (TupE es) (TupT tups) (TupT tups')) 
-    (TupE (List.map (fun '(e, ((_, t1), (_, t2))) => SubE e t1 t2) (zip es (zip tups tups'))))
-  (* TODO sub x's *)
-  
+    (TupE (List.map (fun '(e, ((_, t1), (_, t2))) => SubE e (subst_typ sbst1 t1) (subst_typ sbst2 t2)) (zip es (zip tups tups'))))
+  | se_sub_opt : forall s e_opt t1 t2,
+    step_exp s (SubE (OptE e_opt) (IterT t1 I_OPT) (IterT t2 I_OPT)) (OptE (option_map (fun e => SubE e t1 t2) e_opt))
+  | se_sub_list : forall s es t1 t2,
+    step_exp s (SubE (ListE es) (IterT t1 I_STAR) (IterT t2 I_STAR)) (ListE (List.map (fun e => SubE e t1 t2) es))
+  | se_sub_case : forall s (e : il_exp) op e x1 ags1 x2 ags2 t1 t2 tcs1 tcs2 qs1 qs2 prs1 prs2,
+    expand_typ s (VarT x1 ags1) (VariantT tcs1) ->
+    expand_typ s (VarT x2 ags2) (VariantT tcs2) ->
+    List.In (op, qs1, t1, prs1) tcs1 ->
+    List.In (op, qs2, t2, prs2) tcs2 ->
+    step_exp s (SubE (CaseE op e) (VarT x1 ags1) (VarT x2 ags2)) (CaseE op (SubE e t1 t2))
+  | se_sub_str : forall s efs x1 ags1 x2 ags2 t1s t2s tfs1 tfs2 ats es,
+    expand_typ s (VarT x1 ags1) (StructT tfs1) ->
+    expand_typ s (VarT x2 ags2) (StructT tfs2) ->
+    size efs = size tfs1 ->
+    size efs = size tfs2 ->
+    List_Forall3 (fun '(a, t) a' t' => a = a' /\ t = t') (atomtyps tfs2) ats t2s ->
+    List.Forall2 (fun a t => List.In (a, t) (atomtyps tfs1)) ats t1s ->
+    List.Forall2 (fun a e => List.In (a, e) efs) ats es ->
+    step_exp s (SubE (StrE efs) (VarT x1 ags1) (VarT x2 ags2))
+    (StrE (list_map3 (fun '(a, e) t1 t2 => (a, SubE e t1 t2)) (zip ats es) t1s t2s)) 
+
   (* IfE rules *)
   | se_ife_ctx1 : forall s e1 e2 e3 e1',
     step_exp s e1 e1' ->
     step_exp s (IfE e1 e2 e3) (IfE e1' e2 e3)
-  | se_ife_ctx2 : forall s e1 e2 e3 e2',
-    step_exp s e2 e2' ->
-    step_exp s (IfE e1 e2 e3) (IfE e1 e2' e3)
-  | se_ife_ctx3 : forall s e1 e2 e3 e3',
-    step_exp s e3 e3' -> 
-    step_exp s (IfE e1 e2 e3) (IfE e1 e2 e3')
   | se_ife_true : forall s e2 e3,
     step_exp s (IfE (BoolE true) e2 e3) e2
   | se_ife_false : forall s e2 e3,
-    step_exp s (IfE (BoolE false) e2 e3) e3 
+    step_exp s (IfE (BoolE false) e2 e3) e3
 with
 
 step_arg : store -> il_arg -> il_arg -> Prop :=
@@ -274,6 +338,7 @@ step_arg : store -> il_arg -> il_arg -> Prop :=
   | sa_typ : forall s t t',
     step_typ s t t' ->
     step_arg s (TypA t) (TypA t')
+
 with
 
 step_typ : store -> il_typ -> il_typ -> Prop :=
@@ -341,10 +406,49 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     e1' = e2' ->
     step_prems s [LetPr e1 e2] []
   (* IterPr rules *)
-  | sp_iter_ctxl : forall s p it eps p',
+  | sp_iter_ctx1 : forall s p it eps p',
     step_prems s [p] [p'] ->
     step_prems s [IterPr p it eps] [IterPr p' it eps]
-  (* TODO ctx for iter and exppull? *)
+  | sp_iter_ctx2 : forall s p it it' eps p',
+    step_iter s it it' ->
+    step_prems s [IterPr p it eps] [IterPr p' it eps]
+  | sp_iter_ctx3 : forall s pr it eps n ep ep',
+    List.nth_error eps n = Some ep ->
+    step_exppull s ep ep' ->
+    step_prems s [IterPr pr it eps] [IterPr pr it (update eps n ep')]
+  | sp_iter_quest : forall s pr xs es,
+    let es' := List.map opt_to_lst es in
+    let es'' := transpose es' in
+    let es''' := lst_to_opt es'' in
+    same_size es' ->
+    size xs = size es ->
+    size es'' <= 1 ->
+    step_prems s [IterPr pr I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es)]
+    (opt_to_lst (option_map (fun ess => subst_prem (many_svars (zip xs ess)) pr) es'''))
+  | sp_iter_plus : forall s pr xs ess,
+    same_size ess ->
+    seq.all (fun es => size es >= 1) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_prems s [IterPr pr I_PLUS res_ess] [IterPr pr I_STAR res_ess]
+  | sp_iter_star : forall s pr xs ess n,
+    seq.all (fun es => size es == n) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_prems s [IterPr pr I_STAR res_ess] [IterPr pr (I_SUP None (NumE (NatE n))) res_ess]
+  | sp_iter_sup_eps : forall s pr eps e_n y,
+    (* TODO y needs to not clash with any other variable *)
+    step_prems s [IterPr pr (I_SUP None e_n) eps] [IterPr pr (I_SUP y e_n) eps]
+  | sp_iter_sup : forall s pr x_i n xs ess,
+    seq.all (fun es => size es == n) ess ->
+    size xs = size ess -> 
+    let ess' := transpose ess in
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    let res_ess' := (list_mapi (fun i es => 
+      let sbst := subst_svar x_i (NumE (NatE i)) in
+      let sbst' := many_svars (zip xs es) in
+      subst_prem (append_subst sbst sbst') pr 
+    ) ess') in
+    step_prems s [IterPr pr (I_SUP (Some x_i) (NumE (NatE n))) res_ess] res_ess'
+
   (* TODO other iter rules *)
   (* NegPr rules *)
   | sp_neg_ctx : forall s p p',
@@ -360,6 +464,13 @@ step_iter : store -> iter -> iter -> Prop :=
     step_exp s e e' ->
     step_iter s (I_SUP x e) (I_SUP x e')
 
+with
+
+step_exppull : store -> exppull -> exppull -> Prop :=
+  | sep_ctx : forall s x e e',
+    step_exp s e e' ->
+    step_exppull s (x, e) (x, e')
+
 with 
 
 reduce_exp : store -> il_exp -> il_exp -> Prop :=
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index e6b03e8d9f..e4ad644bdc 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -54,6 +54,13 @@ Record dom : Type :=
   }
 .
 
+Fixpoint many_svars (xs : list (il_id * il_exp)) : il_subst :=
+  match xs with
+  | [] => subst_empty 
+  | (x, e) :: xs' => append_subst (subst_svar x e) (many_svars xs')
+  end
+.
+
 Definition append_dom (d1 d2 : dom) : dom :=
   {|
   D_EXP := d1.(D_EXP) ++ d2.(D_EXP);
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 913fbcc7c6..0f11729216 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -164,7 +164,7 @@ Inductive il_prem : Type :=
   | IfPr : il_exp -> il_prem
   | ElsePr
   | LetPr : il_exp -> il_exp -> il_prem
-  | IterPr : il_prem -> iter -> list (il_id * il_exp) -> il_prem
+  | IterPr : il_prem -> iter -> list exppull -> il_prem
   | NegPr : il_prem -> il_prem
 .
 
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index dcf136fe56..fced01312d 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -4,13 +4,6 @@ From MetaSpectec Require Import syntax env reduction subst utils.
 Import ListNotations.
 Open Scope env_scope.
 
-Fixpoint disjoint {X : eqType} (xs : list X) : bool :=
-  match xs with
-  | [] => true
-  | x :: xs => negb (x \in xs) && disjoint xs
-  end
-.
-
 Inductive composable_typ : il_env -> il_typ -> Prop :=
   | ct_iter : forall env t t' it,
     expand_typ (env_to_store env) t (AliasT (IterT t' it)) ->
@@ -37,7 +30,7 @@ Inductive sub_typ : il_env -> il_typ -> il_typ -> Prop :=
     let env' := (single_var x1 t1) in
     let sbst := (subst_svar x2 (VarE x1)) in
     sub_typ env t1 t2 ->
-    sub_typ (append_env env env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
+    sub_typ (env @@ env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
     sub_typ env (TupT ((x1, t1) :: tups)) (TupT ((x2, t2) :: tups'))
   | st_struct : forall env t1 t2 tfs1 tfs2,
     expand_typ (env_to_store env) t1 (StructT tfs1) ->
@@ -62,7 +55,7 @@ Inductive sub_param : il_env -> il_param -> il_param -> il_subst -> Prop :=
   | sp_fun : forall env x1 ps1 t1 x2 ps2 t2 sbst,
     let penv2 := paramenv ps2 in
     sub_params env ps2 ps1 sbst ->
-    sub_typ (append_env env penv2) (subst_typ sbst t1) t2 ->
+    sub_typ (env @@ penv2) (subst_typ sbst t1) t2 ->
     sub_param env (DefP x1 ps1 t1) (DefP x2 ps2 t2) (subst_sfun x2 x1)
 
 with
@@ -248,7 +241,7 @@ ok_typ : il_env -> il_typ -> Prop :=
   | okt_tup : forall env x1 t1 tups,
     let env' := single_var x1 t1 in
     ok_typ env t1 ->
-    ok_typ (append_env env env') (TupT tups) ->
+    ok_typ (env @@ env') (TupT tups) ->
     ok_typ env (TupT ((x1, t1) :: tups))
   | okt_iter : forall env t it,
     ok_typ env t ->
@@ -331,7 +324,7 @@ ok_param : il_env -> il_param -> Prop :=
   | okpa_fun : forall env x ps t, 
     let penv := paramenv ps in
     ok_params env ps ->
-    ok_typ (append_env env penv) t ->
+    ok_typ (env @@ penv) t ->
     ok_param env (DefP x ps t)
 
 with
@@ -340,7 +333,7 @@ ok_params : il_env -> list il_param -> Prop :=
   | okpas_emp : forall env, ok_params env []
   | okpas_cons : forall env p1 ps,
     ok_param env p1 ->
-    ok_params (append_env env (paramenv [p1])) ps
+    ok_params (env @@ (paramenv [p1])) ps
 .
 
 Inductive ok_typfield : il_env -> typfield -> Prop :=
@@ -348,8 +341,8 @@ Inductive ok_typfield : il_env -> typfield -> Prop :=
     let tenv := tupenv t in
     let qsenv := paramenv qs in
     ok_typ env t ->
-    ok_params (append_env env tenv) qs ->
-    List.Forall (fun p => ok_prem (append_env env (append_env tenv qsenv)) p) prems ->
+    ok_params (env @@ tenv) qs ->
+    List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
     ok_typfield env (a, qs, t, prems)
 .
 
@@ -358,8 +351,8 @@ Inductive ok_typcase : il_env -> typcase -> Prop :=
     let tenv := tupenv t in
     let qsenv := paramenv qs in
     ok_typ env t ->
-    ok_params (append_env env tenv) qs ->
-    List.Forall (fun p => ok_prem (append_env env (append_env tenv qsenv)) p) prems ->
+    ok_params (env @@ tenv) qs ->
+    List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
     ok_typcase env (m, qs, t, prems)
 .
 
@@ -383,16 +376,16 @@ Inductive ok_deftyp : il_env -> il_deftyp -> Prop :=
 Inductive ok_inst : il_env -> il_inst -> list il_param -> Prop :=
   | oki_inst : forall env qs ags dt ps sbst,
     ok_params env qs ->
-    ok_args (append_env env (paramenv qs)) ags ps sbst ->
-    ok_deftyp (append_env env (paramenv qs)) dt ->
+    ok_args (env @@ (paramenv qs)) ags ps sbst ->
+    ok_deftyp (env @@ (paramenv qs)) dt ->
     ok_inst env (qs, ags, dt) ps
 .
 
 Inductive ok_rule : il_env -> il_rule -> il_typ -> Prop :=
   | okr_rule : forall env qs e prems t,
     ok_params env qs ->
-    ok_exp (append_env env (paramenv qs)) e t ->
-    List.Forall (fun p => ok_prem (append_env env (paramenv qs)) p) prems ->
+    ok_exp (env @@ (paramenv qs)) e t ->
+    List.Forall (fun p => ok_prem (env @@ (paramenv qs)) p) prems ->
     ok_rule env (qs, e, prems) t
 .
 
@@ -400,9 +393,9 @@ Inductive ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
   | okc_clause : forall env qs ags e prems ps t sbst,
     let qsenv := paramenv qs in
     ok_params env qs ->
-    ok_args (append_env env qsenv) ags ps sbst ->
-    ok_exp (append_env env qsenv) e t ->
-    List.Forall (fun p => ok_prem (append_env env qsenv) p) prems ->
+    ok_args (env @@ qsenv) ags ps sbst ->
+    ok_exp (env @@ qsenv) e t ->
+    List.Forall (fun p => ok_prem (env @@ qsenv) p) prems ->
     ok_clause env (qs, ags, e, prems) ps t
 .
 
@@ -411,22 +404,22 @@ Inductive ok_def : il_env -> il_def -> il_env -> Prop :=
     let env' := single_envtyp x ps insts in
     ok_params env ps ->
     List.Forall (fun inst => ok_inst env inst ps) insts ->
-    ok_def env (TypD x ps insts) (append_env env env')
+    ok_def env (TypD x ps insts) (env @@ env')
   | okd_rel : forall env x ps t rules,
     let env' := single_rel x ps t rules in
     let penv := paramenv ps in
     ok_params env ps ->
-    List.Forall (fun rule => ok_rule (append_env env penv) rule t) rules ->
-    ok_def env (RelD x ps t rules) (append_env env env')
+    List.Forall (fun rule => ok_rule (env @@ penv) rule t) rules ->
+    ok_def env (RelD x ps t rules) (env @@ env')
   | okd_fun : forall env x ps t clauses,
     let env' := single_def x ps t clauses in
     let penv := paramenv ps in
     ok_params env ps ->
-    List.Forall (fun clause => ok_clause (append_env env penv) clause ps t) clauses ->
-    ok_def env (DecD x ps t clauses) (append_env env env')
+    List.Forall (fun clause => ok_clause (env @@ penv) clause ps t) clauses ->
+    ok_def env (DecD x ps t clauses) (env @@ env')
   (* TODO recs doesn't make much sense *)
   | okd_rec : forall env env' defs,
-    ok_defs (append_env env env') defs env' ->
+    ok_defs (env @@ env') defs env' ->
     ok_def env (RecD defs) env'
   
 with
diff --git a/spectec/metatheory/theories/utils.v b/spectec/metatheory/theories/utils.v
index c41c31dd62..4610d263b4 100644
--- a/spectec/metatheory/theories/utils.v
+++ b/spectec/metatheory/theories/utils.v
@@ -11,6 +11,30 @@ Inductive option_forall {T : Type} (P : (T -> Prop)) : option T -> Prop :=
     option_forall P (Some x)
 .
 
+Definition opt_to_lst {X : Type} (x : option X) : list X :=
+  match x with
+  | Some a => [a]
+  | None => []
+  end
+.
+
+(* PRE: size xs <= 1 *)
+Definition lst_to_opt {X : Type} (xs : list X) : option X :=
+  match xs with
+  | [] => None
+  | [x] => Some x
+  (* Should not happen *)
+  | _ => None
+  end
+.
+
+Definition option_map {X Y : Type} (f : X -> Y) (x_opt : option X) : option Y :=
+  match x_opt with
+  | Some x => Some (f x)
+  | None => None
+  end
+.
+
 Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
 	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
 
@@ -33,6 +57,67 @@ Definition is_plaintyp (t : il_typ) : bool :=
   end
 .
 
+Fixpoint disjoint {X : eqType} (xs : list X) : bool :=
+  match xs with
+  | [] => true
+  | x :: xs => negb (x \in xs) && disjoint xs
+  end
+.
+
+Definition same_size {X : Type} (xss : list (list X)) : bool :=
+  match xss with
+  | [] => true
+  | [_] => true
+  | xs :: xss' => seq.all (fun xs' => size xs == size xs') xss'
+  end
+.
+
+(* PRE: all lists in xss are of same size *)
+Fixpoint transpose_helper {X : Type} (xss : list (list X)) (n : nat) : list (list X) :=
+  match n with
+  | O => []
+  | S n' =>
+    let heads := (List.flat_map (fun xs => 
+      match xs with
+      | [] => []
+      | x :: xs' => [x]
+      end
+    ) xss) in
+    heads :: transpose_helper (List.map behead xss) n'
+  end
+.
+
+Definition transpose {X : Type} (xss : list (list X)) : list (list X) :=
+  match xss with
+  | [] => []
+  | (xs :: xss') => transpose_helper xss (size xs)
+  end
+.
+
+Definition list_mapi {X Y : Type} (f : nat -> X -> Y) (xs : list X) : list Y :=
+  let idxs := iota 0 (size xs) in
+  List.map (fun '(i, x) => f i x) (zip idxs xs)
+.
+
+Inductive List_Forall3 {A B C: Type} (R : A -> B -> C -> Prop): seq A -> seq B -> seq C -> Prop :=
+	| Forall3_nil : List_Forall3 R nil nil nil
+	| Forall3_cons : forall x y z l l' l'',
+		R x y z -> List_Forall3 R l l' l'' -> List_Forall3 R (x :: l) (y :: l') (z :: l'').
+
+Definition list_map3 {A B C D: Type} (f : A -> B -> C -> D) (xs : seq A) (ys : seq B) (zs : seq C) : seq D :=
+	seq.map (fun '(x, (y, z)) => f x y z) (seq.zip xs (seq.zip ys zs)).
+
+Definition atomtyp (x : typfield) : atom * il_typ :=
+  match x with
+  | (a, _, t, _) => (a, t)
+  end
+.
+
+Definition atomtyps (xs : list typfield) : list (atom * il_typ) :=
+  List.map atomtyp xs.
+
+(* Decidable equality axiom *)
+
 Lemma eq_dec_Equality_axiom :
   forall (T : Type) (eq_dec : forall (x y : T), decidable (x = y)),
   let eqb v1 v2 := is_left (eq_dec v1 v2) in Equality.axiom eqb.
@@ -41,6 +126,8 @@ Proof.
   case: (eq_dec x y); by [apply: ReflectT | apply: ReflectF].
 Qed.
 
+(* Decidable equality for atoms *)
+
 Definition atom_eq_dec : forall (v1 v2 : atom),
   {v1 = v2} + {v1 <> v2}.
 Proof. do ? decide equality. Defined.
@@ -52,6 +139,8 @@ Definition eqatomP : Equality.axiom (atom_eqb) :=
 
 HB.instance Definition _ := hasDecEq.Build (atom) (eqatomP).
 
+(* Decidable equality for mixops *)
+
 Definition mixop_eq_dec : forall (v1 v2 : mixop),
   {v1 = v2} + {v1 <> v2}.
 Proof. do ? decide equality. Defined.

From 372a40f313334e62b3716deef6b774731833e07d Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Wed, 18 Mar 2026 12:06:39 +0000
Subject: [PATCH 09/11] Made changes (except reduction) to reflect pattern
 matching changes

---
 spectec/metatheory/theories/env.v       |  7 ++
 spectec/metatheory/theories/reduction.v | 30 ++++-----
 spectec/metatheory/theories/subst.v     | 76 +++++++++++++--------
 spectec/metatheory/theories/syntax.v    | 61 ++++++++++++-----
 spectec/metatheory/theories/typing.v    | 90 +++++++++++++++----------
 5 files changed, 167 insertions(+), 97 deletions(-)

diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
index 30c31e646d..3e436c9165 100644
--- a/spectec/metatheory/theories/env.v
+++ b/spectec/metatheory/theories/env.v
@@ -49,6 +49,13 @@ Definition append_env (e1 e2 : il_env) : il_env :=
 Definition single_var (x : il_id) (t : il_typ) : il_env :=
   {| VARS := singleton x t; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
 
+Fixpoint many_vars (xs : list (il_id * il_typ)) : il_env :=
+  match xs with
+  | [] => env_empty
+  | (x, t) :: xs' => append_env (single_var x t) (many_vars xs')
+  end
+.  
+
 Definition single_envtyp (x : il_id) (ps : list il_param) (insts : list il_inst) : il_env :=
   {| VARS := empty_vars; TYPS := singleton x (ps, insts); DEFS := empty_defs; RELS := empty_rels |}.
 
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 0595db29d5..63f7aadc71 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -232,34 +232,33 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     let es' := List.map opt_to_lst es in
     let es'' := transpose es' in
     let es''' := lst_to_opt es'' in
+    let ids := List.map fst xs in 
     same_size es' ->
     size xs = size es ->
     size es'' <= 1 ->
     step_exp s (IterE e I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es))
-    (OptE (option_map (fun ess => subst_exp (many_svars (zip xs ess)) e) es'''))
+    (OptE (option_map (fun ess => subst_exp (many_svars (zip ids ess)) e) es'''))
   | se_iter_plus : forall s e xs ess,
     same_size ess ->
     seq.all (fun es => size es >= 1) ess ->
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
     step_exp s (IterE e I_PLUS res_ess) (IterE e I_STAR res_ess)
-  | se_iter_star : forall s e xs ess n,
+  | se_iter_star : forall s e xs ess n y,
     seq.all (fun es => size es == n) ess ->
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
-    step_exp s (IterE e I_STAR res_ess) (IterE e (I_SUP None (NumE (NatE n))) res_ess)
-  | se_iter_sup_eps : forall s e eps e_n y,
-    (* TODO y needs to not clash with any other variable *)
-    step_exp s (IterE e (I_SUP None e_n) eps) (IterE e (I_SUP y e_n) eps)
+    step_exp s (IterE e I_STAR res_ess) (IterE e (I_SUP y (NumE (NatE n))) res_ess)
   | se_iter_sup : forall s e x_i n xs ess,
     seq.all (fun es => size es == n) ess ->
     size xs = size ess -> 
     let ess' := transpose ess in
+    let ids := List.map fst xs in
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
     let res_ess' := (list_mapi (fun i es => 
       let sbst := subst_svar x_i (NumE (NatE i)) in
-      let sbst' := many_svars (zip xs es) in
+      let sbst' := many_svars (zip ids es) in
       subst_exp (append_subst sbst sbst') e 
     ) ess') in
-    step_exp s (IterE e (I_SUP (Some x_i) (NumE (NatE n))) res_ess) (ListE res_ess')
+    step_exp s (IterE e (I_SUP x_i (NumE (NatE n))) res_ess) (ListE res_ess')
 
   (* CallE rules *)
   | se_call_ctx : forall s x ags n a a',
@@ -420,34 +419,33 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     let es' := List.map opt_to_lst es in
     let es'' := transpose es' in
     let es''' := lst_to_opt es'' in
+    let ids := List.map fst xs in 
     same_size es' ->
     size xs = size es ->
     size es'' <= 1 ->
     step_prems s [IterPr pr I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es)]
-    (opt_to_lst (option_map (fun ess => subst_prem (many_svars (zip xs ess)) pr) es'''))
+    (opt_to_lst (option_map (fun ess => subst_prem (many_svars (zip ids ess)) pr) es'''))
   | sp_iter_plus : forall s pr xs ess,
     same_size ess ->
     seq.all (fun es => size es >= 1) ess ->
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
     step_prems s [IterPr pr I_PLUS res_ess] [IterPr pr I_STAR res_ess]
-  | sp_iter_star : forall s pr xs ess n,
+  | sp_iter_star : forall s pr xs ess n y,
     seq.all (fun es => size es == n) ess ->
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
-    step_prems s [IterPr pr I_STAR res_ess] [IterPr pr (I_SUP None (NumE (NatE n))) res_ess]
-  | sp_iter_sup_eps : forall s pr eps e_n y,
-    (* TODO y needs to not clash with any other variable *)
-    step_prems s [IterPr pr (I_SUP None e_n) eps] [IterPr pr (I_SUP y e_n) eps]
+    step_prems s [IterPr pr I_STAR res_ess] [IterPr pr (I_SUP y (NumE (NatE n))) res_ess]
   | sp_iter_sup : forall s pr x_i n xs ess,
     seq.all (fun es => size es == n) ess ->
     size xs = size ess -> 
     let ess' := transpose ess in
     let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    let ids := List.map fst xs in 
     let res_ess' := (list_mapi (fun i es => 
       let sbst := subst_svar x_i (NumE (NatE i)) in
-      let sbst' := many_svars (zip xs es) in
+      let sbst' := many_svars (zip ids es) in
       subst_prem (append_subst sbst sbst') pr 
     ) ess') in
-    step_prems s [IterPr pr (I_SUP (Some x_i) (NumE (NatE n))) res_ess] res_ess'
+    step_prems s [IterPr pr (I_SUP x_i (NumE (NatE n))) res_ess] res_ess'
 
   (* TODO other iter rules *)
   (* NegPr rules *)
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index e4ad644bdc..59fd94aeb9 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -61,6 +61,13 @@ Fixpoint many_svars (xs : list (il_id * il_exp)) : il_subst :=
   end
 .
 
+Fixpoint compose_substs (xs : list il_subst) : il_subst :=
+  match xs with
+  | [] => subst_empty
+  | x :: xs' => append_subst x (compose_substs xs')
+  end
+.
+
 Definition append_dom (d1 d2 : dom) : dom :=
   {|
   D_EXP := d1.(D_EXP) ++ d2.(D_EXP);
@@ -99,12 +106,7 @@ Definition subst_fun (s : il_subst) (x : il_id) : il_id :=
   end
 .
 
-Definition subst_iter (s : il_subst) (i : iter) : iter :=
-  match i with
-  | I_SUP x e => I_SUP x e
-  | _ => i
-  end
-.
+
 
 Fixpoint subst_typ (s : il_subst) (t : il_typ) : il_typ :=
   match t with
@@ -115,6 +117,10 @@ Fixpoint subst_typ (s : il_subst) (t : il_typ) : il_typ :=
     end
   | TupT xts => TupT (List.map (fun '(x, t) => (x, subst_typ s t)) xts)
   | IterT t' it => IterT (subst_typ s t') (subst_iter s it)
+  | MatchT x args insts =>
+    MatchT x (List.map (subst_arg s) args) (List.map (fun '(qs, args', deftyp) =>
+      (List.map (subst_param s) qs, List.map (subst_arg s) args, subst_deftyp s deftyp)
+    ) insts)
   | _ => t
   end
 
@@ -140,16 +146,19 @@ subst_exp (s : il_subst) (e : il_exp) : il_exp :=
   | LenE e' => LenE (subst_exp s e')
   | MemE e1 e2 => MemE (subst_exp s e1) (subst_exp s e2)
   | CatE e1 e2 => CatE (subst_exp s e1) (subst_exp s e2)
-  | CompE e1 e2 => CompE (subst_exp s e1) (subst_exp s e2)
   | IdxE e1 e2 => IdxE (subst_exp s e1) (subst_exp s e2)
   | SliceE e1 e2 e3 => SliceE (subst_exp s e1) (subst_exp s e2) (subst_exp s e3)
   | AccE e' p => AccE (subst_exp s e') (subst_path s p)
   | UpdE e1 p e2 => UpdE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
   | ExtE e1 p e2 => ExtE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
   | CallE x args => CallE x (List.map (subst_arg s) args)
-  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun '(x, e) => (x, subst_exp s e)) xexps)
+  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun '(x, t, e) => (x, subst_typ s t, subst_exp s e)) xexps)
   | CvtE e' nt1 nt2 => CvtE (subst_exp s e') nt1 nt2
   | SubE e' t1 t2 => SubE (subst_exp s e') (subst_typ s t1) (subst_typ s t2)
+  | MatchE args clauses =>
+    MatchE (List.map (subst_arg s) args) (List.map (fun '(qs, args', e, prems) =>
+      (List.map (subst_param s) qs, List.map (subst_arg s) args, subst_exp s e, List.map (subst_prem s) prems)
+    ) clauses)   
   | _ => e
   end
 
@@ -173,27 +182,52 @@ subst_arg (s : il_subst) (a : il_arg) : il_arg :=
   | TypA t => TypA (subst_typ s t)
   | DefA x => DefA (subst_fun s x)
   end
-.
 
-Fixpoint subst_param (s : il_subst) (p : il_param) : il_param :=
+with
+
+subst_param (s : il_subst) (p : il_param) : il_param :=
   match p with
   | ExpP x t => ExpP x (subst_typ s t)
   | TypP x => TypP x
   | DefP x ps t => DefP x (List.map (subst_param s) ps) (subst_typ s t)
   end
-.
+with
 
-Definition subst_quant (s : il_subst) (p : il_quant) : il_quant := subst_param s p.
+subst_iter (s : il_subst) (i : iter) : iter :=
+  match i with
+  | I_SUP x e => I_SUP x (subst_exp s e)
+  | _ => i
+  end
 
-Fixpoint subst_prem (s : il_subst) (p : il_prem) : il_prem :=
+
+with 
+
+subst_prem (s : il_subst) (p : il_prem) : il_prem :=
   match p with
   | RulePr x args e => RulePr x (List.map (subst_arg s) args) (subst_exp s e)
   | IfPr e => IfPr (subst_exp s e)
   | ElsePr => ElsePr
   | LetPr e1 e2 => LetPr (subst_exp s e1) (subst_exp s e2)
-  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun '(x, e) => (x, subst_exp s e)) xexps)
+  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun '(x, t, e) => (x, subst_typ s t, subst_exp s e)) xexps)
   | NegPr p' => NegPr (subst_prem s p')
-  end.
+  end
+
+with 
+
+subst_deftyp (s : il_subst) (dt : il_deftyp) : il_deftyp :=
+  match dt with
+  | AliasT t => AliasT (subst_typ s t)
+  | StructT typfields => StructT (List.map (fun '(a, qs, t, prems) =>
+    (a, List.map (subst_param s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typfields)
+  | VariantT typcases => VariantT (List.map (fun '(m, qs, t, prems) =>
+    (m, List.map (subst_param s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typcases)
+  end
+.
+
+
+Definition subst_quant (s : il_subst) (p : il_quant) : il_quant := subst_param s p.
 
 Definition arg_for_param (a : il_arg) (p : il_param) : il_subst :=
   match a, p with
@@ -213,18 +247,6 @@ Fixpoint args_for_params (ags : list il_arg) (ps : list il_param) : il_subst :=
   end
 .
 
-Definition subst_deftyp (s : il_subst) (dt : il_deftyp) : il_deftyp :=
-  match dt with
-  | AliasT t => AliasT (subst_typ s t)
-  | StructT typfields => StructT (List.map (fun '(a, qs, t, prems) =>
-    (a, List.map (subst_quant s) qs, subst_typ s t, List.map (subst_prem s) prems) 
-  ) typfields)
-  | VariantT typcases => VariantT (List.map (fun '(m, qs, t, prems) =>
-    (m, List.map (subst_quant s) qs, subst_typ s t, List.map (subst_prem s) prems) 
-  ) typcases)
-  end
-.
-
 Definition param_to_arg (p : il_param) : il_arg :=
   match p with
   | ExpP x _ => ExpA (VarE x)
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 0f11729216..a478b20af6 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -82,6 +82,17 @@ Inductive il_num : Type :=
   | RealE : R -> il_num
 .
 
+Inductive il_val : Type :=
+  | NumV : il_num -> il_val
+  | BoolV : bool -> il_val
+  | TextV : text -> il_val
+  | TupV : list il_val -> il_val
+  | CaseV : mixop -> il_val -> il_val
+  | OptV : option il_val -> il_val
+  | ListV : list il_val -> il_val
+  | StrV : list (atom * il_val) -> il_val
+.
+
 Inductive il_typ : Type :=
   | VarT : il_id -> list il_arg -> il_typ
   | BoolT
@@ -89,6 +100,7 @@ Inductive il_typ : Type :=
   | NumT : numtyp -> il_typ
   | TupT : list (il_id * il_typ) -> il_typ
   | IterT : il_typ -> iter -> il_typ
+  | MatchT : il_id -> list il_arg -> list (list il_param * list il_arg * il_deftyp) -> il_typ
 
 with
 
@@ -106,7 +118,6 @@ il_exp : Type :=
   | OptE : option il_exp -> il_exp
   | StrE : list (atom * il_exp) -> il_exp
   | DotE : il_exp * atom -> il_exp
-  | CompE : il_exp -> il_exp -> il_exp
   | ListE : list il_exp -> il_exp
   | LiftE : il_exp -> il_exp
   | MemE : il_exp -> il_exp -> il_exp
@@ -118,10 +129,11 @@ il_exp : Type :=
   | UpdE : il_exp -> il_path -> il_exp -> il_exp
   | ExtE : il_exp -> il_path -> il_exp -> il_exp
   | CallE : il_id -> list il_arg -> il_exp
-  | IterE : il_exp -> iter -> list (il_id * il_exp) -> il_exp
+  | IterE : il_exp -> iter -> list (il_id * il_typ * il_exp) -> il_exp
   | CvtE : il_exp -> numtyp -> numtyp -> il_exp
   | SubE : il_exp -> il_typ -> il_typ -> il_exp
   | IfE : il_exp -> il_exp -> il_exp -> il_exp
+  | MatchE : list il_arg -> list (list il_param * list il_arg * il_exp * list il_prem) -> il_exp
 
 with
 
@@ -146,41 +158,40 @@ iter : Type :=
   | I_STAR
   | I_OPT
   | I_PLUS
-  | I_SUP : option il_id -> il_exp -> iter
-.
+  | I_SUP : il_id -> il_exp -> iter
 
-Definition exppull : Type := (il_id * il_exp).
+with 
 
-Inductive il_param : Type :=
+il_param : Type :=
   | ExpP : il_id -> il_typ -> il_param
   | TypP : il_id -> il_param
   | DefP : il_id -> list il_param -> il_typ -> il_param
-.
 
-Definition il_quant : Type := il_param.
+with 
 
-Inductive il_prem : Type :=
+il_prem : Type :=
   | RulePr : il_id -> list il_arg -> il_exp -> il_prem
   | IfPr : il_exp -> il_prem
   | ElsePr
   | LetPr : il_exp -> il_exp -> il_prem
-  | IterPr : il_prem -> iter -> list exppull -> il_prem
+  | IterPr : il_prem -> iter -> list (il_id * il_typ * il_exp) -> il_prem
   | NegPr : il_prem -> il_prem
-.
 
-Definition typfield : Type := atom * list il_quant * il_typ * list il_prem.
-Definition typcase : Type := mixop * list il_quant * il_typ * list il_prem.
+with 
 
-Inductive il_deftyp : Type :=
+il_deftyp : Type :=
   | AliasT : il_typ -> il_deftyp
-  | StructT : list typfield -> il_deftyp
-  | VariantT : list typcase -> il_deftyp
+  | StructT : list (atom * list il_param * il_typ * list il_prem) -> il_deftyp
+  | VariantT : list (mixop * list il_param * il_typ * list il_prem) -> il_deftyp
 .
 
-Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
+Definition exppull : Type := (il_id * il_typ * il_exp).
+Definition il_quant : Type := il_param.
+Definition typfield : Type := atom * list il_quant * il_typ * list il_prem.
+Definition typcase : Type := mixop * list il_quant * il_typ * list il_prem.
 
+Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
 Definition il_rule : Type := list il_quant * il_exp * list il_prem.
-
 Definition il_clause : Type := list il_quant * list il_arg * il_exp * list il_prem.
 
 Inductive il_def : Type :=
@@ -191,3 +202,17 @@ Inductive il_def : Type :=
 .
 
 Definition script : Type := list il_def.
+
+Fixpoint val_to_exp (v : il_val) : il_exp :=
+  match v with
+  | NumV n => NumE n
+  | BoolV b => BoolE b
+  | TextV t => TextE t
+  | TupV vs => TupE (List.map val_to_exp vs)
+  | CaseV m v => CaseE m (val_to_exp v)
+  | OptV (Some v) => OptE (Some (val_to_exp v))
+  | OptV None => OptE None
+  | ListV vs => ListE (List.map val_to_exp vs)
+  | StrV valfields => StrE (List.map (fun '(a, v) => (a, val_to_exp v)) valfields)
+  end
+.
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index fced01312d..84a71f4b4b 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -4,14 +4,14 @@ From MetaSpectec Require Import syntax env reduction subst utils.
 Import ListNotations.
 Open Scope env_scope.
 
-Inductive composable_typ : il_env -> il_typ -> Prop :=
+Inductive catable_typ : il_env -> il_typ -> Prop :=
   | ct_iter : forall env t t' it,
     expand_typ (env_to_store env) t (AliasT (IterT t' it)) ->
-    composable_typ env t
+    catable_typ env t
   | ct_struct : forall env t typfields,
     expand_typ (env_to_store env) t (StructT typfields) ->
-    List.Forall (fun p => composable_typ env (snd (fst p))) typfields ->
-    composable_typ env t
+    List.Forall (fun p => catable_typ env (snd (fst p))) typfields ->
+    catable_typ env t
 .
 
 Inductive sub_numtyp : numtyp -> numtyp -> Prop :=
@@ -161,12 +161,8 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
   | oke_cat : forall env e1 e2 t,
     ok_exp env e1 (IterT t I_STAR) ->
     ok_exp env e2 (IterT t I_STAR) ->
+    catable_typ env t ->
     ok_exp env (CatE e1 e2) (IterT t I_STAR)
-  | oke_comp : forall env e1 e2 t,
-    ok_exp env e1 t ->
-    ok_exp env e2 t ->
-    composable_typ env t ->
-    ok_exp env (CompE e1 e2) t
   | oke_acc : forall env e p t t',
     ok_exp env e t ->
     ok_path env p t t' ->
@@ -185,7 +181,14 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
     StringMap.find x (DEFS env) = Some (ps, rt, clauses) ->
     ok_args env ags ps sbst ->
     ok_exp env (CallE x ags) (subst_typ sbst rt)
-  (* TODO iterE valid *)
+  | oke_iter : forall env env' e iter xps t iter',
+    ok_iter env iter iter' env' ->
+    List.Forall (fun p => ok_typ env (snd (fst p))) xps ->
+    List.Forall (fun p => ok_exp env (snd p) (IterT (snd (fst p)) iter')) xps ->
+    let envs := many_vars (List.map fst xps) in
+    ok_exp (env @@ envs @@ env') e t ->
+    ok_typ env t ->
+    ok_exp env (IterE e iter xps) (IterT t iter')
   | oke_cvt : forall env e nt1 nt2,
     ok_exp env e (NumT nt1) ->
     ok_exp env (CvtE e nt1 nt2) (NumT nt2)
@@ -193,6 +196,12 @@ Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
     ok_exp env e t1 ->
     sub_typ env t1 t2 ->
     ok_exp env (SubE e t1 t2) t2
+  | oke_match : forall env ags ps clauses t sbst,
+    ok_args env ags ps sbst -> 
+    ok_params env ps ->
+    let penv := paramenv ps in 
+    List.Forall (fun c => ok_clause (append_env env penv) c ps t) clauses ->
+    ok_exp env (MatchE ags clauses) t
   | ok_exp_conv : forall env e t t',
     ok_exp env e t' ->
     eq_typ (env_to_store env) t t' ->
@@ -251,6 +260,11 @@ ok_typ : il_env -> il_typ -> Prop :=
     (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
     ok_args env ags ps sbst ->
     ok_typ env (VarT x ags)
+  | okt_match : forall env x ags ps insts sbst,
+    (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
+    ok_args env ags ps sbst ->
+    List.Forall (fun inst => ok_inst env inst ps) insts ->
+    ok_typ env (MatchT x ags insts)
 
 with
 
@@ -258,12 +272,9 @@ ok_iter : il_env -> iter -> iter -> il_env -> Prop :=
   | oki_quest : forall env, ok_iter env I_OPT I_OPT env_empty 
   | oki_star : forall env, ok_iter env I_STAR I_STAR env_empty
   | oki_plus : forall env, ok_iter env I_PLUS I_STAR env_empty
-  | oki_sup_none : forall env e,
-    ok_exp env e (NumT NatT) ->
-    ok_iter env (I_SUP None e) I_STAR env_empty
   | oki_sup_some : forall env e x,
     ok_exp env e (NumT NatT) ->
-    ok_iter env (I_SUP (Some x) e) I_STAR (single_var x (NumT NatT))
+    ok_iter env (I_SUP x e) I_STAR (single_var x (NumT NatT))
 
 with
 
@@ -282,9 +293,13 @@ ok_prem : il_env -> il_prem -> Prop :=
     ok_exp env e1 t ->
     ok_exp env e2 t ->
     ok_prem env (LetPr e1 e2)
-  (* | okp_iter : forall env pr it it' env'' expps,
-    let env' := single_var x  
-    ok_iter env it it' env' -> *)
+  | okp_iter : forall env pr it it' env' xps,
+    ok_iter env it it' env' ->
+    List.Forall (fun p => ok_typ env (snd (fst p))) xps ->
+    List.Forall (fun p => ok_exp env (snd p) (IterT (snd (fst p)) it')) xps ->
+    let envs := many_vars (List.map fst xps) in
+    ok_prem (env @@ envs @@ env') pr ->
+    ok_prem env (IterPr pr it xps)
   | okp_neg : forall env p,
     ok_prem env p ->
     ok_prem env (NegPr p)
@@ -298,7 +313,6 @@ ok_arg : il_env -> il_arg -> il_param -> il_subst -> Prop :=
   | oka_typ : forall env t x,
     ok_typ env t ->
     ok_arg env (TypA t) (TypP x) (subst_styp x t)
-  (* TODO fun arg *)
   | oka_fun : forall env y x ps rt ps' rt' clauses sbst,
     StringMap.find y (DEFS env) = Some (ps', rt', clauses) ->
     sub_params env ps ps' sbst ->
@@ -334,9 +348,10 @@ ok_params : il_env -> list il_param -> Prop :=
   | okpas_cons : forall env p1 ps,
     ok_param env p1 ->
     ok_params (env @@ (paramenv [p1])) ps
-.
 
-Inductive ok_typfield : il_env -> typfield -> Prop :=
+with
+
+ok_typfield : il_env -> typfield -> Prop :=
   | oktypfield : forall env a t qs prems,
     let tenv := tupenv t in
     let qsenv := paramenv qs in
@@ -344,9 +359,10 @@ Inductive ok_typfield : il_env -> typfield -> Prop :=
     ok_params (env @@ tenv) qs ->
     List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
     ok_typfield env (a, qs, t, prems)
-.
 
-Inductive ok_typcase : il_env -> typcase -> Prop :=
+with
+
+ok_typcase : il_env -> typcase -> Prop :=
   | oktypcase : forall env m t qs prems,
     let tenv := tupenv t in
     let qsenv := paramenv qs in
@@ -354,9 +370,10 @@ Inductive ok_typcase : il_env -> typcase -> Prop :=
     ok_params (env @@ tenv) qs ->
     List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
     ok_typcase env (m, qs, t, prems)
-.
 
-Inductive ok_deftyp : il_env -> il_deftyp -> Prop :=
+with
+
+ok_deftyp : il_env -> il_deftyp -> Prop :=
   | okd_alias : forall env t,
     ok_typ env t ->
     ok_deftyp env (AliasT t)
@@ -370,26 +387,19 @@ Inductive ok_deftyp : il_env -> il_deftyp -> Prop :=
     List.Forall (fun tc => ok_typcase env tc) tcs ->
     disjoint mixops ->
     ok_deftyp env (VariantT tcs)
-.
- 
 
-Inductive ok_inst : il_env -> il_inst -> list il_param -> Prop :=
+with 
+
+ok_inst : il_env -> il_inst -> list il_param -> Prop :=
   | oki_inst : forall env qs ags dt ps sbst,
     ok_params env qs ->
     ok_args (env @@ (paramenv qs)) ags ps sbst ->
     ok_deftyp (env @@ (paramenv qs)) dt ->
     ok_inst env (qs, ags, dt) ps
-.
 
-Inductive ok_rule : il_env -> il_rule -> il_typ -> Prop :=
-  | okr_rule : forall env qs e prems t,
-    ok_params env qs ->
-    ok_exp (env @@ (paramenv qs)) e t ->
-    List.Forall (fun p => ok_prem (env @@ (paramenv qs)) p) prems ->
-    ok_rule env (qs, e, prems) t
-.
+with
 
-Inductive ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
+ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
   | okc_clause : forall env qs ags e prems ps t sbst,
     let qsenv := paramenv qs in
     ok_params env qs ->
@@ -399,6 +409,14 @@ Inductive ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
     ok_clause env (qs, ags, e, prems) ps t
 .
 
+Inductive ok_rule : il_env -> il_rule -> il_typ -> Prop :=
+  | okr_rule : forall env qs e prems t,
+    ok_params env qs ->
+    ok_exp (env @@ (paramenv qs)) e t ->
+    List.Forall (fun p => ok_prem (env @@ (paramenv qs)) p) prems ->
+    ok_rule env (qs, e, prems) t
+.
+
 Inductive ok_def : il_env -> il_def -> il_env -> Prop :=
   | okd_typ : forall env x ps insts,
     let env' := single_envtyp x ps insts in

From 1452967563cc2423855750bd1ef76816a5ed2a22 Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Mon, 13 Apr 2026 11:26:36 +0200
Subject: [PATCH 10/11] Adding pattern matching in progress

---
 spectec/metatheory/theories/numerics.v  |  13 ++-
 spectec/metatheory/theories/reduction.v | 114 +++++++++++++++++++++---
 spectec/metatheory/theories/subst.v     |  15 ++++
 spectec/metatheory/theories/syntax.v    |  10 +++
 spectec/metatheory/theories/utils.v     |   8 ++
 5 files changed, 145 insertions(+), 15 deletions(-)

diff --git a/spectec/metatheory/theories/numerics.v b/spectec/metatheory/theories/numerics.v
index 32c7705ce0..bf88a513a2 100644
--- a/spectec/metatheory/theories/numerics.v
+++ b/spectec/metatheory/theories/numerics.v
@@ -24,7 +24,7 @@ Definition boolbin (op : boolbinop) (b1 b2 : bool) : bool :=
   end
 .
 
-Definition iszero(x : il_num) : bool := 
+Definition iszero (x : il_num) : bool := 
   match x with
   | NatE n => n == 0%nat
   | IntE i => i == 0%R
@@ -33,7 +33,7 @@ Definition iszero(x : il_num) : bool :=
   end
 .
 
-Definition isone(x : il_num) : bool := 
+Definition isone (x : il_num) : bool := 
   match x with
   | NatE n => n == 1%nat
   | IntE i => i == 1%R
@@ -42,6 +42,15 @@ Definition isone(x : il_num) : bool :=
   end
 .
 
+Definition isneg (x : il_num) : bool :=
+  match x with
+  | NatE n => false
+  | IntE i => (i < 0)%R
+  | RatE r => (r < 0)%R 
+  | RealE r => (r < 0)%R
+  end
+.
+
 Definition option_map {α β : Type} (f : α -> β) (x : option α) : option β :=
 	match x with
   | Some x => Some (f x)
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 63f7aadc71..678dc191f2 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -9,6 +9,8 @@ Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> i
     match_args s ags qs ags' sbst
 .
 
+
+
 Inductive expand_typ : store -> il_typ -> il_deftyp -> Prop :=
   | et_plain : forall s t,
     is_plaintyp t ->
@@ -290,6 +292,8 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_sub_ctx3 : forall s e t1 t2 t2',
     step_typ s t2 t2' ->
     step_exp s (SubE e t1 t2) (SubE e t1 t2')
+  | se_sub_refl : forall s e t,
+    step_exp s (SubE e t t) e
   | se_sub_sub : forall s e' t1' t2' t1 t2,
     step_exp s (SubE (SubE e' t1' t2') t1 t2) (SubE e' t1' t2)
   | se_sub_tup : forall s es tups tups',
@@ -303,21 +307,21 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     step_exp s (SubE (OptE e_opt) (IterT t1 I_OPT) (IterT t2 I_OPT)) (OptE (option_map (fun e => SubE e t1 t2) e_opt))
   | se_sub_list : forall s es t1 t2,
     step_exp s (SubE (ListE es) (IterT t1 I_STAR) (IterT t2 I_STAR)) (ListE (List.map (fun e => SubE e t1 t2) es))
-  | se_sub_case : forall s (e : il_exp) op e x1 ags1 x2 ags2 t1 t2 tcs1 tcs2 qs1 qs2 prs1 prs2,
-    expand_typ s (VarT x1 ags1) (VariantT tcs1) ->
-    expand_typ s (VarT x2 ags2) (VariantT tcs2) ->
-    List.In (op, qs1, t1, prs1) tcs1 ->
-    List.In (op, qs2, t2, prs2) tcs2 ->
-    step_exp s (SubE (CaseE op e) (VarT x1 ags1) (VarT x2 ags2)) (CaseE op (SubE e t1 t2))
-  | se_sub_str : forall s efs x1 ags1 x2 ags2 t1s t2s tfs1 tfs2 ats es,
-    expand_typ s (VarT x1 ags1) (StructT tfs1) ->
-    expand_typ s (VarT x2 ags2) (StructT tfs2) ->
+  | se_sub_case : forall s (e : il_exp) op e x1 x2 t1 t2 t1' t2' tcs1 tcs2 qs1 qs2 prs1 prs2,
+    t1 = MatchT x1 [] [([], [], VariantT tcs1)] ->
+    t2 = MatchT x2 [] [([], [], VariantT tcs2)] ->    
+    List.In (op, qs1, t1', prs1) tcs1 ->
+    List.In (op, qs2, t2', prs2) tcs2 ->
+    step_exp s (SubE (CaseE op e) t1 t2) (CaseE op (SubE e t1' t2'))
+  | se_sub_str : forall s efs x1 x2 t1 t2 t1s t2s tfs1 tfs2 ats es,
+    t1 = MatchT x1 [] [([], [], StructT tfs1)] ->
+    t2 = MatchT x2 [] [([], [], StructT tfs2)] -> 
     size efs = size tfs1 ->
     size efs = size tfs2 ->
     List_Forall3 (fun '(a, t) a' t' => a = a' /\ t = t') (atomtyps tfs2) ats t2s ->
     List.Forall2 (fun a t => List.In (a, t) (atomtyps tfs1)) ats t1s ->
     List.Forall2 (fun a e => List.In (a, e) efs) ats es ->
-    step_exp s (SubE (StrE efs) (VarT x1 ags1) (VarT x2 ags2))
+    step_exp s (SubE (StrE efs) t1 t2)
     (StrE (list_map3 (fun '(a, e) t1 t2 => (a, SubE e t1 t2)) (zip ats es) t1s t2s)) 
 
   (* IfE rules *)
@@ -328,6 +332,15 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     step_exp s (IfE (BoolE true) e2 e3) e2
   | se_ife_false : forall s e2 e3,
     step_exp s (IfE (BoolE false) e2 e3) e3
+  (* MatchE rules *)
+  | se_matche_ctx1 : forall s ags cs a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_exp s (MatchE ags cs) (MatchE (update ags n a') cs)
+  | se_matche_ctx2 : forall s ags cs c c' n,
+    List.nth_error cs n = Some c -> 
+    step_clause s c c' ->
+    step_exp s (MatchE ags cs) (MatchE ags (update cs n c'))
 with
 
 step_arg : store -> il_arg -> il_arg -> Prop :=
@@ -345,9 +358,9 @@ step_typ : store -> il_typ -> il_typ -> Prop :=
     List.nth_error ags n = Some a ->
     step_arg s a a' ->
     step_typ s (VarT x ags) (VarT x (update ags n a'))
-  | st_var_app : forall s x ags t, 
-    expand_typ s (VarT x ags) (AliasT t) ->
-    step_typ s (VarT x ags) t
+  | st_var_app : forall s x ags ps insts,
+    StringMap.find x (TYPS (store_to_env s)) = Some (ps, insts) ->
+    step_typ s (VarT x ags) (MatchT x ags insts)
   | st_tup_ctx : forall s tups n x t,
     List.nth_error tups n = Some (x, t) ->
     step_typ s (TupT tups) (TupT (update tups n (x, t)))
@@ -486,6 +499,81 @@ reduce_prems : store -> list il_prem -> list il_prem -> Prop :=
     step_prems s p1 p2 ->
     reduce_prems s p2 p3 ->
     reduce_prems s p1 p3
+
+with
+
+step_inst : store -> il_inst -> il_inst -> Prop :=
+  | sti_ctx : forall s qs ags t a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_inst s (qs, ags, t) (qs, update ags n a', t)
+
+with
+
+step_clause : store -> il_clause -> il_clause -> Prop :=
+  | stc_ctx1 : forall s qs ags e prems a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_clause s (qs, ags, e, prems) (qs, update ags n a', e, prems)
+  | stc_ctx2 : forall s qs ags e prems e',
+    step_exp s e e' ->
+    step_clause s (qs, ags, e, prems) (qs, ags, e', prems)
+  | stc_ctx3 : forall s qs ags e prems prems',
+    step_prems s prems prems' ->
+    step_clause s (qs, ags, e, prems) (qs, ags, e, prems')
+
+with
+
+step_argmatch_plain : store -> list argmatch -> list argmatch -> Prop :=
+  | sagp_ctx1 : forall s a a' a'',
+    step_arg s a a'' ->
+    step_argmatch_plain s [MatchA a a'] [MatchA a'' a']
+  | sagp_ctx2 : forall s a a' a'',
+    step_arg s a' a'' ->
+    step_argmatch_plain s [MatchA a a'] [MatchA a a'']
+  | sagp_eq : forall s a,
+    step_argmatch_plain s [MatchA a a] []
+
+with
+
+step_expmatch_plain : store -> list expmatch -> list expmatch -> Prop :=
+  | semp_ctx1 : forall s e e' e'',
+    step_exp s e e'' ->
+    step_expmatch_plain s [MatchEM e e'] [MatchEM e'' e']
+  | semp_ctx2 : forall s e e' e'',
+    step_exp s e' e'' ->
+    step_expmatch_plain s [MatchEM e e'] [MatchEM e e'']
+  | semp_eq : forall s e,
+    step_expmatch_plain s [MatchEM e e] []
+  | semp_unplus : forall s num e,
+    negb (isneg num) ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop PlusOp) e)] [MatchEM (NumE num) e]
+  | semp_unplus_false : forall s num e,
+    isneg num ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop PlusOp) e)] [FailEM]
+  | semp_unminus : forall s num num' e,
+    isneg num ->
+    numun MinusOp num = Some num' ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop MinusOp) e)] [MatchEM (NumE num') e] 
+  | semp_unminus_false : forall s num e,
+    negb (isneg num) ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop MinusOp) e)] [FailEM]
+  | semp_cvt : forall s num e nt1 nt2 num',
+    numcvt nt1 num = Some num' ->
+    step_expmatch_plain s [MatchEM (NumE num) (CvtE e nt1 nt2)] [MatchEM (NumE num') e]
+  | semp_cvt_false : forall s num e nt1 nt2,
+    numcvt nt1 num = None ->
+    step_expmatch_plain s [MatchEM (NumE num) (CvtE e nt1 nt2)] [FailEM]
+  | semp_tup : forall s tups tups',
+    size tups = size tups' ->
+    step_expmatch_plain s [MatchEM (TupE tups) (TupE tups')] (list_zipWith (fun e e' => MatchEM e e') tups tups')
+  | semp_case : forall s e e' op,
+    step_expmatch_plain s [MatchEM (CaseE op e) (CaseE op e')] [MatchEM e e']
+  | semp_case_fail : forall s e e' op op',
+    op <> op' ->
+    step_expmatch_plain s [MatchEM (CaseE op e) (CaseE op' e')] [MatchEM e e']
+  (* | semp_opt : forall s e e',
+     *)
 .
 
 Inductive reduce_arg : store -> il_arg -> il_arg -> Prop :=
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index 59fd94aeb9..7e25bccf5c 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -255,6 +255,21 @@ Definition param_to_arg (p : il_param) : il_arg :=
   end
 .
 
+Definition subst_argmatch (s : il_subst) (a : argmatch) : argmatch :=
+  match a with
+  | FailA => FailA
+  | MatchA a' a'' => MatchA (subst_arg s a') (subst_arg s a'')
+  end
+.
+
+Definition subst_expmatch (s : il_subst) (e : expmatch) : expmatch :=
+  match e with
+  | FailEM => FailEM
+  | MatchEM e' e'' => MatchEM (subst_exp s e') (subst_exp s e'')
+  end
+.
+
+(* TODO *)
 Inductive ok_subst : il_env -> il_subst -> list il_quant -> Prop := 
   | Subst_OK : forall E s q_lst,
     ok_subst E s q_lst.
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index a478b20af6..0a30102a21 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -216,3 +216,13 @@ Fixpoint val_to_exp (v : il_val) : il_exp :=
   | StrV valfields => StrE (List.map (fun '(a, v) => (a, val_to_exp v)) valfields)
   end
 .
+
+Inductive argmatch : Type :=
+  | MatchA : il_arg -> il_arg -> argmatch
+  | FailA : argmatch
+.
+
+Inductive expmatch : Type :=
+  | MatchEM : il_exp -> il_exp -> expmatch
+  | FailEM : expmatch
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/utils.v b/spectec/metatheory/theories/utils.v
index 4610d263b4..6073dd564d 100644
--- a/spectec/metatheory/theories/utils.v
+++ b/spectec/metatheory/theories/utils.v
@@ -35,6 +35,14 @@ Definition option_map {X Y : Type} (f : X -> Y) (x_opt : option X) : option Y :=
   end
 .
 
+Definition same_opt {X : Type} (x_opt : option X) (y_opt : option X) : bool :=
+  match x_opt, y_opt with
+  | Some _, Some _ => true
+  | None, None => true
+  | _, _ => false
+  end
+.
+
 Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
 	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
 

From 3a10283c5b56989689ca4d36a6cc559e3783246f Mon Sep 17 00:00:00 2001
From: DCupello1 <dc1020@ic.ac.uk>
Date: Tue, 14 Apr 2026 15:17:05 +0200
Subject: [PATCH 11/11] Pattern matching ported

---
 spectec/metatheory/theories/reduction.v | 299 +++++++++++++++++++-----
 spectec/metatheory/theories/subst.v     |   6 +
 spectec/metatheory/theories/syntax.v    |   2 +
 spectec/metatheory/theories/typing.v    |  22 +-
 spectec/metatheory/theories/utils.v     |  36 ++-
 5 files changed, 287 insertions(+), 78 deletions(-)

diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
index 678dc191f2..3db73b318a 100644
--- a/spectec/metatheory/theories/reduction.v
+++ b/spectec/metatheory/theories/reduction.v
@@ -2,6 +2,7 @@ From Stdlib Require Import List String Reals.
 From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
 From MetaSpectec Require Import syntax subst env numerics utils.
 Import ListNotations.
+Open Scope env_scope.
 
 Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> il_subst -> Prop :=
   | ma_rule : forall s ags qs ags' sbst,
@@ -9,24 +10,6 @@ Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> i
     match_args s ags qs ags' sbst
 .
 
-
-
-Inductive expand_typ : store -> il_typ -> il_deftyp -> Prop :=
-  | et_plain : forall s t,
-    is_plaintyp t ->
-    expand_typ s t (AliasT t)
-  | et_alias : forall s x ags t dt,
-    expand_typ s (VarT x ags) (AliasT t) ->
-    expand_typ s t dt ->
-    expand_typ s (VarT x ags) dt
-  | et_step : forall s e x ags ags' dt ps insts n qs sbst,
-    store_to_env s = e ->
-    StringMap.find x (TYPS e) = Some (ps, insts) ->
-    List.nth_error insts n = Some (qs, ags', dt) ->
-    match_args s ags qs ags' sbst ->
-    expand_typ s (VarT x ags) (subst_deftyp sbst dt)
-.
-
 Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   (* UnE Rules *)
   | se_unop_ctx : forall s op e1 e2,
@@ -58,12 +41,18 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_cmp_ctxr : forall s op e1 e2 e2',
     step_exp s e2 e2' ->
     step_exp s (CmpE op e1 e2) (CmpE op e1 e2')
-  | se_cmp_eq_true : forall s e1 e2,
-    e1 = e2 ->
-    step_exp s (CmpE (BoolCmpop EqOp) e1 e2) (BoolE true)
-  | se_cmp_ne_false : forall s e1 e2,
-    e1 = e2 ->
-    step_exp s (CmpE (BoolCmpop NeqOp) e1 e2) (BoolE false)
+  | se_cmp_eq_true : forall s v1 v2,
+    v1 = v2 ->
+    step_exp s (CmpE (BoolCmpop EqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE true)
+  | se_cmp_eq_false : forall s v1 v2,
+    v1 <> v2 ->
+    step_exp s (CmpE (BoolCmpop EqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE false)
+  | se_cmp_ne_false : forall s v1 v2,
+    v1 = v2 ->
+    step_exp s (CmpE (BoolCmpop NeqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE false)
+  | se_cmp_ne_true : forall s v1 v2,
+    v1 <> v2 ->
+    step_exp s (CmpE (BoolCmpop NeqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE true)
   | se_cmp_num : forall s numcmpop n1 n2 b,
     (numcmp numcmpop n1 n2) = Some b ->
     step_exp s (CmpE (NumCmpop numcmpop) (NumE n1) (NumE n2)) (BoolE b)
@@ -121,18 +110,12 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
   | se_mem_ctxr : forall s e1 e2 e2',
     step_exp s e2 e2' ->
     step_exp s (MemE e1 e2) (MemE e1 e2')
-  | se_mem_opt_true : forall s e1 e2,
-    e1 = e2 ->
-    step_exp s (MemE e1 (OptE (Some e2))) (BoolE true)
-  | se_mem_opt_false : forall s e1 e2_opt,
-    option_forall (fun e2 => e1 <> e2) e2_opt ->
-    step_exp s (MemE e1 (OptE e2_opt)) (BoolE false)
-  | se_mem_list_true : forall s e1 e2s,
-    List.In e1 e2s ->
-    step_exp s (MemE e1 (ListE e2s)) (BoolE true)
-  | se_mem_list_false : forall s e1 e2s,
-    List.Forall (fun e2 => e1 <> e2) e2s ->
-    step_exp s (MemE e1 (ListE e2s)) (BoolE false)
+  | se_mem_true : forall s v1 v2s,
+    List.In v1 v2s ->
+    step_exp s (MemE (val_to_exp v1) (ListE (List.map val_to_exp v2s))) (BoolE true)
+  | se_mem_false : forall s v1 v2s,
+    List.Forall (fun v2 => v1 <> v2) v2s ->
+    step_exp s (MemE (val_to_exp v1) (ListE (List.map val_to_exp v2s))) (BoolE false)
 
   (* CatE rules *)
   | se_cat_ctxl : forall s e1 e1' e2,
@@ -267,12 +250,9 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     List.nth_error ags n = Some a ->
     step_arg s a a' ->
     step_exp s (CallE x ags) (CallE x (update ags n a'))
-  | se_call_app : forall s x ags ags' ps qs t cs e prems sbst n,
+  | se_call_app : forall s x ags cs ps t,
     StringMap.find x (DEFS (store_to_env s)) = Some (ps, t, cs) ->
-    List.nth_error cs n = Some (qs, ags', e, prems) ->
-    match_args s ags qs ags' sbst ->
-    reduce_prems s (List.map (subst_prem sbst) prems) [] ->
-    step_exp s (CallE x ags) (subst_exp sbst e)
+    step_exp s (CallE x ags) (MatchE ags cs)
 
   (* CvtE rules *)
   | se_cvt_ctx : forall s e nt1 nt2 e',
@@ -332,6 +312,7 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     step_exp s (IfE (BoolE true) e2 e3) e2
   | se_ife_false : forall s e2 e3,
     step_exp s (IfE (BoolE false) e2 e3) e3
+
   (* MatchE rules *)
   | se_matche_ctx1 : forall s ags cs a a' n,
     List.nth_error ags n = Some a ->
@@ -341,6 +322,25 @@ Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
     List.nth_error cs n = Some c -> 
     step_clause s c c' ->
     step_exp s (MatchE ags cs) (MatchE ags (update cs n c'))
+  | se_matche_match : forall s ags qs ags' e prems cs ags'' ags''' qs' sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    let ams' := list_zipWith (fun a a' => MatchA a a') ags'' ags''' in
+    let new_c1 := (qs', ags''', subst_exp sbst e, List.map (subst_prem sbst) prems) in
+    let new_c2 := ([], ags'', MatchE ags (cs), []) in
+    step_argmatch s qs ams sbst qs' ams' ->
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags'' [new_c1; new_c2])
+  | se_matche_fail : forall s ags qs ags' e prems cs sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    step_argmatch s qs ams sbst [] [FailA] ->
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags cs)
+  | se_matche_guess : forall s ags qs ags' e prems cs sbst,
+    (* TODO ok subst *)
+    (* NOTE: non-computational rule *)
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags (([], List.map (subst_arg sbst) ags', e, prems) :: cs))
+  | se_matche_matchtrue : forall s e cs,
+    step_exp s (MatchE [] (([], [], e, []) :: cs)) e
+  | se_matche_matchfalse : forall s e prems cs,
+    step_exp s (MatchE [] (([], [], e, (IfPr (BoolE false)) :: prems) :: cs)) (MatchE [] cs)
 with
 
 step_arg : store -> il_arg -> il_arg -> Prop :=
@@ -361,12 +361,34 @@ step_typ : store -> il_typ -> il_typ -> Prop :=
   | st_var_app : forall s x ags ps insts,
     StringMap.find x (TYPS (store_to_env s)) = Some (ps, insts) ->
     step_typ s (VarT x ags) (MatchT x ags insts)
-  | st_tup_ctx : forall s tups n x t,
+  | st_tup_ctx : forall s tups n x t t',
     List.nth_error tups n = Some (x, t) ->
-    step_typ s (TupT tups) (TupT (update tups n (x, t)))
+    step_typ s t t' ->
+    step_typ s (TupT tups) (TupT (update tups n (x, t')))
   | st_iter_ctx : forall s t t' it,
     step_typ s t t' ->
     step_typ s (IterT t it) (IterT t' it)
+  | st_match_ctx1 : forall s x ags insts n a_n a_n',
+    List.nth_error ags n = Some a_n ->
+    step_arg s a_n a_n' ->
+    step_typ s (MatchT x ags insts) (MatchT x (update ags n a_n') insts)
+  | st_match_ctx2 : forall s x ags insts n inst_n inst_n',
+    List.nth_error insts n = Some inst_n ->
+    step_inst s inst_n inst_n' ->
+    step_typ s (MatchT x ags insts) (MatchT x ags (update insts n inst_n'))
+  | st_match_alias : forall s x t insts,
+    step_typ s (MatchT x [] (([], [], AliasT t) :: insts)) t
+  | st_match_match : forall s x ags ags' ags'' qs qs' ags''' insts dt sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    let ams' := list_zipWith (fun a a' => MatchA a a') ags'' ags''' in
+    let new_dt := AliasT (MatchT x ags insts) in
+    step_argmatch s qs ams sbst qs' ams' ->
+    step_typ s (MatchT x ags ((qs, ags', dt) :: insts)) (MatchT x ags'' [(qs', ags''', subst_deftyp sbst dt); ([], ags'', new_dt)])
+  | st_match_fail : forall s x ags ags' qs insts dt sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    step_argmatch s qs ams sbst [] [FailA] ->
+    step_typ s (MatchT x ags ((qs, ags', dt) :: insts)) (MatchT x ags insts)
+
 
 with
 
@@ -402,12 +424,14 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
   | sp_ctx : forall s p ps p' ps',
     step_prems s [p] p' ->
     step_prems s (p :: ps) (p' ++ ps')
+
   (* IfPr rules *)
   | sp_if_ctx : forall s e e',
     step_exp s e e' ->
     step_prems s [IfPr e] [IfPr e']
   | sp_if_true : forall s,
     step_prems s [IfPr (BoolE true)] []
+
   (* LetPr rules *)
   | sp_let_ctx : forall s e1 e2 e2',
     step_exp s e2 e2' ->
@@ -417,6 +441,7 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     reduce_exp s e2 e2' ->
     e1' = e2' ->
     step_prems s [LetPr e1 e2] []
+
   (* IterPr rules *)
   | sp_iter_ctx1 : forall s p it eps p',
     step_prems s [p] [p'] ->
@@ -460,13 +485,24 @@ step_prems : store -> list il_prem -> list il_prem -> Prop :=
     ) ess') in
     step_prems s [IterPr pr (I_SUP x_i (NumE (NatE n))) res_ess] res_ess'
 
-  (* TODO other iter rules *)
+  (* ElsePr rule *)
+  | sp_else : forall s,
+    step_prems s [ElsePr] [IfPr (BoolE true)]
+
   (* NegPr rules *)
   | sp_neg_ctx : forall s p p',
     step_prems s [p] [p'] ->
     step_prems s [NegPr p] [NegPr p']
   | sp_neg_bool: forall s b,
     step_prems s [NegPr (IfPr (BoolE b))] [IfPr (BoolE (negb b))]
+  
+  (* RelPr rule (Non-computational) *)
+  | sp_rel : forall s x ags e sbst prems e' ps t rules qs,
+    StringMap.find x (RELS (store_to_env s)) = Some (ps, t, rules) ->
+    let rules' := List.map (fun r => subst_rule (args_for_params ags ps) r) rules in
+    List.In (qs, e', prems) rules' ->    
+    (* TODO ok_subst *) 
+    step_prems s [RulePr x ags e] (List.map (subst_prem sbst) prems ++ [IfPr (CmpE (BoolCmpop EqOp) (subst_exp sbst e') e)])
 
 with
 
@@ -533,6 +569,7 @@ step_argmatch_plain : store -> list argmatch -> list argmatch -> Prop :=
     step_argmatch_plain s [MatchA a a'] [MatchA a a'']
   | sagp_eq : forall s a,
     step_argmatch_plain s [MatchA a a] []
+    (* TODO disjointness *)
 
 with
 
@@ -572,8 +609,170 @@ step_expmatch_plain : store -> list expmatch -> list expmatch -> Prop :=
   | semp_case_fail : forall s e e' op op',
     op <> op' ->
     step_expmatch_plain s [MatchEM (CaseE op e) (CaseE op' e')] [MatchEM e e']
-  (* | semp_opt : forall s e e',
-     *)
+  | semp_opt : forall s e e',
+    same_opt e e' ->
+    step_expmatch_plain s [MatchEM (OptE e) (OptE e')] (list_zipWith (fun e1 e2 => MatchEM e1 e2) (opt_to_lst e) (opt_to_lst e'))
+  | semp_opt_fail : forall s e e',
+    negb (same_opt e e') ->
+    step_expmatch_plain s [MatchEM (OptE e) (OptE e')] [FailEM]
+  | semp_list : forall s es es',
+    size es = size es' ->
+    step_expmatch_plain s [MatchEM (ListE es) (ListE es')] (list_zipWith (fun e1 e2 => MatchEM e1 e2) es es')
+  | semp_list_fail : forall s es es',
+    size es <> size es' ->
+    step_expmatch_plain s [MatchEM (ListE es) (ListE es')] [FailEM]
+  | semp_lift : forall s es e,
+    size es <= 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (LiftE e)] [MatchEM (OptE (lst_to_opt es)) e]
+  | semp_lift_fail : forall s es e,
+    size es > 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (LiftE e)] [FailEM]
+  | semp_cat_left : forall s e1s e2s e1s' e2',
+    size e1s = size e1s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE (ListE e1s') e2')] [MatchEM (ListE e1s) (ListE e1s'); MatchEM (ListE e2s) e2']
+  | semp_cat_left_fail : forall s e1s e2s e1s' e2',
+    size e1s <> size e1s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE (ListE e1s') e2')] [FailEM]
+  | semp_cat_right : forall s e1s e2s e1' e2s',
+    size e2s = size e2s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE e1' (ListE e2s'))] [MatchEM (ListE e1s) e1'; MatchEM (ListE e2s) (ListE e2s')]
+  | semp_cat_right_fail : forall s e1s e2s e1' e2s',
+    size e2s <> size e2s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE e1' (ListE e2s'))] [FailEM] 
+  | semp_str : forall s efs efs' es,
+    List.Forall2 (fun '(l, e) '(l', e') => l = l' /\ List.In (l, e) efs) es efs' ->
+    step_expmatch_plain s [MatchEM (StrE efs) (StrE efs')] (list_zipWith (fun ef ef' => MatchEM (exp_from_field ef) (exp_from_field ef')) es efs')
+  | semp_iter_plus : forall s es e' eps,
+    size es >= 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [MatchEM (ListE es) (IterE e' I_STAR eps)]
+  | semp_iter_plus_fail : forall s es e' eps,
+    es = [] ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [FailEM]
+  | semp_iter_star : forall s es e' eps y n,
+    size es = n ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [MatchEM (ListE es) (IterE e' (I_SUP y (NumE (NatE n))) eps)]
+    (* TODO y fresh *)
+  | semp_sub_sub : forall s e t1 t2 e' t1' t2',
+    sub_typ (store_to_env s) t1 t1' ->
+    step_expmatch_plain s [MatchEM (SubE e t1 t2) (SubE e' t1' t2')] [MatchEM (SubE e t1 t1') e']
+    (* TODO disjointness *)
+  | semp_sub_tup : forall s es e' typs typs',
+    size es = size typs ->
+    size typs = size typs' ->
+    let sbst1 := many_svars (list_mapi (fun i '(e, (x, _)) => (x, ProjE e i)) (zip es typs)) in
+    let sbst2 := many_svars (list_mapi (fun i '(e, (x, _)) => (x, ProjE e i)) (zip es typs')) in
+    let tups := List.map (fun '((_, t1), (_, t2)) => SubE e' (subst_typ sbst1 t1) (subst_typ sbst2 t2)) (zip typs typs') in
+    step_expmatch_plain s [MatchEM (TupE es) (SubE e' (TupT typs) (TupT typs'))] 
+    [MatchEM (TupE tups) e']
+
+with
+
+step_argmatch : store -> list il_quant -> list argmatch -> il_subst -> list il_quant -> list argmatch -> Prop :=
+  | sam_plain : forall s qs ams ams',
+    step_argmatch_plain s ams ams' ->
+    step_argmatch s qs ams subst_empty qs ams'
+  | sam_seq : forall s q1s qs qs' q2s am1s am am2s ams' sbst,
+    step_argmatch s qs [am] sbst qs' ams' ->
+    let new_q2s :=  List.map (subst_quant sbst) q2s in
+    let new_am2s := List.map (subst_argmatch sbst) am2s in
+    step_argmatch s (q1s ++ qs ++ q2s) (am1s ++ [am] ++ am2s) sbst (q1s ++ qs' ++ new_q2s) (am1s ++ ams' ++ new_am2s)
+  | sam_seq_fail : forall s q1s qs q2s am1s am am2s sbst,
+    step_argmatch s qs [am] sbst [] [FailA] ->
+    step_argmatch s (q1s ++ qs ++ q2s) (am1s ++ [am] ++ am2s) sbst [] [FailA]
+  | sam_typ : forall s x t,
+    let sbst := subst_styp x t in
+    step_argmatch s [TypP x] [MatchA (TypA t) (TypA (VarT x []))] sbst [] []
+  | sam_exp : forall s x t e,
+    let sbst := subst_svar x e in
+    step_argmatch s [ExpP x t] [MatchA (ExpA e) (ExpA (VarE x))] sbst [] []
+  | sam_fun : forall s x ps t y,
+    let sbst := subst_sfun x y in
+    step_argmatch s [DefP x ps t] [MatchA (DefA y) (DefA x)] sbst [] []
+  | sam_exp_exp : forall s qs qs' em ems' sbst,
+    step_expmatch s qs [em] sbst qs' ems' ->
+    step_argmatch s qs [to_argmatch em] sbst qs' (List.map to_argmatch ems')
+  | sam_exp_exp_fail : forall s qs em sbst,
+    step_expmatch s qs [em] sbst [] [FailEM] ->
+    step_argmatch s qs [to_argmatch em] sbst [] [FailA]
+
+with
+
+step_expmatch : store -> list il_quant -> list expmatch -> il_subst -> list il_quant -> list expmatch -> Prop :=
+  | sem_plain : forall s qs ems ems',
+    step_expmatch_plain s ems ems' ->
+    step_expmatch s qs ems subst_empty qs ems'
+  | sem_seq : forall s q1s qs qs' q2s em1s em em2s ems' sbst,
+    step_expmatch s qs [em] sbst qs' ems' ->
+    let new_q2s :=  List.map (subst_quant sbst) q2s in
+    let new_em2s := List.map (subst_expmatch sbst) em2s in
+    step_expmatch s (q1s ++ qs ++ q2s) (em1s ++ [em] ++ em2s) sbst (q1s ++ qs' ++ new_q2s) (em1s ++ ems' ++ new_em2s)
+  | sem_seq_fail : forall s q1s qs q2s em1s em em2s sbst,
+    step_expmatch s qs [em] sbst [] [FailEM] ->
+    step_expmatch s (q1s ++ qs ++ q2s) (em1s ++ [em] ++ em2s) sbst [] [FailEM]
+  | sem_iter_sup : forall s qs es e' y e_n eps n (xss : list (list il_id)),
+    size es = n ->
+    seq.all (fun xs => size xs == size es) xss ->
+    let xss' := transpose xss in
+    let qs' := List.concat (List.map (fun xs => list_zipWith (fun '(_, t, _) x => ExpP x t) eps xs) xss) in
+    let ems := list_mapi (fun i '(xs, e) => 
+      let sup_sbst := subst_svar y (NumE (NatE i)) in 
+      let sbst := many_svars (List.map (fun '((x, _, _), x') => (x, VarE x')) (zip eps xs)) in
+      MatchEM e (subst_exp (append_subst sup_sbst sbst) e') 
+    ) (zip xss es) in
+    let num_match := [MatchEM (NumE (NatE n)) e_n] in
+    let list_match := list_zipWith (fun xs' '(_, _, ep) => MatchEM (ListE (List.map VarE xs')) ep) xss' eps in
+    step_expmatch s qs [MatchEM (ListE es) (IterE e' (I_SUP y e_n) eps)] subst_empty (qs' ++ qs) (ems ++ num_match ++ list_match)
+  | sem_iter_opt : forall s qs e e' eps (xss : option (list il_id)),
+    let xss' := transpose_opt xss in
+    let qs' := List.concat (List.map (fun xs => list_zipWith (fun '(_, t, _) x => ExpP x t) eps xs) (opt_to_lst xss)) in
+    let ems := list_zipWith (fun xs e => 
+      let sbst := many_svars (List.map (fun '((x, _, _), x') => (x, VarE x')) (zip eps xs)) in
+      MatchEM e (subst_exp sbst e') 
+    ) (opt_to_lst xss) (opt_to_lst e) in
+    let opt_match := list_zipWith (fun xs' '(_, _, ep) => MatchEM (OptE (option_map VarE xs')) ep) xss' eps in
+    step_expmatch s qs [MatchEM (OptE e) (IterE e' I_OPT eps)] subst_empty (qs' ++ qs) (ems ++ opt_match)
+
+with
+
+sub_typ : il_env -> il_typ -> il_typ -> Prop :=
+  | st_tup : forall env x1 t1 x2 t2 tups tups',
+    let env' := (single_var x1 t1) in
+    let sbst := (subst_svar x2 (VarE x1)) in
+    sub_typ env t1 t2 ->
+    sub_typ (env @@ env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
+    sub_typ env (TupT ((x1, t1) :: tups)) (TupT ((x2, t2) :: tups'))
+  | st_struct : forall env t1 t2 tfs1 tfs2,
+    expand_typ (env_to_store env) t1 (StructT tfs1) ->
+    expand_typ (env_to_store env) t2 (StructT tfs2) -> 
+    sub_typ env t1 t2
+  | st_iter : forall env t1 t2 it,
+    sub_typ env t1 t2 ->
+    sub_typ env (IterT t1 it) (IterT t2 it) 
+  | st_refl : forall env t, sub_typ env t t
+  | st_trans : forall env t1 t2 t',
+    sub_typ env t1 t' ->
+    sub_typ env t' t2 ->
+    sub_typ env t1 t2
+
+with
+
+expand_typ : store -> il_typ -> il_deftyp -> Prop :=
+  | et_plain : forall s t t',
+    is_plaintyp t ->
+    reduce_typ s t t' ->
+    expand_typ s t (AliasT t)
+  | et_def : forall s t dt x insts,
+    reduce_typ s t (MatchT x [] (([], [], dt) :: insts)) -> 
+    expand_typ s t dt
+
+with
+
+reduce_typ : store -> il_typ -> il_typ -> Prop :=
+  | rt_refl : forall s t, reduce_typ s t t
+  | rt_step : forall s t1 t2 t3,
+    step_typ s t1 t2 ->
+    reduce_typ s t2 t3 ->
+    reduce_typ s t1 t3
 .
 
 Inductive reduce_arg : store -> il_arg -> il_arg -> Prop :=
@@ -584,14 +783,6 @@ Inductive reduce_arg : store -> il_arg -> il_arg -> Prop :=
     reduce_arg s a1 a3
 .
 
-Inductive reduce_typ : store -> il_typ -> il_typ -> Prop :=
-  | rt_refl : forall s t, reduce_typ s t t
-  | rt_step : forall s t1 t2 t3,
-    step_typ s t1 t2 ->
-    reduce_typ s t2 t3 ->
-    reduce_typ s t1 t3
-.
-
 Inductive eq_typ : store -> il_typ -> il_typ -> Prop :=
   | eq_typ_rule : forall s t1 t2 t1' t2',
     reduce_typ s t1 t1' ->
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
index 7e25bccf5c..38d703a476 100644
--- a/spectec/metatheory/theories/subst.v
+++ b/spectec/metatheory/theories/subst.v
@@ -269,6 +269,12 @@ Definition subst_expmatch (s : il_subst) (e : expmatch) : expmatch :=
   end
 .
 
+Definition subst_rule (s : il_subst) (r : il_rule) : il_rule :=
+  match r with
+  | (qs, exp, prems) => (List.map (subst_param s) qs, subst_exp s exp, List.map (subst_prem s) prems)
+  end
+.
+
 (* TODO *)
 Inductive ok_subst : il_env -> il_subst -> list il_quant -> Prop := 
   | Subst_OK : forall E s q_lst,
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
index 0a30102a21..55d7abc0d8 100644
--- a/spectec/metatheory/theories/syntax.v
+++ b/spectec/metatheory/theories/syntax.v
@@ -190,6 +190,8 @@ Definition il_quant : Type := il_param.
 Definition typfield : Type := atom * list il_quant * il_typ * list il_prem.
 Definition typcase : Type := mixop * list il_quant * il_typ * list il_prem.
 
+Definition expfield : Type := atom * il_exp.
+
 Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
 Definition il_rule : Type := list il_quant * il_exp * list il_prem.
 Definition il_clause : Type := list il_quant * list il_arg * il_exp * list il_prem.
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
index 84a71f4b4b..af3d0bb75f 100644
--- a/spectec/metatheory/theories/typing.v
+++ b/spectec/metatheory/theories/typing.v
@@ -25,27 +25,6 @@ Inductive sub_numtyp : numtyp -> numtyp -> Prop :=
     sub_numtyp nt1 nt2
 .
 
-Inductive sub_typ : il_env -> il_typ -> il_typ -> Prop :=
-  | st_tup : forall env x1 t1 x2 t2 tups tups',
-    let env' := (single_var x1 t1) in
-    let sbst := (subst_svar x2 (VarE x1)) in
-    sub_typ env t1 t2 ->
-    sub_typ (env @@ env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
-    sub_typ env (TupT ((x1, t1) :: tups)) (TupT ((x2, t2) :: tups'))
-  | st_struct : forall env t1 t2 tfs1 tfs2,
-    expand_typ (env_to_store env) t1 (StructT tfs1) ->
-    expand_typ (env_to_store env) t2 (StructT tfs2) -> 
-    sub_typ env t1 t2
-  | st_iter : forall env t1 t2 it,
-    sub_typ env t1 t2 ->
-    sub_typ env (IterT t1 it) (IterT t2 it) 
-  | st_refl : forall env t, sub_typ env t t
-  | st_trans : forall env t1 t2 t',
-    sub_typ env t1 t' ->
-    sub_typ env t' t2 ->
-    sub_typ env t1 t2
-.
-
 Inductive sub_param : il_env -> il_param -> il_param -> il_subst -> Prop :=
   | sp_exp : forall env x1 t1 x2 t2,
     sub_typ env t1 t2 ->
@@ -68,6 +47,7 @@ sub_params : il_env -> list il_param -> list il_param -> il_subst -> Prop :=
     sub_params env (p1 :: p1s) (p2 :: p2s) (append_subst sbst sbst')
 .
 
+
 Inductive ok_numunop : numunop -> numtyp -> numtyp -> Prop :=
   | ok_unop_sign : forall numop nt,
     sub_numtyp IntT nt ->
diff --git a/spectec/metatheory/theories/utils.v b/spectec/metatheory/theories/utils.v
index 6073dd564d..5e4be81264 100644
--- a/spectec/metatheory/theories/utils.v
+++ b/spectec/metatheory/theories/utils.v
@@ -102,6 +102,27 @@ Definition transpose {X : Type} (xss : list (list X)) : list (list X) :=
   end
 .
 
+Definition transpose_opt {X : Type} (xss : option (list X)) : list (option X) :=
+  match xss with
+  | None => []
+  | Some xss' => List.map (fun x => Some x) xss'
+  end
+.
+
+Definition is_expmatch (x : argmatch) : bool :=
+  match x with
+  | MatchA (ExpA _) (ExpA _) => true
+  | _ => false
+  end
+.
+
+Definition to_argmatch (x : expmatch) : argmatch :=
+  match x with
+  | FailEM => FailA
+  | MatchEM e e' => MatchA (ExpA e) (ExpA e')
+  end
+.
+
 Definition list_mapi {X Y : Type} (f : nat -> X -> Y) (xs : list X) : list Y :=
   let idxs := iota 0 (size xs) in
   List.map (fun '(i, x) => f i x) (zip idxs xs)
@@ -110,10 +131,12 @@ Definition list_mapi {X Y : Type} (f : nat -> X -> Y) (xs : list X) : list Y :=
 Inductive List_Forall3 {A B C: Type} (R : A -> B -> C -> Prop): seq A -> seq B -> seq C -> Prop :=
 	| Forall3_nil : List_Forall3 R nil nil nil
 	| Forall3_cons : forall x y z l l' l'',
-		R x y z -> List_Forall3 R l l' l'' -> List_Forall3 R (x :: l) (y :: l') (z :: l'').
+		R x y z -> List_Forall3 R l l' l'' -> List_Forall3 R (x :: l) (y :: l') (z :: l'')
+.
 
 Definition list_map3 {A B C D: Type} (f : A -> B -> C -> D) (xs : seq A) (ys : seq B) (zs : seq C) : seq D :=
-	seq.map (fun '(x, (y, z)) => f x y z) (seq.zip xs (seq.zip ys zs)).
+	seq.map (fun '(x, (y, z)) => f x y z) (seq.zip xs (seq.zip ys zs))
+.
 
 Definition atomtyp (x : typfield) : atom * il_typ :=
   match x with
@@ -122,7 +145,14 @@ Definition atomtyp (x : typfield) : atom * il_typ :=
 .
 
 Definition atomtyps (xs : list typfield) : list (atom * il_typ) :=
-  List.map atomtyp xs.
+  List.map atomtyp xs
+.
+
+Definition exp_from_field (x : expfield) : il_exp :=
+  match x with
+  | (a, e) => e
+  end
+.
 
 (* Decidable equality axiom *)