From dd0c7b01ecc6a990b3411150ce7d062bf08411e9 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sat, 29 Aug 2026 10:27:09 +0200
Subject: [PATCH 1/3] add attribute

---
 RandomDo.lean                 |  1 +
 RandomDo/Tactic/Deriving.lean | 88 +++++++++++++++++++++++++++++++++++
 2 files changed, 89 insertions(+)
 create mode 100644 RandomDo/Tactic/Deriving.lean

diff --git a/RandomDo.lean b/RandomDo.lean
index 342175a..eb84dc7 100644
--- a/RandomDo.lean
+++ b/RandomDo.lean
@@ -7,6 +7,7 @@ public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances
 public import RandomDo.Monad.MeasurableSpace
 public import RandomDo.Monad.Notation
+public import RandomDo.Tactic.Deriving
 public import RandomDo.Tactic.Elab
 public import RandomDo.Tactic.Examples
 public import RandomDo.Tactic.ForInStep
diff --git a/RandomDo/Tactic/Deriving.lean b/RandomDo/Tactic/Deriving.lean
new file mode 100644
index 0000000..17bfd2b
--- /dev/null
+++ b/RandomDo/Tactic/Deriving.lean
@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import RandomDo.Tactic.Elab
+
+/-!
+# The `@[is_markov]` attribute
+
+Writing an `rdo` program and then stating that it is a Markov kernel are two separate steps, and
+the second is mechanical: it is what `is_markov` does. This attribute runs it at the declaration,
+so a program carries its own instance:
+
+```
+@[is_markov]
+noncomputable def centred (c : ℝ) : Measure ℝ := rdo
+  let x ← gaussianReal c 1
+  return x
+```
+
+## Why not `deriving IsMarkov`
+
+A `deriving` clause under a `def` parses, but core commits to *delta deriving* whenever any of the
+named declarations is a definition (`Lean.Elab.Deriving.Basic.elabDeriving`): it unfolds the
+definition and infers pre-existing instances, and never consults a registered
+`DerivingHandler`. Delta deriving cannot run a tactic, and in any case looks for a class parameter
+that the fully applied `centred c : Measure ℝ` fits, which `IsMarkov`'s `γ → Measure α` is not.
+Supporting that spelling would mean overriding core's `deriving` command elaborator wholesale.
+
+## Which statement is derived
+
+A program's *last* argument is read as the kernel's parameter when it is explicit, giving
+`IsMarkov`. Otherwise the program denotes one fixed distribution and the statement is
+`IsProbabilityMeasure`. So `centred` above yields `IsMarkov centred`, while a parameterless program
+yields `IsProbabilityMeasure` of it, and a program whose trailing arguments are instance-implicit —
+`(μ : Measure ℝ) [IsProbabilityMeasure μ]` — yields `IsProbabilityMeasure` of it too, with those
+arguments bound.
+-/
+
+public meta section
+
+open Lean Meta Elab Term MeasureTheory
+
+namespace RDo.Tactic
+
+/-- The statement to prove for `declName`, as described in the module docstring. -/
+def isMarkovStatement (declName : Name) : MetaM Expr := do
+  let info ← getConstInfo declName
+  forallTelescope info.type fun args body ↦ do
+    unless body.isAppOfArity ``MeasureTheory.Measure 2 do
+      throwError "`IsMarkov` can only be derived for a declaration valued in `Measure`, but \
+        {declName} is valued in{indentExpr body}"
+    let f := mkAppN (mkConst declName (info.levelParams.map .param)) args
+    if h : 0 < args.size then
+      let last := args[args.size - 1]
+      if (← last.fvarId!.getDecl).binderInfo.isExplicit then
+        return ← mkForallFVars args.pop (← mkAppM ``IsMarkov #[← mkLambdaFVars #[last] f])
+    mkForallFVars args (← mkAppM ``MeasureTheory.IsProbabilityMeasure #[f])
+
+/-- Prove `isMarkovStatement declName` with the `is_markov` tactic and register it as an
+instance. -/
+def addIsMarkovInstance (declName : Name) : TermElabM Unit := do
+  let goal ← isMarkovStatement declName
+  let proof ← Term.elabTerm (← `(by intros; is_markov)) (some goal)
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let info ← getConstInfo declName
+  let instName := declName ++ `isMarkov
+  addDecl (.thmDecl { name := instName, levelParams := info.levelParams, type := goal,
+                      value := ← instantiateMVars proof })
+  Meta.addInstance instName .global 1000
+
+/-- The `@[is_markov]` attribute. -/
+initialize registerBuiltinAttribute {
+  name := `is_markov
+  descr := "prove that this `rdo` program is a Markov kernel, and register it as an instance"
+  applicationTime := .afterCompilation
+  add := fun declName _stx kind ↦ do
+    unless kind == AttributeKind.global do
+      throwError "`is_markov` must be a global attribute"
+    (addIsMarkovInstance declName).run'.run'
+}
+
+end RDo.Tactic
+
+end

From edabe25929e5d6dfc452382e43e39aee1a27ee2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Mon, 31 Aug 2026 15:14:45 +0200
Subject: [PATCH 2/3] Update RandomDo/Tactic/Deriving.lean

---
 RandomDo/Tactic/Deriving.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/RandomDo/Tactic/Deriving.lean b/RandomDo/Tactic/Deriving.lean
index 17bfd2b..926d870 100644
--- a/RandomDo/Tactic/Deriving.lean
+++ b/RandomDo/Tactic/Deriving.lean
@@ -21,15 +21,6 @@ noncomputable def centred (c : ℝ) : Measure ℝ := rdo
   return x
 ```
 
-## Why not `deriving IsMarkov`
-
-A `deriving` clause under a `def` parses, but core commits to *delta deriving* whenever any of the
-named declarations is a definition (`Lean.Elab.Deriving.Basic.elabDeriving`): it unfolds the
-definition and infers pre-existing instances, and never consults a registered
-`DerivingHandler`. Delta deriving cannot run a tactic, and in any case looks for a class parameter
-that the fully applied `centred c : Measure ℝ` fits, which `IsMarkov`'s `γ → Measure α` is not.
-Supporting that spelling would mean overriding core's `deriving` command elaborator wholesale.
-
 ## Which statement is derived
 
 A program's *last* argument is read as the kernel's parameter when it is explicit, giving

From 1ee85b12a4bad88a0d9f7f2b82bb4a31a35dfef7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Mon, 31 Aug 2026 15:14:53 +0200
Subject: [PATCH 3/3] Update RandomDo/Tactic/Deriving.lean

---
 RandomDo/Tactic/Deriving.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/RandomDo/Tactic/Deriving.lean b/RandomDo/Tactic/Deriving.lean
index 926d870..6129c23 100644
--- a/RandomDo/Tactic/Deriving.lean
+++ b/RandomDo/Tactic/Deriving.lean
@@ -21,7 +21,7 @@ noncomputable def centred (c : ℝ) : Measure ℝ := rdo
   return x
 ```
 
-## Which statement is derived
+## Which statement is generated
 
 A program's *last* argument is read as the kernel's parameter when it is explicit, giving
 `IsMarkov`. Otherwise the program denotes one fixed distribution and the statement is