Merge pull request #29 from gaetanserre/dev

Refactor

Author: gaetanserre

.github/workflows/create-release.yml

@@ -0,0 +1,22 @@
+name: Create Release
+
+on:
+  push:
+    branches:
+      - 'main'
+      - 'master'
+    paths:
+      - 'lean-toolchain'
+
+jobs:
+  lean-release-tag:
+    name: Add Lean release tag
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+    - name: lean-release-tag action
+      uses: leanprover-community/lean-release-tag@v1
+      with:
+        do-release: true
+        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/create_release.yml

@@ -247,7 +247,7 @@ lemma tensorHom {κ : Kernel X Y} [IsSFiniteKernel κ] {η : Kernel V Z} [IsSFin
   ext : 1; dsimp
   simp only [hom]
   rw [id_parallelComp_comp_parallelComp_id, comap_parallelComp_comap, map_parallelComp_map]
-  · congr
+  · rfl
   all_goals fun_prop
 
 end tensorHom

KernelHom/Kernel/Hom.lean

@@ -290,8 +290,8 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level)
   | [forwardGoal, backwardGoal] =>
     setGoals [forwardGoal]
     evalTactic (← `(tactic| intro h))
-    for e in op_data do
-      match e with
+    for op in op_data do
+      match op with
       | .leftUnitor_hom _ sfinker equiv =>
         let sfinkerStx ← Term.exprToSyntax sfinker
         let equivStx ← Term.exprToSyntax equiv
@@ -372,8 +372,8 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level)
         evalTactic congr_tac
       catch _ =>
         pure ()
-      for e in op_data do
-        match e with
+      for op in op_data do
+        match op with
         | .WhiskerLeft sfinker equiv =>
           let sfinkerStx ← Term.exprToSyntax sfinker
           let equivStx ← Term.exprToSyntax equiv
@@ -415,8 +415,8 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level)
 
     setGoals [backwardGoal]
     evalTactic (← `(tactic| intro h))
-    for e in op_data do
-      match e with
+    for op in op_data do
+      match op with
       | .leftUnitor_hom _ sfinker equiv =>
         let sfinkerStx ← Term.exprToSyntax sfinker
         let equivStx ← Term.exprToSyntax equiv
@@ -497,8 +497,8 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level)
         evalTactic congr_tac
       catch _ =>
         pure ()
-      for e in op_data do
-        match e with
+      for op in op_data do
+        match op with
         | .WhiskerLeft sfinker equiv =>
           let sfinkerStx ← Term.exprToSyntax sfinker
           let equivStx ← Term.exprToSyntax equiv
@@ -542,7 +542,7 @@ def mkHomKernelEqProof (eqProofType : Expr) (eLevel : Level)
     throwError "Expected exactly two goals after `constructor`"
   if !(← getGoals).isEmpty then
     setGoals savedGoals
-    throwError "Failed to solve all goals while building kernel_hom equivalence proof"
+    throwError "Failed to solve all goals while building hom_kernel equivalence proof"
   setGoals savedGoals
   instantiateMVars mvar
 

KernelHom/Tactic/Hom/HomKernel.lean

@@ -7,7 +7,6 @@ module
 
 public import Lean.Elab.Tactic.Location
 public import KernelHom.Kernel.MonoidalComp
-public import KernelHom.Mathlib.MeasurableEquiv
 public import KernelHom.Tactic.LocTactic
 public import KernelHom.Tactic.Hom.Universe
 public import KernelHom.Tactic.Hom.Utils
@@ -24,7 +23,7 @@ kernels into equivalent equalities in the monoidal category.
   categorical morphism expressions.
 * `mkKernelHomEqProof`: construction of the equivalence proof used by the
   tactic.
-* `applyKernelHom`: core implementation on goals and hypotheses.
+* `applyKernelHom`: core implementation of `kernel_hom` on goals and hypotheses.
 * `kernel_hom`: user-facing tactic (with location support).
 -/
 
