CPDT in lean

Stream: lean4

[Remi]

Hi, I currently rewriting code from CPDT and stuck with stack machine semantic proof.
I have several questions about lean:

• How can I make non-opaque alias for type.
• Is there any tactic for automatic proofs like sauto.

There's also a problem with actual proof.

p : List Instr
s : List Nat
bop : BinOp
e₁ e₂ : Expr
ih₁ : programDenote (compile e₁ ++ p) s = programDenote p (exprDenote e₁ :: s) [Click to join video call](https://meet.jit.si/185444530925654)
ih₂ : programDenote (compile e₂ ++ p) s = programDenote p (exprDenote e₂ :: s)
⊢ programDenote (compile e₂ ++ (compile e₁ ++ ([iBinOp bop] ++ p))) s =
    programDenote p (binOpDenote bop (exprDenote e₁) (exprDenote e₂) :: s)

In this proof context lean doesn't want to rewrite with ih₂, but this expression obviously has an appropriate type and works fine with simple rewrite tactic in coq.
There's a link to full code

[Chris B]

There's no hammer equivalent in Lean4. You can make a non-opaque alias with either abbrev <name> := ..or @[reducible] def <name> := ...

[Chris B]

w.r.t. sauto, There's library_search, but it's not as beefy as other proof search stuff.

[Joe Hendrix]

@Remi I'd expect ih_1 and ih_2 to have the form Forall (p:List Instr), if they had that form, then simp or rewrite should likely work.

[Reid Barton]

Right, ih₂ is about some specific program p, but the goal is about some different program built from p, so ih₂ doesn't apply.

[Reid Barton]

A bit hard to guess without context, but maybe you want to generalize p before doing an induction.

[Chris B]

theorem compileCorrect' e (p:List Instr) (s:List Nat) : programDenote (compile e ++ p) s = programDenote p (exprDenote e :: s) := by
  induction e generalizing p with
  | const => rfl
  | binOp bop e₁ e₂ ih₁ ih₂ =>
    simp [compile]
    simp [exprDenote]
    rw [List.append_assoc]
    rw [List.append_assoc]
    generalize hx : (compile e₁ ++ ([iBinOp bop] ++ p)) = p'
    rw [ih₂] -- succeeds now.
    sorry

[Reid Barton]

ah whoops, I missed that there was a link to the code!

[Remi]

@Chris B Can you explain what differs your code from mine?

[Chris B]

The generalizing bit in induction e generalizing p.

[Chris B]

It changes the inductive hypotheses.

[Remi]

Oh, now I understand.
Thank's everyone for the help!

[Chris B]

@Remi btw stuff to the right of the colon gets generalized automatically, some people find that more intuitive. This achieves the same result:

theorem compileCorrect' e : ∀ (p:List Instr) (s:List Nat), programDenote (compile e ++ p) s = programDenote p (exprDenote e :: s) := by
  induction e with

[Remi]

There's full proof :smile: .

theorem compileCorrect' (e:Expr) (p:List Instr) (s:List Nat) : programDenote (compile e ++ p) s = programDenote p (exprDenote e :: s) := by
  induction e generalizing p s with
  | const => rfl
  | binOp bop e₁ e₂ ih₁ ih₂ =>
    simp [compile, exprDenote]
    rw [List.append_assoc, List.append_assoc]
    rw [ih₂, ih₁]
    simp [programDenote, instrDenote]
    rfl
    done

[Chris B]

Way to go. By the way, where did you see that syntax for addressing the induction cases with . instead of | constructor .. => ?

[Remi]

@Chris B https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics