Software Foundations

Stream: new members

[Phiroc]

Hello,
Has anyone here worked through the exercises in the Software Foundations Book, in Lean 3 or 4? If not, would anyone like to collaborate on finding solutions? I am using Lean 4.

[Kevin Buzzard]

When I was learning Lean I went through most of the first SF book and ported solutions to Lean 3 (and didn't keep them); I can certainly say that it taught me a lot (I didn't know anything about theorem provers at the time and SF seemed to be a good teaching resource). I am not going to go through this stuff again myself but I would definitely say that if there are beginners out there who want to read a good teaching textbook written in a language close to Lean then this might be a great opportunity.

[Julian Berman]

@Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

[Phiroc]

Julian Berman said:

Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

Hi Julian, I've just created a private Software-Foundations-In-Lean project on GitHub. Once I have made sufficient progress, I'll make it public so that anyone who wants to can contribute.

[Shing Tak Lam]

Phiroc said:

Julian Berman said:

Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

Hi Julian, I've just created a private Software-Foundations-In-Lean project on GitHub. Once I have made sufficient progress, I'll make it public so that anyone who wants to can contribute.

By the way, the authors of SF ask that the solutions to exercises are not made public, and although SF is written in Coq, Lean is similar enough that it might be transferrable. I don't think they would mind if the repo contains only the exercises.

[Guilherme Espada]

Why do they ask for the solutions not to be made public? Seems a bit weird for self-learning

[Scott Morrison]

Presumably because it makes it hard to use the problems as homework assignments for students.

[Phiroc]

I’ll therefore translate the code examples and implementations to Lean 4, and leave out the answers, or answer attempts, to the exercises . It’s a pity though, because I am having a hard time finding answers to some exercises, in idiomatic Lean.

[Iocta]

(deleted)

[Alex J. Best]

I guess there's nothing wrong with asking for idiomatic lean ways of doing specific questions here, just not writing an easy to find least of solutions to every exercise would be bad for instructors of classes

[Gihan Marasingha]

@Phiroc I've got a private repo going for this on Lean 3. I'm in the middle of the Inductive Propositions chapter from book 1 at the moment. Would be very happy to share ideas / join your project. This would be a good opportunity for me to learn Lean 4.

[Kevin Buzzard]

I found the inductive props chapter really enlightening.

[Gihan Marasingha]

On this point, is set! the Lean 3 equivalent of Coq's remember tactic? I had difficulty translating star_app (see the relevant section of Software Foundations) and tried different tactics (including generalize, generalize' and induction') until this worked.

Here's what I wrote. Do let me know if there's a more idiomatic way to write the proof!

import tactic

inductive reg_exp (T : Type)
| EmptySet  : reg_exp
| EmptyStr  : reg_exp
| Char (t : T)  : reg_exp
| App (r₁ r₂ : reg_exp) : reg_exp
| Union (r₁ r₂ : reg_exp) : reg_exp
| Star (r : reg_exp) : reg_exp

open reg_exp list

inductive exp_match {T} : list T → reg_exp T → Prop
| MEmpty : exp_match [] EmptyStr
| MChar (x) : exp_match [x] (Char x)
| MApp (s₁ re₁ s₂ re₂) (h₁ : exp_match s₁ re₁) (h₂ : exp_match s₂ re₂) :
  exp_match (s₁ ++ s₂) (App re₁ re₂)
| MUnionL (s₁ re₁ re₂) (h₁ : exp_match s₁ re₁) : exp_match s₁ (Union re₁ re₂)
| MUnionR (re₁ s₂ re₂) (h₂ : exp_match s₂ re₂) : exp_match s₂ (Union re₁ re₂)
| MStar0 (re) : exp_match [] (Star re)
| MStarApp (s₁ s₂ re) (h₁ : exp_match s₁ re) (h₂ : exp_match s₂ (Star re)) :
  exp_match (s₁ ++ s₂) (Star re)

infix ` =~ `:80 := exp_match

open exp_match

lemma star_app : ∀ T (s1 s2 : list T) (re : reg_exp T), s1 =~ Star re → s2 =~ Star re →
  (s1 ++ s2) =~ Star re :=
begin
  intros T s1 s2 re h1,
  set! re' := (Star re)  with hres,
  induction h1 generalizing s2,
  case MEmpty : { intro h, dsimp, exact h, },
  case MChar : { cases hres, },
  case MApp : { cases hres, },
  case MUnionL : { cases hres, },
  case MUnionR : { cases hres, },
  case MStar0 : { intro h, dsimp, exact h, },
  case MStarApp : s1 s2' re h1 h12 ih1 ih2
  { rw list.append_assoc, intro h, apply MStarApp,
    { apply h1, },
    { apply ih2 hres, apply h, }, },
end

[Kevin Cheung]

Is there now a public Software-Foundations-In-Lean? I thought I saw it once somewhere but I can't seem to find it anymore. Help is greatly appreciated.

[Bulhwi Cha]

• Text: https://alashworth.github.io/sf-lean/index.html
• GitHub repo: https://github.com/alashworth/sf-lean

The text and the repository are incomplete.

[Kevin Cheung]

Bulhwi Cha said:

• Text: https://alashworth.github.io/sf-lean/index.html
• GitHub repo: https://github.com/alashworth/sf-lean

The text and the repository are incomplete.

Thank you!

[rami3l]

FWIW, I'm currently learning Lean by trying to convert Agda proofs from Programming Language Foundations in Agda into Lean 4: https://github.com/rami3l/plfl