Add an unsolved goal with special conditions

Stream: new members

[Zihao Zhang]

Like this, after executing evalTactic a, I want to add an unsolved goal that has the same tactic state with goal1, which means their hyps and conclusions are same.

let goal1 ← getMainGoal
  let ctx ← getLCtx
  evalTactic a
  let t ← goal1.getType
  let newGoal ← mkFreshExprSyntheticOpaqueMVar t
  pushGoals [newGoal.mvarId!]

  evalTactic (← `(tactic| clear *-))
  ctx.forM (fun (decl : Lean.LocalDecl) => do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declType := decl.type -- Find the type of the declaration.
    let declName := decl.userName -- Find the name of the declaration.
    logInfo m!" local decl: name: {declName} | expr: {declExpr} | type: {declType}"
  )

[Zihao Zhang]

@Kyle Miller I successfully add the goal same as goal1 to the goals, but I don't know how to reset its hyps(or call its ctx) while doesn't change other goals' ctx. Could you help me?

[Robin Arnez]

can you explain exactly what you want?

[Robin Arnez]

as in what should happen with the goal state

[Zihao Zhang]

@Robin Arnez
See this, this tactic achieves the following: when the hypotheses before and after evalTactic a are the same, and the goals map one-to-one or one-to-many, it extracts the theorems (goal1 as a hyp). It also ensures that my_tool tactic_name has the same effect in the proof as tactic_name itself, without altering the tactic state—meaning it can be inserted like extract_goal without disrupting the tactic state.

elab "my_tool"  a:tactic :tactic => do
  let goal1 ← getMainGoal
  let t ← goal1.getType
  let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque `h100
  evalTactic a
  --let extractedInfos ← withoutModifyingState do
  let goals ← getUnsolvedGoals
  let newGoals ← goals.mapM fun goal2 => do
    goal2.withContext do
      let (_, goal3) ← MVarId.intro1P $ ← goal2.assert `h100 t p
      return goal3
  pushGoals newGoals
  let goals ← getUnsolvedGoals
  for _ in List.range (goals.length) do
    evalTactic (← `(tactic| extract_goal))
    let _ ← popMainGoal

  pushGoals newGoals
  let goals ← getUnsolvedGoals
  let newGoals2 ← goals.mapM fun goal => do
    goal.withContext do
      let some ldecl := (← getLCtx).findFromUserName? `h100 |
        throwTacticEx `delete_h1 (← getMainGoal) m!"h100 doesn't exist"
      let goal' ← (← getMainGoal).clear ldecl.fvarId
      return goal'
  pushGoals newGoals2

[Zihao Zhang]

However, when the hypotheses change after evalTactic a, it is no longer applicable. So I want to improve it so that the changed hypotheses also become new goals, not just the goals produced by evalTactic a. To achieve this, I think modifying goal1 is better than modifying the resulting goal2s. Therefore, I want to keep an unsolved goal1 along with its hypotheses.

[Zihao Zhang]

(deleted)

[Robin Arnez]

hmm, I'm not quite sure what you mean...
for example, is this what you want..?

example (a : Nat) : a = 1 := by
  my_tool skip -- theorem extracted_1 (a : ℕ) (h100 : a = 1) : a = 1 := sorry

[Zihao Zhang]

yes!

[Robin Arnez]

why the h100 though

[Robin Arnez]

oh wait it goes the wrong way, no?

[Zihao Zhang]

Give me some time to give you an example

[Robin Arnez]

example (a : Nat) : a = 1 := by
  my_tool rw [← Nat.add_zero 1] -- theorem extracted_1 (a : ℕ) (h100 : a = 1) : a = 1 + 0 := sorry

I'd expect it to go from a = 1 + 0 to a = 1 because a = 1 was the original goal

[Robin Arnez]

Zihao Zhang schrieb:

Give me some time to give you an example

okay sure

[Zihao Zhang]

