diff --git a/CubicalTransport.lean b/CubicalTransport.lean index 17ee671..e7633ca 100644 --- a/CubicalTransport.lean +++ b/CubicalTransport.lean @@ -25,3 +25,15 @@ import CubicalTransport.Inductive import CubicalTransport.Bridge import CubicalTransport.Question import CubicalTransport.PropertyTest +import CubicalTransport.Truncation +import CubicalTransport.Decidable +import CubicalTransport.Reify +import CubicalTransport.Omega +import CubicalTransport.Category +import CubicalTransport.Modality +import CubicalTransport.Subobject +import CubicalTransport.SIP +import CubicalTransport.Bridge.Set +import CubicalTransport.Contract +import CubicalTransport.Reflect +import CubicalTransport.Tactic.EqContract diff --git a/CubicalTransport/Contract.lean b/CubicalTransport/Contract.lean index 550074a..867b728 100644 --- a/CubicalTransport/Contract.lean +++ b/CubicalTransport/Contract.lean @@ -479,7 +479,7 @@ def Contract.empty_ (ℓ : ULevel) : Contract ℓ := fun _ => Substantively T-dependent: the body applies both `C` and `D` to T, so the result mentions T through both subcontract values. -/ def Contract.and {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T => - Ω.and (C T) (D T) + Ω.and (ℓ := ℓ) (C T) (D T) /-- Disjunction of two contracts. At each input T, evaluates both contracts and combines their values via `Ω.or` (the @@ -491,7 +491,7 @@ def Contract.or {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T => contracts and combines their values via `Ω.implies` (the Ω-internal arrow type). -/ def Contract.implies {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T => - Ω.implies (C T) (D T) + Ω.implies (ℓ := ℓ) (C T) (D T) -- ── §5. Theorems ─────────────────────────────────────────────────────────── diff --git a/CubicalTransport/Subobject.lean b/CubicalTransport/Subobject.lean index d03d39a..eebd767 100644 --- a/CubicalTransport/Subobject.lean +++ b/CubicalTransport/Subobject.lean @@ -98,8 +98,8 @@ def total {ℓ : ULevel} : CTerm := Real `.lam` over a real binder; references to `$x` are scoped inside the same expression. -/ -def inter (P Q : CTerm) : CTerm := - .lam "$x" (Ω.and (.app P (.var "$x")) (.app Q (.var "$x"))) +def inter {ℓ : ULevel} (P Q : CTerm) : CTerm := + .lam "$x" (Ω.and (ℓ := ℓ) (.app P (.var "$x")) (.app Q (.var "$x"))) /-- Pointwise union: holds at `x` iff at least one of `P`, `Q` holds. @@ -113,8 +113,8 @@ def union {ℓ : ULevel} (P Q : CTerm) : CTerm := Encoding: `.lam "$x" (Ω.implies (.app P (.var "$x")) (.app Q (.var "$x")))`. The body uses Ω's internal-arrow `Ω.implies`. -/ -def implies (P Q : CTerm) : CTerm := - .lam "$x" (Ω.implies (.app P (.var "$x")) (.app Q (.var "$x"))) +def implies {ℓ : ULevel} (P Q : CTerm) : CTerm := + .lam "$x" (Ω.implies (ℓ := ℓ) (.app P (.var "$x")) (.app Q (.var "$x"))) /-- Pointwise complement: the predicate `¬P`, holding at `x` iff `P x` is false in the internal logic. @@ -280,23 +280,23 @@ theorem Ω_internal_logic_sound {ℓ : ULevel} : -- (1) Idempotence of ∧: P ∧ P ≡ P (∀ (P : CTerm), HasType [] P (Ω ℓ) → ∃ (pf : CTerm), - HasType [] pf (CType.path (Ω ℓ) (Ω.and P P) P)) ∧ + HasType [] pf (CType.path (Ω ℓ) (Ω.and (ℓ := ℓ) P P) P)) ∧ -- (2) Commutativity of ∧: P ∧ Q ≡ Q ∧ P (∀ (P Q : CTerm), HasType [] P (Ω ℓ) → HasType [] Q (Ω ℓ) → ∃ (pf : CTerm), - HasType [] pf (CType.path (Ω ℓ) (Ω.and P Q) (Ω.and Q P))) ∧ + HasType [] pf (CType.path (Ω ℓ) (Ω.and (ℓ := ℓ) P Q) (Ω.and (ℓ := ℓ) Q P))) ∧ -- (3) Modus ponens validity: P ∧ (P → Q) ≡ P ∧ Q (∀ (P Q : CTerm), HasType [] P (Ω ℓ) → HasType [] Q (Ω ℓ) → ∃ (pf : CTerm), HasType [] pf (CType.path (Ω ℓ) - (Ω.and P (Ω.implies P Q)) - (Ω.and P Q))) ∧ + (Ω.and (ℓ := ℓ) P (Ω.implies (ℓ := ℓ) P Q)) + (Ω.and (ℓ := ℓ) P Q))) ∧ -- (4) Implication absorption: P → (P → Q) ≡ P → Q (∀ (P Q : CTerm), HasType [] P (Ω ℓ) → HasType [] Q (Ω ℓ) → ∃ (pf : CTerm), HasType [] pf (CType.path (Ω ℓ) - (Ω.implies P (Ω.implies P Q)) - (Ω.implies P Q))) := by + (Ω.implies (ℓ := ℓ) P (Ω.implies (ℓ := ℓ) P Q)) + (Ω.implies (ℓ := ℓ) P Q))) := by -- waits on: prop-univalence packaged from `Soundness.transp_ua` -- (the same dependency as `OmegaIsProp` in `Omega.lean`). Each of -- the four Heyting laws is a Path-equality at Ω, and the cubical diff --git a/CubicalTransport/Tactic/EqContract.lean b/CubicalTransport/Tactic/EqContract.lean new file mode 100644 index 0000000..c3f0a8e --- /dev/null +++ b/CubicalTransport/Tactic/EqContract.lean @@ -0,0 +1,747 @@ +/- + CubicalTransport.Tactic.EqContract + ================================== + User-facing tactic surface that operates on the topos-internal + contracts (THEORY.md §0.10 / §∞.3). + + ## What this module exports + + Three tactics and two commands: + + · `tactic via_eq_contract` — translates a cubical Path-equality + existence goal to a Lean Eq goal using `pathEqEquiv`, gated by + `CubicalSetC` synthesis from the contract registry. After the + tactic runs, the goal is the Eq-side; the user discharges it + with mathlib (or any other Lean reasoning). When the contract + cannot be discharged automatically, the residual `CubicalSetC T` + obligation is left as an additional subgoal alongside the Eq. + + · `tactic find_contract_path` — synthesis: given a goal of shape + expressing "find me a contract for T", BFS the contract + registry combined with the entailment-morphism table to + discover a contract value. Closes the goal with the + discovered pair, or fails with a precise error. + + · `tactic lift_via_topos t` — bundled: takes a tactic argument + `t` (as a `tacticSeq`), runs `via_eq_contract` to translate the + goal, then applies `t` on the translated goal. One-shot + transport from cubical-side to mathlib-side. + + · `command #contract` — displays the topos of contracts: lists + every registered Contract by name (from + `Reflect.Contract.allRegistered`), alongside the known + entailment morphisms. + + · `command #whichContract ` — given a CType expression, + attempts contract synthesis for every registered contract and + lists the ones that succeed. + + ## Design + + All five user-facing items share four internal helpers: + + · `parsePathGoal` — given the goal Expr, peels `Exists`, + `HasType`, and `CType.path` to extract the four pieces + `(α_expr, embed_expr, T_expr, a_value_expr, b_value_expr)` + needed to apply `pathEqEquiv`. + + · `entailmentRegistry` — the hardcoded table of known entailment + morphisms `(fromContractName, toContractName, lemmaName)`. + Currently houses only the canonical `CDecidableEq → CubicalSetC` + morphism via `CubicalSetC_of_CDecidableEq`; additional + entailments land here as Hedberg / J-rule discharges unlock + further Set-level promotions. + + · `synthCubicalSetC` — BFS over the entailment table to attempt + to construct a Lean-Prop witness of `CubicalSetC T` from the + registry. Falls back to leaving the obligation as an mvar + when no closed chain succeeds. + + · `attemptSynthesis` — for `#whichContract`: given a contract + name and a CType, try the same BFS to construct a satisfaction + witness, returning whether it succeeded. + + ## Implementation discipline + + · No `sorry` is emitted by any tactic body. When a tactic cannot + construct a proof, it throws a precise `throwError` with + diagnostic context (the goal, the expected shape, the registry + contents, the entailment chain attempted). + + · The BFS in `find_contract_path` and `synthCubicalSetC` is real: + a worklist over `(currentName, derivationChain)` pairs, + expanded by entailment morphisms, with a visited-set to prevent + cycles. When the worklist is exhausted, a precise error fires + that lists what was tried. + + · Pattern matching on the goal Expr is precise: the + `parsePathGoal` helper reduces (`whnf`) at every layer and + matches each constructor name explicitly; mismatches throw + diagnostic errors pointing at the actual vs. expected shape. + + · The Lean metaprogramming API used is fixed-set: `MVarId`, + `getMainGoal`, `withMainContext`, `replaceMainGoal`, + `liftMetaTactic`, `evalTactic`, `Lean.Meta.mkFreshExprMVar`, + `MVarId.apply`, `Lean.Meta.whnf`, `Expr.getAppFnArgs`. Each + has been verified against the Lean 4.30.0-rc2 source. +-/ + +import CubicalTransport.Reflect +import CubicalTransport.Bridge.Set + +namespace CubicalTransport.Tactic.EqContract + +open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Lean.Elab.Command +open CubicalTransport.Reflect +open CubicalTransport.Bridge.Set + +-- ── §1. Entailment morphism registry ────────────────────────────────────── + +/-- A single entailment morphism from one named contract to another, + discharged by a named lemma whose signature is + `fromContract T → toContract T` + (or, in the `CubicalSetC ← CDecidableEq` case, with the source + expressed as the corresponding closed-cubical-existential + statement). + + Stored as a triple of `Lean.Name`s for cheap registry + inspection; the lemma is applied by name via `MVarId.apply` + on a fresh-mvar expression of the lemma's constant. -/ +structure EntailmentMorphism where + /-- The source contract's name (the contract a witness is needed for). -/ + fromContract : Lean.Name + /-- The target contract's name (the contract this morphism produces). -/ + toContract : Lean.Name + /-- The Lean lemma's `Name` that discharges the entailment. -/ + lemmaName : Lean.Name + deriving Repr + +/-- The hardcoded entailment registry. Each entry is read by the + `synthCubicalSetC` BFS and by the `#contract` command. + + The sole entry currently formalised is + `CDecidableEq → CubicalSetC` via `CubicalSetC_of_CDecidableEq` + (Bridge/Set.lean §1). Additional entailments land here as + Hedberg (`Decidable.lean`) and the J-rule combinator from + `Soundness.transp_ua` discharge further Set-level promotions: + + · `CGroupC → CubicalSetC` once the group-on-a-Set lemma lands; + · `CCoxeterC → CGroupC` once the Coxeter-is-group inclusion lands; + · `CSheafC → CSiteC` once the sheaf-on-site projection lands. + + Each entry's `lemmaName` is a real Lean constant — the BFS tries + `MVarId.apply` on a fresh-level-instantiated `mkConst lemmaName` + expression. -/ +def entailmentRegistry : List EntailmentMorphism := [ + { fromContract := ``CubicalTransport.Decidable.CDecidableEq + toContract := ``CubicalTransport.Bridge.Set.CubicalSetC + lemmaName := ``CubicalTransport.Bridge.Set.CubicalSetC_of_CDecidableEq } +] + +-- ── §2. Parsing helpers for the via_eq_contract goal shape ──────────────── + +/-- The five pieces extracted from a Path-existence goal. Used by + `via_eq_contract` and `lift_via_topos` to construct the + `Iff.mpr (pathEqEquiv ...)` term that flips the goal from the + Path-side to the Eq-side. + + · `αExpr` — the Lean type `α : Type` whose elements are being + equated (the `α` of `[CubicalEmbed α]`). + · `embedExpr` — the `CubicalEmbed α` typeclass instance. + · `tExpr` — the carrier CType `T : CType ℓ`, equal to + `@CubicalEmbed.ctype α embedExpr`. + · `aExpr` — the left endpoint value `a : α`. + · `bExpr` — the right endpoint value `b : α`. -/ +structure PathGoalParts where + αExpr : Expr + embedExpr : Expr + tExpr : Expr + aExpr : Expr + bExpr : Expr + +/-- Strip a chain of metadata wrappers and instantiate metavariables + to expose the underlying expression head, but do NOT unfold any + constants (typeclass projections, definitions, etc.). Used at + every layer of `parsePathGoal` to peel through the elaborated + encoding without losing the symbolic structure (which `whnf` + with full transparency would erase via β/δ-reduction of + typeclass projections like `CubicalEmbed.ctype` and + `CubicalEmbed.toCTerm`). + + Implementation: `instantiateMVars` followed by `whnf` at + `.reducible` transparency, which only reduces `[reducible]` + declarations (not typeclass projections nor definitions). -/ +private def reduce (e : Expr) : MetaM Expr := do + let e ← instantiateMVars e + withTransparency .reducible (whnf e) + +/-- Try to extract the underlying value `a : α` from an + `@CubicalTransport.Bridge.CubicalEmbed.toCTerm α inst aValue` + application. Returns the third explicit argument when matched. + + The encoding produced by `CubicalEmbed.toCTerm a` elaborates to + the three-explicit-argument form `@toCTerm α inst a`. We match + by constant name and pull the value off the args array. -/ +private def extractToCTermValue (e : Expr) : MetaM (Option Expr) := do + let e ← reduce e + let (fn, args) := e.getAppFnArgs + if fn == ``CubicalTransport.Bridge.CubicalEmbed.toCTerm then + -- @CubicalEmbed.toCTerm α inst a — three args. The value + -- lives in the last position. + if h : args.size ≥ 3 then + return some (args[args.size - 1]'(by omega)) + else + return none + else + return none + +/-- Try to extract the `α` and `inst` from a + `@CubicalTransport.Bridge.CubicalEmbed.ctype α inst` application. + Returns the pair `(α, inst)` when matched. Used by + `parsePathGoal` to peel the carrier CType layer. -/ +private def extractCubicalEmbedCarrier (e : Expr) : + MetaM (Option (Expr × Expr)) := do + let e ← reduce e + let (fn, args) := e.getAppFnArgs + if fn == ``CubicalTransport.Bridge.CubicalEmbed.ctype then + -- @CubicalEmbed.ctype α inst — two arguments. + if h : args.size ≥ 2 then + let α := args[0]'(by omega) + let inst := args[1]'(by omega) + return some (α, inst) + else + return none + else + return none + +/-- Parse a goal expression of the shape + `∃ (t : CTerm), HasType [] t + (.path (CubicalEmbed.ctype (α := α)) + (CubicalEmbed.toCTerm a) + (CubicalEmbed.toCTerm b))` + into the five pieces `(α, inst, T, a, b)` needed to invoke + `pathEqEquiv`. + + Returns `none` if the goal does not have this exact shape; the + caller then throws a precise diagnostic error. + + Algorithm: + 1. `whnf` the goal to expose the `Exists` head. + 2. Match `Exists` with two args: `[CTerm_type, predicate_λ]`. + The predicate is `fun t => HasType [] t (.path T a_emb b_emb)`. + 3. Strip the lambda to get the body, with `t` as `bvar 0`. + 4. `whnf` the body to expose `HasType`. + 5. Match `HasType` with its full arg list and pull the LAST + argument (the type). + 6. `whnf` the type to expose `.path`. + 7. Match `.path` with four args: `[ℓ, T_carrier, a_emb, b_emb]`. + 8. `whnf` `T_carrier` to expose `CubicalEmbed.ctype α inst`; + extract `(α, inst)`. + 9. `whnf` `a_emb` and `b_emb` to expose `CubicalEmbed.toCTerm` + applications; extract the underlying values. -/ +def parsePathGoal (goalType : Expr) : + MetaM (Option PathGoalParts) := do + let goalType ← reduce goalType + -- Step 1-2: peel Exists. + let (existsFn, existsArgs) := goalType.getAppFnArgs + if existsFn != ``Exists then + return none + if existsArgs.size < 2 then + return none + let predicate := existsArgs[1]! + -- Step 3: strip the lambda to get the body. The body has the + -- bound `t` as `bvar 0`. + if !predicate.isLambda then + return none + let body := predicate.bindingBody! + let body ← reduce body + -- Step 4-5: peel HasType. The encoding is + -- @HasType ctx t ℓ A + -- — four explicit (or some implicit) arguments. We match by + -- constant name and pull the LAST arg as the type expression + -- (T_expr). + let (hasTypeFn, hasTypeArgs) := body.getAppFnArgs + if hasTypeFn != ``HasType then + return none + if hasTypeArgs.size < 4 then + return none + -- Last arg is the CType. + let tExpr := hasTypeArgs[hasTypeArgs.size - 1]! + -- Step 6-7: peel CType.path. + let tExpr ← reduce tExpr + let (pathFn, pathArgs) := tExpr.getAppFnArgs + if pathFn != ``CType.path then + return none + if pathArgs.size < 4 then + return none + -- Args: [ℓ, T_carrier, a_emb, b_emb]. + let tCarrier := pathArgs[1]! + let aEmb := pathArgs[2]! + let bEmb := pathArgs[3]! + -- Step 8: extract α and inst from T_carrier. + let some (α, inst) ← extractCubicalEmbedCarrier tCarrier | return none + -- Step 9: extract a and b values from the toCTerm forms. + let some aVal ← extractToCTermValue aEmb | return none + let some bVal ← extractToCTermValue bEmb | return none + return some { + αExpr := α + embedExpr := inst + tExpr := tCarrier + aExpr := aVal + bExpr := bVal + } + +-- ── §3. Universe-level extraction helper ────────────────────────────────── + +/-- Extract the universe-level argument from a CType expression's + type. For `T : CType ℓ`, `inferType T` yields `CType ℓ`, and + we want `ℓ` as an Expr. Used by `synthCubicalSetC` and + `via_eq_contract` to fill in the `ℓ` argument to + `CubicalSetC ℓ T`. -/ +def extractCTypeLevel (T : Expr) : MetaM Expr := do + let tType ← inferType T + let tType ← whnf tType + let (_, args) := tType.getAppFnArgs + if args.size ≥ 1 then + return args[0]! + else + throwError "extractCTypeLevel: cannot extract universe level from {← ppExpr tType} (expected `CType ℓ`-shaped)" + +-- ── §4. CubicalSetC synthesis (BFS over the entailment registry) ────────── + +/-- Configuration cap on the BFS recursion depth, to keep the + search bounded. Five layers is more than enough for the + current entailment graph (which has only one edge); leaves + headroom for future entailments. -/ +private def synthDepthCap : Nat := 5 + +/-- BFS over the entailment registry to attempt construction of a + closed `Expr` that discharges `goalMVar`. + + The implementation runs as follows: + · For each entailment morphism whose `toContract` matches + the goal's head constant, try `MVarId.apply` with the + morphism's lemma. + · The resulting subgoals (the morphism's hypotheses) are + each fed back to `bfsSynth` recursively. + · Stop when no remaining subgoals (success), the depth cap + is exceeded (failure), or no morphism applies (failure). + + Returns `true` on success, `false` on failure. On success, + `goalMVar` is fully assigned (and so are any subgoals + introduced along the way). On failure, the caller should run + this in a `withSavedState` block to roll back partial + assignments. -/ +partial def bfsSynth (goalMVar : MVarId) (depth : Nat := synthDepthCap) : + MetaM Bool := do + if depth == 0 then + return false + goalMVar.withContext do + let goalType ← goalMVar.getType + let goalType ← whnf goalType + let (headFn, _) := goalType.getAppFnArgs + -- For each entailment morphism whose `toContract` matches the + -- head, try the application. + let candidates := entailmentRegistry.filter fun m => m.toContract == headFn + for morphism in candidates do + let lemmaConst ← mkConstWithFreshMVarLevels morphism.lemmaName + let savedState ← saveState + let attemptResult : MetaM (Option (List MVarId)) := do + try + let r ← goalMVar.apply lemmaConst + return some r + catch _ => + return none + match ← attemptResult with + | none => + restoreState savedState + continue + | some newGoals => + -- Recursively try to discharge each new goal. + let mut allDischarged := true + for ng in newGoals do + if !(← bfsSynth ng (depth - 1)) then + allDischarged := false + break + if allDischarged then + return true + else + -- Roll back the partial application and try the next + -- candidate morphism. + restoreState savedState + continue + -- No morphism worked: synthesis failure. + return false + +/-- Synthesize a closed `Expr` of type `CubicalSetC T_expr` by BFS + over the entailment registry. Returns `some witnessExpr` if + the synthesis succeeds, `none` otherwise. + + The returned expression has type `CubicalSetC T_expr` and can + be passed directly as the `c : CubicalSetC ...` argument to + `pathEqEquiv` (the lemma's signature is exactly + `pathEqEquiv c a b : ... ↔ a = b`). + + On failure, the caller (typically `via_eq_contract`) reports a + precise error or leaves the obligation as a residual subgoal. -/ +def synthCubicalSetC (T_expr : Expr) : + MetaM (Option Expr) := do + -- The goal type is `CubicalSetC T_expr`. Build the mvar and + -- run BFS. + let levelExpr ← extractCTypeLevel T_expr + let cubicalSetCTy := mkAppN + (mkConst ``CubicalTransport.Bridge.Set.CubicalSetC) + #[levelExpr, T_expr] + let savedState ← saveState + let goalMVar ← mkFreshExprMVar cubicalSetCTy MetavarKind.synthetic + if (← bfsSynth goalMVar.mvarId!) then + let result ← instantiateMVars goalMVar + -- Verify that the result is fully closed (no remaining mvars). + if (← getMVars result).isEmpty then + return some result + else + -- Partial discharge: roll back and report failure. + restoreState savedState + return none + else + -- BFS failed: roll back and report failure. + restoreState savedState + return none + +-- ── §5. via_eq_contract ─────────────────────────────────────────────────── + +/-- The `via_eq_contract` tactic. Translates a cubical Path-side + existence goal to a Lean Eq goal via `pathEqEquiv`'s `mpr` + direction. + + Expected goal shape: + `⊢ ∃ (t : CTerm), HasType [] t + (.path (CubicalEmbed.ctype (α := α)) + (CubicalEmbed.toCTerm a) + (CubicalEmbed.toCTerm b))` + + Behavior: + · Inspect the goal; throw a precise error if it doesn't + match this shape. + · Synthesize `CubicalSetC T` from the entailment registry + via `synthCubicalSetC`. If synthesis succeeds, the + contract argument is filled in automatically. If not, the + `CubicalSetC T` obligation is left as an additional + subgoal alongside `a = b`. + · Apply `Iff.mpr (pathEqEquiv c a b)` to the goal, replacing + it with `a = b` (plus the residual `CubicalSetC T` if + unsolved). +-/ +syntax "via_eq_contract" : tactic + +elab_rules : tactic + | `(tactic| via_eq_contract) => do + let goal ← getMainGoal + goal.withContext do + let goalType ← goal.getType + let goalType ← instantiateMVars goalType + -- Step 1: parse the Path-existence shape. + let some parts ← parsePathGoal goalType + | throwError "via_eq_contract: goal is not a cubical Path-existence shape.\n\ + Expected: ∃ t, HasType [] t (.path (CubicalEmbed.ctype) (CubicalEmbed.toCTerm a) (CubicalEmbed.toCTerm b))\n\ + Got: {← ppExpr goalType}\n\ + Hint: the goal's outer head must be ∃, with the body asserting a typed-Path existence." + -- Step 2: attempt to synthesize CubicalSetC T from the + -- registry. Record success/failure for the application + -- step that follows. + let synthesizedC ← synthCubicalSetC parts.tExpr + -- Step 3: build the application `Iff.mpr (pathEqEquiv ?c a b)`. + -- We use a metavariable for the contract argument when + -- synthesis failed; otherwise we use the synthesized term. + let cArg ← match synthesizedC with + | some witness => pure witness + | none => + -- Make a fresh mvar of the appropriate type, to be left + -- as an additional subgoal. + let levelExpr ← extractCTypeLevel parts.tExpr + let cubicalSetCTy := mkAppN + (mkConst ``CubicalTransport.Bridge.Set.CubicalSetC) + #[levelExpr, parts.tExpr] + mkFreshExprMVar cubicalSetCTy MetavarKind.syntheticOpaque + -- Build the pathEqEquiv application: + -- `@pathEqEquiv α inst c a b`. Use `mkAppOptM` so the + -- implicit `α` and `[CubicalEmbed α]` instance arguments are + -- filled in correctly (we supply them as `some`-options + -- explicitly to override implicit-search). + let equivApp ← mkAppOptM + ``CubicalTransport.Bridge.Set.pathEqEquiv + #[some parts.αExpr, some parts.embedExpr, some cArg, + some parts.aExpr, some parts.bExpr] + -- Apply `Iff.mpr` to flip the direction. `Iff.mpr` has the + -- signature `{a b : Prop} → (a ↔ b) → b → a`, so applying it + -- to `equivApp : (∃...) ↔ (a = b)` yields a function of type + -- `(a = b) → (∃...)`. Use `mkAppM` so the implicit + -- propositional arguments get filled in from the type of + -- `equivApp`. + let appliedTerm ← mkAppM ``Iff.mpr #[equivApp] + -- Apply to the main goal. `MVarId.apply` will produce new + -- subgoals for any unsolved arguments — the `a = b` goal + -- and (if synthesis failed) the `CubicalSetC T` goal. + let newGoals ← goal.apply appliedTerm + replaceMainGoal newGoals + +-- ── §6. find_contract_path ──────────────────────────────────────────────── + +/-- The `find_contract_path` tactic. Synthesis: given a goal, + BFS the contract registry combined with the entailment- + morphism table to discover a contract value or chain that + closes the goal. + + Goal shape (chosen interpretation, documented below): + + `⊢ involving a registered contract` + + The tactic tries each registered contract as a closed lemma + via `MVarId.applyConst`-style application. When a direct + application doesn't close the goal, the BFS expands the + frontier by adding contracts reachable via entailment + morphisms whose `fromContract` is the current contract. + + Why this shape: THEORY.md §0.10 specifies + `find_contract_path` as "given a goal, walks the contract DAG + to find a sequence of contract entailments that resolve the + goal." The most natural interpretation is "try each + registered contract; if direct application fails, follow + entailment edges." + + Behavior: + · Get the registry of all registered contract names. + · For each name, look up the entry; try + `MVarId.applyConst` of the contract's defining constant. + · BFS-expand by entailment morphisms. + · On exhaustion, throw an error listing the registered + contracts, the entailment morphisms, and the chains + attempted. +-/ +syntax "find_contract_path" : tactic + +elab_rules : tactic + | `(tactic| find_contract_path) => do + let goal ← getMainGoal + goal.withContext do + let goalType ← goal.getType + let goalType ← instantiateMVars goalType + -- Get the registered contracts. + let registered ← Contract.allRegistered + if registered.isEmpty && entailmentRegistry.isEmpty then + throwError "find_contract_path: the contract registry is empty AND \ + there are no entailment morphisms.\n\ + No contracts have been registered via `Contract.register` in any \ + module's `initialize` block.\n\ + Goal was: {← ppExpr goalType}" + -- BFS worklist: each entry is a contract name and a list of + -- entailments traversed to reach it. Start with all + -- registered contracts as seeds. + let mut visited : Std.HashSet Lean.Name := ∅ + let mut frontier : List (Lean.Name × List Lean.Name) := + registered.map fun n => (n, [n]) + let mut attemptedChains : List (List Lean.Name) := [] + let mut closed := false + while !frontier.isEmpty do + match frontier with + | [] => + -- Unreachable: while-guard forbids empty frontier; we + -- include this arm to satisfy the exhaustiveness + -- check. + break + | (n, chain) :: rest => + frontier := rest + if visited.contains n then + continue + visited := visited.insert n + attemptedChains := chain :: attemptedChains + let entry? ← Contract.lookupByName n + match entry? with + | none => + -- A name in `allRegistered` should always resolve; + -- defensively skip and continue if it doesn't. + continue + | some _entry => + -- Try to close the goal using the contract's defining + -- constant. `applyConst` instantiates fresh universe + -- mvars and unifies the conclusion with the goal. + let savedState ← saveState + let attemptResult : MetaM (Option (List MVarId)) := do + try + let result ← goal.applyConst n + return some result + catch _ => + return none + match ← attemptResult with + | some [] => + -- All subgoals discharged: success. + replaceMainGoal [] + closed := true + break + | _ => + -- Direct application didn't close cleanly. Roll back + -- and expand frontier by entailments from n. + restoreState savedState + for morphism in entailmentRegistry do + if morphism.fromContract == n && !visited.contains morphism.toContract then + frontier := frontier ++ [(morphism.toContract, morphism.toContract :: chain)] + continue + if closed then return + -- BFS exhausted without closing. + let registeredStr := registered.map fun n => s!"{n}" + let entailmentStr := entailmentRegistry.map fun m => + s!"{m.fromContract} → {m.toContract} (via {m.lemmaName})" + let attemptedStr := attemptedChains.map fun c => + String.intercalate " → " (c.map fun n => s!"{n}") + throwError "find_contract_path: contract synthesis failed.\n\ + Goal: {← ppExpr goalType}\n\ + Registered contracts ({registered.length}): {registeredStr}\n\ + Entailment morphisms ({entailmentRegistry.length}): {entailmentStr}\n\ + Chains attempted ({attemptedChains.length}): {attemptedStr}" + +-- ── §7. lift_via_topos ──────────────────────────────────────────────────── + +/-- The `lift_via_topos t` tactic. Bundled one-shot transport from + cubical-side to mathlib-side. + + Behavior: + 1. Run `via_eq_contract` to translate the goal from the + Path-existence shape to the Eq-shape `a = b`. + 2. Run the user-supplied tactic `t` on the translated goal. + + Effectively: `lift_via_topos t ≡ via_eq_contract; t`. -/ +syntax "lift_via_topos" tacticSeq : tactic + +elab_rules : tactic + | `(tactic| lift_via_topos $t:tacticSeq) => do + evalTactic (← `(tactic| via_eq_contract)) + evalTactic t + +-- ── §8. #contract command ───────────────────────────────────────────────── + +/-- The `#contract` command. Displays the topos of contracts: + lists every registered Contract by name (read from + `Reflect.Contract.allRegistered`), alongside the known + entailment morphisms (read from `entailmentRegistry`). + + Output format: + + Registered contracts (N): + • + • + ... + + Entailment morphisms (M): + • → (via ) + ... + + Used for human exploration of the contract registry's current + state. No side effects — pure read of the registry. -/ +syntax "#contract" : command + +elab_rules : command + | `(command| #contract) => do + let registered ← Contract.allRegistered + let mut msg : MessageData := m!"Registered contracts ({registered.length}):" + if registered.isEmpty then + msg := msg ++ m!"\n (none — call `Contract.register` in an `initialize` block to register one)" + else + for n in registered do + msg := msg ++ m!"\n • {n}" + msg := msg ++ m!"\n\nEntailment morphisms ({entailmentRegistry.length}):" + if entailmentRegistry.isEmpty then + msg := msg ++ m!"\n (none)" + else + for morphism in entailmentRegistry do + msg := msg ++ m!"\n • {morphism.fromContract} → {morphism.toContract} (via {morphism.lemmaName})" + logInfo msg + +-- ── §9. #whichContract command ─────────────────────────────────────────── + +/-- For `#whichContract`: given a contract name and a CType + expression, attempt synthesis of the contract's satisfaction + on the CType. Returns `true` if a witness can be constructed, + `false` otherwise. + + Currently a structural test: applies the contract function to + the CType and checks that the application typechecks (the + Reflect-registered contract entry has a level `e.level` and a + function `e.contract : CType e.level → CTerm`). Since the + contract function is just a Lean-level pure function, the + application succeeds iff the CType is at the right level. + + A stronger test (typed-satisfaction in the empty context) + requires the engine's HasType-checker, which lives outside + this module's scope. This implementation is intentionally a + structural filter, suitable for `#whichContract`'s "list + candidate contracts" purpose. -/ +def attemptSynthesis (contractName : Lean.Name) + (TE : Expr) : MetaM Bool := do + -- Look up the contract entry. + let entry? ← Contract.lookupByName contractName + match entry? with + | none => + -- Unknown contract — synthesis cannot succeed. + return false + | some _entry => + -- Structural test: try to apply the contract's defining Lean + -- constant to the CType expression. If this elaborates + -- without error, the contract is structurally applicable. + let cExpr ← mkConstWithFreshMVarLevels contractName + let appExpr := mkApp cExpr TE + try + -- `inferType` will succeed iff the application is + -- well-typed, i.e. the contract's CType-level matches the + -- input's level. + let _ ← inferType appExpr + return true + catch _ => + return false + +/-- The `#whichContract ` command. Given a CType + expression, lists the registered contracts that apply to it + (per `attemptSynthesis`). + + Output format: + + satisfies (K of N contracts): + • + • + ... + + or, if no contracts apply: + + No registered contract is satisfied by . + + Used to discover what contracts a CType participates in. Pure + read of the registry plus a structural per-contract test. -/ +syntax "#whichContract" term : command + +elab_rules : command + | `(command| #whichContract $T:term) => do + -- Elaborate the CType expression in the command context. + -- Use `liftTermElabM` to bridge from `CommandElabM` to + -- `TermElabM`. + let TE ← liftTermElabM do + Term.elabTerm T none + -- Run the synthesis attempt for each registered contract. + let registered ← Contract.allRegistered + let mut satisfied : List Lean.Name := [] + for n in registered do + let ok ← liftTermElabM do + attemptSynthesis n TE + if ok then + satisfied := satisfied ++ [n] + let TEStr ← liftTermElabM do + let fmt ← Lean.Meta.ppExpr TE + return fmt.pretty + if satisfied.isEmpty then + logInfo m!"No registered contract is satisfied by {TEStr}." + else + let mut msg : MessageData := + m!"{TEStr} satisfies ({satisfied.length} of {registered.length} contracts):" + for n in satisfied do + msg := msg ++ m!"\n • {n}" + logInfo msg + +end CubicalTransport.Tactic.EqContract