How to properly define the "Syll" tactic?

Stream: lean4

[Andrew Naguib]

I am trying to define a new tactic "Syll" to finish goals that could be deduced from a chain of implications. But, I am not sure how to construct the proof term as to finish the goal by only invoking the tactic. Here is how I implemented it:

open Lean Meta Elab Tactic Term in
elab "Syll " : tactic => Lean.Elab.Tactic.withMainContext do
  let lctx ← Lean.MonadLCtx.getLCtx
  let goal ← Lean.Elab.Tactic.getMainGoal
  let goalType ← Lean.Elab.Tactic.getMainTarget

  let hyps ← getLocalHyps
  let (hyp1, hyp2) := (hyps.get! 0, hyps.get! 1)

  -- defining a list of pairs
  let mut chain : List (Expr × Expr) := []

  let getImplicationType (e : Expr) : MetaM (Option (Expr × Expr)) := do
    match (← inferType e) with
    | Expr.forallE _ p q _ => return some (p, q)
    | _ => return none

  for hyp in ← getLocalHyps do
    match (← getImplicationType hyp) with
    | some (p, q) => chain := chain ++ [(p, q)]
    | none =>
      dbg_trace f! /- f-string notation -/
      "Expression {hyp} is not of the form `p → q`"

  let Expr.forallE _ p r _ :=
    goalType | throwError "Goal type is not of the form `p → r`"

  if not (← isExprDefEq (chain.get! 0).1 p) then
    throwError "The first hypothesis does not match the goal's antecedent"

  if not (← isExprDefEq (chain.get! (chain.length - 1)).2 r) then
    throwError "The last hypothesis does not match the goal's consequent"

  let mut validChain := true
  for i in [:chain.length - 1] do
    if not (← isExprDefEq chain[i]!.2 chain[i+1]!.1) then
      validChain := false
      throwError "Syll could not verify the chain of implications"

  if validChain then
    dbg_trace "Goal can be deduced from the provided chain of hypotheses"
    -- How to construct the proofTerm here?
  else
    throwError "The chain of implications is not valid"

For example, to finish the goal in the following theorem:

