Add geolog examples to the project

examples/geolog/README.md

@@ -0,0 +1,470 @@
+# Geolog DSL Structure
+
+This directory contains example `.geolog` files that use a richer DSL than the
+minimal `.chase` script language in `examples/scripts/`.
+
+This README summarizes the Geolog DSL structure as it appears in the examples in
+this directory. It should be read as a practical, example-driven reference, not
+as a formal or complete language specification.
+
+## At a Glance
+
+- Top-level declarations are `theory` and `instance`.
+- The main kind of type is `Sort`.
+- Symbols can denote sorts, constants, functions, predicates, or nested
+  instances.
+- Axioms use sequent-style syntax: `premise |- conclusion`.
+- Instance bodies can be plain literals (`= { ... }`) or chase blocks
+  (`= chase { ... }`).
+- Function application is postfix, and qualified names use `/`.
+
+## Informal File Shape
+
+```text
+file := { comment | theory_decl | instance_decl }
+
+comment := // ...
+
+theory_decl :=
+  theory theory_params? Name {
+    theory_item*
+  }
+
+instance_decl :=
+  instance Name : theory_app = {
+    instance_item*
+  }
+
+  | instance Name : theory_app = chase {
+      instance_item*
+    }
+```
+
+In practice, a file is usually a sequence of theory declarations followed by one
+or more example instances.
+
+## Top-Level Declarations
+
+### `theory`
+
+A theory introduces sorts, symbols, and axioms.
+
+```text
+theory Graph {
+  V : Sort;
+  Edge : [src: V, tgt: V] -> Prop;
+}
+```
+
+Theories may also be parameterized.
+
+```text
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+}
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+```
+
+Observed parameter forms:
+
+- sort parameters: `(X : Sort)`
+- instance parameters: `(N : PetriNet instance)`
+- dependent instance parameters: `(RP : N ReachabilityProblem instance)`
+
+### `instance`
+
+An instance provides concrete elements and assignments for a theory.
+
+```text
+instance Triangle : Graph = {
+  A : V;
+  B : V;
+  C : V;
+}
+```
+
+Instances may target parameterized theories by writing the arguments before the
+theory name.
+
+```text
+instance MyMap : MyBase Map = { ... }
+instance solution0 : ExampleNet problem0 Solution = { ... }
+instance AB_Iso : As/a Bs/b Iso = { ... }
+```
+
+## Theory Body Items
+
+The examples show the following declaration forms inside a theory body.
+
+### Sort declarations
+
+```text
+V : Sort;
+E : Sort;
+```
+
+This introduces carrier sorts.
+
+### Constants or distinguished elements
+
+```text
+elem : X;
+```
+
+This introduces a named element of an existing sort.
+
+### Functions
+
+```text
+src : E -> V;
+fwd : X -> Y;
+token/of : token -> N/P;
+```
+
+Names may contain `/`, which is used heavily for structured or qualified names.
+
+### Predicates and relations
+
+Unary predicates:
+
+```text
+completed : Item -> Prop;
+```
+
+Record-shaped predicates:
+
+```text
+Edge : [src: V, tgt: V] -> Prop;
+depends : [item: Item, on: Item] -> Prop;
+```
+
+### Product-valued functions
+
+Functions may return record-shaped values.
+
+```text
+pair_of : A -> [left: B, right: C];
+W/src : W -> [firing: F, arc: N/out];
+```
+
+### Nested instance slots
+
+Theories can contain fields whose values are themselves instances.
+
+```text
+initial_marking : N Marking instance;
+trace : N Trace instance;
+initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+```
+
+### Axioms
+
+Axioms use a sequent-like form.
+
+```text
+ax/trans : forall x, y, z : V.
+  [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path;
+```
+
+An axiom declaration has the observed structure:
+
+```text
+name : forall binders. premise |- conclusion;
+```
+
+## Formula and Term Syntax
+
+The examples use the following building blocks inside axioms and assignments.
+
+### Quantifiers
+
+Universal binders appear after `forall`.
+
+```text
+forall x : X, y : Y.
+```
+
+Existentials appear directly inside conclusions or disjuncts.
+
+```text
+exists r : R. r R/data = [x: a, y: b]
+exists w : W. w W/src_firing = f, w W/src_arc = arc
+```
+
+### Sequents
+
+The central connective is `|-`, separating premise from conclusion.
+
+```text
+premise1, premise2 |- conclusion1, conclusion2;
+```
+
+In the examples:
+
+- commas act as conjunctions
+- the left side is the premise
+- the right side is the conclusion
+
+### Equality
+
+Equality is used for ordinary values and compound values.
+
+```text
+ab src = A
+r R/data = [x: a, y: b]
+x fwd bwd = x
+```
+
+### Truth constants
+
+```text
+|- true;
+|- false;
+```
+
+### Disjunction
+
+Disjunction is written as `\/`.
+
+```text
+[item: x, on: y] depends |- x blocked \/ y completed;
+```
+
+### Predicate atoms
+
+Unary predicate atoms:
+
+```text
+x blocked
+y completed
+```
+
+Record-shaped predicate atoms:
+
+```text
+[src: x, tgt: y] Edge
+[a: x, f: i] id
+```
+
+### Postfix application
+
+Function application is postfix and can be chained.
+
+```text
+e src
+x id
+x fwd bwd
+w W/src_arc N/out/tgt
+```
+
+This is one of the most distinctive traits of the DSL.
+
+### Qualified paths
+
+The slash `/` is used for qualification and nested access.
+
+Observed examples include:
+
+```text
+R/data
+N/P
+N/out/src
+trace/input_terminal
+RP/initial_marking/token
+ExampleNet/A
+```
+
+### Record literals
+
+Records are written with brackets and named fields.
+
+```text
+[x: a, y: b]
+[firing: f, arc: arc]
+```
+
+The examples also show positional shorthand for record arguments when the field
+order is known:
+
+```text
+[e, e] mul = e;
+[cook_dinner, on: buy_groceries] depends;
+```
+
+### Field projection
+
+Record-valued terms support field projection.
+
+```text
+r R/data .x = a
+```
+
+## Instance Body Items
+
+The examples show the following forms inside instance bodies.
+
+### Element declarations
+
+```text
+a : V;
+tok : token;
+ab : T;
+```
+
+### Function assignments
+
+```text
+ab src = A;
+tok token/of = ExampleNet/A;
+a1 map = MyBase/b1;
+```
+
+### Predicate facts
+
+Unary facts:
+
+```text
+buy_groceries completed;
+```
+
+Record-shaped facts:
+
+```text
+[src: a, tgt: b] Edge;
+[item: x, on: y] depends;
+```
+
+### Product-valued assignments
+
+```text
+a1 pair_of = [left: b1, right: c1];
+ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+```
+
+### Nested instance literals
+
+Instance-valued fields can be assigned inline blocks.
+
+```text
+initial_marking = {
+  tok : token;
+  tok token/of = ExampleNet/A;
+};
+```
+
+## `= { ... }` vs `= chase { ... }`
+
+The examples consistently use two instance forms.
+
+### Plain instance
+
+```text
+instance Triangle : Graph = {
+  ...
+}
+```
+
+This gives a direct structure with only the explicitly listed elements and
+assignments.
+
+### Chase instance
+
+```text
+instance Chain : Graph = chase {
+  ...
+}
+```
+
+This marks an instance whose contents should be extended by the theory axioms.
+Examples use this for transitive closure, existential witness generation, and
+trace/reachability constructions.
+
+## Observed Design Patterns
+
+### Parameterized theories
+
+Theories can be abstract over:
+
+- a sort, such as `theory (X : Sort) Container`
+- an instance, such as `theory (N : PetriNet instance) Marking`
+- multiple arguments, such as `theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution`
+
+### Theory application by adjacency
+
+Theory arguments are written before the theory name.
+
+```text
+N Marking instance
+MyBase Map
+ExampleNet problem0 Solution
+```
+
+### Nested structure via qualified names
+
+Many examples model dependent structure by naming into earlier declarations.
+
+```text
+token/of : token -> N/P;
+initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+```
+
+## What Seems Outside the File DSL
+
+Some example comments refer to interactive commands such as:
+
+```text
+:source
+:load
+:inspect
+:chase
+:solve
+```
+
+Those commands appear to belong to an external REPL or tool environment rather
+than to the `.geolog` file grammar itself.
+
+## Best Example Files by Feature
+
+- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage
+- `graph.geolog`: plain structural instances
+- `monoid.geolog`: postfix application and positional record syntax
+- `todo_list.geolog`: unary predicates and disjunction
+- `sort_param_simple.geolog`: sort and instance parameters
+- `nested_instance_test.geolog`: nested instance-valued fields
+- `product_codomain_test.geolog`: record-valued function codomains
+- `field_projection_test.geolog`: field projection syntax
+- `record_existential_test.geolog`: existential witness creation with records
+- `petri_net_showcase.geolog`: large multi-theory composition
+- `solver_demo.geolog`: satisfiability-oriented axiom patterns
+
+## Minimal Example
+
+```text
+theory Graph {
+  V : Sort;
+  Edge : [src: V, tgt: V] -> Prop;
+  Path : [src: V, tgt: V] -> Prop;
+
+  ax/base : forall x, y : V.
+    [src: x, tgt: y] Edge |- [src: x, tgt: y] Path;
+}
+
+instance Chain : Graph = chase {
+  a : V;
+  b : V;
+  [src: a, tgt: b] Edge;
+}
+```
+
+That small example already shows the core structure of the DSL:
+
+- a `theory`
+- sort and predicate declarations
+- an axiom written as a sequent
+- an `instance`
+- a `chase` block that asks for closure under the theory axioms

