feat(goal): Branch unification #217

aniva · 2025-06-20T12:27:36-07:00

aniva commented

2025-06-20 12:27:36 -07:00

This allows merger of goal states.

We have to refactor the existing handling mechanism for conv and calc since the old interface is not conducive to any branch unification.

refactor(goal): Existing conv and calc handlers into fragmented tactic objects, which could be compatible with syntax-level features.

This allows merger of goal states. We have to refactor the existing handling mechanism for `conv` and `calc` since the old interface is not conducive to any branch unification. - refactor(goal): Existing `conv` and `calc` handlers into fragmented tactic objects, which could be compatible with syntax-level features.

aniva added this to the 0.3.3 milestone 2025-06-20 12:27:36 -07:00

aniva added the

labels 2025-06-20 12:27:36 -07:00

aniva self-assigned this 2025-06-20 12:27:36 -07:00

aniva added a new dependency 2025-06-20 12:41:14 -07:00

#132 Branch unification

aniva added 1 commit 2025-06-20 17:25:42 -07:00

343ecc2659

feat(goal): GoalState.replay stub

aniva added 1 commit 2025-06-20 17:26:16 -07:00

cb7c4d2723

chore: Add `_m` suffix to replay

aniva added 1 commit 2025-06-23 13:09:26 -07:00

05a8e3b13c

feat: Branch unification (modulo conv/calc)

aniva added 1 commit 2025-06-23 20:58:12 -07:00

58ae791da3

refactor: `conv` and `calc` into tactic fragments

aniva commented

2025-06-24 10:02:35 -07:00

We need to think about the interaction between tactic fragments and resumption.

Before the existence of tactic fragments, we assume every goal can become dormant and can participate in the type unification process. This allows goals to be solved in-passing.

Examples

e.g. If there are states G = { ?0, ?1f } (where ?0f has a fragment) and G' = { ?2, ?3 }, it should be possible to resume G''s goals into G (no fragments). This would not affect things very much.

However, if we have G = { ?0, ?1f } and G' = { ?2, ?3f }, such resumption demands a state with multiple tactic fragments. We can permit this possibility in principle.

Syntax-Level Fragment

The real trouble begins when we have syntax-level fragments. Suppose we implement this so the user can execute on ?1 the fragment (assuming x is an inductive with multiple cases)

match x with
| .zero => sorry

it would feed back that there are missing cases for x. However, we cannot actually assign anything to ?1 yet, since the above expression cannot be fully elaborated. It would be stored as a syntax level stub.

At this point, nothing troublesome is happening yet. However, if the goal is allowed to become dormant, and during the solution of ?2, it modifies ?1 in passing, there is no immediate feedback into ?1 upon resumption. This lack of immediate feedback violates the design principle of Pantograph.

This is less of an issue for conv and calc since they operate on the expression level.

Possible Solutions

Before this PR, there could be at most one tactic fragment in a goal state, and syntax-level tactics do not exist yet.

In Lean there is no absolute way of preventing a metavariable from being assigned (other than context depth which should not be used here). Even .syntheticOpaque metavariables can be assigned with withAssignableSyntheticOpaque. Hence one solution is that upon the completion of tactic fragments, its assignment has to unify against the existing assignment if one exists. When such unification is impossible, the tactic fragment is not allowed to conclude.
Another solution is to not permit syntax-level fragments.
The early refutation design principle means we will have to permit dormant goals to some extent. During resumption, if a dormant goal with fragment is already assigned in some way, the resumption will fail. The downside is it makes resumption fallible which is a massive problem.
We could decide that syntax-level fragments (or more generally any fragment requiring elaboration) must conclude before it goes dormant. This prevents any tactic from acting on sideline goals when a fragment exists. The downside is that early refutation becomes impossible.

Property	S1	S2	S3	S4
Syntax-Level Fragments	✓	-	✓	✓
Early refutation (main)	-	✓	✓	-
Early refutation (side)	✓	✓	✓	-
Infallible Resume	✓	✓	-	✓
No Dormant Fragment	✓	✓	-	✓
Multiple Syntax Fragments	✓	✓	✓	-

