# Zulip Chat Archive

## Stream: new members

### Topic: Software Foundations

#### Phiroc (Mar 18 2021 at 12:49):

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 (Mar 18 2021 at 13:08):

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 (Mar 18 2021 at 16:24):

@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 (Mar 18 2021 at 19:32):

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 (Mar 18 2021 at 19:42):

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 (Mar 18 2021 at 21:31):

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

#### Scott Morrison (Mar 18 2021 at 22:07):

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

#### Phiroc (Mar 19 2021 at 07:16):

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 (Mar 19 2021 at 08:46):

(deleted)

#### Alex J. Best (Mar 19 2021 at 21:58):

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 (Jun 04 2021 at 13:48):

@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 (Jun 04 2021 at 14:06):

I found the inductive props chapter really enlightening.

#### Gihan Marasingha (Jun 04 2021 at 14:44):

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 (May 26 2023 at 13:41):

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 (May 26 2023 at 15:47):

- 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 (May 26 2023 at 17:04):

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 (Jun 04 2023 at 02:55):

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

Last updated: Dec 20 2023 at 11:08 UTC