examples/geolog/category.geolog

@@ -0,0 +1,86 @@
+// Category theory in current geolog syntax
+//
+// This is the "desugared" version of the aspirational syntax in
+// loose_thoughts/2026-01-21_dependent_sorts_and_functional_relations.md
+
+theory Category {
+  ob : Sort;
+  mor : Sort;
+
+  // Morphism source and target
+  src : mor -> ob;
+  tgt : mor -> ob;
+
+  // Composition: comp(f, g, h) means "h = f ; g" (f then g)
+  // Domain constraint: f.tgt = g.src
+  comp : [f: mor, g: mor, h: mor] -> Prop;
+
+  // Identity: id(a, f) means "f is the identity on a"
+  id : [a: ob, f: mor] -> Prop;
+
+  // === Axioms ===
+
+  // Identity morphisms have matching source and target
+  ax/id_src : forall x : ob, i : mor. [a: x, f: i] id |- i src = x;
+  ax/id_tgt : forall x : ob, i : mor. [a: x, f: i] id |- i tgt = x;
+
+  // Composition domain constraint
+  ax/comp_dom : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- p tgt = q src;
+
+  // Composition source/target
+  ax/comp_src : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- r src = p src;
+  ax/comp_tgt : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- r tgt = q tgt;
+
+  // Existence of identities (one per object)
+  ax/id_exists : forall x : ob. |- exists i : mor. [a: x, f: i] id;
+
+  // Existence of composites (when composable)
+  ax/comp_exists : forall p : mor, q : mor.
+    p tgt = q src |- exists r : mor. [f: p, g: q, h: r] comp;
+
+  // Left unit: id_a ; f = f
+  ax/unit_left : forall x : ob, i : mor, p : mor, r : mor.
+    [a: x, f: i] id, p src = x, [f: i, g: p, h: r] comp |- r = p;
+
+  // Right unit: f ; id_b = f
+  ax/unit_right : forall y : ob, i : mor, p : mor, r : mor.
+    [a: y, f: i] id, p tgt = y, [f: p, g: i, h: r] comp |- r = p;
+
+  // Associativity: (f ; g) ; h = f ; (g ; h)
+  ax/assoc : forall p : mor, q : mor, r : mor, pq : mor, qr : mor, pqr1 : mor, pqr2 : mor.
+    [f: p, g: q, h: pq] comp, [f: pq, g: r, h: pqr1] comp,
+    [f: q, g: r, h: qr] comp, [f: p, g: qr, h: pqr2] comp
+    |- pqr1 = pqr2;
+
+  // Uniqueness of composition (functional)
+  ax/comp_unique : forall p : mor, q : mor, r1 : mor, r2 : mor.
+    [f: p, g: q, h: r1] comp, [f: p, g: q, h: r2] comp |- r1 = r2;
+
+  // Uniqueness of identity (one per object)
+  ax/id_unique : forall x : ob, i1 : mor, i2 : mor.
+    [a: x, f: i1] id, [a: x, f: i2] id |- i1 = i2;
+}
+
+// The "walking arrow" category: A --f--> B
+//
+// Now we can declare just objects and non-identity morphisms!
+// The chase derives:
+// - Identity morphisms for each object (via ax/id_exists)
+// - Composition facts (via ax/comp_exists)
+// - Source/target for compositions (via ax/comp_src, ax/comp_tgt)
+//
+// The equality saturation (via congruence closure) collapses:
+// - id;id;id;... = id (via ax/unit_left and ax/unit_right)
+// - Duplicate compositions (via ax/comp_unique)
+// Without CC, the chase would loop forever creating id;id, id;id;id, ...
+instance Arrow : Category = chase {
+  // Objects
+  A : ob;
+  B : ob;
+
+  // Non-identity morphism
+  f : mor; f src = A; f tgt = B;
+}

examples/geolog/field_projection_chase_test.geolog

@@ -0,0 +1,27 @@
+// Test: Field projection in chase
+
+theory FieldProjectionChaseTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Marker sort for elements whose x field matches a given a
+  XMatches : Sort;
+  XMatches/r : XMatches -> R;
+  XMatches/a : XMatches -> A;
+
+  // Axiom: if r's x field equals a, create an XMatches
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists m : XMatches. m XMatches/r = r, m XMatches/a = a;
+}
+
+instance Test : FieldProjectionChaseTest = chase {
+  a1 : A;
+  a2 : A;
+  b1 : B;
+  r1 : R;
+  r1 R/data = [x: a1, y: b1];
+  r2 : R;
+  r2 R/data = [x: a2, y: b1];
+}

examples/geolog/field_projection_test.geolog

@@ -0,0 +1,12 @@
+// Test: Field projection syntax
+
+theory FieldProjectionTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Axiom using field projection: r R/data .x
+  ax1 : forall r : R, a : A. r R/data .x = a |- true;
+}

examples/geolog/graph.geolog

@@ -0,0 +1,79 @@
+// Directed Graph: vertices and edges with source/target functions
+//
+// This is the canonical example of a "presheaf" - a functor from a small
+// category (the "walking arrow" • → •) to Set.
+
+theory Graph {
+  V : Sort;  // Vertices
+  E : Sort;  // Edges
+
+  src : E -> V;  // Source of an edge
+  tgt : E -> V;  // Target of an edge
+}
+
+// A simple triangle graph: A → B → C → A
+instance Triangle : Graph = {
+  // Vertices
+  A : V;
+  B : V;
+  C : V;
+
+  // Edges
+  ab : E;
+  bc : E;
+  ca : E;
+
+  // Edge endpoints
+  ab src = A;
+  ab tgt = B;
+  bc src = B;
+  bc tgt = C;
+  ca src = C;
+  ca tgt = A;
+}
+
+// A self-loop: one vertex with an edge to itself
+instance Loop : Graph = {
+  v : V;
+  e : E;
+  e src = v;
+  e tgt = v;
+}
+
+// The "walking arrow": two vertices, one edge
+instance Arrow : Graph = {
+  s : V;
+  t : V;
+  f : E;
+  f src = s;
+  f tgt = t;
+}
+
+// A more complex graph: diamond shape with two paths from top to bottom
+//
+//       top
+//      /   \
+//    left  right
+//      \   /
+//      bottom
+//
+instance Diamond : Graph = {
+  top : V;
+  left : V;
+  right : V;
+  bottom : V;
+
+  top_left : E;
+  top_right : E;
+  left_bottom : E;
+  right_bottom : E;
+
+  top_left src = top;
+  top_left tgt = left;
+  top_right src = top;
+  top_right tgt = right;
+  left_bottom src = left;
+  left_bottom tgt = bottom;
+  right_bottom src = right;
+  right_bottom tgt = bottom;
+}

examples/geolog/iso_instance_test.geolog

@@ -0,0 +1,29 @@
+// Multi-parameter theory instantiation test
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+theory A { a : Sort; }
+theory B { b : Sort; }
+
+instance As : A = {
+  a1 : a;
+  a2 : a;
+}
+
+instance Bs : B = {
+  b1 : b;
+  b2 : b;
+}
+
+// Can we create an Iso instance with sort parameters?
+instance AB_Iso : As/a Bs/b Iso = {
+  a1 fwd = Bs/b1;
+  a2 fwd = Bs/b2;
+  b1 bwd = As/a1;
+  b2 bwd = As/a2;
+}

examples/geolog/iso_theory_test.geolog

@@ -0,0 +1,9 @@
+// Multi-parameter theory test (Iso from vision)
+
+// First just try sorts as parameters
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  // Axioms would need chained function application...
+  // fb : forall x : X. |- x fwd bwd = x;
+}

examples/geolog/monoid.geolog