@@ -342,8 +341,8 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
   | [forwardGoal, backwardGoal] =>
     setGoals [forwardGoal]
     evalTactic (← `(tactic| intro h))
-    for e in op_data do
-      match e with
+    for op in op_data do
+      match op with
       | .leftUnitor_hom lvl sfinker equiv =>
         let punitLevelStx ← liftMacroM <| levelToSyntax lvl
         let sfinkerStx ← Term.exprToSyntax sfinker
@@ -412,10 +411,9 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
         evalTactic congr_tac
       catch _ =>
         pure ()
-      for e in op_data do
-        match e with
+      for op in op_data do
+        match op with
         | .WhiskerLeft sfinker equiv =>
-          logInfo m! "WhiskerLeft: {sfinker}, {equiv}"
           let sfinkerStx ← Term.exprToSyntax sfinker
           let equivStx ← Term.exprToSyntax equiv
           evalTactic (← `(tactic| nth_rw 1 [
@@ -425,7 +423,6 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
           catch _ =>
             pure ()
         | .WhiskerRight sfinker equiv =>
-          logInfo m! "WhiskerRight: {sfinker}, {equiv}"
           let sfinkerStx ← Term.exprToSyntax sfinker
           let equivStx ← Term.exprToSyntax equiv
           evalTactic (← `(tactic| nth_rw 1 [
@@ -435,7 +432,6 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
           catch _ =>
             pure ()
         | .MonoidalComp sfinkerW ew sfinkerX ex sfinkerY ey sfinkerZ ez =>
-          logInfo m! "MonoidalComp: {sfinkerW}, {ew}, {sfinkerX}, {ex}, {sfinkerY}, {ey}, {sfinkerZ}, {ez}"
           let sfinkerWStx ← Term.exprToSyntax sfinkerW
           let ewStx ← Term.exprToSyntax ew
           let sfinkerXStx ← Term.exprToSyntax sfinkerX
@@ -459,8 +455,8 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
 
     setGoals [backwardGoal]
     evalTactic (← `(tactic| intro h))
-    for e in op_data do
-      match e with
+    for op in op_data do
+      match op with
       | .leftUnitor_hom lvl sfinker equiv =>
         let punitLevelStx ← liftMacroM <| levelToSyntax lvl
         let sfinkerStx ← Term.exprToSyntax sfinker
@@ -531,8 +527,8 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
         evalTactic congr_tac
       catch _ =>
         pure ()
-      for e in op_data do
-        match e with
+      for op in op_data do
+        match op with
         | .WhiskerLeft sfinker equiv =>
           let sfinkerStx ← Term.exprToSyntax sfinker
           let equivStx ← Term.exprToSyntax equiv
@@ -581,33 +577,6 @@ def mkKernelHomEqProof (eqProofType rhs lhs : Expr) (maxLvl : Level)
   setGoals savedGoals
   instantiateMVars mvar
 
-/-- Construct the proof of equivalence between the original equality and the transformed one. -/
-def mkKernelHomEqProofSorry (eqProofType rhs lhs : Expr) (maxLvl : Level)
-    (op_data : List CategoryOP) : TacticM Expr := do
-  let maxLvlStx ← liftMacroM <| levelToSyntax maxLvl
-  let rhsStx ← Term.exprToSyntax rhs
-  let lhsStx ← Term.exprToSyntax lhs
-  let op_data := op_data.reverse
-  let savedGoals ← getGoals
-  let mvar ← mkFreshExprSyntheticOpaqueMVar eqProofType
-  let mvarId := mvar.mvarId!
-  setGoals [mvarId]
-  evalTactic (← `(tactic| apply propext))
-  evalTactic (← `(tactic| constructor))
-  let goalsAfterConstructor ← getGoals
-  match goalsAfterConstructor with
-  | [forwardGoal, backwardGoal] =>
-    setGoals [forwardGoal]
-    evalTactic (← `(tactic| sorry))
-
-    setGoals [backwardGoal]
-    evalTactic (← `(tactic| sorry))
-  | _ =>
-    setGoals savedGoals
-    throwError "Expected exactly two goals after `constructor`"
-  setGoals savedGoals
-  instantiateMVars mvar
-
 /-- The `kernel_hom` tactic transforms a kernel equality to an equivalent equality in
 the category of measurable spaces and s-finite kernels.
 

KernelHom/Tactic/Hom/KernelHom.lean

@@ -68,7 +68,7 @@ def computeMaxUniverse (levels : List Level) : MetaM Level :=
     | [] => throwError "Expected at least one universe level, got an empty list"
     | head :: tail => pure (tail.foldl Level.max head)
 
-/-- Get the category universe level from the left side of an equality expression. -/
+/-- Get the universe level from the left side of an equality expression. -/
 def getUniverseFromEq (eq : Expr) : MetaM Level := do
   let eq ← instantiateMVars eq
   let eq ← zetaReduce eq

KernelHom/Tactic/Hom/Universe.lean

@@ -5,6 +5,7 @@ Authors: Gaëtan Serré
 -/
 module
 
+public import KernelHom.Mathlib.MeasurableEquiv
 public import Lean
 public import Mathlib.Probability.Kernel.Composition.Prod
 public import Mathlib.Probability.Kernel.Composition.CompProd
@@ -57,10 +58,10 @@ partial def constructMeasurableEquiv (e : Expr) (eLevel maxLvl : Level) : MetaM
     let yLevel := univs[1]!
     let ex ← constructMeasurableEquiv X xLevel maxLvl
     let ey ← constructMeasurableEquiv Y yLevel maxLvl
-    let res ← mkAppOptM' (Expr.const `MeasurableEquiv.prod [maxLvl, xLevel, yLevel])
+    let res ← mkAppOptM' (Expr.const ``MeasurableEquiv.prod [maxLvl, xLevel, yLevel])
       #[none, none, none, none, none, none, none, none, ex, ey]
     return res
-  | _ => mkAppOptM' (Expr.const `MeasurableEquiv.ulift [eLevel, maxLvl]) #[e, none]
+  | _ => mkAppOptM' (Expr.const ``MeasurableEquiv.ulift [eLevel, maxLvl]) #[e, none]
 
 /-- Categorical operations recorded during transformation for later rewriting. -/
 inductive CategoryOP