Skip to content

Commit 3d313da

Browse files
watchthelightwatchthelight
committed
release: v1.8.0-pre - Elaboration and Tactics
Phase 8 implements the elaboration and tactics systems for HoTTGo: Elaboration System (internal/elab/): - Surface syntax with implicit arguments and holes - Bidirectional type checking (synth/check modes) - Metavariable store for unification - Zonking for metavariable substitution Unification (internal/unify/): - Miller pattern unification - Constraint solving with occurs check - Support for all term types (Pi, Sigma, Path, etc.) Tactics (tactics/): - Proof state management with goals - Core tactics: Intro, Exact, Assumption, Apply, Reflexivity, Split, Rewrite - Tactic combinators: Seq, OrElse, Try, Repeat, First, All - Go Prover API for programmatic proof construction Parser Integration: - Surface syntax parsing (holes, implicit arguments) - S-expression format support Test Coverage: - internal/elab: 88.7% - internal/unify: 95.0% - tactics: 90.9% - tactics/proofstate: 97.5% - internal/parser: 86.5%
1 parent b2a8a7c commit 3d313da

20 files changed

Lines changed: 11102 additions & 1 deletion

‎CHANGELOG.md‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,71 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
77

88
## [Unreleased]
99

10+
## [1.8.0-pre] - 2026-01-08
11+
12+
### Added
13+
- **Elaboration System** (`internal/elab/`)
14+
- Surface syntax with implicit arguments and holes (`surface.go`)
15+
- Metavariable store for type inference (`meta.go`)
16+
- Elaboration context extending kernel context (`context.go`)
17+
- Bidirectional elaboration algorithm (`elab.go`)
18+
- Zonking (metavariable substitution) (`zonk.go`)
19+
- Comprehensive test suite (`elab_test.go`) - 88.7% coverage
20+
21+
- **Unification** (`internal/unify/`)
22+
- Miller pattern unification algorithm
23+
- Pattern inversion with variable shifting
24+
- Occurs check for cycle detection
25+
- Constraint solving and deferred constraints
26+
- Zonk functions for metavariable substitution
27+
- Comprehensive test suite - 95.0% coverage
28+
29+
- **Surface Syntax Parser** (`internal/parser/surface.go`)
30+
- Implicit Pi types: `{x : A} -> B`
31+
- Implicit lambdas: `\{x}. body`
32+
- Holes: `_` (anonymous) and `?name` (named)
33+
- Implicit application: `f {arg}`
34+
- S-expression forms compatibility
35+
- FormatSurfaceTerm for pretty printing
36+
- Extended test suite - 86.5% coverage
37+
38+
- **Tactics System** (`tactics/`)
39+
- Proof state management (`proofstate/state.go`) - 97.5% coverage
40+
- Tactic type and result (`tactic.go`)
41+
- Tactic combinators (`combinators.go`):
42+
- `Seq`: Sequential composition
43+
- `OrElse`: Try first, fallback to second
44+
- `Try`: Succeed even on failure
45+
- `Repeat`: Apply until failure
46+
- `First`: First successful tactic
47+
- `All`: Apply to all goals
48+
- `Focus`: Apply to specific goal
49+
- `Progress`: Fail if no progress
50+
- `Complete`: Require full proof
51+
- Core tactics (`core.go`):
52+
- `Intro`, `IntroN`, `Intros`: Introduce hypotheses
53+
- `Exact`: Provide exact proof term
54+
- `Assumption`: Use hypothesis
55+
- `Apply`: Apply function to goal
56+
- `Reflexivity`: Prove reflexivity goals
57+
- `Split`: Split sigma/product types
58+
- `Simpl`: Normalize goal
59+
- `Rewrite`, `RewriteRev`: Rewrite with equality
60+
- `Trivial`, `Auto`: Automation
61+
- Prover Go API (`prover.go`):
62+
- `NewProver`: Create interactive prover
63+
- Fluent API methods for chaining
64+
- `Prove`, `MustProve`: Convenience functions
65+
- Comprehensive test suite - 90.9% coverage
66+
67+
### Tests
68+
- Extensive test coverage for Phase 8 components:
69+
- `internal/elab`: 88.7% coverage with tests for zonk, meta store, context, and elaboration
70+
- `internal/unify`: 95.0% coverage with tests for all term types and edge cases
71+
- `tactics/proofstate`: 97.5% coverage with comprehensive proof state tests
72+
- `tactics`: 90.9% coverage with tests for combinators and core tactics
73+
- `internal/parser`: 86.5% coverage for surface syntax parsing
74+
1075
## [1.7.1] - 2026-01-08
1176

1277
### Added

‎DESIGN.md‎

