Introduction, question (eliminating if-then-else in conv)

Stream: new members

[Jozef Mikušinec]

Hi!

This is my zeroth post, so I'll introduce myself. I'm graduate in computing science, I'm interested in sound type systems, and one day, I'd like to create a programming language with one expressive enough to serve as a convenient theorem prover for general mathematics.

I decided to try to use Lean 4 to make sure I don't have mistakes in my proofs (since I discovered some pretty embarrassing, although easily fixable ones, in my magister thesis.)

Question -- I have code like this (simplified):

open Classical

-- An opaque proposition
def someComplexProp (a: Nat → Nat): Prop := ∀ n, a n = 10

-- An if-then-else defined on the proposition
noncomputable def f (a: Nat → Nat): Bool :=
  if someComplexProp a then true else false

-- A value satisfying the prop, along with a proof
def x: Nat → Nat := fun _ => 10
def proofOfSomeComplexProp: someComplexProp x := fun _ => rfl

-- I'd like to prove this without simp or ▸.
def fxEqTrue: f x = true := by conv =>
  unfold f; simp [proofOfSomeComplexProp]; exact trivial

How can I find out what magic simp uses under the hood and
use it directly? I'd be fine with using simp, but because of
this issue,
I can't. What step can I use in conversion mode to eliminate the
if-then-else?

Thank you.

[Adam Topaz]

def fxEqTrue: f x = true := by
  unfold f
  rw [if_pos]
  apply proofOfSomeComplexProp

[Adam Topaz]

if you wanted the negative case of the if-then-else, then you could use docs4#if_neg instead

[Adam Topaz]

In general, the tactic show_term will give you the (usually unreadable) term produced by a tactic proof. I think show_term has alreaedy been implemented in mathlib4, but I'm not 100% sure.

[Adam Topaz]

Also, simp? or squeeze_simp are mathlib(3) tactics that will show you what lemmas an invocation of simp uses. I don't know if these have been implemented in mathlib4 yet.

[Jozef Mikušinec]

Thank you! I think that should work for me. However, I'm afraid I simplified my example too much - my defs are actually local definitions, and it seems unfold does not actually unfold let declarations, so the unfolding was also handled by simp. (Indeed if I delete it it still compiles.) So can you also show me how to unfold a particular let binding?

The modified example:

open Classical

noncomputable def wat :=
  -- An opaque proposition
  let someComplexProp (a: Nat → Nat): Prop := ∀ n, ∃ m, a n = m

  -- An if-then-else defined on the proposition
  let f (a: Nat → Nat): Bool :=
    if someComplexProp a then true else false

  -- A value satisfying the prop, along with a proof
  let x: Nat → Nat := fun _ => 10
  let proofOfSomeComplexProp: someComplexProp x := fun n => ⟨x n, rfl⟩

  -- I'd like to prove this without simp or ▸.
  let fxEq10: true = f x := by conv => unfold f; rw [if_pos]; apply proofOfSomeComplexProp

  42

[Mario Carneiro]

let bindings are definitionally equal to their definitions, so you can just apply a theorem that would apply if the definition was already unfolded

[Mario Carneiro]

here's a tactic-free proof:

  let fxEq10: true = f x := (if_pos proofOfSomeComplexProp).symm

[Mario Carneiro]

you can also be more explicit about the unfolding by using show:

    show true = (if someComplexProp x then true else false) from
    (if_pos proofOfSomeComplexProp).symm

[Jozef Mikušinec]

Yes, the tactic-free proof worked for me, thank you very much!

[Mario Carneiro]

show is just syntax for an application of the identity function id with the specified type in order to force a definitional unfolding

[Mario Carneiro]

tactics like unfold f or dsimp only [f] amount to a use of show / @id T in the generated term

[Adam Topaz]

Also, dsimp by itself will unfold all of the local let bindings:

noncomputable def wat :=
  -- An opaque proposition
  let someComplexProp (a: Nat → Nat): Prop := ∀ n, ∃ m, a n = m

  -- An if-then-else defined on the proposition
  let f (a: Nat → Nat): Bool :=
    if someComplexProp a then true else false

  -- A value satisfying the prop, along with a proof
  let x: Nat → Nat := fun _ => 10
  let proofOfSomeComplexProp: someComplexProp x := fun n => ⟨x n, rfl⟩

  -- I'd like to prove this without simp or ▸.
  let fxEq10: true = f x := by
    dsimp
    -- Goal is now `⊢ true = if Nat → ∃ m, 10 = m then true else false`
    rw [if_pos]
    apply proofOfSomeComplexProp

  42

[Adam Topaz]

By the way, I'm not sure why you insist on conv.

[Mario Carneiro]

By the way, dsimp doesn't generate any proof term, it just uses rewriting with definitional equalities in order to come up with the new goal and then applies show with the final goal to assert, and the type theory does the hard work of checking that this is well typed by proving that the new goal is defeq to the original one