Simple CNN training example

This is the small image-classification counterpart to SimpleMlpTrain.lean.

It remains in Quickstart as a next-step file for users who have finished the core five-file path (TensorBasics, Widgets, AutogradBasics, SimpleMlpTrain, Proofs). For broader maintained vision models, prefer NN/Examples/Models.

It uses the same public training API:

1. define a SeqTask,
2. build samples,
3. call fit,
4. inspect loss / accuracy.

The only difference is the model and the sample shape.

Check this tutorial module directly:

• lake build NN.Examples.Quickstart.SimpleCnnTrain

For the maintained command-line CNN trainer, use NN/Examples/Models/Vision/Cnn.lean:

• python3 scripts/datasets/download_example_data.py --cifar10
• lake exe torchlean cnn --cpu --n-total 20 --steps 1

Optional flags:

• --epochs E
• --batch N

Public API used here:

• nn.conv, nn.relu, nn.flattenBatch, nn.linear
• train.classificationOneHot
• Data.labeled, Data.batchLoader
• train.fitLoaderWith + train.Callbacks

Reader note:

• the model type here is already batched: Images batch 1 4 4 -> batch × Vec 2;
• Semantics.Scalar α / Runtime.Scalar α mean the same thing as in the other tutorials: α must both support the model's math and be executable as a runtime backend.

See NN/Examples/Quickstart/README.md for the shared conventions in this folder.

def NN.Examples.Quickstart.SimpleCNNTrain.mkModel {batch : ℕ} : API.nn.M (API.nn.Sequential (Shape.Images batch 1 4 4) (Tensor.shapeOfDims [batch, 2]))

def NN.Examples.Quickstart.SimpleCNNTrain.runOnce {batch : ℕ} (task : API.train.Task (Shape.Images batch 1 4 4) (Tensor.shapeOfDims [batch, 2])) {α : Type} [API.Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [API.Runtime.Scalar α] (runner : API.train.Runner α task) (epochs : ℕ := 20) (seed : ℕ := 0) : IO Unit

def NN.Examples.Quickstart.SimpleCNNTrain.main (args : List String) : IO Unit