Pantograph/docs/agent-search.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "ec3abb52-d7cd-471f-b3b7-2d9681c79360",
   "metadata": {},
   "source": [
    "# Search\n",
    "\n",
    "Pantograph supports basic proof search. In this case, Pantograph treats goals as nodes on an and-or tree. The user supplies an agent which should provide two functions:\n",
    "\n",
    "1. *Tactic*: Which tactic should be used on a goal?\n",
    "2. *Guidance*: What is the search priority on a goal?\n",
    "\n",
    "The user agent should inherit from `pantograph.search.Agent`. Here is a brute force agent example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "959458f5-02e4-4f73-ae28-16a756aebed9",
   "metadata": {},
   "outputs": [],
   "source": [
    "from typing import Optional\n",
    "import collections\n",
    "from pantograph import Server\n",
    "from pantograph.search import Agent\n",
    "from pantograph.expr import GoalState, Tactic"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "8b402602-3ae5-43e4-9a62-2fa9e2c039fa",
   "metadata": {},
   "outputs": [],
   "source": [
    "class DumbAgent(Agent):\n",
    "\n",
    "    def __init__(self):\n",
    "        super().__init__()\n",
    "\n",
    "        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)\n",
    "        self.intros = [\n",
    "            \"intro\",\n",
    "        ]\n",
    "        self.tactics = [\n",
    "            \"intro h\",\n",
    "            \"cases h\",\n",
    "            \"apply Or.inl\",\n",
    "            \"apply Or.inr\",\n",
    "        ]\n",
    "        self.no_space_tactics = [\n",
    "            \"assumption\",\n",
    "        ]\n",
    "\n",
    "    def next_tactic(\n",
    "            self,\n",
    "            state: GoalState,\n",
    "            goal_id: int,\n",
    "    ) -> Optional[Tactic]:\n",
    "        key = (state.state_id, goal_id)\n",
    "        i = self.goal_tactic_id_map[key]\n",
    "\n",
    "        target = state.goals[goal_id].target\n",
    "        if target.startswith('∀'):\n",
    "            tactics = self.intros\n",
    "        elif ' ' in target:\n",
    "            tactics = self.tactics\n",
    "        else:\n",
    "            tactics = self.no_space_tactics\n",
    "\n",
    "        if i >= len(tactics):\n",
    "            return None\n",
    "\n",
    "        self.goal_tactic_id_map[key] = i + 1\n",
    "        return tactics[i]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "665db9d0-5fff-4b26-9cea-32d06a6e1e04",
   "metadata": {},
   "source": [
    "Execute the search with `agent.search`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "1c7961d1-b1fa-498c-ab75-16feb784ca2c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16)"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "server = Server()\n",
    "agent = DumbAgent()\n",
    "goal_state = server.goal_start(\"∀ (p q: Prop), Or p q -> Or q p\")\n",
    "agent.search(server=server, goal_state=goal_state, verbose=False)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "141e0116-cbb6-4957-aaea-2a1100f80ece",
   "metadata": {},
   "source": [
    "## Automatic and Manual Modes\n",
    "\n",
    "The agent chooses one goal and executes a tactic on this goal. What happens to the other goals that are not chosen? By default, the server runs in automatic mode. In automatic mode, all other goals are automatically inherited by a child state, so a user agent could declare a proof finished when there are no more goals remaining in the current goal state.\n",
    "\n",
    "Some users may wish to handle sibling goals manually. For example, Aesop's treatment of metavariable coupling is not automatic. To do this, pass the flag `options={ \"automaticMode\" : False }` to the `Server` constructor."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2090e538-d196-4923-937c-b83fedf1d9a2",
   "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.12.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}