Lines changed: 102 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,4 +44,105 @@
4444
## Phase 0 acceptance criteria
4545
- `DESIGN.md` checked in with decisions above.
4646
- Skeleton packages compile with `go test ./...` (smoke tests).
47-
- Kernel exposes a tiny API surface with typed “unimplemented” errors to be filled in later phases.
47+
- Kernel exposes a tiny API surface with typed "unimplemented" errors to be filled in later phases.
48+
49+
## Elaboration System (Phase 8)
50+
51+
The elaboration system transforms surface syntax with implicit arguments and holes into fully explicit core terms.
52+
53+
### Surface Syntax (`internal/elab/surface.go`)
54+
Surface syntax extends core syntax with:
55+
- Implicit arguments marked with `{}`
56+
- Holes: `_` (anonymous) and `?name` (named)
57+
- User-friendly names instead of de Bruijn indices
58+
59+
### Metavariables (`internal/elab/meta.go`)
60+
- `MetaStore` manages metavariables created during elaboration
61+
- Each metavariable tracks: ID, expected type, context, solution (if solved)
62+
- States: `Unsolved`, `Solved`, `Frozen`
63+
64+
### Elaboration Algorithm (`internal/elab/elab.go`)
65+
Bidirectional type checking:
66+
- `synth`: Synthesize type from term
67+
- `check`: Check term against expected type
68+
Key operations:
69+
- Hole → Fresh metavariable
70+
- Implicit Pi application → Auto-insert `{?α}`
71+
- Implicit lambda inference when checking against implicit Pi
72+
73+
### Unification (`internal/unify/unify.go`)
74+
Miller pattern unification:
75+
- Solves constraints of form `?α[σ] =? t`
76+
- Patterns: metavariable applied to distinct bound variables
77+
- Occurs check prevents cyclic solutions
78+
- Defers non-pattern constraints
79+
80+
### Zonking (`internal/elab/zonk.go`)
81+
Substitutes solved metavariables with their solutions throughout a term.
82+
83+
## Tactics System (Phase 8)
84+
85+
Ltac-style proof scripting for interactive theorem proving.
86+
87+
### Proof State (`tactics/proofstate/`)
88+
- `Goal`: Single proof obligation with hypotheses and goal type
89+
- `ProofState`: Collection of goals, metastore, undo history
90+
- Focus management for working on specific goals
91+
92+
### Tactics (`tactics/`)
93+
A tactic transforms a proof state:
94+
```go
95+
type Tactic func(*proofstate.ProofState) TacticResult
96+
```
97+
98+
**Combinators** (`combinators.go`):
99+
- `Seq`: Sequential composition
100+
- `OrElse`: Try first, fallback to second
101+
- `Try`: Succeed even on failure
102+
- `Repeat`: Apply until failure
103+
- `First`: First successful tactic
104+
- `All`: Apply to all goals
105+
106+
**Core Tactics** (`core.go`):
107+
- `Intro`: Introduce hypothesis from Pi type
108+
- `Exact`: Provide exact proof term
109+
- `Assumption`: Solve from hypothesis
110+
- `Reflexivity`: Prove Id/Path reflexivity
111+
- `Split`: Split sigma types
112+
- `Rewrite`: Use equality for rewriting
113+
- `Auto`: Automatic proof search
114+
115+
### Prover API (`prover.go`)
116+
```go
117+
prover := tactics.NewProver(goalType)
118+
prover.Intro_("x").Intro_("y").Assumption_()
119+
term, err := prover.Extract()
120+
```
121+
122+
## Package Structure (Updated)
123+
124+
```
125+
internal/
126+
├── ast/ — Core and Raw AST
127+
├── elab/ — Elaboration system
128+
│ ├── surface.go — Surface syntax types
129+
│ ├── meta.go — Metavariable store
130+
│ ├── context.go — Elaboration context
131+
│ ├── elab.go — Elaboration algorithm
132+
│ └── zonk.go — Zonking
133+
├── unify/ — Unification
134+
│ └── unify.go — Miller pattern unification
135+
├── eval/ — NbE evaluator
136+
├── parser/ — Parsing
137+
│ ├── sexpr.go — Core term parser
138+
│ └── surface.go — Surface syntax parser
139+
└── ...
140+
141+
tactics/
142+
├── proofstate/
143+
│ └── state.go — Proof state management
144+
├── tactic.go — Tactic type
145+
├── combinators.go — Tactic combinators
146+
├── core.go — Core tactics
147+
└── prover.go — Go API
148+
```

‎internal/ast/term.go‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,3 +135,14 @@ func MkApps(t Term, us ...Term) Term {
135135
}
136136
return t
137137
}
138+
139+
// Meta represents a metavariable (hole) to be solved during elaboration.
140+
// Metavariables are placeholders for unknown terms that are filled in
141+
// by unification. Each metavariable has a unique ID and may be applied
142+
// to a spine of arguments representing the local context.
143+
type Meta struct {
144+
ID int // Unique identifier for this metavariable
145+
Args []Term // Spine of arguments (local context variables)
146+
}
147+
148+
func (Meta) isCoreTerm() {}

0 commit comments

Comments
 (0)