Merge branch 'master' of github.com:lecopivo/SciLean

.devcontainer/Dockerfile

@@ -0,0 +1,9 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+ENV HOME=/home/vscode
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -0,0 +1,21 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu
+{
+  "name": "Lean DevContainer on Ubuntu",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+
+  "onCreateCommand": "lake exe cache get! && lake build",
+
+  "postStartCommand": "git config --global --add safe.directory ${containerWorkspaceFolder}",
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [
+        "leanprover.lean4",
+        "mhutchie.git-graph"
+      ]
+    }
+  }
+}

.github/workflows/main.yml

@@ -26,21 +26,15 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  build: 
+  build:
     runs-on: ubuntu-latest
     steps:
-      - name: Install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - name: Checkout
-        uses: actions/checkout@v3
-      - name: Download cached build
-        run: lake exe cache get
-      - name: Build SciLean
-        run: lake build
+      - name: checkout
+        uses: actions/checkout@v4
+      - name: lean action
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: "--log-level=error"
       - name: Run Tests
         run: make test
       - name: Run Examples

SciLean/Data/FinProd.lean

@@ -0,0 +1,61 @@
+import SciLean.Data.IndexType
+
+namespace SciLean
+
+/-- Give `Fin n₁ × ... × Fin nₘ` for a list `[n₁,..., nₘ]`  -/
+def FinProd : List Nat → Type
+  | [] => Unit
+  | [n] => Fin n
+  | n :: (m :: ns) => Fin n × FinProd (m :: ns)
+
+instance instIndexTypeFinProd (l : List Nat) : IndexType (FinProd l) :=
+  match l with
+  | []  => by simp[FinProd]; infer_instance
+  | [n] => by simp[FinProd]; infer_instance
+  | n :: m :: ns =>
+    have e := instIndexTypeFinProd (m :: ns)
+    by simp[FinProd]; infer_instance
+
+instance instToStringFinProd (l : List Nat) : ToString (FinProd l) :=
+  match l with
+  | []  => by simp[FinProd]; infer_instance
+  | [n] => by simp[FinProd]; infer_instance
+  | n :: m :: ns =>
+    have e := instToStringFinProd (m :: ns)
+    by simp[FinProd]; infer_instance
+
+/-- Given `(i₁, ..., iₘ) : Fin n₁ × ... × Fin nₘ` return `[i₁.1,..., iₘ.1]` -/
+def FinProd.toList {l} (is : FinProd l) : List Nat :=
+  match l, is with
+  | [], _ => []
+  | [_], i => [i.1]
+  | _ :: _ :: _, (i, is) => i :: is.toList
+
+/-- Given `(i₁, ..., iₘ) : Fin n₁ × ... × Fin nₘ` return `[n₁-i₁.1-1,..., nₘ-iₘ.1-1]` -/
+def FinProd.toListComplement {l} (is : FinProd l) : List Nat :=
+  match l, is with
+  | [], _ => []
+  | [n], i => [n-i.1-1]
+  | n :: _ :: _, (i, is) => (n-i.1-1) :: is.toListComplement
+
+
+-- #eval show IO Unit from do
+--   let l := [2,3,4]
+--   let N := size (FinProd l)
+--   for i in fullRange (Fin N) do
+--     let x : FinProd l := IndexType.fromFin i
+--     IO.println s!"{x}"
+
+--   IO.println "hoho"
+
+--   for i in fullRange (FinProd [2,3]) do
+--     IO.println s!"{i}"
+
+--   IO.println "hihi"
+
+
+--- tests
+example : FinProd [] = Unit := by rfl
+example (n) : FinProd [n] = (Fin n) := by rfl
+example (n m) : FinProd [n,m] = (Fin n × Fin m) := by rfl
+example : FinProd [1,2,4] = (Fin 1 × Fin 2 × Fin 4) := by rfl

SciLean/Data/IndexType.lean

@@ -5,6 +5,8 @@ import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Algebra.Order.GroupWithZero.Canonical
+import Mathlib.Tactic.ProxyType
+import Mathlib.Tactic.DeriveFintype
 
 import SciLean.Util.SorryProof
 import SciLean.Tactic.RefinedSimp
@@ -27,6 +29,30 @@ instance (a : List α) : Size a where
 
 inductive IndexType.Range (I : Type u)
   | full
