{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "c5106980-4850-4bea-a333-5a1b2e4d1dc5",
   "metadata": {},
   "source": [
    "# Goals and Tactics\n",
    "\n",
    "Executing tactics in Pantograph is simple. To start a proof, call the\n",
    "`Server.goal_start` function and supply an expression."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "3257de2b-41ca-4cfe-b66c-1ef4781c98b0",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pantograph import Server\n",
    "from pantograph.expr import TacticHave, TacticCalc, TacticExpr"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "6783d478-d8c7-4c4e-a56e-8170384297ef",
   "metadata": {},
   "outputs": [],
   "source": [
    "server = Server()\n",
    "state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bfe5a9df-33c2-4538-a9ce-fc0e02c92ff2",
   "metadata": {},
   "source": [
    "This creates a *goal state*, which consists of a finite number of goals. In this\n",
    "case since it is the beginning of a state, it has only one goal."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "eefc9094-9574-4f92-9aa2-c39beb85389b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "⊢ forall (p q: Prop), Or p q -> Or q p\n"
     ]
    }
   ],
   "source": [
    "print(state0)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "26dbe212-e09e-42dd-ab15-65ee2fba6234",
   "metadata": {},
   "source": [
    "To execute a tactic on a goal state, use `Server.goal_tactic`. This function\n",
    "takes a goal id and a tactic. Most Lean tactics are strings."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c907dbb6-4d6a-4aa7-b173-60220165ba9e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "a : Prop\n",
      "⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
     ]
    }
   ],
   "source": [
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro a\")\n",
    "print(state1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9978fdcf-a12b-4f22-9551-5e04c262e5e0",
   "metadata": {},
   "source": [
    "Executing a tactic produces a new goal state. If this goal state has no goals,\n",
    "the proof is complete. You can recover the usual form of a goal with `str()`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "16595c5e-2285-49d5-8340-397ad1e6c9e7",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'a : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a'"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "str(state1.goals[0])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67f2a75d-6851-4393-bac9-a091400f1906",
   "metadata": {},
   "source": [
    "## Error Handling and GC\n",
    "\n",
    "When a tactic fails, it throws an exception:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "c9784ba2-3810-4f80-a6c4-33d5eef3003e",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\"tactic 'assumption' failed\\na : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a\"]\n"
     ]
    }
   ],
   "source": [
    "try:\n",
    "    state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
    "    print(\"Should not reach this\")\n",
    "except Exception as e:\n",
    "    print(e)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1ae60d9e-8656-4f26-b495-d04bced250fc",
   "metadata": {},
   "source": [
    "A state with no goals is considered solved"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "1cb96b19-d3bb-4533-abeb-a7dbc5bc8c3e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "GoalState(state_id=5, goals=[], _sentinel=[0, 1])"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
    "state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
    "state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
    "state3"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a2945e71-e583-4ae0-9c0f-83035f0492f2",
   "metadata": {},
   "source": [
    "Execute `server.gc()` once in a while to delete unused goals."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "d53624ff-c720-4847-98f7-28e109eb76e7",
   "metadata": {},
   "outputs": [],
   "source": [
    "server.gc()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0b59e05e-7d8c-4fad-b8ca-375ea995ea5b",
   "metadata": {},
   "source": [
    "## Special Tactics\n",
    "\n",
    "Lean has special provisions for some tactics. This includes `have`, `let`,\n",
    "`calc`. To execute one of these tactics, create a `TacticHave`, `TacticLet`,\n",
    "`TacticCalc` instance and feed it into `server.goal_tactic`.\n",
    "\n",
    "Technically speaking `have` and `let` are not tactics in Lean, so their execution requires special attention."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "526d620b-064f-4ec0-a7b2-6a1ef3c6f6e7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "⊢ 2 = 1 + 1\n",
      "h : 2 = 1 + 1\n",
      "⊢ 1 + 1 = 2\n"
     ]
    }
   ],
   "source": [
    "state0 = server.goal_start(\"1 + 1 = 2\")\n",
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch=\"2 = 1 + 1\", binder_name=\"h\"))\n",
    "print(state1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c415d436-ed0d-475f-bf5e-b8dc63954c7e",
   "metadata": {},
   "source": [
    "The `TacticExpr` \"tactic\" parses an expression and assigns it to the current\n",
    "goal.  This leverages Lean's type unification system and is as expressive as\n",
    "Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression\n",
    "and tactic forms."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "e1f06441-4d77-45a7-a1c3-b800b96a8105",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n"
     ]
    }
   ],
   "source": [
    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro p\")\n",
    "state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticExpr(\"fun h => h\"))\n",
    "print(state2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d6bcd026-507b-4b1c-8dee-006df53636b0",
   "metadata": {},
   "source": [
    "To execute the `conv` tactic, use `server.goal_conv_begin` to enter conv mode on\n",
    "one goal, and use `server.goal_conv_end` to exit from conv mode. Pantograph will\n",
    "provide interactive feedback upon every tactic executed in `conv` mode."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2b0b27c6-0c69-4255-aed1-c0713c227ccc",
   "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.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}