Merge pull request #49 from paulcadman/associative_alpha

associative alpha

lake-manifest.json

@@ -5,11 +5,91 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
+   "inputRev": "v4.14.0",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.47",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "raylean",
  "lakeDir": ".lake"}

lakefile.lean

@@ -5,7 +5,8 @@ def optionUseBundle : Bool := get_config? bundle == some "on"
 
 def optionDisableResvg : Bool := get_config? resvg == some "disable"
 
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ "01f4969b6e861db6a99261ea5eadd5a9bb63011b" -- Lean v4.14.0-rc1
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.14.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.14.0"
 
 package «raylean» where
   srcDir := "lean"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.14.0

lean/Examples/ImageDenotation.lean

@@ -5,8 +5,8 @@ open Raylean.Types
 
 namespace ImageDenotation
 
-def screenWidth := 80
-def screenHeight := 60
+def screenWidth := 200
+def screenHeight := 200
 
 def main : IO Unit := do
   initWindow screenWidth screenHeight "Image Denotation"

lean/Raylean/Graphics2D/Image.lean

@@ -1,6 +1,7 @@
 import Raylean.Types
 import Raylean.Core
 import Batteries
+import Mathlib.Tactic.Linarith
 
 namespace Raylean.Image
 
@@ -35,20 +36,29 @@ def lift2 (f : α → β → γ) : (Image α → Image β → Image γ) :=
 
 def monochrome (a : α) := lift0 a
 
--- C = Ca*Aa*(1-Ab) + Cb*Ab
--- https://stackoverflow.com/questions/26317267/rgba-color-mixing-css
-def blendRat (c1 c2 alpha1 alpha2 : Rat) : Rat := c1 * alpha1 * (1 - alpha2) + c2 * alpha2
+-- R = S + D × (1 − S_a)
+-- https://ciechanow.ski/alpha-compositing/#compositing-done-right
+def blendRat (src dst alpha : Rat) : Rat := src + dst - dst * alpha
 
 def blend (c1 c2 : Color) : Color :=
   ⟨
-    blendRat c1.r c2.r c1.alpha c2.alpha,
-    blendRat c1.g c2.g c1.alpha c2.alpha,
-    blendRat c1.b c2.b c1.alpha c2.alpha,
-    blendRat 1 1 c1.alpha c2.alpha
+    blendRat c1.r c2.r c1.alpha,
+    blendRat c1.g c2.g c1.alpha,
+    blendRat c1.b c2.b c1.alpha,
+    blendRat c1.alpha c2.alpha c1.alpha
   ⟩
 
 theorem blendIsAssocociative (c1 c2 c3 : Color) : blend c1 (blend c2 c3) = blend (blend c1 c2) c3 := by
-  sorry
+  unfold blend
+  simp
+  unfold blendRat
+  apply And.intro
+  · linarith
+  apply And.intro
+  · linarith
+  apply And.intro
+  · linarith
+  · linarith
 
 def over [BEq α] [Inhabited α] (a1 a2 : α) : α :=
   if a1 == default then a2 else a1