+  -- endpoint
+  -- startpoint
+  -- interval
+
+@[inline]
+def IndexType.Range.ofEquiv (_ : I ≃ J) (i : Range I) : Range J :=
+  match i with
+  | .full => .full
+
+@[inline]
+def IndexType.Range.ofProd (i : Range (I×J)) : Range I × Range J :=
+  match i with
+  | .full => (.full, .full)
+
+@[inline]
+def IndexType.Range.prod (i : Range I) (j : Range J) : Range (I×J) :=
+  match i, j with
+  | .full, .full => .full
+
+@[inline]
+def IndexType.Range.ofSigma (i : Range ((_:I)×J)) : Range I × Range J :=
+  match i with
+  | .full => (.full, .full)
+
 
 inductive IndexType.Stream (I : Type u) where
   /-- Stream for range `range` that has not been started -/
@@ -36,6 +62,48 @@ inductive IndexType.Stream (I : Type u) where
   -- /-- Stream that has been exhausted -/
   -- | done
 
+@[inline]
+def IndexType.Stream.val! [Inhabited I] (s : Stream I) : I :=
+  match s with
+  | .start _ => panic! "can't take value of start stream!"
+  | .val i _ => i
+
+@[inline]
+def IndexType.Stream.ofEquiv (f : I ≃ J) (i : Stream I) : Stream J :=
+  match i with
+  | .start r => .start (r.ofEquiv f)
+  | .val i r => .val (f i) (r.ofEquiv f)
+
+@[inline]
+def IndexType.Stream.ofProd (i : Stream (I×J)) : Stream I × Stream J :=
+  match i with
+  | .start r =>
+    let (r,s) := r.ofProd
+    (.start r, .start s)
+  | .val (i,j) r =>
+    let (r, s) := r.ofProd
+    (.val i r, .val j s)
+
+@[inline]
+def IndexType.Stream.prod (i : Stream I) (j : Stream J) : Stream (I×J) :=
+  match i, j with
+  | .start ri, .start rj => .start (ri.prod rj)
+  | .start ri, .val _ rj => .start (ri.prod rj)
+  | .val _ ri, .start rj => .start (ri.prod rj)
+  | .val i ri, .val j rj => .val (i,j) (ri.prod rj)
+
+
+@[inline]
+def IndexType.Stream.ofSigma (i : Stream ((_:I)×J)) : Stream I × Stream J :=
+  match i with
+  | .start r =>
+    let (r,s) := r.ofSigma
+    (.start r, .start s)
+  | .val ⟨i,j⟩ r =>
+    let (r, s) := r.ofSigma
+    (.val i r, .val j s)
+
+
 -- This is alternative to LeanColls.IndexType which unfortunatelly has two universe parameters
 -- and because of that it is very difficult to work with.
 class IndexType (I : Type u) extends Fintype I, Stream (IndexType.Stream I) I, Size I where
@@ -50,7 +118,13 @@ def IndexType.first? (I : Type u) [IndexType I] : Option I :=
   else
     .none
 
-
+def IndexType.Range.first? {I : Type u} [IndexType I] (r : Range I) : Option I :=
+  match r with
+  | .full =>
+    if h : size I ≠ 0 then
+      .some (IndexType.fromFin ⟨0, by omega⟩)
+    else
+      .none
 
 
 instance : IndexType Empty where
@@ -65,6 +139,18 @@ instance : IndexType Unit where
   fromFin _ := ()
   next? _ := .none
 
+instance : IndexType Bool where
+  size := 2
+  toFin x := match x with | false => 0 | true => 1
+  fromFin x := match x with | ⟨0,_⟩ => false | ⟨1,_⟩ => true
+  next? s :=
+    match s with
+    | .start r => .some (false, .val false r)
+    | .val val r =>
+      match val with
+      | false => .some (true, .val true r)
+      | true => .none
+
 instance : IndexType (Fin n) where
   size := n
   toFin x := x
@@ -93,23 +179,70 @@ instance {α β} [IndexType α] [IndexType β] : IndexType (α × β) where
     let i : Fin (size α) := ⟨ij.1 % size α, by sorry_proof⟩
     let j : Fin (size β) := ⟨ij.1 / size α, by sorry_proof⟩
     (IndexType.fromFin i, IndexType.fromFin j)
