Zulip Chat Archive

Stream: new members

Topic: Converting a \forall into a \exists inside a tactic

florath (Sep 12 2024 at 10:37):

Hello!
As a first project in meta-programming I'm trying to write a tactic that handles expressions in First-Order-Logic, like:

example : True := by handle_logic
example : (∃ (x1 : Prop), x1) := by handle_logic
example : (∀ (x1 : Prop), (((x1 → (x1)) → ((∃ (x4 : Prop), (x4 → x4)) ∨ x1)))) := by handle_logic

If a proof exists, it should output the used tactics, e.g.

example : ((∃ (x4 : Prop), x4) ∧ (∃ (x5 : Prop), x5)) := by  handle_logic

Output:

  constructor
  apply Exists.intro True
  decide
  apply Exists.intro True
  decide

Some operators are working (like Or, And, Implication, ...), but I did not get the "handleForall" completed.

What I want to do is: if a "∀ (<var_name> : <var_type>), <body>" is found, I want to add a "have : ∃ (<var_name> : <var_type>), <body>" tactic. The idea is then to check for True and False and if one resolves into False, the "∀" is False if not it's True. (I know that I'm mixing different levels of True/False but I hope it is understandable.)

I did not manage to get all the needed information in the correct form (types) and put them together and execute the tactic.

Here are the first some lines of my function that handles the Forall case:

partial def handleForall (expr : Expr) (lB : IO.Ref (List String)) (tB : IO.Ref (List String)): TacticM NodeState := do
  logB lB s!"handleForall: expression [{expr}]"
  let body := expr.bindingBody! -- Get the body of the forall
  logB lB s!"handleForall: body [{body}]"
  let varType := expr.bindingDomain! -- Get the type of the bound variable
  logB lB s!"handleForall: varType [{varType}]"
  let localTB ← IO.mkRef ([] : List String)

  -- Extract the variable and body of the forall expression
  let varName := expr.bindingName!
  logB lB s!"handleForall: Bound variable [{varName}]"

  -- Convert varName, varType, and body to TSyntax format for use in tactics
  --  let varNameSyntax := mkIdent varName
  let varNameSyntax : TSyntax `ident := mkIdent varName
  logB lB s!"handleForall: varNameSyntax [{varNameSyntax}]"
  let varTypeSyntax ← Expr.toSyntax varType
  logB lB s!"handleForall: varTypeSyntax [{varTypeSyntax}]"
  let bodySyntax ← Expr.toSyntax body
  logB lB s!"handleForall: bodySyntax [{bodySyntax}]"

  -- Try substituting the bound variable with False
  logB lB "handleForall: Trying exists False"
  let localFalseTB ← IO.mkRef ([] : List String)
  -- XXX Test for "(∀ (x1 : Prop), x1)" as I have no idea how to
  --     extract and use the variable and the term.
  evalTactic (← `(tactic| have h_false : ∃ (x1 : $varTypeSyntax), $bodySyntax := by
exists False))
  -- XXX "varNameSyntax" has type TSyntax `ident : Type but is expected to have type TSyntax `Lean.binderIdent : Type
  -- XXX "varName" has type Name : Type but is expected to have type TSyntax `Lean.binderIdent : Type
  -- evalTactic (← `(tactic| have h_false : ∃ ($varName : $varTypeSyntax), $bodySyntax := by exists False))

  -- XXX What is the state of the goal? Is this now an "∃" statement?

And logs from a simple test:

handleForall: expression [forall (x1 : Prop), x1]
handleForall: body [#0]
handleForall: varType [Prop]
handleForall: Bound variable [x1]
handleForall: varNameSyntax [`x1]
handleForall: varTypeSyntax [(Term.syntheticHole "?" `a._@.miniF2F-Lean4.lean4.src.test.ap039._hyg.8059)]

My questions:

  1. How to correctly construct the "have" tactic?
  2. How to get the correct goal (i.e. the ∃ (<var_name> : <var_type>), <body>?

Any hint is welcome!

Last updated: May 02 2025 at 03:31 UTC