@@ -0,0 +1,78 @@
+// Monoid: a set with an associative binary operation and identity element
+//
+// This is the simplest algebraic structure with interesting axioms.
+// Note: geolog uses postfix function application.
+
+theory Monoid {
+  M : Sort;
+
+  // Binary operation: M × M → M
+  mul : [x: M, y: M] -> M;
+
+  // Identity element: we use a unary function from M to M that
+  // "picks out" the identity (any x maps to e)
+  // A cleaner approach would use Unit → M but that needs product support.
+  id : M -> M;
+
+  // Left identity: id(x) * y = y (id(x) is always e)
+  ax/left_id : forall x : M, y : M.
+    |- [x: x id, y: y] mul = y;
+
+  // Right identity: x * id(y) = x
+  ax/right_id : forall x : M, y : M.
+    |- [x: x, y: y id] mul = x;
+
+  // Associativity: (x * y) * z = x * (y * z)
+  ax/assoc : forall x : M, y : M, z : M.
+    |- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul;
+
+  // id is constant: id(x) = id(y) for all x, y
+  ax/id_const : forall x : M, y : M.
+    |- x id = y id;
+}
+
+// Trivial monoid: single element, e * e = e
+instance Trivial : Monoid = {
+  e : M;
+
+  // Multiplication table: e * e = e
+  // Using positional syntax: [a, b] maps to [x: a, y: b]
+  [e, e] mul = e;
+
+  // Identity: e is the identity element
+  e id = e;
+}
+
+// Boolean "And" monoid: {T, F} with T as identity
+// T and T = T, T and F = F, F and T = F, F and F = F
+instance BoolAnd : Monoid = {
+  T : M;
+  F : M;
+
+  // Identity: T is the identity element
+  T id = T;
+  F id = T;
+
+  // Multiplication table for "and":
+  [x: T, y: T] mul = T;
+  [x: T, y: F] mul = F;
+  [x: F, y: T] mul = F;
+  [x: F, y: F] mul = F;
+}
+
+// Boolean "Or" monoid: {T, F} with F as identity
+// T or T = T, T or F = T, F or T = T, F or F = F
+instance BoolOr : Monoid = {
+  T : M;
+  F : M;
+
+  // Identity: F is the identity element
+  T id = F;
+  F id = F;
+
+  // Multiplication table for "or":
+  [x: T, y: T] mul = T;
+  [x: T, y: F] mul = T;
+  [x: F, y: T] mul = T;
+  [x: F, y: F] mul = F;
+}

examples/geolog/nested_instance_test.geolog

@@ -0,0 +1,33 @@
+// Test: Nested instance declarations (following vision pattern)
+
+theory Place {
+  P : Sort;
+}
+
+theory (Pl : Place instance) Token {
+  token : Sort;
+  token/of : token -> Pl/P;
+}
+
+theory (Pl : Place instance) Problem {
+  initial_marking : Pl Token instance;
+  target_marking : Pl Token instance;
+}
+
+// Create a place instance
+instance MyPlaces : Place = {
+  p1 : P;
+  p2 : P;
+}
+
+// Test nested instance declarations
+instance TestProblem : MyPlaces Problem = {
+  initial_marking = {
+    t1 : token;
+    t1 token/of = MyPlaces/p1;
+  };
+  target_marking = {
+    t2 : token;
+    t2 token/of = MyPlaces/p2;
+  };
+}

examples/geolog/petri_net.geolog

@@ -0,0 +1,135 @@
+// Petri Net: a bipartite graph between places and transitions
+//
+// Petri nets model concurrent systems. Places hold tokens, transitions
+// fire when their input places have tokens, consuming inputs and
+// producing outputs.
+//
+// This encoding uses explicit "arc" sorts for input/output connections,
+// which is more faithful to the categorical semantics (a span).
+
+theory PetriNet {
+  P : Sort;    // Places
+  T : Sort;    // Transitions
+  In : Sort;   // Input arcs (from place to transition)
+  Out : Sort;  // Output arcs (from transition to place)
+
+  // Input arc endpoints
+  in/place : In -> P;
+  in/trans : In -> T;
+
+  // Output arc endpoints
+  out/trans : Out -> T;
+  out/place : Out -> P;
+}
+
+// A simple producer-consumer net:
+//
+//   (ready) --[produce]--> (buffer) --[consume]--> (done)
+//
+instance ProducerConsumer : PetriNet = {
+  // Places
+  ready : P;
+  buffer : P;
+  done : P;
+
+  // Transitions
+  produce : T;
+  consume : T;
+
+  // Input arcs
+  i1 : In;
+  i1 in/place = ready;
+  i1 in/trans = produce;
+
+  i2 : In;
+  i2 in/place = buffer;
+  i2 in/trans = consume;
+
+  // Output arcs
+  o1 : Out;
+  o1 out/trans = produce;
+  o1 out/place = buffer;
+
+  o2 : Out;
+  o2 out/trans = consume;
+  o2 out/place = done;
+}
+
+// Mutual exclusion: two processes competing for a shared resource
+//
+//   (idle1) --[enter1]--> (crit1) --[exit1]--> (idle1)
+//                 ^                    |
+//                 |      (mutex)       |
+//                 |                    v
+//   (idle2) --[enter2]--> (crit2) --[exit2]--> (idle2)
+//
+instance MutualExclusion : PetriNet = {
+  // Places for process 1
+  idle1 : P;
+  crit1 : P;
+
+  // Places for process 2
+  idle2 : P;
+  crit2 : P;
+
+  // Shared mutex token
+  mutex : P;
+
+  // Transitions
+  enter1 : T;
+  exit1 : T;
+  enter2 : T;
+  exit2 : T;
+
+  // Process 1 enters: needs idle1 AND mutex
+  i_enter1_idle : In;
+  i_enter1_idle in/place = idle1;
+  i_enter1_idle in/trans = enter1;
+
+  i_enter1_mutex : In;
+  i_enter1_mutex in/place = mutex;
+  i_enter1_mutex in/trans = enter1;
+
+  o_enter1 : Out;
+  o_enter1 out/trans = enter1;
+  o_enter1 out/place = crit1;
+
+  // Process 1 exits: releases mutex
+  i_exit1 : In;
+  i_exit1 in/place = crit1;
+  i_exit1 in/trans = exit1;
+
+  o_exit1_idle : Out;
+  o_exit1_idle out/trans = exit1;
+  o_exit1_idle out/place = idle1;
+
+  o_exit1_mutex : Out;
+  o_exit1_mutex out/trans = exit1;
+  o_exit1_mutex out/place = mutex;
+
+  // Process 2 enters: needs idle2 AND mutex
+  i_enter2_idle : In;
+  i_enter2_idle in/place = idle2;
+  i_enter2_idle in/trans = enter2;
+
+  i_enter2_mutex : In;
+  i_enter2_mutex in/place = mutex;
+  i_enter2_mutex in/trans = enter2;
+
+  o_enter2 : Out;
+  o_enter2 out/trans = enter2;
+  o_enter2 out/place = crit2;
+
+  // Process 2 exits: releases mutex
+  i_exit2 : In;
+  i_exit2 in/place = crit2;
+  i_exit2 in/trans = exit2;
+
+  o_exit2_idle : Out;
+  o_exit2_idle out/trans = exit2;
+  o_exit2_idle out/place = idle2;
+
+  o_exit2_mutex : Out;
+  o_exit2_mutex out/trans = exit2;
+  o_exit2_mutex out/place = mutex;
+}

examples/geolog/petri_net_full.geolog