We need to think about the interaction between tactic fragments and resumption. Before the existence of tactic fragments, we assume every goal can become dormant and can participate in the type unification process. This allows goals to be solved in-passing. ## Examples e.g. If there are states `G = { ?0, ?1f }` (where `?0f` has a fragment) and `G' = { ?2, ?3 }`, it should be possible to resume `G'`'s goals into `G` (no fragments). This would not affect things very much. However, if we have `G = { ?0, ?1f }` and `G' = { ?2, ?3f }`, such resumption demands a state with multiple tactic fragments. We can permit this possibility in principle. ## Syntax-Level Fragment The real trouble begins when we have syntax-level fragments. Suppose we implement this so the user can execute on `?1` the fragment (assuming `x` is an inductive with multiple cases) ``` match x with | .zero => sorry ``` it would feed back that there are missing cases for `x`. However, we cannot actually assign anything to `?1` yet, since the above expression cannot be fully elaborated. It would be stored as a syntax level stub. At this point, nothing troublesome is happening yet. However, if the goal is allowed to become dormant, and during the solution of `?2`, it modifies `?1` in passing, there is no immediate feedback into `?1` upon resumption. This lack of immediate feedback violates the design principle of Pantograph. This is less of an issue for `conv` and `calc` since they operate on the expression level. ## Possible Solutions Before this PR, there could be at most one tactic fragment in a goal state, and syntax-level tactics do not exist yet. 1. In Lean there is no absolute way of preventing a metavariable from being assigned (other than context depth which should not be used here). Even `.syntheticOpaque` metavariables can be assigned with `withAssignableSyntheticOpaque`. Hence one solution is that upon the completion of tactic fragments, its assignment has to unify against the existing assignment if one exists. When such unification is impossible, the tactic fragment is not allowed to conclude. 2. Another solution is to not permit syntax-level fragments. 3. The early refutation design principle means we will have to permit dormant goals to some extent. During resumption, if a dormant goal with fragment is already assigned in some way, the resumption will fail. The downside is it makes resumption fallible which is a massive problem. 4. We could decide that syntax-level fragments (or more generally any fragment requiring elaboration) must conclude before it goes dormant. This prevents any tactic from acting on sideline goals when a fragment exists. The downside is that early refutation becomes impossible. | Property | S1 | S2 | S3 | S4 | |----------|---|----|----|----| | Syntax-Level Fragments | ✓ | - | ✓ | ✓ | | Early refutation (main) | - | ✓ | ✓ | - | | Early refutation (side) | ✓ | ✓ | ✓ | - | | Infallible Resume | ✓ | ✓ | - | ✓ | | No Dormant Fragment | ✓ | ✓ | - | ✓ | | Multiple Syntax Fragments | ✓ | ✓ | ✓ | - |

aniva commented

2025-06-24 11:16:13 -07:00

There is one more problem about conversion tactic mode. In such a mode, a goal state could have a mixture of conversion and non-conversion goals. When we decree an exit from conversion tactic mode, all sibling conversion goals must be concluded via rfl. This is an operation in between goal level and state level.

There is one more problem about conversion tactic mode. In such a mode, a goal state could have a mixture of conversion and non-conversion goals. When we decree an exit from conversion tactic mode, all sibling conversion goals must be concluded via `rfl`. This is an operation in between goal level and state level.

aniva added 1 commit 2025-06-24 13:33:35 -07:00

9d4b1ae755

refactor(goal): Allow multiple fragments

aniva added 1 commit 2025-06-24 13:38:11 -07:00

9b0d96f422

feat(goal): Trace messages for replay

aniva added 1 commit 2025-06-24 13:51:57 -07:00

7837ddff4f

feat(goal): Unify fragments in replay

aniva added 1 commit 2025-06-24 13:55:56 -07:00

9eb5533166

Merge branch 'dev' into goal/branch-unification