simp without rfl

Stream: lean4

[xiao]

I come from Coq. In Coq, if you want to prove not true = false, you have to first simplify not true to false, then use rfl to prove the equality by reflexivity.

Example not_true: (negb true) = false.
Proof. simpl. reflexivity. Qed.

But in lean, a single simp will finish the proof.

example: not true = false := by
  simp

Is there any tactic to simplify terms without finishing the proof just like Coq? I know lean's behavior might be useful, but if I want to explain to others how a proof assistant works, I need those intermediate steps like true=true to illustrate Curry-Howard correspondence.

[Mario Carneiro]

I don't believe so. You can use rewrite [not] or unfold not to unfold not without trying to close the goal, but this yields a match expression and the usual tool to reduce these, dsimp only, also tries to close syntactic reflexivity goals, and I don't believe there is a simp option to turn this off

[Mario Carneiro]

of course you can prevent it from closing the goal by not making it a syntactic reflexivity:

def myFalse := false
example: not true = myFalse := by
  dsimp only [not]
  -- ⊢ false = myFalse

[xiao]

Then it is a bit disappointing. I think the essence behind simp is trying all equalities, but they are propositional ones, while the simp in Coq only does beta reductions till a normal form, which is a judgemental(definitional) equality. I don’t understand why dsimp also tries to close a propositional equality as it is called definitional.

[Mario Carneiro]

definitional equalities in lean are usually written using = and a proof using rfl

[Joël Riou]

dsimp tries only those simp lemmas that are definitional equalities (proved by rfl).

[Mario Carneiro]

ultimately this is just a tactic trying to be useful and not create busywork for the user

[Mario Carneiro]

it is possible to make your own dsimp' that skips this step

[Mario Carneiro]

oh, you can also use the dsimp conv it seems, this one does not try to close the goal... although I think the conv block itself might

[Mario Carneiro]

import Lean

namespace MyDSimp

open Lean.Parser.Tactic
syntax (name := dsimp') "dsimp'" (config)? (discharger)? (&" only")?
  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic

open Lean Elab Tactic Meta Simp

def dsimpGoal' (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
    (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   mvarId.withContext do
    mvarId.checkNotAssigned `simp
    let mut mvarIdNew := mvarId
    let mut stats : Stats := stats
    for fvarId in fvarIdsToSimp do
      let type ← instantiateMVars (← fvarId.getType)
      let (typeNew, stats') ← dsimp type ctx simprocs
      stats := stats'
      if typeNew.isFalse then
        mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
        return (none, stats)
      if typeNew != type then
        mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
    if simplifyTarget then
      let target ← mvarIdNew.getType
      let (targetNew, stats') ← dsimp target ctx simprocs stats
      stats := stats'
      -- if targetNew.isTrue then
      --   mvarIdNew.assign (mkConst ``True.intro)
      --   return (none, stats)
      -- if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
      --   if (← withReducible <| isDefEq lhs rhs) then
      --     mvarIdNew.assign (← mkEqRefl lhs)
      --     return (none, stats)
      if target != targetNew then
        mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
    if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
      throwError "dsimp made no progress"
    return (some mvarIdNew, stats)

def dsimpLocation' (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
  match loc with
  | Location.targets hyps simplifyTarget =>
    withMainContext do
      let fvarIds ← getFVarIds hyps
      go fvarIds simplifyTarget
  | Location.wildcard =>
    withMainContext do
      go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
where
  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
    let mvarId ← getMainGoal
    let (result?, stats) ← dsimpGoal' mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
    match result? with
    | none => replaceMainGoal []
    | some mvarId => replaceMainGoal [mvarId]
    if tactic.simp.trace.get (← getOptions) then
      mvarId.withContext <| traceSimpCall (← getRef) stats.usedTheorems
    return stats.diag

@[tactic dsimp'] def evalDSimp' : Tactic := fun stx => do
  let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
  dsimpLocation' ctx simprocs (expandOptLocation stx[5])

end MyDSimp

example: not true = false := by
  dsimp' [not]; rfl

[Arthur Paulino]

xiao said:

Then it is a bit disappointing

This is similar to my first frustration with Lean, since I had started learning about theorem proving in Coq and I wanted Lean to behave in the same way. But later on I realized that tactics are really customizable (though with a learning curve), as Mario has just shown

[Mario Carneiro]

and just to be clear, I didn't write all that code myself, it's a copy paste of the original dsimp with the offending lines commented out

[xiao]

Thank you guys. I finally noticed that lean admits uniqueness of identity proof (uip), which is not admitted in Coq. Since I am learning homotopy type theory, the equalities used in definitions (judgemental, in meta language) and the provable equalities (propositional) are significantly different to me. This is why I tend to use a simplification only for computation (judgement).

theorem uip.{u}: forall (A: Sort u) (x y: A) (p q: x=y), p = q := by
  simp