@@ -0,0 +1,195 @@
+// Full Petri Net Reachability - Type-Theoretic Encoding
+//
+// This demonstrates the complete type-theoretic encoding of Petri net
+// reachability from the original geolog design vision.
+//
+// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md
+//
+// Key concepts:
+// - PetriNet: places, transitions, input/output arcs (with proper arc semantics)
+// - Marking: tokens in a net (parameterized by net)
+// - ReachabilityProblem: initial and target markings (nested instances)
+// - Trace: sequence of firings with wires connecting arcs
+// - Iso: isomorphism between two sorts (used for bijections)
+// - Solution: a trace with isomorphisms to markings
+//
+// This encoding is more type-theoretically precise than the simple
+// PlaceReachability: it tracks individual tokens and arc multiplicities,
+// enabling correct handling of "multi-token" transitions.
+
+// ============================================================
+// THEORY: PetriNet
+// Basic structure: places, transitions, and arcs
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  // Each arc knows which place/transition it connects
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking (parameterized by N : PetriNet)
+// A marking assigns tokens to places
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem (parameterized by N : PetriNet)
+// Defines initial and target markings as nested instances
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace (parameterized by N : PetriNet)
+// A trace is a sequence of transition firings with "wires"
+// connecting input and output arcs
+// ============================================================
+
+theory (N : PetriNet instance) Trace {
+  // Firings
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect output of one firing to input of another
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];  // Wire source (firing, output arc)
+  W/tgt : W -> [firing : F, arc : N/in];   // Wire target (firing, input arc)
+
+  // Wire coherence: output arc must belong to source firing's transition
+  ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of;
+  // Wire coherence: input arc must belong to target firing's transition
+  ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of;
+
+  // Wire uniqueness: each (firing, out-arc) pair has at most one wire
+  ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+  // Wire uniqueness: each (firing, in-arc) pair has at most one wire
+  ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2;
+
+  // Terminals: for initial marking tokens (input) and final marking tokens (output)
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Every output arc of every firing must be wired OR be an output terminal
+  ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |-
+    (exists w : W. w W/src = [firing: f, arc: arc]) \/
+    (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+
+  // Every input arc of every firing must be wired OR be an input terminal
+  ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |-
+    (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+    (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+}
+
+// ============================================================
+// THEORY: Iso (parameterized by two sorts)
+// An isomorphism between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution (parameterized by N and RP)
+// A solution to a reachability problem
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  // The witnessing trace
+  trace : N Trace instance;
+
+  // Bijection between input terminals and initial marking tokens
+  initial_marking_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+
+  // Bijection between output terminals and target marking tokens
+  target_marking_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  // Initial marking commutes: token placement matches terminal placement
+  initial_marking_P_comm : forall i : trace/input_terminal.
+    |- i trace/input_terminal/of = i initial_marking_iso/fwd RP/initial_marking/token/of;
+
+  // Target marking commutes: token placement matches terminal placement
+  target_marking_P_comm : forall o : trace/output_terminal.
+    |- o trace/output_terminal/of = o target_marking_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet - a small Petri net
+//
+//   (A) --[ab]--> (B) --[bc]--> (C)
+//    ^             |
+//    +---[ba]------+
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  // Places
+  A : P;
+  B : P;
+  C : P;
+
+  // Transitions
+  ab : T;
+  ba : T;
+  bc : T;
+
+  // A -> B (via ab)
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+
+  // B -> A (via ba)
+  ba_in : in;
+  ba_in in/src = B;
+  ba_in in/tgt = ba;
+  ba_out : out;
+  ba_out out/src = ba;
+  ba_out out/tgt = A;
+
+  // B -> C (via bc)
+  bc_in : in;
+  bc_in in/src = B;
+  bc_in in/tgt = bc;
+  bc_out : out;
+  bc_out out/src = bc;
+  bc_out out/tgt = C;
+}
+
+// ============================================================
+// Example queries (once query solving is implemented):
+//
+// query can_reach_B_from_A {
+//   ? : ExampleNet problem0 Solution instance;
+// }
+//
+// where problem0 : ExampleNet ReachabilityProblem = {
+//   initial_marking = { tok : token; tok token/of = ExampleNet/A; };
+//   target_marking = { tok : token; tok token/of = ExampleNet/B; };
+// }
+// ============================================================

examples/geolog/petri_net_showcase.geolog

@@ -0,0 +1,345 @@
+// Petri Net Reachability - Full Type-Theoretic Encoding
+//
+// This showcase demonstrates geolog's core capabilities through a
+// non-trivial domain: encoding Petri net reachability as dependent types.
+//
+// A solution to a reachability problem is NOT a yes/no boolean but a
+// CONSTRUCTIVE WITNESS: a diagrammatic proof that tokens can flow from
+// initial to target markings via a sequence of transition firings.
+//
+// Key concepts demonstrated:
+// - Parameterized theories (Marking depends on PetriNet instance)
+// - Nested instance types (ReachabilityProblem contains Marking instances)
+// - Sort-parameterized theories (Iso takes two sorts as parameters)
+// - Cross-instance references (solution's trace elements reference problem's tokens)
+//
+// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md
+
+// ============================================================
+// THEORY: PetriNet
+// Places, transitions, and arcs with proper arc semantics
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking (parameterized by N : PetriNet)
+// A marking assigns tokens to places
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem (parameterized by N : PetriNet)
+// Initial and target markings as nested instances
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace (parameterized by N : PetriNet)
+// A trace records transition firings and token flow via wires
+// ============================================================
+//
+// A trace is a diagrammatic proof of reachability:
+// - Firings represent transition occurrences
+// - Wires connect output arcs of firings to input arcs of other firings
+// - Terminals connect to the initial/target markings
+//
+// The completeness axiom (ax/must_be_fed) ensures every input arc
+// of every firing is accounted for - either wired from another firing
+// or fed by an input terminal.
+
+theory (N : PetriNet instance) Trace {
+  // Firings
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect output arcs of firings to input arcs of other firings
+  W : Sort;
+  W/src_firing : W -> F;
+  W/src_arc : W -> N/out;
+  W/tgt_firing : W -> F;
+  W/tgt_arc : W -> N/in;
+
+  // Wire coherence: source arc must belong to source firing's transition
+  ax/wire_src_coherent : forall w : W.
+    |- w W/src_arc N/out/src = w W/src_firing F/of;
+
+  // Wire coherence: target arc must belong to target firing's transition
+  ax/wire_tgt_coherent : forall w : W.
+    |- w W/tgt_arc N/in/tgt = w W/tgt_firing F/of;
+
+  // Wire place coherence: wire connects matching places
+  ax/wire_place_coherent : forall w : W.
+    |- w W/src_arc N/out/tgt = w W/tgt_arc N/in/src;
+
+  // Terminals
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+
+  // Terminals connect to specific firings and arcs
+  input_terminal/tgt_firing : input_terminal -> F;
+  input_terminal/tgt_arc : input_terminal -> N/in;
+  output_terminal/src_firing : output_terminal -> F;
+  output_terminal/src_arc : output_terminal -> N/out;
+
+  // Terminal coherence axioms
+  ax/input_terminal_coherent : forall i : input_terminal.
+    |- i input_terminal/tgt_arc N/in/tgt = i input_terminal/tgt_firing F/of;
+
+  ax/output_terminal_coherent : forall o : output_terminal.
+    |- o output_terminal/src_arc N/out/src = o output_terminal/src_firing F/of;
+
+  // Terminal place coherence
+  ax/input_terminal_place : forall i : input_terminal.
+    |- i input_terminal/of = i input_terminal/tgt_arc N/in/src;
+
+  ax/output_terminal_place : forall o : output_terminal.
+    |- o output_terminal/of = o output_terminal/src_arc N/out/tgt;
+
+  // COMPLETENESS: Every arc of every firing must be accounted for.
+
+  // Input completeness: every input arc must be fed by a wire or input terminal
+  ax/input_complete : forall f : F, arc : N/in.
+    arc N/in/tgt = f F/of |-
+    (exists w : W. w W/tgt_firing = f, w W/tgt_arc = arc) \/
+    (exists i : input_terminal. i input_terminal/tgt_firing = f, i input_terminal/tgt_arc = arc);
+
+  // Output completeness: every output arc must be captured by a wire or output terminal
+  ax/output_complete : forall f : F, arc : N/out.
+    arc N/out/src = f F/of |-
+    (exists w : W. w W/src_firing = f, w W/src_arc = arc) \/
+    (exists o : output_terminal. o output_terminal/src_firing = f, o output_terminal/src_arc = arc);
+}
+
+// ============================================================
+// THEORY: Iso (parameterized by two sorts)
+// Isomorphism (bijection) between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+
+  // Roundtrip axioms ensure this is a true bijection
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution (parameterized by N and RP)
+// A constructive witness that target is reachable from initial
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  trace : N Trace instance;
+
+  // Bijection: input terminals <-> initial marking tokens
+  initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+
+  // Bijection: output terminals <-> target marking tokens
+  target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  // Commutativity axioms (currently unchecked):
+  // ax/init_comm : forall i : trace/input_terminal.
+  //   |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of;
+  // ax/target_comm : forall o : trace/output_terminal.
+  //   |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet
+//
+// A Petri net with places A, B, C and transitions:
+//   ab: consumes 1 token from A, produces 1 token in B
+//   ba: consumes 1 token from B, produces 1 token in A
+//   abc: consumes 1 token from A AND 1 from B, produces 1 token in C
+//
+//       +---[ba]----+
+//       v           |
+//      (A) --[ab]->(B) --+
+//       |                |
+//       +----[abc]-------+--> (C)
+//
+// The abc transition is interesting: it requires BOTH an A-token
+// and a B-token to fire, producing a C-token.
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  A : P; B : P; C : P;
+  ab : T; ba : T; abc : T;
+
+  // A -> B (via ab)
+  ab_in : in;  ab_in in/src = A; ab_in in/tgt = ab;
+  ab_out : out; ab_out out/src = ab; ab_out out/tgt = B;
+
+  // B -> A (via ba)
+  ba_in : in;  ba_in in/src = B; ba_in in/tgt = ba;
+  ba_out : out; ba_out out/src = ba; ba_out out/tgt = A;
+
+  // A + B -> C (via abc) - note: two input arcs!
+  abc_in1 : in; abc_in1 in/src = A; abc_in1 in/tgt = abc;
+  abc_in2 : in; abc_in2 in/src = B; abc_in2 in/tgt = abc;
+  abc_out : out; abc_out out/src = abc; abc_out out/tgt = C;
+}
+
+// ============================================================
+// PROBLEM 0: Can we reach B from A with one token?
+// Initial: 1 token in A
+// Target:  1 token in B
+// ============================================================
+
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// ============================================================
+// SOLUTION 0: Yes! Fire transition 'ab' once.
+//
+// This Solution instance is a CONSTRUCTIVE PROOF:
+// - The trace contains one firing (f1) of transition 'ab'
+// - The input terminal feeds the A-token into f1's input arc
+// - The output terminal captures f1's B-token output
+// - The isomorphisms prove the token counts match exactly
+// ============================================================
+
+instance solution0 : ExampleNet problem0 Solution = {
+  trace = {
+    // One firing of transition 'ab'
+    f1 : F;
+    f1 F/of = ExampleNet/ab;
+
+    // Input terminal: feeds the initial A-token into f1
+    it : input_terminal;
+    it input_terminal/of = ExampleNet/A;
+    it input_terminal/tgt_firing = f1;
+    it input_terminal/tgt_arc = ExampleNet/ab_in;
+
+    // Output terminal: captures f1's B-token output
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/B;
+    ot output_terminal/src_firing = f1;
+    ot output_terminal/src_arc = ExampleNet/ab_out;
+  };
+
+  initial_iso = {
+    trace/it fwd = problem0/initial_marking/tok;
+    problem0/initial_marking/tok bwd = trace/it;
+  };
+
+  target_iso = {
+    trace/ot fwd = problem0/target_marking/tok;
+    problem0/target_marking/tok bwd = trace/ot;
+  };
+}
+
+// ============================================================
+// PROBLEM 2: Can we reach C from two A-tokens?
+// Initial: 2 tokens in A
+// Target:  1 token in C
+//
+// This is interesting because the only path to C is via 'abc',
+// which requires tokens in BOTH A and B simultaneously.
+// ============================================================
+
+instance problem2 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    t1 : token; t1 token/of = ExampleNet/A;
+    t2 : token; t2 token/of = ExampleNet/A;
+  };
+  target_marking = {
+    t : token;
+    t token/of = ExampleNet/C;
+  };
+}
+
+// ============================================================
+// SOLUTION 2: Yes! Fire 'ab' then 'abc'.
+//
+// Token flow diagram:
+//
+//   [it1]--A-->[f1: ab]--B--wire-->[f2: abc]--C-->[ot]
+//   [it2]--A-----------------^
+//
+// Step 1: Fire 'ab' to move one token A -> B
+//         - it1 feeds A-token into f1 via ab_in
+//         - f1 produces B-token via ab_out
+// Step 2: Fire 'abc' consuming one A-token and one B-token
+//         - it2 feeds A-token into f2 via abc_in1
+//         - Wire connects f1's ab_out to f2's abc_in2 (the B-input)
+//         - f2 produces C-token via abc_out
+// ============================================================
+
+instance solution2 : ExampleNet problem2 Solution = {
+  trace = {
+    // Two firings
+    f1 : F; f1 F/of = ExampleNet/ab;   // First: A -> B
+    f2 : F; f2 F/of = ExampleNet/abc;  // Second: A + B -> C
+
+    // Wire connecting f1's B-output to f2's B-input
+    // This is the crucial connection that makes the trace valid!
+    w1 : W;
+    w1 W/src_firing = f1;
+    w1 W/src_arc = ExampleNet/ab_out;
+    w1 W/tgt_firing = f2;
+    w1 W/tgt_arc = ExampleNet/abc_in2;
+
+    // Input terminal 1: feeds first A-token into f1
+    it1 : input_terminal;
+    it1 input_terminal/of = ExampleNet/A;
+    it1 input_terminal/tgt_firing = f1;
+    it1 input_terminal/tgt_arc = ExampleNet/ab_in;
+
+    // Input terminal 2: feeds second A-token into f2
+    it2 : input_terminal;
+    it2 input_terminal/of = ExampleNet/A;
+    it2 input_terminal/tgt_firing = f2;
+    it2 input_terminal/tgt_arc = ExampleNet/abc_in1;
+
+    // Output terminal: captures f2's C-token output
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/C;
+    ot output_terminal/src_firing = f2;
+    ot output_terminal/src_arc = ExampleNet/abc_out;
+  };
+
+  // Bijection: 2 input terminals <-> 2 initial tokens
+  initial_iso = {
+    trace/it1 fwd = problem2/initial_marking/t1;
+    trace/it2 fwd = problem2/initial_marking/t2;
+    problem2/initial_marking/t1 bwd = trace/it1;
+    problem2/initial_marking/t2 bwd = trace/it2;
+  };
+
+  // Bijection: 1 output terminal <-> 1 target token
+  target_iso = {
+    trace/ot fwd = problem2/target_marking/t;
+    problem2/target_marking/t bwd = trace/ot;
+  };
+}

