Use mathlib definition of inverses for Isomorphism.lean

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

lean/Spa/Analysis/Constant.lean

@@ -5,6 +5,8 @@ import Spa.Showable
 
 namespace Spa
 
+open Forward
+
 abbrev ConstLattice : Type := AboveBelow ℤ
 
 namespace ConstAnalysis
@@ -157,7 +159,7 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
-  Spa.analyze_correct ConstLattice prog hrun
+  Forward.analyze_correct ConstLattice prog hrun
 
 end ConstAnalysis
 

lean/Spa/Analysis/Forward.lean

@@ -5,6 +5,8 @@ import Spa.Fixedpoint
 
 namespace Spa
 
+namespace Forward
+
 variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
 
 def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
@@ -116,4 +118,6 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
   walkTrace interp_joinForKey_initialState (prog.trace hrun)
 
+end Forward
+
 end Spa

lean/Spa/Analysis/Forward/Adapters.lean

@@ -2,6 +2,8 @@ import Spa.Analysis.Forward.Evaluation
 
 namespace Spa
 
+namespace Forward
+
 variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
 
 def updateVariablesFromExpression (k : String) (e : Expr)
@@ -51,4 +53,6 @@ instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
           (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
       exact hvs _ _ hk'l' _ hmem'
 
+end Forward
+
 end Spa

lean/Spa/Analysis/Forward/Evaluation.lean

@@ -2,6 +2,8 @@ import Spa.Analysis.Forward.Lattices
 
 namespace Spa
 
+namespace Forward
+
 variable (L : Type) [Lattice L] (prog : Program)
 
 class StmtEvaluator where
@@ -23,4 +25,6 @@ class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
     {bs : BasicStmt},
     EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂
 
+end Forward
+
 end Spa

lean/Spa/Analysis/Forward/Lattices.lean

@@ -4,6 +4,8 @@ import Spa.Interp
 
 namespace Spa
 
+namespace Forward
+
 variable (L : Type) [Lattice L] (prog : Program)
 
 abbrev VariableValues : Type := FiniteMap String L prog.vars
@@ -96,4 +98,6 @@ theorem interp_foldr {vs : VariableValues L prog}
     · exact interp_sup (Or.inl hvs)
     · exact interp_sup (Or.inr (ih hmem'))
 
+end Forward
+
 end Spa

lean/Spa/Analysis/Sign.lean

@@ -5,6 +5,8 @@ import Spa.Showable
 
 namespace Spa
 
+open Forward
+
 inductive Sign where
   | plus
   | minus
@@ -215,7 +217,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
-  Spa.analyze_correct SignLattice prog hrun
+  Forward.analyze_correct SignLattice prog hrun
 
 end SignAnalysis
 

lean/Spa/Fixedpoint.lean

@@ -1,6 +1,8 @@
 import Spa.Lattice
 
-namespace Spa.Fixedpoint
+namespace Spa
+
+namespace Fixedpoint
 
 open FiniteHeightLattice (height)
 
@@ -49,4 +51,6 @@ theorem aFix_le (f : α → α) (hf : Monotone f)
     {a : α} (ha : a = f a) : aFix f hf ≤ a :=
   doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
 
-end Spa.Fixedpoint
+end Fixedpoint
+
+end Spa

lean/Spa/Isomorphism.lean

@@ -5,20 +5,18 @@ namespace Spa
 def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
     [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
     (hf : Monotone f) (hg : Monotone g)
-    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
     FiniteHeightLattice β where
   bot := f ⊥
   top := f ⊤
   height := I.height
   longestChain :=
     { series :=
-        I.longestChain.series.map f
+        I.longestChain.series.map f (hf.strictMono_of_injective hgf.injective)
-          (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
       head_series := congrArg f I.longestChain.head_series
       last_series := congrArg f I.longestChain.last_series
       length_series := I.longestChain.length_series }
   chains_bounded := fun c =>
-    I.chains_bounded
+    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
-      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
 
 end Spa

lean/Spa/Language/Graphs.lean

@@ -89,17 +89,6 @@ def singleton (bss : List BasicStmt) : Graph where
 def wrap (g : Graph) : Graph :=
   singleton [] ⤳ g ⤳ singleton []
 
-end Graph
-
-open Graph in
-def buildCfg : Stmt → Graph
-  | .basic bs => Graph.singleton [bs]
-  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
-  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
-  | .whileLoop _ s => Graph.loop (buildCfg s)
-
-namespace Graph
-
 variable (g : Graph)
 
 def indices : List g.Index := List.finRange g.size
@@ -123,4 +112,11 @@ theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
 
 end Graph
 
+open Graph in
+def buildCfg : Stmt → Graph
+  | .basic bs => Graph.singleton [bs]
+  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
+  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
+  | .whileLoop _ s => Graph.loop (buildCfg s)
+
 end Spa

lean/Spa/Lattice.lean

@@ -61,12 +61,11 @@ class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
   longestChain : PointedLTSeries α ⊥ ⊤ height
   chains_bounded : BoundedChains α height
 
-namespace FixedHeight
+namespace FiniteHeightLattice
 
-variable {α : Type*} [Lattice α] {h : ℕ}
+variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
 
-theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
+theorem bot_le (a : α) : (⊥ : α) ≤ a := by
-  intro a
   by_cases heq : ⊥ ⊓ a = ⊥
   · exact inf_eq_left.mp heq
   · exfalso
@@ -78,14 +77,6 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
     rw [RelSeries.cons_length, lc.length_series] at hbound
     omega
 
-end FixedHeight
-
-namespace FiniteHeightLattice
-
-variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
-
-theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
-
 end FiniteHeightLattice
 
 end Spa

lean/Spa/Lattice/FiniteMap.lean

@@ -516,7 +516,7 @@ def fixedHeight [FiniteHeightLattice B] (ks : List A) :
     FiniteHeightLattice (FiniteMap A B ks) :=
   FiniteHeightLattice.transport
     (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
-    (toIter_ofIter ks) (fun fm => ofIter_toIter fm)
+    (toIter_ofIter ks) ofIter_toIter
 
 instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
   fixedHeight ks

lean/Spa/Lattice/Prod.lean

@@ -27,16 +27,13 @@ theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
   | succ n ih =>
     intro c hn
     have h0 : c.length ≠ 0 := by omega
+    haveI : NeZero c.length := ⟨h0⟩
     obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
       ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
     rw [RelSeries.last_tail] at hl₁ hl₂
     rw [RelSeries.head_tail] at hh₁ hh₂
     rw [RelSeries.tail_length] at hlen
-    have hstep : c.head < c 1 := by
+    have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
-      have h := c.step ⟨0, by omega⟩
-      have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
-        ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
-      rwa [h1] at h
     obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
     rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
       rcases eq_or_lt_of_le hle2 with heq2 | hlt2