Apply on hypothesis

Stream: metaprogramming / tactics

[Francisco Lima]

I am implementing a basic automatic theorem solver, I did a few basic cases, but now I must start to break down the hypotheses, I already can identify for example a h : a ∧ b, bot how do I break it up, into ha : a and hb : b where I give the names for the 2 new hypothesis

[Henrik Böving]

You would have to create two new local hypotheses, one with And.left h and the other And.right h as proof and then register them with the local context.

[Francisco Lima]

I do so using mkAuxDecl? if not where can i find documentation on how to do so?

[Henrik Böving]

No, you likely want to use assertHypotheses on Lean.MVarId

[Francisco Lima]

now I have the problem that h stays in the context and enter a infinite loop of clearing ha and hb

[Aaron Liu]

then clear the h

[Aaron Liu]

docs#Lean.MVarId.clear

[Aaron Liu]

doesn't work if something depends on it though

[Francisco Lima]

thanks, was searching and hadn't found this one

[Francisco Lima]

ok, I am using Qq to match the declType and find a type of the format ~q($a  ∧ $b) but while a : α and b : β the matching is getting a _uniq.158, instead of a is prof of α, how can i extract it correctly?

[Francisco Lima]

theorem a_and_b_then_a {α β : Prop} : α ∧ β → α := by
  intro h
  custom_command

the theorem in question

[Aaron Liu]

#mwe?

[Francisco Lima]

best I could do

• all n are for tracking userReadable and referenceable for tryThis Hints

import Lean
import Qq
open Lean Elab Tactic Meta Qq

syntax (name := endSorry) "sorry?" : tactic

def letters := #["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z" ]

def getName (n : Nat) : Nat × String :=
  let base := letters[n % letters.size]!
  let rest := n / letters.size

  if rest > 0 then
    (n+1, s!"{base}{rest}")
  else
    (n+1, base)

def finished : TacticM Bool := do
  return (← getUnsolvedGoals).length == 0

def handleDefault (goal : MVarId) (n : Nat) : TacticM (String × Nat) := do
  let type ← goal.getType
  let ctx ← getLCtx
  -- do some edge cases detection for goal types like implications, ∀ & ∃

  let nn ← ctx.foldrM (init := n) fun decl (n: Nat) => do
    if decl.isImplementationDetail then return n
    let declExpr := decl.toExpr
    let declType := decl.type
    let declName := decl.userName
    logInfo m!"found {declName} : {declType}"
    match ← inferTypeQ declType with
    | ⟨1, ~q(Prop), ~q($a ∧ $b)⟩ =>
      -- logInfo s!"{declName}: {a} ∧ {b}"
      let (n, na) := getName n
      let ea : Expr := q($a)
      let ha : Hypothesis := { userName := na.toName, type := ← inferType ea, value := ea }
      logInfo s!"{na} : {ea} {declType}"
      let (n, nb) := getName n
      let eb : Expr := q($b)
      let hb : Hypothesis := { userName := nb.toName, type := ← inferType eb, value := eb }
      let (vars, goal) ← goal.assertHypotheses #[ha, hb]
      let goal ← goal.clear decl.fvarId
      replaceMainGoal [goal]
      return n
    | _ => return n

  -- to know if there has been any changes in the context
  if nn != n then return ("", nn)

  Lean.logInfo s!"By default: {type}"
  admitGoal goal
  return (s!"sorry", n)


def process (goal : MVarId) (n : Nat) : TacticM (String × Nat) := do
  let type ← goal.getType
  match ← inferTypeQ type with
  -- do lot of processing based on the goal
  | ⟨1, ~q(Prop), _a⟩ =>
    handleDefault goal n

partial def loop (n := 0) : TacticM (String)  :=
    withMainContext do
      let goal ← getMainGoal

      let (text, n) ← process goal n
      -- to handle the last goal
      if ← finished then
        return text
      else
        let raw ← loop n
        return s!"{text}\n{raw}"

elab_rules : tactic
  | `(tactic| sorry?) => do
    let raw ← loop
    logInfo s!"{raw}"
    return

theorem a_and_b_then_a {α β : Prop} : α ∧ β → α := by
  intro a
  sorry?

[Aaron Liu]

something is wrong with your matching

    match ← inferTypeQ declExpr with
    | ⟨0, ~q($a ∧ $b), declq⟩ =>
      let (n, na) := getName n
      let ea : Expr := q(And.left $declq)
      let ha : Hypothesis := { userName := na.toName, type := a, value := ea }
      let (n, nb) := getName n
      let eb : Expr := q(And.right $declq)
      let hb : Hypothesis := { userName := nb.toName, type := b, value := eb }
      let (vars, goal) ← goal.assertHypotheses #[ha, hb]
      let goal ← goal.clear decl.fvarId
      replaceMainGoal [goal]
      return n

do it like this so you get hypotheses instead of Props

[Aaron Liu]

when logging info, do m! instead of s! to get a message data instead of a string, this lets you see the user names of free variables (instead of the internal names)

  Lean.logInfo m!"By default: {type}"

[Francisco Lima]

Thanks