examples/geolog/petri_net_solution.geolog

@@ -0,0 +1,188 @@
+// Full Petri Net Reachability with Synthesized Solution
+//
+// This file contains the complete type-theoretic encoding of Petri net
+// reachability, plus a manually synthesized solution proving that place B
+// is reachable from place A in the example net.
+//
+// ============================================================
+// This instance was synthesized automatically by Claude Opus 4.5.
+// As was this entire file, and this entire project, really.
+// ============================================================
+
+// ============================================================
+// THEORY: PetriNet - Basic structure with arc semantics
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking - Tokens parameterized by a net
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;  // Which place each token is in
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem - Initial and target markings
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace - A sequence of transition firings with wires
+// ============================================================
+//
+// Simplified version for now - full version with product types commented out below.
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;                                    // Firings
+  F/of : F -> N/T;                             // Which transition each fires
+
+  // Terminals for initial/final marking tokens
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+}
+
+// Full Trace theory with wires and product types (not yet fully supported):
+//
+// theory (N : PetriNet instance) Trace {
+//   F : Sort;                                    // Firings
+//   F/of : F -> N/T;                             // Which transition each fires
+//
+//   W : Sort;                                    // Wires connecting firings
+//   W/src : W -> [firing : F, arc : N/out];      // Wire source
+//   W/tgt : W -> [firing : F, arc : N/in];       // Wire target
+//
+//   // Wire coherence axioms
+//   ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of;
+//   ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of;
+//
+//   // Wire uniqueness
+//   ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+//   ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2;
+//
+//   // Terminals for initial/final marking tokens
+//   input_terminal : Sort;
+//   output_terminal : Sort;
+//   input_terminal/of : input_terminal -> N/P;
+//   output_terminal/of : output_terminal -> N/P;
+//   input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+//   output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+//
+//   // Coverage axioms
+//   ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |-
+//     (exists w : W. w W/src = [firing: f, arc: arc]) \/
+//     (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+//   ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |-
+//     (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+//     (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+// }
+
+// ============================================================
+// THEORY: Iso - Isomorphism between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution - A complete reachability witness
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  trace : N Trace instance;
+
+  initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+  target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  ax/init_comm : forall i : trace/input_terminal.
+    |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of;
+  ax/target_comm : forall o : trace/output_terminal.
+    |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet - A small Petri net
+//
+//   (A) --[ab]--> (B) --[bc]--> (C)
+//    ^             |
+//    +---[ba]------+
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  A : P; B : P; C : P;
+  ab : T; ba : T; bc : T;
+
+  ab_in : in;  ab_in in/src = A; ab_in in/tgt = ab;
+  ab_out : out; ab_out out/src = ab; ab_out out/tgt = B;
+
+  ba_in : in;  ba_in in/src = B; ba_in in/tgt = ba;
+  ba_out : out; ba_out out/src = ba; ba_out out/tgt = A;
+
+  bc_in : in;  bc_in in/src = B; bc_in in/tgt = bc;
+  bc_out : out; bc_out out/src = bc; bc_out out/tgt = C;
+}
+
+// ============================================================
+// INSTANCE: problem0 - Can we reach B from A?
+// ============================================================
+
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// ============================================================
+// INSTANCE: solution0 - YES! Here's the proof.
+// ============================================================
+// This instance was synthesized automatically by Claude Opus 4.5.
+// ============================================================
+
+// The solution proves that place B is reachable from place A by firing
+// transition ab. This creates a trace with one firing and the necessary
+// input/output terminal mappings.
+
+instance solution0 : ExampleNet problem0 Solution = {
+  trace = {
+    f1 : F;
+    f1 F/of = ExampleNet/ab;
+
+    it : input_terminal;
+    it input_terminal/of = ExampleNet/A;
+
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/B;
+  };
+
+  // NOTE: Cross-instance references (e.g., trace/it in initial_iso)
+  // are not yet fully supported. The iso instances would map:
+  // - trace/it <-> problem0/initial_marking/tok
+  // - trace/ot <-> problem0/target_marking/tok
+}

examples/geolog/petri_reachability.geolog