+  next? s :=
+    match s with
+    | .start r =>
+      let (ri, rj) := r.ofProd
+      match ri.first?, rj.first? with
+      | .some i, .some j => .some ((i,j), .val (i,j) r)
+      | _, _ => .none
+    | .val (i,j) r =>
+      let (ri,rj) := r.ofProd
+      let si := IndexType.Stream.val i ri
+      let sj := IndexType.Stream.val j rj
+      match Stream.next? si with
+      | .some (i', si) => .some ((i',j), si.prod sj)
+      | .none =>
+        match ri.first?, Stream.next? sj with
+        | .some i', .some (j', sj) => .some ((i',j'), (IndexType.Stream.val i' ri).prod sj)
+        | _, _ => .none
+    -- match s with
+    -- | .start _r =>
+    --   if let .some a := IndexType.first? α then
+    --     if let .some b := IndexType.first? β then
+    --       .some (⟨a,b⟩, .val ⟨a,b⟩ .full) -- todo: split the range somehow
+    --     else
+    --       .none
+    --   else
+    --     .none
+    -- | .val ⟨a,b⟩ _r =>
+    --   if let .some sa := Stream.next? (IndexType.Stream.val a .full) then
+    --     .some (⟨sa.1,b⟩, .val ⟨sa.1,b⟩ .full)
+    --   else
+    --     if let .some sb := Stream.next? (IndexType.Stream.val b .full) then
+    --       if let .some a := IndexType.first? α then
+    --         .some (⟨a,sb.1⟩, .val ⟨a,sb.1⟩ .full)
+    --       else
+    --         .none
+    --     else
+    --       .none
+
+
+instance {α β} [IndexType α] [IndexType β] : IndexType ((_ : α) × β) where
+  size := size α * size β
+  toFin := fun ⟨a,b⟩ => ⟨(IndexType.toFin a).1 + size α * (IndexType.toFin b).1, by sorry_proof⟩
+  fromFin ij :=
+    -- this choice will result in column major matrices
+    let i : Fin (size α) := ⟨ij.1 % size α, by sorry_proof⟩
+    let j : Fin (size β) := ⟨ij.1 / size α, by sorry_proof⟩
+    ⟨IndexType.fromFin i, IndexType.fromFin j⟩
   next? s :=
     match s with
     | .start _r =>
       if let .some a := IndexType.first? α then
         if let .some b := IndexType.first? β then
-          .some ((a,b), .val (a,b) .full) -- todo: split the range somehow
+          .some (⟨a,b⟩, .val ⟨a,b⟩ .full) -- todo: split the range somehow
         else
           .none
       else
         .none
-    | .val (a,b) _r =>
+    | .val ⟨a,b⟩ _r =>
       if let .some sa := Stream.next? (IndexType.Stream.val a .full) then
-        .some ((sa.1,b), .val (sa.1,b) .full)
+        .some (⟨sa.1,b⟩, .val ⟨sa.1,b⟩ .full)
       else
         if let .some sb := Stream.next? (IndexType.Stream.val b .full) then
           if let .some a := IndexType.first? α then
-            .some ((a,sb.1), .val (a,sb.1) .full)
+            .some (⟨a,sb.1⟩, .val ⟨a,sb.1⟩ .full)
           else
             .none
         else
@@ -183,6 +316,33 @@ instance (a b : Int) : IndexType (Icc a b) where
         .none
 
 
+def IndexType.ofEquiv [IndexType I] [Fintype J] (f : I≃J) : IndexType J where
+  size := size I
+  toFin j := toFin (f.symm j)
+  fromFin idx := f (fromFin idx)
+  next? s :=
+    match Stream.next? (s.ofEquiv f.symm) with
+    | .some (i, si) => .some (f i, si.ofEquiv f)
+    | .none => .none
+
+
+open Lean Elab Command
+def mkIndexTypeInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if declNames.size != 1 then
+    return false -- mutually inductive types are not supported
+  let id : Ident := mkIdent declNames[0]!
+  try
+    elabCommand (← `(deriving instance Fintype for $id))
+  catch _ =>
+    pure ()
+
+  elabCommand (← `(instance : IndexType $id := IndexType.ofEquiv (proxy_equiv% $id)))
+  return true
+
+initialize
+  registerDerivingHandler ``IndexType mkIndexTypeInstanceHandler
+
+
 namespace SciLean
 end SciLean
 
@@ -311,13 +471,13 @@ theorem reduce_linearize {I X : Type _} [IndexType I] (init : X) (f : I → X) (
 
 
 @[sum_push]
-theorem sum_pair {I X : Type _} [Add X] [Zero X] [IndexType I]
-    (f g : I → X) :
+theorem sum_pair {I X : Type _} [Add X] [Zero X] [Add Y] [Zero Y] [IndexType I]
+    (f : I → X) (g : I → Y) :
     ∑ i, (f i, g i) = (∑ i, f i, ∑ i, g i) := sorry_proof
 
 @[sum_pull]
-theorem pair_sum {I X : Type _} [Add X] [Zero X] [IndexType I]
-    (f g : I → X) :
+theorem pair_sum {I X : Type _} [Add X] [Zero X] [Add Y] [Zero Y] [IndexType I]
+    (f : I → X) (g : I → Y) :
     (∑ i, f i, ∑ i, g i) = ∑ i, (f i, g i) := sorry_proof