Generalize finenum sample space

.github/pages-index.html

@@ -0,0 +1,13 @@
+<!doctype html>
+<meta charset="utf-8">
+<title>MDPLib</title>
+<style>
+  body { font-family: system-ui, sans-serif; max-width: 40em; margin: 4em auto; padding: 0 1em; }
+</style>
+<h1>MDPLib</h1>
+<p>Formalizing Markov Decision Processes in Lean.</p>
+<ul>
+  <li><a href="docs/">API documentation</a></li>
+  <li><a href="main.pdf">Companion paper (PDF)</a></li>
+  <li><a href="https://github.com/formalproofs/MDPLib">Source on GitHub</a></li>
+</ul>

.github/workflows/ci.yml

@@ -0,0 +1,69 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build:
+    name: Build library, docs and paper
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Build the Lean library
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: "MDPLib"
+
+      - name: Build the API documentation
+        run: lake -R build MDPLib:docs
+
+      - name: Build the LaTeX paper
+        uses: xu-cheng/latex-action@v3
+        with:
+          root_file: main.tex
+          working_directory: latex
+
+      - name: Assemble the website
+        run: |
+          mkdir -p _site
+          cp -r .lake/build/doc _site/docs
+          find _site/docs \( -name '*.trace' -o -name '*.hash' \) -delete
+          cp latex/main.pdf _site/main.pdf
+          cp .github/pages-index.html _site/index.html
+
+      - name: Upload the paper as a build artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: paper
+          path: latex/main.pdf
+
+      - name: Upload the GitHub Pages artifact
+        if: github.ref == 'refs/heads/main'
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: _site
+
+  deploy:
+    name: Deploy documentation to GitHub Pages
+    needs: build
+    if: github.ref == 'refs/heads/main'
+    runs-on: ubuntu-latest
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - id: deployment
+        uses: actions/deploy-pages@v4

MDPLib.lean

@@ -4,6 +4,7 @@
 import MDPLib.Probability.Prelude
 import MDPLib.Probability.Defs
 import MDPLib.Probability.Basic
+import MDPLib.Probability.Matrix
 import MDPLib.Probability.Quantile
 
 import MDPLib.Risk.VaR

MDPLib/MDP/Histories.lean

@@ -33,7 +33,7 @@ structure MDP : Type where
   A : ℕ
   A_ne : 0 < A
   /-- transition probability s, a, s' -/
-  P : Fin S → Fin A → Δ S
+  P : Fin S → Fin A → Δ (Fin S)
   /-- reward function s, a, s' -/
   r : Fin S → Fin A → Fin S → ℝ
 
@@ -373,16 +373,17 @@ theorem hist_horiz_exact (t : ℕ) (h : Hist M) (hh : h ∈ M.HistoriesHorizon t
     unfold MDP.HistoriesHorizon state2hist_emb MDP.state2hist at hh 
     rewrite [Finset.mem_map] at hh
     obtain ⟨s, sin, sf⟩ := hh
-    subst sf 
-    simp only [Hist.length]
+    subst sf
+    rfl
   case succ t' ih => 
     unfold MDP.HistoriesHorizon emb_tuple2hist MDP.tuple2hist at hh 
     rw [Finset.mem_map] at hh
-    obtain ⟨has, hasi, em⟩ := hh 
-    subst em 
-    unfold Hist.length
+    obtain ⟨has, hasi, em⟩ := hh
+    subst em
+    obtain ⟨h', a, s⟩ := has
     rewrite [Finset.mem_product] at hasi
-    rewrite [ih has.1 hasi.1]
+    show 1 + h'.length = t' + 1
+    rw [ih h' hasi.1]
     exact Nat.add_comm 1 t'
 
 def MDP.HistoriesHorizonT (M : MDP) (t : ℕ) : Finset (M.HistT t) := 
@@ -397,7 +398,7 @@ theorem hist_horiz_complete_t (t : ℕ) (h : M.HistT t) : h ∈ M.HistoriesHoriz
     extract_lets H f finj 
     apply Finset.mem_map.mpr 
     use ⟨h.1, hist_horiz_complete t h⟩
-    simp [f]
+    exact ⟨Finset.mem_attach _ _, rfl⟩
 
 instance (M : MDP) (t : ℕ) : Fintype (M.HistT t) where 
     elems := M.HistoriesHorizonT t