/* global React, Shape, Peek, Cite, ENT */
const { useState: useStatePf } = React;

function ProofPage({ peekPattern = "drawer" }) {
  const [view, setView] = useStatePf("seq"); // 'seq' | 'tree'
  const [treeMode, setTreeMode] = useStatePf("outline"); // 'outline' | 'graph'
  const [peeked, setPeeked] = useStatePf(null);
  const open = (e) => setPeeked(e);
  const close = () => setPeeked(null);

  const steps = [
    {
      n: "01", stmt: "Form the difference quotient at x.",
      math: "(f∘g)(x+h) − (f∘g)(x)\n―――――――――――――――――\n        h",
      comm: "Direct from the definition.",
      just: { rule: "def.calc.derivative", note: "Limit of this expression as h → 0 is, by definition, (f∘g)′(x)." }
    },
    {
      n: "02", stmt: "Multiply numerator and denominator by Δg = g(x+h) − g(x), assuming Δg ≠ 0 in a punctured neighborhood of x.",
      math: "f(g(x+h)) − f(g(x))     g(x+h) − g(x)\n―――――――――――――――――  ·  ―――――――――――――\n  g(x+h) − g(x)              h",
      comm: "The Δg = 0 case is handled in step 06.",
      just: { rule: "algebraic identity", note: "Multiplying by 1 in the form Δg / Δg is valid because Δg ≠ 0." }
    },
    {
      n: "03", current: true,
      stmt: "Recognize the first factor as the difference quotient of f at g(x), with increment Δg.",
      math: "lim_{h→0}  [f(g(x)+Δg) − f(g(x))] / Δg",
      comm: "As h→0, Δg → 0 by continuity of g (which differentiability implies).",
      just: { rule: "thm.calc.diff_implies_cont", note: "Differentiability ⟹ continuity. So Δg→0 follows from h→0." }
    },
    {
      n: "04", stmt: "Take the limit. The first factor → f′(g(x)); the second → g′(x).",
      math: "= f′(g(x)) · g′(x)",
      comm: "Apply the product-of-limits law since both limits exist.",
      just: { rule: "thm.calc.limit_product", note: "lim(AB) = (lim A)(lim B) when both factors converge." }
    },
    {
      n: "05", stmt: "Edge case: Δg = 0 for h arbitrarily close to 0.",
      math: "(f∘g)′(x) = f′(g(x)) · 0 = 0",
      comm: "If Δg vanishes infinitely often, then g′(x) = 0, and the composition's difference quotient is 0 there too.",
      just: { rule: "Carathéodory characterization", note: "A standard workaround; see lem.calc.caratheodory." }
    },
  ];

  return (
    <div className="pf" style={{ position: "relative", minHeight: "100%" }}>
      <header className="pf__top">
        <div style={{ display: "flex", alignItems: "center", gap: 10 }}>
          <span className="t-mono" style={{ fontSize: 11, color: "var(--ink-4)" }}>← chain rule</span>
        </div>
        <div style={{ display: "flex", alignItems: "center", gap: 12 }}>
          <span className="type-chip" style={{ borderColor: "var(--ink)" }}>
            <span style={{ display: "inline-block", width: 9, height: 9, background: "var(--ink)" }}></span>
            <span>proof</span>
          </span>
          <span className="t-mono" style={{ fontSize: 11, color: "var(--ink-4)" }}>pf.calc.chain_rule.0</span>
          <div className="pf__viewseg">
            <button className={`pf__viewseg-btn ${view === "seq" ? "is-on" : ""}`} onClick={() => setView("seq")}>sequential</button>
            <button className={`pf__viewseg-btn ${view === "tree" ? "is-on" : ""}`} onClick={() => setView("tree")}>tree</button>
          </div>
        </div>
      </header>

      <section className="pf__hero">
        <div className="pf__target-label">proof of</div>
        <div className="pf__target">
          (f ∘ g)′(x) = f′(g(x)) · g′(x), &nbsp;under <Cite entity={ENT.diffAtPoint} onPeek={open} /> of f at g(x) and of g at x.
        </div>
        <div className="pf__meta-row">
          <span><strong style={{ color: "var(--ink)" }}>strategy</strong> &nbsp;direct from definition</span>
          <span><strong style={{ color: "var(--ink)" }}>length</strong> &nbsp;7 steps · ~6 min read</span>
          <span><strong style={{ color: "var(--ink)" }}>citations</strong> &nbsp;3 def · 2 thm · 1 lem</span>
          <span><strong style={{ color: "var(--ink)" }}>your progress</strong> &nbsp;<span style={{ color: "var(--accent)" }}>step 03 / 7</span></span>
        </div>
      </section>

      {view === "seq" && (
        <div className="pf__seq">
          {steps.map((s, i) => (
            <div key={i} className={`pf__step ${s.current ? "pf__step--current" : ""}`}>
              <div className="pf__step-n">{s.n}</div>
              <div className="pf__step-body">
                <div className="pf__step-stmt">{s.stmt}</div>
                <div style={{
                  fontFamily: "var(--font-text)", fontSize: 19,
                  whiteSpace: "pre", padding: "10px 14px",
                  background: "var(--paper-2)", borderLeft: "2px solid var(--ink-4)"
                }}>{s.math}</div>
                <div className="pf__step-comm">— {s.comm}</div>
              </div>
              <div className="pf__step-just">
                <span className="pf__step-just-h">justified by</span>
                <span className="t-mono" style={{ color: "var(--accent)", fontSize: 11 }}>{s.just.rule}</span>
                <span className="pf__step-just-body">{s.just.note}</span>
              </div>
            </div>
          ))}
          <div style={{ padding: "14px 0", textAlign: "center", color: "var(--ink-4)",
            fontFamily: "var(--font-mono)", fontSize: 11, letterSpacing: "0.1em",
            textTransform: "uppercase", borderBottom: "1px solid var(--rule-3)" }}>
            — 2 more steps · combine cases —
          </div>
          <div className="pf__qed">
            <span className="pf__qed-mark"></span>
            <span style={{ fontWeight: 500 }}>Q.E.D.</span>
            <span style={{ color: "var(--ink-4)", marginLeft: "auto", fontFamily: "var(--font-mono)", fontSize: 11 }}>
              7 steps · 1 edge case · 6 cited entities
            </span>
          </div>
        </div>
      )}

      {view === "tree" && (
        <div className="pf__tree">
          <div className="pf__tree-mode">
            <button className={treeMode === "outline" ? "is-on" : ""} onClick={() => setTreeMode("outline")}>outline</button>
            <button className={treeMode === "graph" ? "is-on" : ""} onClick={() => setTreeMode("graph")}>graph</button>
          </div>

          {treeMode === "outline" ? (
            <div className="pf__outline">
              {[
                ["1", "Set up the difference quotient", "step", "l1"],
                ["1.1", "Apply def.calc.derivative", "cite", "l2"],
                ["1.2", "Substitute composition (f∘g)(x) = f(g(x))", "step", "l2"],
                ["2", "Reduce to a product of difference quotients", "step", "l1"],
                ["2.1", "Multiply by Δg / Δg, assuming Δg ≠ 0", "step", "l2"],
                ["2.2", "Identify f's difference quotient with increment Δg", "step", "l2"],
                ["2.2.1", "Use thm.calc.diff_implies_cont so Δg → 0 as h → 0", "cite", "l3"],
                ["3", "Pass to the limit", "step", "l1"],
                ["3.1", "Apply thm.calc.limit_product", "cite", "l2"],
                ["3.2", "First factor → f′(g(x)); second → g′(x)", "step", "l2"],
                ["4", "Handle the edge case Δg = 0 frequently near x", "step", "l1"],
                ["4.1", "Apply lem.calc.caratheodory", "cite", "l2"],
                ["5", "Combine cases · QED", "step", "l1"],
              ].map(([n, t, kind, lvl]) => (
                <div key={n} className={`pf__outline-item pf__outline-item--${lvl}`}>
                  <span className="t-mono" style={{ color: kind === "cite" ? "var(--accent)" : "var(--ink-4)" }}>{n}</span>
                  <span>{t}</span>
                  <span className="t-mono" style={{ fontSize: 10, color: "var(--ink-4)" }}>{kind}</span>
                </div>
              ))}
            </div>
          ) : (
            <svg viewBox="0 0 920 460" className="pf__svg-tree">
              {/* Tree of dependencies — nodes are theorems/defs the proof rests on */}
              {/* Root: the proof */}
              <g>
                <rect x={400} y={30} width={120} height={36} fill="var(--ink)" />
                <text x={460} y={53} textAnchor="middle" fill="var(--paper)" fontFamily="var(--font-mono)" fontSize="11">
                  pf.chain_rule
                </text>
              </g>

              {/* Edges */}
              {[
                [460, 66, 140, 130], [460, 66, 320, 130], [460, 66, 500, 130], [460, 66, 680, 130], [460, 66, 820, 130],
                [140, 158, 80, 230], [140, 158, 200, 230],
                [320, 158, 280, 230], [320, 158, 380, 230],
                [500, 158, 500, 230],
                [680, 158, 640, 230], [680, 158, 740, 230],
                [820, 158, 820, 230],
                [80, 258, 80, 360], [200, 258, 200, 360],
                [380, 258, 380, 360], [500, 258, 500, 360], [640, 258, 640, 360], [740, 258, 740, 360],
              ].map(([x1, y1, x2, y2], i) => (
                <line key={i} x1={x1} y1={y1} x2={x2} y2={y2} stroke="var(--ink-4)" strokeWidth="1" />
              ))}

              {/* L1 — proof skeleton */}
              {[
                [80, 130, "step 01"], [260, 130, "step 02"], [440, 130, "step 03"],
                [620, 130, "step 04"], [760, 130, "step 05"]
              ].map(([x, y, t], i) => (
                <g key={i}>
                  <rect x={x} y={y} width={120} height={28} fill="var(--paper)" stroke="var(--ink-3)" />
                  <text x={x + 60} y={y + 18} textAnchor="middle" fontFamily="var(--font-mono)" fontSize="10" fill="var(--ink-2)">{t}</text>
                </g>
              ))}

              {/* L2 — cited rules (circles for defs, squares for theorems) */}
              {[
                [80, 230, "circle", "def.deriv"], [200, 230, "square", "alg.id"],
                [320, 230, "square", "limit_prod"], [440, 230, "square", "diff⟹cont"],
                [560, 230, "circle", "limit"], [680, 230, "square", "factor"],
                [800, 230, "square", "caratheo"]
              ].map(([x, y, sh, t], i) => (
                <g key={"l2-" + i}>
                  {sh === "circle"
                    ? <circle cx={x + 30} cy={y + 14} r="14" fill="var(--ink)" />
                    : <rect x={x + 16} y={y} width={28} height={28} fill="var(--ink)" />}
                  <text x={x + 30} y={y + 50} textAnchor="middle" fontFamily="var(--font-mono)" fontSize="10" fill="var(--ink-3)">{t}</text>
                </g>
              ))}
            </svg>
          )}
        </div>
      )}

      <Peek pattern={peekPattern} entity={peeked} onClose={close} />
    </div>
  );
}

window.ProofPage = ProofPage;