By the code below, we extract 5 theorems (the last doesn't extract a theorem), and their proofs lengths all are 1.

theorem tmp_1 {a b:ℝ} :(a+b)^2=a^2+2*a*b+b^2:=by
  my_tool repeat rw [pow_two]
  my_tool rw [add_mul]
  my_tool repeat rw [mul_add]
  my_tool rw [←add_assoc]
  my_tool nth_rw 3 [mul_comm]
  my_tool ring

But if we use the code below,we extract 6 theorems with different proof lengths:6, 5, 4, 3, 2, 1.

theorem tmp_1 {a b:ℝ} :(a+b)^2=a^2+2*a*b+b^2:=by
  extract_goal
  repeat rw [pow_two]
  extract_goal
  rw [add_mul]
  extract_goal
  repeat rw [mul_add]
  extract_goal
  rw [←add_assoc]
  extract_goal
  nth_rw 3 [mul_comm]
  extract_goal
  ring

The former theorems just prove one step, but the latter aren't.

[Robin Arnez]

I still claim that you are going the wrong way round, take this:

example : True := by
  my_tool exfalso -- theorem extracted_1 (h100 : True) : False := sorry

The extracted theorem is false and doesn't represent what exfalso did here.
It should probably be:

example : True := by
  my_tool exfalso -- theorem extracted_1 (h100 : False) : True := sorry

instead

[Zihao Zhang]

Will any proof of math theorems use exfalso? I think it is illegal in math proving.

[Robin Arnez]

... no..? it's the principle of explosion

[Robin Arnez]

let's take a different example:

theorem myTheorem (a : Nat) (h : a = 1) : a ≤ 1 := by
  rw [h]

example : a ≤ 1 := by
  my_tool apply myTheorem -- theorem extracted_1 {a : ℕ} (h100 : a ≤ 1) : a = 1 := sorry

what my tool suggests is the opposite of the theorem I used

[Zihao Zhang]

But, we will use my_tool to extract theorems from proofs of math theorem. And apply myTheorem will not lead to a successful proof for any math theorem.

[Zihao Zhang]

A math theorem with a finished proof. It is what my_tool will apply to.

[Robin Arnez]

we can use apply myTheorem to write a "successful proof" of the "math theorem" "a = 1 → a ≤ 1`:

example : a = 1 → a ≤ 1 := by
  intro h
  my_tool apply myTheorem -- theorem extracted_1 {a : ℕ} (h100 : a ≤ 1) : a = 1 := sorry
  exact h

[Zihao Zhang]

Yes, and theorem extracted_1 {a : ℕ} (h : a = 1) (h100 : a ≤ 1) : a = 1 := sorry is a provable theorem.

[Zihao Zhang]

I think my logic is not wrong, it is not my idea, it is the idea of our team after strict talkings.

[Robin Arnez]

yes, but we don't need apply myTheorem to solve that

[Zihao Zhang]

We just want to extract theorems which split the original proofs. By applying the original tactics at h100 (also need some small changes), the extracted theorems is provable with no counterexamples.

[Zihao Zhang]

I know what you're thinking—you want to turn goal2 into a hypothesis h100, and make goal1 the conclusion, so that the proof after evalTactic a can be completed with exact h100. That’s correct, but it’s not what we want.

[Zihao Zhang]

Maybe you are right, I am also puzzled now and try to prove this logic in strict math language.

[Robin Arnez]

maybe this is more like what you want:

import Mathlib
import Lean.Elab.Tactic

open Lean Elab Tactic Meta

elab "to_theorem" t:tactic : tactic => do
  let goal ← Lean.Elab.Tactic.getMainGoal
  let levels ← Term.getLevelNames
  let type ← goal.getType
  let goal' := (← goal.withContext <| mkFreshExprSyntheticOpaqueMVar type).mvarId!
  let goals ← getGoals
  setGoals [goal']
  evalTactic t
  setGoals goals
  let some proof ← getExprMVarAssignment? goal' |
    throwError "tactic made no progress"
  let (_, state) ← (collectMVars proof).run {}
  let type ← instantiateMVars type
  let proof ← instantiateMVars proof
  let mvars := state.result
  let type' := type.abstract (mvars.map mkMVar)
  let proof' := proof.abstract (mvars.map mkMVar)
  let (type'', proof'') ← mvars.foldrM (fun mvar (type, proof) =>
    return (
      Expr.forallE (← mvar.getTag) (← mvar.getType) type .default,
      Expr.lam (← mvar.getTag) (← mvar.getType) proof .default
    )
  ) (type', proof')
  let (type''', proof''') ← goal'.withContext do
    let fvars := (← getLCtx).decls.toArray.filterMap
      (fun d => d.bind fun x => if x.isImplementationDetail then none else some <| Expr.fvar x.fvarId)
    (← getLCtx).decls.foldrM (fun decl (type, proof) => do
      match decl with
      | none => return (type, proof)
      | some decl =>
        if decl.isLet then
          return (
            Expr.letE decl.userName decl.type decl.value type false,
            Expr.letE decl.userName decl.type decl.value proof false
          )
        else if !decl.isImplementationDetail then
          return (
            Expr.forallE decl.userName decl.type type decl.binderInfo,
            Expr.lam decl.userName decl.type proof decl.binderInfo
          )
        else
          return (type, proof)
    ) (type''.abstract fvars, proof''.abstract fvars)
  let some declName ← Term.getDeclName? | throwError "not in declaration"
  let thmVal : TheoremVal := {
    name := ← mkAuxName (.str declName "extracted") 1
    levelParams := levels
    type := type'''
    value := proof'''
  }
  let decl : Declaration := .thmDecl thmVal
  try
    Lean.addDecl decl
    let newProof := Expr.const thmVal.name (levels.map Level.param)
    Lean.logInfo m!"theorem generated under {newProof}"
    let newProof' ← goal.withContext do
      let fvars := (← getLCtx).decls.toArray.filterMap
        (fun d => d.bind fun x => if x.isImplementationDetail || x.isLet then none else some <| Expr.fvar x.fvarId)
      return mkAppN newProof fvars
    let newProof' := mvars.foldl (fun proof mvar => mkApp proof (.mvar mvar)) newProof'
    goal.assign newProof'
    replaceMainGoal mvars.toList
  catch e =>
    throwTacticEx `to_theorem goal m!"failed to generate theorem: {e.toMessageData}"

theorem tmp_1 {a b:ℝ} : (a+b)^2=a^2+2*a*b+b^2:=by
  to_theorem repeat rw [pow_two]
  to_theorem rw [add_mul]
  to_theorem repeat rw [mul_add]
  to_theorem rw [←add_assoc]
  to_theorem nth_rw 3 [mul_comm]
  to_theorem ring

/--
info: theorem tmp_1 : ∀ {a b : ℝ}, (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 :=
fun {a b} =>
  tmp_1.extracted_1 (tmp_1.extracted_2 (tmp_1.extracted_3 (tmp_1.extracted_4 (tmp_1.extracted_5 tmp_1.extracted_6))))
-/
#guard_msgs in
#print tmp_1

[Zihao Zhang]

@Robin Arnez In a provable theorem's finished proof, before and after a tactic a, the two tactic states

$$hyps1\to goals1\\ hyps2\to goals2$$

are true,

$$hyps1\Rightarrow hyps2$$

(because you can never add new condition unprovable by the known conditions),so the following are true, and that is what I want to extract.

$$(hyps1,goals1)\to hyps2\\ (hyps1,goals1)\to goals2$$

[Zihao Zhang]

I think it is a strict proof. Sorry it takes time to write in latex

[Zihao Zhang]

@Robin Arnez Thank you so much for your help — I truly appreciate it! I’ll try hard to figure out your code.