any advise on the correct attitude for leaning lean?

Stream: new members

[Shanghe Chen]

Hi! I am learning the Lean prover to better understand content in abstract algebra, commutative algebra, category theory and even algebraic geometry because I used to think that Lean can eliminate the vague and even fuzzy and jumpy content in traditional textbooks. But while doing the exercises using tactics it seems that I am now doing Lean more "programming style": For doing definitions or proving theorems I just repeated the loop of "change the code, try if rfl works, try simp with results already got as more as possible, ..." until no errors are reported. Finally, I got some correct results with the Lean Prover's powerful tactic system. But in the end, it becomes a proof similar to some traditional textbook I still don't know how the result is proved rigorously. It seems kind of backing to the starting point. To understand proof in Lean, I have to know the plain style proof. But to understand the plain proof, I want also Lean's assistance.

[Shanghe Chen]

An example is an exercise in TPIL section 8, where I solved it with the following snippet

theorem fuse_eq (v : Nat → Nat) : ∀ e: Expr, eval v (fuse e) = eval v e := by
intro e
match e with
| const n => rfl
| var n => rfl
| plus (const _) (const _) => rfl
| plus (const _) (var _) => rfl
| plus (const _) (plus _ _) => simp [fuse, simpConst_eq, eval, fuse_eq]
| plus (const _) (times _ _) => simp [fuse, simpConst_eq, eval, fuse_eq]
| plus (var _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]
| plus (plus _ _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]
| plus (times _ _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]
| times (const _) (const _) => rfl
| times (const _) (var _) => rfl
| times (const _) (plus _ _) => simp [fuse, simpConst_eq, eval, fuse_eq]
| times (const _) (times _ _) => simp [fuse, simpConst_eq, eval, fuse_eq]
| times (var _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]
| times (plus _ _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]
| times (times _ _) _ => simp [fuse, simpConst_eq, eval, fuse_eq]

But I worked this out by trying to see if rfl or simp works (i.e., no error showed up). At the end it was proved, it seems I still don't understand how it is proved. It's like a textbook proof now: "For showing they are the same, split them into cases and use the definitions and do it inductively"

[Patrick Massot]

This kind of exercise is really hard to compare with the kind of mathematics you mentioned.

[Patrick Massot]

About your general question, this is part of the mission of informalisation to help you access the details provided by automation, but we are not yet there.

[Eric Wieser]

Finally, I got some correct results with the Lean Prover's powerful tactic system. But in the end, it becomes a proof similar to some traditional textbook I still don't know how the result is proved rigorously.

Bebehind the scenes, these tactics are constructing a rigorous proof. You can use #print your_theorem to see this proof, though this won't help understand why it is rigorous.

[Shanghe Chen]

Yeah.. after knowing it's true with Lean, I think I can try to figure the rigorous proof out from all related tactics. Anyway, understanding proof in a textbook without lean is also time-consuming hence it should not bother me to do it manually. Thank you very much, Eric and Patrick :tada:

[Bulhwi Cha]

My solution is simpler:

My solution

inductive Expr where
  | const : Nat → Expr
  | var   : Nat → Expr
  | plus  : Expr → Expr → Expr
  | times : Expr → Expr → Expr
  deriving Repr

open Expr

def sampleExpr : Expr := plus (times (var 0) (const 7)) (times (const 2) (var 1))

def eval (v : Nat → Nat) : Expr → Nat
  | const n => n
  | var n   => v n
  | plus e₁ e₂  => eval v e₁ + eval v e₂
  | times e₁ e₂ => eval v e₁ * eval v e₂

def sampleVal : Nat → Nat
  | 0 => 5
  | 1 => 6
  | _ => 0

#eval eval sampleVal sampleExpr -- output: 47

def simpConst : Expr → Expr
  | plus  (const n₁) (const n₂) => const (n₁ + n₂)
  | times (const n₁) (const n₂) => const (n₁ * n₂)
  | e => e

def fuse : Expr → Expr
  | const n => const n
  | var n   => var n
  | plus e₁ e₂  => simpConst (plus (fuse e₁) (fuse e₂))
  | times e₁ e₂ => simpConst (times (fuse e₁) (fuse e₂))

theorem simpConst_eq (v : Nat → Nat) : ∀ (e : Expr), eval v (simpConst e) = eval v e := by
  intro e
  rw [simpConst]
  split <;>
  rfl

theorem fuse_eq (v : Nat → Nat) : ∀ (e : Expr), eval v (fuse e) = eval v e := by
  intro e
  induction e with
  | const n => rfl
  | var n   => rfl
  | _ e₁ e₂ ih₁ ih₂ =>
    rw [fuse]
    rw [simpConst_eq]
    repeat rw [eval]
    rw [ih₁, ih₂]

[Shanghe Chen]

Yeah it’s much more simpler.