@@ -0,0 +1,164 @@
+// Petri Net Reachability - Full Example
+//
+// This demonstrates the core ideas from the original geolog design document:
+// modeling Petri net reachability using geometric logic with the chase algorithm.
+//
+// Original design: loose_thoughts/2025-12-12_12:10.md
+//
+// Key concepts:
+// - PetriNet: places, transitions, input/output arcs
+// - Marking: assignment of tokens to places (parameterized theory)
+// - Trace: sequence of transition firings connecting markings
+// - Reachability: computed via chase algorithm
+
+// ============================================================
+// THEORY: PetriNet
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  In : Sort;     // Input arcs (place -> transition)
+  Out : Sort;    // Output arcs (transition -> place)
+
+  // Arc structure
+  in/place : In -> P;
+  in/trans : In -> T;
+  out/trans : Out -> T;
+  out/place : Out -> P;
+}
+
+// ============================================================
+// THEORY: Marking (parameterized)
+// A marking assigns tokens to places in a specific net
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  Token : Sort;
+  of : Token -> N/P;
+}
+
+// ============================================================
+// THEORY: PlaceReachability
+// Simplified reachability at the place level
+// ============================================================
+
+theory PlaceReachability {
+  P : Sort;
+  T : Sort;
+
+  // Which transition connects which places
+  // Fires(t, from, to) means transition t can move a token from 'from' to 'to'
+  Fires : [trans: T, from: P, to: P] -> Prop;
+
+  // Reachability relation (transitive closure)
+  CanReach : [from: P, to: P] -> Prop;
+
+  // Reflexivity: every place can reach itself
+  ax/refl : forall p : P.
+    |- [from: p, to: p] CanReach;
+
+  // Transition firing creates reachability
+  ax/fire : forall t : T, x : P, y : P.
+    [trans: t, from: x, to: y] Fires |- [from: x, to: y] CanReach;
+
+  // Transitivity: reachability composes
+  ax/trans : forall x : P, y : P, z : P.
+    [from: x, to: y] CanReach, [from: y, to: z] CanReach |- [from: x, to: z] CanReach;
+}
+
+// ============================================================
+// INSTANCE: SimpleNet
+// A -> B -> C with bidirectional A <-> B
+//
+//   (A) <--[ba]-- (B) --[bc]--> (C)
+//    |             ^
+//    +---[ab]------+
+// ============================================================
+
+// Uses chase to derive CanReach from axioms (reflexivity, fire, transitivity)
+instance SimpleNet : PlaceReachability = chase {
+  // Places
+  A : P;
+  B : P;
+  C : P;
+
+  // Transitions
+  ab : T;   // A -> B
+  ba : T;   // B -> A
+  bc : T;   // B -> C
+
+  // Firing relations
+  [trans: ab, from: A, to: B] Fires;
+  [trans: ba, from: B, to: A] Fires;
+  [trans: bc, from: B, to: C] Fires;
+}
+
+// ============================================================
+// INSTANCE: MutexNet
+// Two processes competing for a mutex
+//
+//   idle1 --[enter1]--> crit1 --[exit1]--> idle1
+//              ^                    |
+//              |       mutex        |
+//              |                    v
+//   idle2 --[enter2]--> crit2 --[exit2]--> idle2
+// ============================================================
+
+// Uses chase to derive reachability relation
+instance MutexNet : PlaceReachability = chase {
+  // Places
+  idle1 : P;
+  crit1 : P;
+  idle2 : P;
+  crit2 : P;
+  mutex : P;
+
+  // Transitions
+  enter1 : T;
+  exit1 : T;
+  enter2 : T;
+  exit2 : T;
+
+  // Process 1 acquires mutex: idle1 + mutex -> crit1
+  // (simplified: we track place-level, not token-level)
+  [trans: enter1, from: idle1, to: crit1] Fires;
+  [trans: enter1, from: mutex, to: crit1] Fires;
+
+  // Process 1 releases mutex: crit1 -> idle1 + mutex
+  [trans: exit1, from: crit1, to: idle1] Fires;
+  [trans: exit1, from: crit1, to: mutex] Fires;
+
+  // Process 2 acquires mutex: idle2 + mutex -> crit2
+  [trans: enter2, from: idle2, to: crit2] Fires;
+  [trans: enter2, from: mutex, to: crit2] Fires;
+
+  // Process 2 releases mutex: crit2 -> idle2 + mutex
+  [trans: exit2, from: crit2, to: idle2] Fires;
+  [trans: exit2, from: crit2, to: mutex] Fires;
+}
+
+// ============================================================
+// INSTANCE: ProducerConsumerNet
+// Producer creates items, consumer processes them
+//
+//   ready --[produce]--> buffer --[consume]--> done
+// ============================================================
+
+// Uses chase to derive reachability relation
+instance ProducerConsumerNet : PlaceReachability = chase {
+  // Places
+  ready : P;
+  buffer : P;
+  done : P;
+
+  // Transitions
+  produce : T;
+  consume : T;
+
+  // Produce: ready -> buffer
+  [trans: produce, from: ready, to: buffer] Fires;
+
+  // Consume: buffer -> done
+  [trans: consume, from: buffer, to: done] Fires;
+}

examples/geolog/petri_reachability_full_vision.geolog

@@ -0,0 +1,72 @@
+// Full Petri Net Reachability Vision Test
+// From 2025-12-12_12:10_VanillaPetriNetRechability.md
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// Simplified Trace theory without disjunctions for now
+theory (N : PetriNet instance) SimpleTrace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Simplified ax5: every firing+arc gets an output terminal
+  ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc];
+
+  // Simplified ax6: every firing+arc gets an input terminal
+  ax6 : forall f : F, arc : N/in. |- exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc];
+}
+
+instance ExampleNet : PetriNet = {
+  A : P;
+  B : P;
+  ab : T;
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+}
+
+// Test nested instance elaboration
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// Test chase with SimpleTrace
+instance trace0 : ExampleNet SimpleTrace = chase {
+  f1 : F;
+  f1 F/of = ExampleNet/ab;
+}

examples/geolog/petri_reachability_vision.geolog

@@ -0,0 +1,94 @@
+// Petri Net Reachability Vision Test
+// Based on 2025-12-12 design document
+
+// Basic Petri net structure
+theory PetriNet {
+  // Places
+  P : Sort;
+
+  // Transitions
+  T : Sort;
+
+  // Arcs (input to transitions, output from transitions)
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// A marking is a multiset of tokens, each at a place
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// A reachability problem is: can we get from initial marking to target?
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// A trace is a sequence of firings connected by wires
+theory (N : PetriNet instance) Trace {
+  // Firings of transitions
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect firing outputs to firing inputs
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  // Terminals are unconnected arc endpoints (to/from the initial/target markings)
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+}
+
+// Example Petri net: A <--ab/ba--> B, (A,B) --abc--> C
+instance ExampleNet : PetriNet = {
+  A : P;
+  B : P;
+  C : P;
+  ab : T;
+  ba : T;
+  abc : T;
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+  ba_in : in;
+  ba_in in/src = B;
+  ba_in in/tgt = ba;
+  ba_out : out;
+  ba_out out/src = ba;
+  ba_out out/tgt = A;
+  abc_in1 : in;
+  abc_in1 in/src = A;
+  abc_in1 in/tgt = abc;
+  abc_in2 : in;
+  abc_in2 in/src = B;
+  abc_in2 in/tgt = abc;
+  abc_out : out;
+  abc_out out/src = abc;
+  abc_out out/tgt = C;
+}
+
+// Reachability problem: Can we reach B from A?
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    t : token;
+    t token/of = ExampleNet/A;
+  };
+  target_marking = {
+    t : token;
+    t token/of = ExampleNet/B;
+  };
+}

examples/geolog/petri_trace_axioms.geolog

@@ -0,0 +1,66 @@
+// Test Trace theory with axioms using product codomains
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// Trace theory with axioms
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Axiom: wires are injective on source
+  // forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+  // (Commented out - requires product codomain equality in premises)
+
+  // Axiom: every arc endpoint must be wired or terminated
+  // forall f : F, arc : N/out. arc N/out/src = f F/of |-
+  //   (exists w : W. w W/src = [firing: f, arc: arc]) \/
+  //   (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+  // (Commented out - requires product codomain values in conclusions)
+}
+
+// Simple net for testing
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Test that the basic theory without axioms still works
+instance SimpleTrace : SimpleNet Trace = {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+
+  it : input_terminal;
+  it input_terminal/of = SimpleNet/A;
+  it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in];
+
+  ot : output_terminal;
+  ot output_terminal/of = SimpleNet/B;
+  ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+}

examples/geolog/petri_trace_coverage_test.geolog

@@ -0,0 +1,36 @@
+// Test: Trace coverage axiom (simplified)
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  out : Sort;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  output_terminal : Sort;
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Simplified ax5: for every arc and firing, if the arc's source is the firing's transition,
+  // create an output terminal
+  ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc];
+}
+
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Trace with just a firing - chase should create a terminal
+instance TestTrace : SimpleNet Trace = chase {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+}

examples/geolog/petri_trace_full_vision.geolog

@@ -0,0 +1,57 @@
+// Trace theory with wires and disjunctions
+// Testing the full vision from 2025-12-12
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Every out arc of every firing: either wired or terminal
+  ax5 : forall f : F, arc : N/out. |-
+    (exists w : W. w W/src = [firing: f, arc: arc]) \/
+    (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+
+  // Every in arc of every firing: either wired or terminal
+  ax6 : forall f : F, arc : N/in. |-
+    (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+    (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+}
+
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Chase should create both wires AND terminals (naive chase adds all disjuncts)
+instance trace_test : SimpleNet Trace = chase {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+}

examples/geolog/petri_trace_test.geolog

@@ -0,0 +1,58 @@
+// Test that Trace theory with product codomains works
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// Simple Petri net: A --t--> B
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Trace theory with product codomains for wire endpoints
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+}
+
+// A simple trace: one firing of t, with input/output terminals
+instance SimpleTrace : SimpleNet Trace = {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+
+  // Input terminal (token comes from external marking)
+  it : input_terminal;
+  it input_terminal/of = SimpleNet/A;
+  it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in];
+
+  // Output terminal (token goes to external marking)
+  ot : output_terminal;
+  ot output_terminal/of = SimpleNet/B;
+  ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+}

examples/geolog/preorder.geolog

