scripts/demo-lean4.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "829b7005",
   "metadata": {},
   "source": [
    "LeanDojo Demo\n",
    "=============\n",
    "\n",
    "This notebook demonstrates the main features of LeanDojo (using Lean 4). Please refer to the [documentation](https://leandojo.readthedocs.io/en/latest/) for more details."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "f3c23856",
   "metadata": {},
   "outputs": [],
   "source": [
    "from lean_dojo import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7d400df8",
   "metadata": {},
   "source": [
    "## Extract Data from Lean"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "ef2ab5b2",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5')"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "repo = LeanGitRepo(\n",
    "    \"https://github.com/leanprover-community/mathlib4\",\n",
    "    \"29dcec074de168ac2bf835a77ef68bbe069194c5\",\n",
    ")\n",
    "\n",
    "repo"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "dd959495",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Expected behavior: this line should open another tab and take you to the website of the repo to be traced.\n",
    "repo.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "4c2945c2",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'content': 'leanprover/lean4:v4.10.0-rc1\\n'}"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "repo.get_config(\"lean-toolchain\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "1a9c39cc",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[32m2024-07-02 12:59:44.406\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m246\u001b[0m - \u001b[1mLoading the traced repo from /private/home/kaiyuy/.cache/lean_dojo/leanprover-community-mathlib4-29dcec074de168ac2bf835a77ef68bbe069194c5/mathlib4\u001b[0m\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "2024-07-02 12:59:48,851\tINFO worker.py:1761 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
      "100%|██████████| 5674/5674 [11:37<00:00,  8.13it/s]  \n"
     ]
    }
   ],
   "source": [
    "# A few minutes if the traced repo is in the cache; many hours otherwise.\n",
    "traced_repo = trace(repo)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "25ccf173",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<networkx.classes.digraph.DiGraph at 0x7f0d08727e80>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "traced_repo.traced_files_graph"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "375023d4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "5674"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(traced_repo.traced_files)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "1c725a11",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TracedFile(root_dir=PosixPath('/private/home/kaiyuy/.cache/lean_dojo/leanprover-community-mathlib4-29dcec074de168ac2bf835a77ef68bbe069194c5/mathlib4'), repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5'), lean_file=LeanFile(path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean')))"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "traced_file = traced_repo.get_traced_file(\"Mathlib/Algebra/BigOperators/Pi.lean\")\n",
    "\n",
    "traced_file"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "153f37ce",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{'full_name': 'Pi.list_prod_apply',\n",
       "  'code': '@[to_additive]\\ntheorem list_prod_apply {α : Type*} {β : α → Type*} [∀ a, Monoid (β a)] (a : α)\\n    (l : List (∀ a, β a)) : l.prod a = (l.map fun f : ∀ a, β a ↦ f a).prod',\n",
       "  'start': [22, 1],\n",
       "  'end': [25, 38],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Pi.multiset_prod_apply',\n",
       "  'code': '@[to_additive]\\ntheorem multiset_prod_apply {α : Type*} {β : α → Type*} [∀ a, CommMonoid (β a)] (a : α)\\n    (s : Multiset (∀ a, β a)) : s.prod a = (s.map fun f : ∀ a, β a ↦ f a).prod',\n",
       "  'start': [29, 1],\n",
       "  'end': [32, 42],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Finset.prod_apply',\n",
       "  'code': '@[to_additive (attr := simp)]\\ntheorem Finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (a : α)\\n    (s : Finset γ) (g : γ → ∀ a, β a) : (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a',\n",
       "  'start': [38, 1],\n",
       "  'end': [41, 38],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Finset.prod_fn',\n",
       "  'code': '@[to_additive \"An \\'unapplied\\' analogue of `Finset.sum_apply`.\"]\\ntheorem Finset.prod_fn {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (s : Finset γ)\\n    (g : γ → ∀ a, β a) : ∏ c ∈ s, g c = fun a ↦ ∏ c ∈ s, g c a',\n",
       "  'start': [45, 1],\n",
       "  'end': [49, 41],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Fintype.prod_apply',\n",
       "  'code': '@[to_additive]\\ntheorem Fintype.prod_apply {α : Type*} {β : α → Type*} {γ : Type*} [Fintype γ]\\n    [∀ a, CommMonoid (β a)] (a : α) (g : γ → ∀ a, β a) : (∏ c, g c) a = ∏ c, g c a',\n",
       "  'start': [53, 1],\n",
       "  'end': [56, 36],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'prod_mk_prod',\n",
       "  'code': '@[to_additive prod_mk_sum]\\ntheorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α)\\n    (g : γ → β) : (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)',\n",
       "  'start': [60, 1],\n",
       "  'end': [64, 88],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'pi_eq_sum_univ',\n",
       "  'code': 'theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [Semiring R]\\n    (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0',\n",
       "  'start': [68, 1],\n",
       "  'end': [72, 7],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Finset.univ_prod_mulSingle',\n",
       "  'code': '@[to_additive]\\ntheorem Finset.univ_prod_mulSingle [Fintype I] (f : ∀ i, Z i) :\\n    (∏ i, Pi.mulSingle i (f i)) = f',\n",
       "  'start': [80, 1],\n",
       "  'end': [84, 7],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'MonoidHom.functions_ext',\n",
       "  'code': '@[to_additive]\\ntheorem MonoidHom.functions_ext [Finite I] (G : Type*) [CommMonoid G] (g h : (∀ i, Z i) →* G)\\n    (H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h',\n",
       "  'start': [88, 1],\n",
       "  'end': [94, 16],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': \"MonoidHom.functions_ext'\",\n",
       "  'code': '@[to_additive (attr := ext)\\n      \"\\\\nThis is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons\\n      explained in note [partially-applied ext lemmas].\"]\\ntheorem MonoidHom.functions_ext\\' [Finite I] (M : Type*) [CommMonoid M] (g h : (∀ i, Z i) →* M)\\n    (H : ∀ i, g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)) : g = h',\n",
       "  'start': [98, 1],\n",
       "  'end': [105, 56],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'RingHom.functions_ext',\n",
       "  'code': '@[ext]\\ntheorem RingHom.functions_ext [Finite I] (G : Type*) [NonAssocSemiring G] (g h : (∀ i, f i) →+* G)\\n    (H : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h',\n",
       "  'start': [118, 1],\n",
       "  'end': [122, 72],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Prod.fst_prod',\n",
       "  'code': '@[to_additive]\\ntheorem fst_prod : (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1',\n",
       "  'start': [131, 1],\n",
       "  'end': [133, 35],\n",
       "  'kind': 'commanddeclaration'},\n",
       " {'full_name': 'Prod.snd_prod',\n",
       "  'code': '@[to_additive]\\ntheorem snd_prod : (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2',\n",
       "  'start': [137, 1],\n",
       "  'end': [139, 35],\n",
       "  'kind': 'commanddeclaration'}]"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "traced_file.get_premise_definitions()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "77e58935",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "13"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "traced_theorems = traced_file.get_traced_theorems()\n",
    "\n",
    "len(traced_theorems)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "00042165",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TracedTheorem(theorem=Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5'), file_path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean'), full_name='pi_eq_sum_univ'))"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "thm = traced_file.get_traced_theorem(\"pi_eq_sum_univ\")\n",
    "\n",
    "thm"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "4d9ed905",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Expected behavior: this line should open another tab and take you to the website of the traced theorem.\n",
    "thm.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "eafb6369",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5'), file_path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean'), full_name='pi_eq_sum_univ')"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "thm.theorem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "5e00cba9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((69, 1), (72, 7))"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "thm.start, thm.end"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "14c611f4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "thm.has_tactic_proof()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "24bc67e9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "thm.get_num_tactics()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "3fa19ef3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "by\n",
      "  ext\n",
      "  simp\n"
     ]
    }
   ],
   "source": [
    "proof_node = thm.get_proof_node()\n",
    "proof = proof_node.lean_file[proof_node.start : proof_node.end]\n",
    "print(proof)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "1fae1876",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[TracedTactic(tactic=ext, state_before=ι : Type u_1\n",
       " inst✝² : Fintype ι\n",
       " inst✝¹ : DecidableEq ι\n",
       " R : Type u_2\n",
       " inst✝ : Semiring R\n",
       " x : ι → R\n",
       " ⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0, state_after=case h\n",
       " ι : Type u_1\n",
       " inst✝² : Fintype ι\n",
       " inst✝¹ : DecidableEq ι\n",
       " R : Type u_2\n",
       " inst✝ : Semiring R\n",
       " x : ι → R\n",
       " x✝ : ι\n",
       " ⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝),\n",
       " TracedTactic(tactic=simp, state_before=case h\n",
       " ι : Type u_1\n",
       " inst✝² : Fintype ι\n",
       " inst✝¹ : DecidableEq ι\n",
       " R : Type u_2\n",
       " inst✝ : Semiring R\n",
       " x : ι → R\n",
       " x✝ : ι\n",
       " ⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝, state_after=no goals)]"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "traced_tactics = thm.get_traced_tactics()\n",
    "\n",
    "traced_tactics"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "39fbe993",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TracedTactic(tactic=simp, state_before=case h\n",
       "ι : Type u_1\n",
       "inst✝² : Fintype ι\n",
       "inst✝¹ : DecidableEq ι\n",
       "R : Type u_2\n",
       "inst✝ : Semiring R\n",
       "x : ι → R\n",
       "x✝ : ι\n",
       "⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝, state_after=no goals)"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tac = traced_tactics[1]\n",
    "\n",
    "tac"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "84b1c8b6",
   "metadata": {},
   "source": [
    "## Interact with Lean Programmatically"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "f3d3f736",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5')"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "repo"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fb39a5a0",
   "metadata": {},
   "source": [
    "### Interact through Tactics"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "10364e0f",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[32m2024-07-02 13:12:29.881\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m147\u001b[0m - \u001b[33m\u001b[1mRunning tactics without a hard timeout may hang indefinitely.\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "theorem = Theorem(repo, \"Mathlib/Algebra/BigOperators/Pi.lean\", \"pi_eq_sum_univ\")\n",
    "\n",
    "# For some theorems, it might take a few minutes.\n",
    "dojo, state_0 = Dojo(theorem).__enter__()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "a7d4ad9a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "TacticState(pp='ι : Type u_1\\ninst✝² : Fintype ι\\ninst✝¹ : DecidableEq ι\\nR : Type u_2\\ninst✝ : Semiring R\\nx : ι → R\\n⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0', id=0, message=None)"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state_0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "af88893b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "ι : Type u_1\n",
      "inst✝² : Fintype ι\n",
      "inst✝¹ : DecidableEq ι\n",
      "R : Type u_2\n",
      "inst✝ : Semiring R\n",
      "x : ι → R\n",
      "⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n"
     ]
    }
   ],
   "source": [
    "print(state_0.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "4ca2dca9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "ι : Type u_1\n",
      "inst✝² : Fintype ι\n",
      "inst✝¹ : DecidableEq ι\n",
      "R : Type u_2\n",
      "inst✝ : Semiring R\n",
      "⊢ ∀ (x : ι → R), x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n"
     ]
    }
   ],
   "source": [
    "state_1 = dojo.run_tac(state_0, \"revert x\")\n",
    "\n",
    "print(state_1.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "89a62c89",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "LeanError(error='<stdin>:1:1: unknown tactic')"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state_2 = dojo.run_tac(state_0, \"hello world!\")\n",
    "\n",
    "state_2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "10b5f013",
   "metadata": {},
   "outputs": [
    {
     "ename": "RuntimeError",
     "evalue": "Attempting to run a tactic on an invalid state LeanError(error='<stdin>:1:1: unknown tactic').",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mRuntimeError\u001b[0m                              Traceback (most recent call last)",
      "Cell \u001b[0;32mIn[28], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mdojo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrun_tac\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstate_2\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mskip\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m)\u001b[49m\n",
      "File \u001b[0;32m~/LeanDojo/src/lean_dojo/interaction/dojo.py:360\u001b[0m, in \u001b[0;36mDojo.run_tac\u001b[0;34m(self, state, tactic)\u001b[0m\n\u001b[1;32m    358\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrun_tac\u001b[39m(\u001b[38;5;28mself\u001b[39m, state: TacticState, tactic: \u001b[38;5;28mstr\u001b[39m) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m TacticResult:\n\u001b[1;32m    359\u001b[0m     \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(state, TacticState):\n\u001b[0;32m--> 360\u001b[0m         \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\n\u001b[1;32m    361\u001b[0m             \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mAttempting to run a tactic on an invalid state \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mstate\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m.\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    362\u001b[0m         )\n\u001b[1;32m    363\u001b[0m     \u001b[38;5;28;01massert\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(tactic, \u001b[38;5;28mstr\u001b[39m), \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mInvalid tactic \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mtactic\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    365\u001b[0m     tsid \u001b[38;5;241m=\u001b[39m state\u001b[38;5;241m.\u001b[39mid\n",
      "\u001b[0;31mRuntimeError\u001b[0m: Attempting to run a tactic on an invalid state LeanError(error='<stdin>:1:1: unknown tactic')."
     ]
    }
   ],
   "source": [
    "dojo.run_tac(state_2, \"skip\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "65bae6ea",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "ProofGivenUp()"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_tac(state_0, \"sorry\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "c373865a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "ι : Type u_1\n",
      "inst✝² : Fintype ι\n",
      "inst✝¹ : DecidableEq ι\n",
      "R : Type u_2\n",
      "inst✝ : Semiring R\n",
      "x : ι → R\n",
      "⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n"
     ]
    }
   ],
   "source": [
    "print(state_0.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "a5d0156f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "case h\n",
      "ι : Type u_1\n",
      "inst✝² : Fintype ι\n",
      "inst✝¹ : DecidableEq ι\n",
      "R : Type u_2\n",
      "inst✝ : Semiring R\n",
      "x : ι → R\n",
      "x✝ : ι\n",
      "⊢ x x✝ = (∑ i : ι, x i • fun j => if i = j then 1 else 0) x✝\n"
     ]
    }
   ],
   "source": [
    "state_3 = dojo.run_tac(state_0, \"ext\")\n",
    "\n",
    "print(state_3.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "71ab5854",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "ProofFinished(tactic_state_id=3, message='')\n"
     ]
    }
   ],
   "source": [
    "state_4 = dojo.run_tac(state_3, \"simp\")\n",
    "\n",
    "print(state_4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "fdb44496",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.is_successful"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ca87e34",
   "metadata": {},
   "source": [
    "### Interact through Commands"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "243ea43c",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[32m2024-07-02 13:12:55.056\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m147\u001b[0m - \u001b[33m\u001b[1mRunning tactics without a hard timeout may hang indefinitely.\u001b[0m\n"
     ]
    }
   ],
   "source": [
    "entry = (repo, \"Mathlib/Algebra/Module/Equiv.lean\", 953)  # (repo, file_path, line_nb)\n",
    "dojo, state_0 = Dojo(entry).__enter__()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "5ebd615c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CommandState(id=0, message=None)"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state_0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "b1e079fa",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CommandState(id=1, message='1')"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_cmd(state_0, \"#eval 1\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "31c9bada",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "LeanError(error=\"unknown identifier 'x'\")"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_cmd(state_0, \"#eval x\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "b638bfbf",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CommandState(id=3, message='')"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state_1 = dojo.run_cmd(state_0, \"def x := 1\")\n",
    "\n",
    "state_1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "bdc4f14d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CommandState(id=4, message='1')"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_cmd(state_1, \"#eval x\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "ef47afb8",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CommandState(id=5, message='addMonoidHomLequivNat.{u_17, u_18, u_19} {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommMonoid A]\\n[AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B')"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_cmd(state_0, \"#check addMonoidHomLequivNat\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "c6b8b9a5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "LeanError(error=\"unknown identifier 'addMonoidEndRingEquivInt'\")"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dojo.run_cmd(state_0, \"#check addMonoidEndRingEquivInt\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "791875ec",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.14"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}