Danila Fedorin
e2df847139
Convert every theorem to lemma (mathlib's default) except the headline results a reader of each module seeks out: analyze_correct (Forward/Sign/Constant), aFix_eq/aFix_le (Fixedpoint), trace (Language), and Stmt.cfg_sufficient (Language/Properties). lemma and theorem are interchangeable keywords, so no references change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
51 lines
1.4 KiB
Lean4
51 lines
1.4 KiB
Lean4
import Spa.Lattice.Prod
|
||
import Spa.Lattice.Unit
|
||
|
||
namespace Spa
|
||
|
||
universe u
|
||
|
||
def IterProd (A B : Type u) : ℕ → Type u
|
||
| 0 => B
|
||
| k + 1 => A × IterProd A B k
|
||
|
||
namespace IterProd
|
||
|
||
variable {A B : Type u}
|
||
|
||
instance lattice [Lattice A] [Lattice B] :
|
||
∀ k, Lattice (IterProd A B k)
|
||
| 0 => inferInstanceAs (Lattice B)
|
||
| k + 1 => @Prod.instLattice A (IterProd A B k) _ (lattice k)
|
||
|
||
instance decidableEq [DecidableEq A] [DecidableEq B] :
|
||
∀ k, DecidableEq (IterProd A B k)
|
||
| 0 => inferInstanceAs (DecidableEq B)
|
||
| k + 1 => @instDecidableEqProd A (IterProd A B k) _ (decidableEq k)
|
||
|
||
def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
|
||
| 0 => b
|
||
| k + 1 => (a, build a b k)
|
||
|
||
variable [Lattice A] [Lattice B]
|
||
|
||
def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
|
||
∀ k, FiniteHeightLattice (IterProd A B k)
|
||
| 0 => inferInstanceAs (FiniteHeightLattice B)
|
||
| k + 1 => @Spa.prod A (IterProd A B k) _ (lattice k) _ (fixedHeight k)
|
||
|
||
instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
|
||
FiniteHeightLattice (IterProd A B k) := fixedHeight k
|
||
|
||
lemma bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
|
||
∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
|
||
| 0 => rfl
|
||
| k + 1 => by
|
||
show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
|
||
= ((⊥ : A), build (⊥ : A) (⊥ : B) k)
|
||
rw [bot_fixedHeight k]
|
||
|
||
end IterProd
|
||
|
||
end Spa
|