@@ -0,0 +1,42 @@
+// Preorder: a set with a reflexive, transitive relation
+//
+// This demonstrates RELATIONS (predicates) as opposed to functions.
+// A relation R : A -> Prop is a predicate on A.
+// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop
+
+theory Preorder {
+  X : Sort;
+
+  // The ordering relation: x ≤ y
+  leq : [x: X, y: X] -> Prop;
+
+  // Reflexivity: x ≤ x
+  ax/refl : forall x : X.
+    |- [x: x, y: x] leq;
+
+  // Transitivity: x ≤ y ∧ y ≤ z → x ≤ z
+  ax/trans : forall x : X, y : X, z : X.
+    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
+}
+
+// The discrete preorder: only reflexive pairs
+// (no elements are comparable except to themselves)
+// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl.
+instance Discrete3 : Preorder = chase {
+  a : X;
+  b : X;
+  c : X;
+}
+
+// A total order on 3 elements: a ≤ b ≤ c
+// Uses `chase` to derive reflexive and transitive closure.
+instance Chain3 : Preorder = chase {
+  bot : X;
+  mid : X;
+  top : X;
+
+  // Assert the basic ordering; chase will add reflexive pairs
+  // and transitive closure (bot ≤ top)
+  [x: bot, y: mid] leq;
+  [x: mid, y: top] leq;
+}

examples/geolog/product_codomain_equality_test.geolog

@@ -0,0 +1,23 @@
+// Test: Product codomain equality in premise (ax3 pattern)
+
+theory ProductCodomainEqTest {
+  A : Sort;
+  B : Sort;
+
+  W : Sort;
+  W/src : W -> [x: A, y: B];
+
+  // ax3 pattern: forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2
+  // This should make W injective on src
+  ax_inj : forall w1 : W, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+}
+
+// Instance with two wires that have the same src - should be identified by chase
+instance Test : ProductCodomainEqTest = {
+  a1 : A;
+  b1 : B;
+  w1 : W;
+  w1 W/src = [x: a1, y: b1];
+  w2 : W;
+  w2 W/src = [x: a1, y: b1];
+}

examples/geolog/product_codomain_test.geolog

@@ -0,0 +1,51 @@
+// Test: Product Codomain Support
+//
+// This tests the new feature where functions can have product codomains,
+// allowing record literal assignments like:
+//   elem func = [field1: v1, field2: v2];
+
+theory ProductCodomainTest {
+  A : Sort;
+  B : Sort;
+  C : Sort;
+
+  // Function with product codomain: maps A elements to (B, C) pairs
+  pair_of : A -> [left: B, right: C];
+}
+
+instance TestInstance : ProductCodomainTest = {
+  // Elements
+  a1 : A;
+  b1 : B;
+  b2 : B;
+  c1 : C;
+
+  // Assign product codomain value using record literal
+  a1 pair_of = [left: b1, right: c1];
+}
+
+// A more realistic example: Edges in a graph
+theory DirectedGraph {
+  V : Sort;
+  E : Sort;
+
+  // Edge endpoints as a product codomain
+  endpoints : E -> [src: V, tgt: V];
+}
+
+instance TriangleGraph : DirectedGraph = {
+  // Vertices
+  v0 : V;
+  v1 : V;
+  v2 : V;
+
+  // Edges
+  e01 : E;
+  e12 : E;
+  e20 : E;
+
+  // Assign edge endpoints using record literals
+  e01 endpoints = [src: v0, tgt: v1];
+  e12 endpoints = [src: v1, tgt: v2];
+  e20 endpoints = [src: v2, tgt: v0];
+}

examples/geolog/record_existential_test.geolog

@@ -0,0 +1,18 @@
+// Test: Record literals in existential conclusions
+
+theory RecordExistentialTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Axiom: given any a:A and b:B, there exists an R with that data
+  ax1 : forall a : A, b : B. |-
+    exists r : R. r R/data = [x: a, y: b];
+}
+
+instance Test : RecordExistentialTest = chase {
+  a1 : A;
+  b1 : B;
+}

examples/geolog/record_in_axiom_test.geolog

@@ -0,0 +1,12 @@
+// Test: Record literals in axioms
+
+theory RecordAxiomTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Test axiom with record literal RHS
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- true;
+}

examples/geolog/record_premise_chase_test.geolog

@@ -0,0 +1,23 @@
+// Test: Chase with record literals in premises
+
+theory RecordPremiseTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Derived sort for processed items
+  Processed : Sort;
+  Processed/r : Processed -> R;
+
+  // Axiom: given r with data [x: a, y: b], create a Processed for it
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists p : Processed. p Processed/r = r;
+}
+
+instance Test : RecordPremiseTest = {
+  a1 : A;
+  b1 : B;
+  r1 : R;
+  r1 R/data = [x: a1, y: b1];
+}

examples/geolog/relalg_simple.geolog

@@ -0,0 +1,130 @@
+// Example: RelAlgIR query plan instances
+//
+// This demonstrates creating query plans as RelAlgIR instances.
+// These show the string diagram representation of relational algebra.
+//
+// First we need to load both GeologMeta (for Srt, Func, etc.) and RelAlgIR.
+// This file just defines instances; load theories first in the REPL:
+//   :load theories/GeologMeta.geolog
+//   :load theories/RelAlgIR.geolog
+//   :load examples/geolog/relalg_simple.geolog
+//
+// Note: RelAlgIR extends GeologMeta, so a RelAlgIR instance contains
+// elements from both GeologMeta sorts (Srt, Func, Elem) and RelAlgIR
+// sorts (Wire, Schema, ScanOp, etc.)
+
+// ============================================================
+// Example 1: Simple Scan
+// ============================================================
+// Query: "scan all elements of sort V"
+// Plan:  () --[ScanOp]--> Wire
+
+instance ScanV : RelAlgIR = chase {
+  // -- Schema (target theory) --
+  target_theory : GeologMeta/Theory;
+  target_theory GeologMeta/Theory/parent = target_theory;
+
+  v_srt : GeologMeta/Srt;
+  v_srt GeologMeta/Srt/theory = target_theory;
+
+  // -- Query Plan --
+  v_base_schema : BaseSchema;
+  v_base_schema BaseSchema/srt = v_srt;
+
+  v_schema : Schema;
+  v_base_schema BaseSchema/schema = v_schema;
+
+  scan_out : Wire;
+  scan_out Wire/schema = v_schema;
+
+  scan : ScanOp;
+  scan ScanOp/srt = v_srt;
+  scan ScanOp/out = scan_out;
+
+  scan_op : Op;
+  scan ScanOp/op = scan_op;
+}
+
+// ============================================================
+// Example 2: Filter(Scan)
+// ============================================================
+// Query: "scan E, filter where src(e) = some vertex"
+// Plan:  () --[Scan]--> w1 --[Filter]--> w2
+//
+// This demonstrates composition via wire sharing.
+
+// Uses chase to derive relations.
+instance FilterScan : RelAlgIR = chase {
+  // -- Schema (representing Graph theory) --
+  target_theory : GeologMeta/Theory;
+  target_theory GeologMeta/Theory/parent = target_theory;
+
+  // Sorts: V (vertices), E (edges)
+  v_srt : GeologMeta/Srt;
+  v_srt GeologMeta/Srt/theory = target_theory;
+
+  e_srt : GeologMeta/Srt;
+  e_srt GeologMeta/Srt/theory = target_theory;
+
+  // Functions: src : E -> V
+  // First create the DSort wrappers
+  v_base_ds : GeologMeta/BaseDS;
+  v_base_ds GeologMeta/BaseDS/srt = v_srt;
+
+  e_base_ds : GeologMeta/BaseDS;
+  e_base_ds GeologMeta/BaseDS/srt = e_srt;
+
+  v_dsort : GeologMeta/DSort;
+  v_base_ds GeologMeta/BaseDS/dsort = v_dsort;
+
+  e_dsort : GeologMeta/DSort;
+  e_base_ds GeologMeta/BaseDS/dsort = e_dsort;
+
+  src_func : GeologMeta/Func;
+  src_func GeologMeta/Func/theory = target_theory;
+  src_func GeologMeta/Func/dom = e_dsort;
+  src_func GeologMeta/Func/cod = v_dsort;
+
+  // NOTE: For a complete example, we'd also need an Instance element
+  // and Elem elements. For simplicity, we use a simpler predicate structure.
+
+  // Using TruePred for now (matches all, demonstrating structure)
+
+  // -- Query Plan --
+  // Schema for E
+  e_base_schema : BaseSchema;
+  e_base_schema BaseSchema/srt = e_srt;
+
+  e_schema : Schema;
+  e_base_schema BaseSchema/schema = e_schema;
+
+  // Wire 1: output of Scan (E elements)
+  w1 : Wire;
+  w1 Wire/schema = e_schema;
+
+  // Wire 2: output of Filter (filtered E elements)
+  w2 : Wire;
+  w2 Wire/schema = e_schema;
+
+  // Scan operation
+  scan : ScanOp;
+  scan ScanOp/srt = e_srt;
+  scan ScanOp/out = w1;
+
+  scan_op : Op;
+  scan ScanOp/op = scan_op;
+
+  // Predicate: TruePred (matches all - demonstrates filter structure)
+  true_pred : TruePred;
+  pred_elem : Pred;
+  true_pred TruePred/pred = pred_elem;
+
+  // Filter operation: w1 --[Filter(pred)]--> w2
+  filter : FilterOp;
+  filter FilterOp/in = w1;
+  filter FilterOp/out = w2;
+  filter FilterOp/pred = pred_elem;
+
+  filter_op : Op;
+  filter FilterOp/op = filter_op;
+}

examples/geolog/solver_demo.geolog