theorem test_Syll (p q r: Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll

[Kyle Miller]

In case you'd be happy using a pre-existing tactic, Lean itself has solve_by_elim, and Mathlib has tauto and cc. The first works using backtracking search, but could fail in some cases, and the second should always work. I think the third does some sort of saturation thing that's more clever (though it's supposed to be used for equations, not implications).

[Kyle Miller]

Here's a debugged version of your tactic, with proof construction:

open Lean Meta Elab Tactic Term

structure ImpProof where
  (ant cons : Expr)
  (proof : Expr)
  deriving Inhabited

theorem compose {p q r : Prop} (pq : p → q) (qr : q → r) : p → r :=
  qr ∘ pq

/-- Compose two implication proofs using the `compose` theorem. -/
def ImpProof.compose (pq : ImpProof) (qr : ImpProof) : MetaM ImpProof := do
  unless ← isDefEq pq.cons qr.ant do
    throwError "\
      Consequent{indentD pq.cons}\n\
      is not definitionally equal to antecedent{indentD qr.ant}"
  let proof := mkApp5 (.const ``compose []) pq.ant pq.cons qr.cons pq.proof qr.proof
  return { ant := pq.ant, cons := qr.cons, proof := proof }

/-- Create the proof of `p -> p` using the `id` function. -/
def ImpProof.rfl (p : Expr) : ImpProof :=
  { ant := p, cons := p, proof := .app (.const ``id [.zero]) p}

elab "Syll " : tactic => liftMetaTactic1 fun goal => do
  let goalType ← goal.getType

  -- A list of implications from the local context.
  let mut chain : Array ImpProof := #[]

  let getImplication? (e : Expr) : MetaM (Option (Expr × Expr)) := do
    -- There may be metadata and metavariables, so do some unfolding if necessary:
    let ty ← instantiateMVars (← whnfR e)
    -- Check if it is a non-dependent forall:
    if ty.isArrow then
      return (ty.bindingDomain!, ty.bindingBody!)
    else
      return none

  for hyp in ← getLocalHyps do
    match ← getImplication? (← inferType hyp) with
    | some (p, q) => chain := chain.push {ant := p, cons := q, proof := hyp}
    | none => logInfo m!"Expression {hyp} is not of the form `p → q`"

  let some (p, q) ← getImplication? goalType
    | throwError "Goal type is not of the form `p → q`"

  if chain.isEmpty then
    throwError "Local context has no implications"

  unless ← isExprDefEq chain[0]!.ant p do
    throwError "The first hypothesis does not match the goal's antecedent"

  unless ← isExprDefEq chain[chain.size - 1]!.cons q do
    throwError "The last hypothesis does not match the goal's consequent"

  let comp ← chain.foldlM (init := ImpProof.rfl p) (fun pf1 pf2 => pf1.compose pf2)

  -- It's good to do one last check that the proof has the correct type before assignment.
  unless ← isDefEq (← inferType comp.proof) goalType do
    throwError "Invalid proof of goal"
  goal.assign comp.proof

  return none


theorem test_Syll (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll

[Kyle Miller]

For a more sophisticated version, here's a tactic that allows the implications to come in any order and with any arity.

theorem test1 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll

theorem test1' (p q r : Prop) (H2 : q → r) (H1 : p → q) : p → r := by
  Syll

theorem test2 (p q r : Prop) (h1 : p → q) (h2 : p → q → r) : p → r := by
  Syll

theorem test3 (p q r s : Prop) (h1 : p → q → r) (h2 : s → q) : p → s → r := by
  Syll

-- Printing proofs:
#print test1
-- fun p q r H1 H2 a ↦ (fun a ↦ H2 a) ((fun a ↦ H1 a) a)
#print test2
-- fun p q r h1 h2 a ↦ (fun a a_1 ↦ h2 a a_1) a ((fun a ↦ h1 a) a)
#print test3
-- fun p q r s h1 h2 a a_1 ↦ (fun a a_2 ↦ h1 a a_2) a ((fun a ↦ h2 a) a_1)

code

import Lean

open Lean Meta Elab Tactic Term

/-- A proof of `a₁ → a₂ → ⋯ → aₙ → c`. (Plain implications)-/
structure ImpProof where
  ants : List Expr
  cons : Expr
  proof : Expr
  deriving Inhabited

/--
Construct an `ImpProof` from a given proof.
Assumption: `Meta.isProp ty` is true.
-/
partial def ImpProof.build (ty : Expr) (proof : Expr) : MetaM ImpProof := do
  let ty' ← whnf ty
  if ty'.isArrow then
    let ty := ty'
    withLocalDecl ty.bindingName! ty.bindingInfo! ty.bindingDomain! fun arg => do
      let pf ← ImpProof.build ty.bindingBody! (.app proof arg)
      -- Cleanup the antecedent
      let ant := (← instantiateMVars (← inferType arg)).cleanupAnnotations
      return { ants := ant :: pf.ants,
               cons := pf.cons,
               proof := ← mkLambdaFVars #[arg] pf.proof }
  else
    -- Base case, a zero-antecedent 'implication'
    -- Clean up the consequent (consumeMData might be enough, but cleanupAnnotations doesn't hurt)
    let cons := (← instantiateMVars ty).cleanupAnnotations
    return { ants := [], cons := cons, proof := proof }

elab "Syll " : tactic => liftMetaTactic1 fun goal => do
  -- First, use the goal itself to create the wanted ImpProof. This is just to figure out
  -- how many times we want to `intro` as well as the goal consequent.
  let wanted ← ImpProof.build (← goal.getType) (.mvar goal)
  let (_, goal) ← goal.introN wanted.ants.length

  goal.withContext do

  -- Collect ImpProofs from the local hypotheses.
  let mut pfs ← (← getLocalHyps).filterMapM fun hyp => do
    if ← Meta.isProof hyp then
      return some (← ImpProof.build (← inferType hyp) hyp)
    else
      return none

  -- Map from propositions to proofs of propositions
  let mut propMap : ExprMap Expr := {}

  -- Seed this with all the proofs we've collected of single propositions.
  for pf in pfs do
    if pf.ants.isEmpty then
      propMap := propMap.insert pf.cons pf.proof

  -- Iteratively add terms we can deduce from `pfs` to `propMap`
  let mut progress : Bool := true
  while progress do
    progress := false
    for pf in pfs do
      unless propMap.contains pf.cons do
        if pf.ants.all propMap.contains then
          let antPfs := pf.ants.map propMap.find!
          let pf' := antPfs.foldl .app pf.proof
          propMap := propMap.insert pf.cons pf'
          progress := true

  if let some pf := propMap.find? wanted.cons then
    unless ← isDefEq (← inferType pf) (← goal.getType) do
      -- This shouldn't happen.
      throwError "Invalid proof of goal"
    goal.assign pf
    return none
  else
    throwError "Could not prove goal"


theorem test1 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll

theorem test1' (p q r : Prop) (H2 : q → r) (H1 : p → q) : p → r := by
  Syll

theorem test2 (p q r : Prop) (h1 : p → q) (h2 : p → q → r) : p → r := by
  Syll

theorem test3 (p q r s : Prop) (h1 : p → q → r) (h2 : s → q) : p → s → r := by
  Syll

-- Printing proofs:
#print test1
-- fun p q r H1 H2 a ↦ (fun a ↦ H2 a) ((fun a ↦ H1 a) a)
#print test2
-- fun p q r h1 h2 a ↦ (fun a a_1 ↦ h2 a a_1) a ((fun a ↦ h1 a) a)
#print test3
-- fun p q r s h1 h2 a a_1 ↦ (fun a a_2 ↦ h1 a a_2) a ((fun a ↦ h2 a) a_1)

[Kyle Miller]

Exercise: get Syll to work with

theorem test4 (p q r s : Prop) (h1 : p → q → r) (h2 : (q → r) → s) : p → s := by
  Syll

[Kyle Miller]

Hmm, I guess it's hard to beat the simplicity of simp, though if you want Syll to intentionally be limited to syllogisms, then this is not the right approach.

import Lean

open Lean Meta Elab Tactic Term

elab "revert_all" : tactic => liftMetaTactic1 fun goal => goal.revertAll

macro "Syll" : tactic => `(tactic| (revert_all; simp (config := { contextual := true })))

theorem test1 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll

theorem test1' (p q r : Prop) (H2 : q → r) (H1 : p → q) : p → r := by
  Syll

theorem test2 (p q r : Prop) (h1 : p → q) (h2 : p → q → r) : p → r := by
  Syll

theorem test3 (p q r s : Prop) (h1 : p → q → r) (h2 : s → q) : p → s → r := by
  Syll

theorem test4 (p q r s : Prop) (h1 : p → q → r) (h2 : (q → r) → s) : p → s := by
  Syll

[Andrew Naguib]

Thank you @Kyle Miller , this is elegant. The debugged version is exactly what I wanted. The version where you handle the syllogism in any arbitrary order was quite interesting.

I am trying to push it a little further so that Syll also optionally accepts hypotheses as arguments, and only proceeds to using ← getLocalHyps if none was passed. E.g., Syll [pq, qr, ...]. Is adding (config)? hyps:rwRuleSeq (I cheated it from the definition of rw) after the identifier the correct way to do it?

[Kyle Miller]

No, rwRuleSeq wouldn't be right, since that has supports other features like ← e rules. Basically, you just need to add ("[" term,* "]")? to the syntax, which means "optionally a square-braced-enclosed comma-delimited sequence of zero or more terms". I also split off a separate syntax definition so that it's possible to make use of the more powerful pattern matching in elab_rules. The syntax there is unfortunately a bit of sorcery, but I copied it from another tactic :-)

The way you process these terms is to use Tactic.elabTerm on each of them. None of the code beyond that actually cares about whether a particular term is a local hypothesis or not.

import Lean

open Lean Meta Elab Tactic Term

structure ImpProof where
  (ant cons : Expr)
  (proof : Expr)
  deriving Inhabited

theorem compose {p q r : Prop} (pq : p → q) (qr : q → r) : p → r :=
  qr ∘ pq

/-- Compose two implication proofs using the `compose` theorem. -/
def ImpProof.compose (pq : ImpProof) (qr : ImpProof) : MetaM ImpProof := do
  unless ← isDefEq pq.cons qr.ant do
    throwError "\
      Consequent{indentD pq.cons}\n\
      is not definitionally equal to antecedent{indentD qr.ant}"
  let proof := mkApp5 (.const ``compose []) pq.ant pq.cons qr.cons pq.proof qr.proof
  return { ant := pq.ant, cons := qr.cons, proof := proof }

/-- Create the proof of `p -> p` using the `id` function. -/
def ImpProof.rfl (p : Expr) : ImpProof :=
  { ant := p, cons := p, proof := .app (.const ``id [.zero]) p}

syntax "Syll" (ppSpace "[" term,* "]")? : tactic

elab_rules : tactic
  | `(tactic| Syll $[[$[$terms?],*]]?) => withMainContext do

    -- Elaborate all the supplied hypotheses, or use the entire local context if not provided.
    let hyps ←
      match terms? with
      | none => getLocalHyps
      | some terms => terms.mapM fun term => Tactic.elabTerm term none

    liftMetaTactic1 fun goal => do
      let goalType ← goal.getType

      -- A list of implications extracted from `hyps`.
      let mut chain : Array ImpProof := #[]

      let getImplication? (e : Expr) : MetaM (Option (Expr × Expr)) := do
        -- There may be metadata and metavariables, so do some unfolding if necessary:
        let ty ← instantiateMVars (← whnfR e)
        -- Check if it is a non-dependent forall:
        if ty.isArrow then
          return (ty.bindingDomain!, ty.bindingBody!)
        else
          return none

      for hyp in hyps do
        match ← getImplication? (← inferType hyp) with
        | some (p, q) => chain := chain.push {ant := p, cons := q, proof := hyp}
        | none => logInfo m!"Expression {hyp} is not of the form `p → q`"

      let some (p, q) ← getImplication? goalType
        | throwError "Goal type is not of the form `p → q`"

      if chain.isEmpty then
        throwError "Local context has no implications"

      unless ← isExprDefEq chain[0]!.ant p do
        throwError "The first hypothesis does not match the goal's antecedent"

      unless ← isExprDefEq chain[chain.size - 1]!.cons q do
        throwError "The last hypothesis does not match the goal's consequent"

      let comp ← chain.foldlM (init := ImpProof.rfl p) (fun pf1 pf2 => pf1.compose pf2)

      -- It's good to do one last check that the proof has the correct type before assignment.
      unless ← isDefEq (← inferType comp.proof) goalType do
        throwError "Invalid proof of goal"
      goal.assign comp.proof

      return none


theorem test1 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll [H1] -- fails

theorem test2 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll [H2] -- fails

theorem test3 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll [H2, H1] -- fails

theorem test4 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll [H1, H2] -- succeeds

theorem test5 (p q r : Prop) (H1 : p → q) (H2 : q → r) : p → r := by
  Syll -- succeeds

[Andrew Naguib]

Thank you @Kyle Miller very much; I didn't know I could specify a regex for the syntax.