@@ -0,0 +1,132 @@
+// Solver Demo: Theories demonstrating the geometric logic solver
+//
+// Use the :solve command to find instances of these theories:
+//   :source examples/geolog/solver_demo.geolog
+//   :solve EmptyModel
+//   :solve Inhabited
+//   :solve Inconsistent
+//
+// The solver uses forward chaining to automatically:
+// - Add witness elements for existentials
+// - Assert relation tuples
+// - Detect unsatisfiability (derivation of False)
+
+// ============================================================================
+// Theory 1: EmptyModel - Trivially satisfiable with empty carrier
+// ============================================================================
+//
+// A theory with no axioms is satisfied by the empty structure.
+// The solver should report SOLVED immediately with 0 elements.
+
+theory EmptyModel {
+  A : Sort;
+  B : Sort;
+  f : A -> B;
+  R : A -> Prop;
+}
+
+// ============================================================================
+// Theory 2: UnconditionalExistential - Requires witness creation
+// ============================================================================
+//
+// Axiom: forall x : P. |- exists y : P. y R
+//
+// SUBTLE: This axiom's premise (True) and conclusion (∃y.R(y)) don't mention x!
+// So even though there's a "forall x : P", the check happens once for an empty
+// assignment. The premise True holds, but ∃y.R(y) doesn't hold for empty P
+// (no witnesses). The solver correctly detects this and adds a witness.
+//
+// This is correct geometric logic semantics! The universal over x doesn't
+// protect against empty P because x isn't used in the formulas.
+
+theory UnconditionalExistential {
+  P : Sort;
+  R : P -> Prop;
+
+  // This effectively says "there must exist some y with R(y)"
+  // because x is unused - the check happens once regardless of |P|
+  ax : forall x : P. |- exists y : P. y R;
+}
+
+// ============================================================================
+// Theory 3: VacuouslyTrue - Axiom that IS vacuously true for empty carriers
+// ============================================================================
+//
+// Axiom: forall x : P. |- x R
+//
+// For every x, assert R(x). When P is empty, there are no x values to check,
+// so the axiom is vacuously satisfied. Compare with UnconditionalExistential!
+
+theory VacuouslyTrue {
+  P : Sort;
+  R : P -> Prop;
+
+  // This truly IS vacuously true for empty P because x IS used in the conclusion
+  ax : forall x : P. |- x R;
+}
+
+// ============================================================================
+// Theory 4: Inconsistent - UNSAT via derivation of False
+// ============================================================================
+//
+// Axiom: forall x. |- false
+//
+// For any element x, we derive False. This is immediately UNSAT.
+// The solver detects this and reports UNSAT.
+
+theory Inconsistent {
+  A : Sort;
+
+  // Contradiction: any element leads to False
+  ax : forall a : A. |- false;
+}
+
+// ============================================================================
+// Theory 5: ReflexiveRelation - Forward chaining asserts reflexive tuples
+// ============================================================================
+//
+// Axiom: forall x. |- R(x, x)
+//
+// For every element x, the pair (x, x) is in relation R.
+// The solver will assert R(x, x) for each element added.
+
+theory ReflexiveRelation {
+  X : Sort;
+  R : [a: X, b: X] -> Prop;
+
+  // Reflexivity: every element is related to itself
+  ax/refl : forall x : X. |- [a: x, b: x] R;
+}
+
+// ============================================================================
+// Theory 6: ChainedWitness - Nested existential body processing
+// ============================================================================
+//
+// Axiom: forall x. |- exists y. exists z. E(x, y), E(y, z)
+//
+// For every x, there exist y and z such that E(x,y) and E(y,z).
+// Forward chaining creates witnesses and asserts the relations.
+
+theory ChainedWitness {
+  N : Sort;
+  E : [src: N, tgt: N] -> Prop;
+
+  // Chain: every node has a two-step path out
+  ax/chain : forall x : N. |- exists y : N. exists z : N. [src: x, tgt: y] E, [src: y, tgt: z] E;
+}
+
+// ============================================================================
+// Theory 7: EqualityCollapse - Equation handling via congruence closure
+// ============================================================================
+//
+// Axiom: forall x, y. |- x = y
+//
+// All elements of sort X are equal. The solver adds equations to the
+// congruence closure and merges equivalence classes.
+
+theory EqualityCollapse {
+  X : Sort;
+
+  // All elements are equal
+  ax/all_equal : forall x : X, y : X. |- x = y;
+}

examples/geolog/sort_param_simple.geolog

@@ -0,0 +1,31 @@
+// Simpler sort parameter test
+
+theory (X : Sort) Container {
+  elem : X;  // not a Sort, but an element of X
+}
+
+// Hmm, this doesn't quite work...
+// Let me try the actual vision pattern
+
+theory Base {
+  A : Sort;
+  B : Sort;
+}
+
+instance MyBase : Base = {
+  a1 : A;
+  a2 : A;
+  b1 : B;
+  b2 : B;
+}
+
+// Now try a theory parameterized by an instance
+theory (Inst : Base instance) Map {
+  map : Inst/A -> Inst/B;
+}
+
+// Instance of Map parameterized by MyBase
+instance MyMap : MyBase Map = {
+  a1 map = MyBase/b1;
+  a2 map = MyBase/b2;
+}

examples/geolog/todo_list.geolog

@@ -0,0 +1,44 @@
+// TodoList: A simple relational model for tracking tasks
+//
+// This demonstrates geolog as a persistent relational database.
+// Elements represent tasks, and relations track their status.
+
+theory TodoList {
+  // The sort of todo items
+  Item : Sort;
+
+  // Unary relations for item status (simple arrow syntax)
+  completed : Item -> Prop;
+  high_priority : Item -> Prop;
+  blocked : Item -> Prop;
+
+  // Binary relation for dependencies
+  depends : [item: Item, on: Item] -> Prop;
+
+  // Axiom: if an item depends on another, either it is blocked
+  // or the dependency is completed
+  ax/dep_blocked : forall x : Item, y : Item.
+    [item: x, on: y] depends |- x blocked \/ y completed;
+}
+
+// Example: An empty todo list ready for interactive use
+instance MyTodos : TodoList = {
+  // Start empty - add items interactively with :add
+}
+
+// Example: A pre-populated todo list
+instance SampleTodos : TodoList = {
+  // Items
+  buy_groceries : Item;
+  cook_dinner : Item;
+  do_laundry : Item;
+  clean_house : Item;
+
+  // Status: unary relations use simple syntax
+  buy_groceries completed;
+  cook_dinner high_priority;
+
+  // Dependencies: cook_dinner depends on buy_groceries
+  // Mixed syntax: first positional arg maps to 'item' field
+  [cook_dinner, on: buy_groceries] depends;
+}

examples/geolog/transitive_closure.geolog

@@ -0,0 +1,77 @@
+// Transitive Closure Example
+//
+// This example demonstrates the chase algorithm computing transitive
+// closure of a relation. We define a Graph theory with Edge and Path
+// relations, where Path is the transitive closure of Edge.
+//
+// Run with:
+//   cargo run -- examples/geolog/transitive_closure.geolog
+// Then:
+//   :source examples/geolog/transitive_closure.geolog
+//   :inspect Chain
+//   :chase Chain
+//
+// The chase will derive Path tuples for all reachable pairs:
+// - Edge(a,b), Edge(b,c), Edge(c,d) as base facts
+// - Path(a,b), Path(b,c), Path(c,d) from base axiom
+// - Path(a,c), Path(b,d) from one step of transitivity
+// - Path(a,d) from two steps of transitivity
+
+theory Graph {
+  V : Sort;
+
+  // Direct edges in the graph
+  Edge : [src: V, tgt: V] -> Prop;
+
+  // Reachability (transitive closure of Edge)
+  Path : [src: V, tgt: V] -> Prop;
+
+  // Base case: every edge is a path
+  ax/base : forall x, y : V.
+    [src: x, tgt: y] Edge |- [src: x, tgt: y] Path;
+
+  // Inductive case: paths compose
+  ax/trans : forall x, y, z : V.
+    [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path;
+}
+
+// A linear chain: a -> b -> c -> d
+// Chase derives Path tuples from Edge via ax/base and ax/trans.
+instance Chain : Graph = chase {
+  a : V;
+  b : V;
+  c : V;
+  d : V;
+
+  // Edges form a chain
+  [src: a, tgt: b] Edge;
+  [src: b, tgt: c] Edge;
+  [src: c, tgt: d] Edge;
+}
+
+// A diamond: a -> b, a -> c, b -> d, c -> d
+// Chase derives all reachable paths.
+instance Diamond : Graph = chase {
+  top : V;
+  left : V;
+  right : V;
+  bottom : V;
+
+  // Two paths from top to bottom
+  [src: top, tgt: left] Edge;
+  [src: top, tgt: right] Edge;
+  [src: left, tgt: bottom] Edge;
+  [src: right, tgt: bottom] Edge;
+}
+
+// A cycle: a -> b -> c -> a
+// Chase derives all reachable paths (full connectivity).
+instance Cycle : Graph = chase {
+  x : V;
+  y : V;
+  z : V;
+
+  [src: x, tgt: y] Edge;
+  [src: y, tgt: z] Edge;
+  [src: z, tgt: x] Edge;
+}