DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Adopt lemma as the default keyword

Browse Source 
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>
This commit is contained in:
Danila Fedorin
2026-06-25 13:59:08 -05:00
parent 5c9c8ac55c
commit e2df847139
20 changed files with 143 additions and 143 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
lean/Spa/Analysis/Constant.lean
View File

@@ -27,13 +27,13 @@ def minus : ConstLattice → ConstLattice → ConstLattice
| _, top => top | _, top => top
| mk z₁, mk z₂ => mk (z₁ - z₂) | mk z₁, mk z₂ => mk (z₁ - z₂)
theorem plus_mono₂ : Monotone₂ plus := lemma plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus AboveBelow.monotone₂_of_strict plus
(fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl) (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl) (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
(fun x hx => by cases x <;> first | exact absurd rfl hx | rfl) (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
theorem minus_mono₂ : Monotone₂ minus := lemma minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus AboveBelow.monotone₂_of_strict minus
(fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl) (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl) (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
@@ -44,7 +44,7 @@ def interpConst : ConstLattice → Value → Prop
| .top, _ => True | .top, _ => True
| .mk z, v => v = .int z | .mk z, v => v = .int z
theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} : lemma interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
rintro ⟨h₁, h₂⟩ rintro ⟨h₁, h₂⟩
rw [h₁] at h₂ rw [h₁] at h₂
@@ -65,7 +65,7 @@ def eval : Expr → VariableValues ConstLattice prog → ConstLattice
if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
| .num n, _ => .mk n | .num n, _ => .mk n
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
induction e with induction e with
| add e₁ e₂ ih₁ ih₂ => | add e₁ e₂ ih₁ ih₂ =>
intro vs₁ vs₂ h intro vs₁ vs₂ h
@@ -93,7 +93,7 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog :=
def output : String := def output : String :=
show' (result ConstLattice prog) show' (result ConstLattice prog)
theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} lemma plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
rcases g₁ with _ | _ | c₁ rcases g₁ with _ | _ | c₁
@@ -110,7 +110,7 @@ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
show Value.int (z₁ + z₂) = Value.int (c₁ + c₂) show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
rw [hz₁, hz₂] rw [hz₁, hz₂]
theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} lemma minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
rcases g₁ with _ | _ | c₁ rcases g₁ with _ | _ | c₁

26
lean/Spa/Analysis/Forward.lean
View File

@@ -13,7 +13,7 @@ def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
VariableValues L prog := VariableValues L prog :=
(prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv) (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
theorem updateVariablesForState_mono (s : prog.State) : lemma updateVariablesForState_mono (s : prog.State) :
Monotone (updateVariablesForState (L := L) s) := fun _ _ hle => Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s) foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)
@@ -21,15 +21,15 @@ def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
FiniteMap.generalizedUpdate id updateVariablesForState FiniteMap.generalizedUpdate id updateVariablesForState
prog.states sv prog.states sv
theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) := lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog} lemma updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
{sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) : {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) :
vs = updateVariablesForState s sv := vs = updateVariablesForState s sv :=
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem
theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) : lemma variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
variablesAt s (updateAll sv) = updateVariablesForState s sv := variablesAt s (updateAll sv) = updateVariablesForState s sv :=
updateAll_mem_eq (variablesAt_mem s (updateAll sv)) updateAll_mem_eq (variablesAt_mem s (updateAll sv))
@@ -38,7 +38,7 @@ variable [FiniteHeightLattice L]
def analyze (sv : StateVariables L prog) : StateVariables L prog := def analyze (sv : StateVariables L prog) : StateVariables L prog :=
updateAll (joinAll sv) updateAll (joinAll sv)
theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle => lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
updateAll_mono (joinAll_mono hle) updateAll_mono (joinAll_mono hle)
variable [DecidableEq L] variable [DecidableEq L]
@@ -48,10 +48,10 @@ def result : StateVariables L prog :=
Fixedpoint.aFix analyze analyze_mono Fixedpoint.aFix analyze analyze_mono
variable (L prog) in variable (L prog) in
theorem result_eq : result L prog = analyze (result L prog) := lemma result_eq : result L prog = analyze (result L prog) :=
Fixedpoint.aFix_eq analyze analyze_mono Fixedpoint.aFix_eq analyze analyze_mono
theorem joinForKey_initialState : lemma joinForKey_initialState :
joinForKey prog.initialState (result L prog) = botV L prog := by joinForKey prog.initialState (result L prog) = botV L prog := by
rw [joinForKey, prog.incoming_initialState_eq_nil] rw [joinForKey, prog.incoming_initialState_eq_nil]
rfl rfl
@@ -59,7 +59,7 @@ theorem joinForKey_initialState :
variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog] variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
omit [FiniteHeightLattice L] [DecidableEq L] in omit [FiniteHeightLattice L] [DecidableEq L] in
theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt} lemma eval_fold_valid {s : prog.State} {bss : List BasicStmt}
{vs : VariableValues L prog} {ρ₁ ρ₂ : Env} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) : (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by ⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
@@ -68,7 +68,7 @@ theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
| cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs) | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)
omit [FiniteHeightLattice L] [DecidableEq L] in omit [FiniteHeightLattice L] [DecidableEq L] in
theorem updateVariablesForState_matches {s : prog.State} lemma updateVariablesForState_matches {s : prog.State}
{sv : StateVariables L prog} {ρ₁ ρ₂ : Env} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
(hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) : (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
@@ -76,14 +76,14 @@ theorem updateVariablesForState_matches {s : prog.State}
eval_fold_valid hbss hvs eval_fold_valid hbss hvs
omit [FiniteHeightLattice L] [DecidableEq L] in omit [FiniteHeightLattice L] [DecidableEq L] in
theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog} lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
{ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) : (hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
rw [variablesAt_updateAll] rw [variablesAt_updateAll]
exact updateVariablesForState_matches hbss hvs exact updateVariablesForState_matches hbss hvs
theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
(hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
@@ -92,7 +92,7 @@ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
rw [variablesAt_joinAll] rw [variablesAt_joinAll]
exact hjoin exact hjoin
theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
(tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
@@ -108,7 +108,7 @@ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
exact ih (interp_foldr hstep hmem) exact ih (interp_foldr hstep hmem)
omit V in omit V in
theorem interp_joinForKey_initialState : lemma interp_joinForKey_initialState :
⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
rw [joinForKey_initialState] rw [joinForKey_initialState]
exact interp_botV_nil exact interp_botV_nil

4
lean/Spa/Analysis/Forward/Adapters.lean
View File

@@ -10,7 +10,7 @@ def updateVariablesFromExpression (k : String) (e : Expr)
(vs : VariableValues L prog) : VariableValues L prog := (vs : VariableValues L prog) : VariableValues L prog :=
FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
theorem updateVariablesFromExpression_mono (k : String) (e : Expr) : lemma updateVariablesFromExpression_mono (k : String) (e : Expr) :
Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) := Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e) FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
@@ -20,7 +20,7 @@ def evalBasicStmt (_ : prog.State) (bs : BasicStmt)
| .assign k e => updateVariablesFromExpression k e vs | .assign k e => updateVariablesFromExpression k e vs
| .noop => vs | .noop => vs
theorem evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) : lemma evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) :
Monotone (evalBasicStmt (L := L) (prog := prog) s bs) := by Monotone (evalBasicStmt (L := L) (prog := prog) s bs) := by
cases bs with cases bs with
| assign k e => exact updateVariablesFromExpression_mono k e | assign k e => exact updateVariablesFromExpression_mono k e

20
lean/Spa/Analysis/Forward/Lattices.lean
View File

@@ -18,7 +18,7 @@ def botV [FiniteHeightLattice L] : VariableValues L prog :=
variable {L prog} variable {L prog}
omit [Lattice L] in omit [Lattice L] in
theorem states_memKey (s : prog.State) (sv : StateVariables L prog) : lemma states_memKey (s : prog.State) (sv : StateVariables L prog) :
FiniteMap.MemKey s sv := FiniteMap.MemKey s sv :=
FiniteMap.MemKey_iff.mpr (prog.states_complete s) FiniteMap.MemKey_iff.mpr (prog.states_complete s)
@@ -27,11 +27,11 @@ def variablesAt (s : prog.State) (sv : StateVariables L prog) :
(FiniteMap.locate (states_memKey s sv)).1 (FiniteMap.locate (states_memKey s sv)).1
omit [Lattice L] in omit [Lattice L] in
theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) : lemma variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
(s, variablesAt s sv) ∈ sv := (s, variablesAt s sv) ∈ sv :=
(FiniteMap.locate (states_memKey s sv)).2 (FiniteMap.locate (states_memKey s sv)).2
theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂) lemma variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
(s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ := (s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
FiniteMap.le_of_mem_mem prog.states_nodup hle FiniteMap.le_of_mem_mem prog.states_nodup hle
(variablesAt_mem s sv₁) (variablesAt_mem s sv₂) (variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
@@ -42,7 +42,7 @@ def joinForKey (k : prog.State) (sv : StateVariables L prog) :
VariableValues L prog := VariableValues L prog :=
(sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog) (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
theorem joinForKey_mono (k : prog.State) : lemma joinForKey_mono (k : prog.State) :
Monotone (joinForKey (L := L) k) := by Monotone (joinForKey (L := L) k) := by
intro sv₁ sv₂ hle intro sv₁ sv₂ hle
exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _) exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
@@ -52,15 +52,15 @@ theorem joinForKey_mono (k : prog.State) :
def joinAll (sv : StateVariables L prog) : StateVariables L prog := def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
FiniteMap.generalizedUpdate id joinForKey prog.states sv FiniteMap.generalizedUpdate id joinForKey prog.states sv
theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) := lemma joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
theorem joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog} lemma joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
{sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) : {sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) :
vs = joinForKey s sv := vs = joinForKey s sv :=
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h
theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
variablesAt s (joinAll sv) = joinForKey s sv := variablesAt s (joinAll sv) = joinForKey s sv :=
joinAll_mem_eq (variablesAt_mem s (joinAll sv)) joinAll_mem_eq (variablesAt_mem s (joinAll sv))
@@ -74,12 +74,12 @@ instance : Interp (VariableValues L prog) (Env → Prop) where
∀ (k : String) (l : L), (k, l) ∈ vs → ∀ (k : String) (l : L), (k, l) ∈ vs →
∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by lemma interp_botV_nil : ⟦ botV L prog ⟧ [] := by
intro k l _ v hmem intro k l _ v hmem
cases hmem cases hmem
omit [FiniteHeightLattice L] in omit [FiniteHeightLattice L] in
theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} lemma interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
(h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by (h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
intro k l hmem v hv intro k l hmem v hv
obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
@@ -87,7 +87,7 @@ theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
· exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv)) · exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
· exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv)) · exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv))
theorem interp_foldr {vs : VariableValues L prog} lemma interp_foldr {vs : VariableValues L prog}
{vss : List (VariableValues L prog)} {ρ : Env} {vss : List (VariableValues L prog)} {ρ : Env}
(hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) : (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by

2
lean/Spa/Analysis/Reaching.lean
View File

@@ -23,7 +23,7 @@ def eval (s : prog.State) :
FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
| .noop, vs => vs | .noop, vs => vs
theorem eval_mono (s : prog.State) (bs : BasicStmt) : lemma eval_mono (s : prog.State) (bs : BasicStmt) :
Monotone (eval prog s bs) := by Monotone (eval prog s bs) := by
cases bs with cases bs with
| assign k e => | assign k e =>

16
lean/Spa/Analysis/Sign.lean
View File

@@ -55,7 +55,7 @@ def minus : SignLattice → SignLattice → SignLattice
| mk .zero, mk .minus => mk .plus | mk .zero, mk .minus => mk .plus
| mk .zero, mk .zero => mk .zero | mk .zero, mk .zero => mk .zero
theorem plus_mono₂ : Monotone₂ plus := lemma plus_mono₂ : Monotone₂ plus :=
AboveBelow.monotone₂_of_strict plus AboveBelow.monotone₂_of_strict plus
(fun y => by cases y <;> rfl) (fun y => by cases y <;> rfl)
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl)) (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
@@ -64,7 +64,7 @@ theorem plus_mono₂ : Monotone₂ plus :=
rcases x with _ | _ | s <;> rcases x with _ | _ | s <;>
first | exact absurd rfl hx | rfl | (cases s <;> rfl)) first | exact absurd rfl hx | rfl | (cases s <;> rfl))
theorem minus_mono₂ : Monotone₂ minus := lemma minus_mono₂ : Monotone₂ minus :=
AboveBelow.monotone₂_of_strict minus AboveBelow.monotone₂_of_strict minus
(fun y => by cases y <;> rfl) (fun y => by cases y <;> rfl)
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl)) (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
@@ -80,7 +80,7 @@ def interpSign : SignLattice → Value → Prop
| .mk .zero, v => v = .int 0 | .mk .zero, v => v = .int 0
| .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1)) | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} : lemma interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
rintro ⟨h₁, h₂⟩ rintro ⟨h₁, h₂⟩
rcases s₁ <;> rcases s₂ <;> try exact hne rfl rcases s₁ <;> rcases s₂ <;> try exact hne rfl
@@ -125,7 +125,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice
| .num 0, _ => .mk .zero | .num 0, _ => .mk .zero
| .num (_ + 1), _ => .mk .plus | .num (_ + 1), _ => .mk .plus
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
induction e with induction e with
| add e₁ e₂ ih₁ ih₂ => | add e₁ e₂ ih₁ ih₂ =>
intro vs₁ vs₂ h intro vs₁ vs₂ h
@@ -154,18 +154,18 @@ def output : String :=
show' (result SignLattice prog) show' (result SignLattice prog)
/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/ /-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by private lemma int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
constructor constructor
· rintro ⟨n, rfl⟩; omega · rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(z - 1).toNat, by omega⟩ · intro h; exact ⟨(z - 1).toNat, by omega⟩
/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/ /-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
constructor constructor
· rintro ⟨n, rfl⟩; omega · rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(-z - 1).toNat, by omega⟩ · intro h; exact ⟨(-z - 1).toNat, by omega⟩
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;> rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
@@ -174,7 +174,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
at h₁ h₂ ⊢ <;> at h₁ h₂ ⊢ <;>
omega omega
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} lemma minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;> rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>

2
lean/Spa/Analysis/Utils.lean
View File

@@ -2,7 +2,7 @@ import Spa.Lattice
namespace Spa namespace Spa
theorem eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O} lemma eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
(hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O} (hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O}
(h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ := (h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ :=
le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂) le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂)

2
lean/Spa/Fixedpoint.lean
View File

@@ -34,7 +34,7 @@ theorem aFix_eq (f : α → α) (hf : Monotone f) :
aFix f hf = f (aFix f hf) := aFix f hf = f (aFix f hf) :=
(fix f hf).2 (fix f hf).2
theorem doStep_le (f : α → α) (hf : Monotone f) lemma doStep_le (f : α → α) (hf : Monotone f)
{b : α} (hb : b = f b) : {b : α} (hb : b = f b) :
∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1) ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
(hle : c.last ≤ f c.last), c.last ≤ b → (hle : c.last ≤ f c.last), c.last ≤ b →

10
lean/Spa/Language.lean
View File

@@ -33,23 +33,23 @@ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
def vars : List String := p.rootStmt.vars.sort (· ≤ ·) def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _ lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
def states : List p.State := p.cfg.indices def states : List p.State := p.cfg.indices
theorem states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
theorem states_nodup : p.states.Nodup := p.cfg.nodup_indices lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
def code (st : p.State) : List BasicStmt := p.cfg.nodes st def code (st : p.State) : List BasicStmt := p.cfg.nodes st
def incoming (s : p.State) : List p.State := p.cfg.predecessors s def incoming (s : p.State) : List p.State := p.cfg.predecessors s
theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] := lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
(by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _) (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
theorem mem_incoming_of_edge {s₁ s₂ : p.State} lemma mem_incoming_of_edge {s₁ s₂ : p.State}
(h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ := (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
p.cfg.mem_predecessors_of_edge h p.cfg.mem_predecessors_of_edge h

30
lean/Spa/Language/Graphs.lean
View File

@@ -41,10 +41,10 @@ def map (f : α → β) (g : GGraph α) : GGraph β where
inputs := g.inputs inputs := g.inputs
outputs := g.outputs outputs := g.outputs
@[simp] theorem map_size (f : α → β) (g : GGraph α) : (g.map f).size = g.size := rfl @[simp] lemma map_size (f : α → β) (g : GGraph α) : (g.map f).size = g.size := rfl
@[simp] theorem map_edges (f : α → β) (g : GGraph α) : (g.map f).edges = g.edges := rfl @[simp] lemma map_edges (f : α → β) (g : GGraph α) : (g.map f).edges = g.edges := rfl
@[simp] theorem map_inputs (f : α → β) (g : GGraph α) : (g.map f).inputs = g.inputs := rfl @[simp] lemma map_inputs (f : α → β) (g : GGraph α) : (g.map f).inputs = g.inputs := rfl
@[simp] theorem map_outputs (f : α → β) (g : GGraph α) : (g.map f).outputs = g.outputs := rfl @[simp] lemma map_outputs (f : α → β) (g : GGraph α) : (g.map f).outputs = g.outputs := rfl
def comp (g₁ g₂ : GGraph α) : GGraph α where def comp (g₁ g₂ : GGraph α) : GGraph α where
size := g₁.size + g₂.size size := g₁.size + g₂.size
@@ -79,9 +79,9 @@ def loop (g : GGraph (List β)) : GGraph (List β) where
inputs := [g.loopIn] inputs := [g.loopIn]
outputs := [g.loopOut] outputs := [g.loopOut]
@[simp] theorem loop_inputs (g : GGraph (List β)) : (loop g).inputs = [g.loopIn] := rfl @[simp] lemma loop_inputs (g : GGraph (List β)) : (loop g).inputs = [g.loopIn] := rfl
@[simp] theorem loop_outputs (g : GGraph (List β)) : (loop g).outputs = [g.loopOut] := rfl @[simp] lemma loop_outputs (g : GGraph (List β)) : (loop g).outputs = [g.loopOut] := rfl
def skipto (g₁ g₂ : GGraph α) : GGraph α where def skipto (g₁ g₂ : GGraph α) : GGraph α where
size := g₁.size + g₂.size size := g₁.size + g₂.size
@@ -101,10 +101,10 @@ def singleton (a : α) : GGraph α where
def wrap (g : GGraph (List β)) : GGraph (List β) := def wrap (g : GGraph (List β)) : GGraph (List β) :=
singleton [] ⤳ g ⤳ singleton [] singleton [] ⤳ g ⤳ singleton []
@[simp] theorem map_singleton (f : α → β) (a : α) : @[simp] lemma map_singleton (f : α → β) (a : α) :
(singleton a).map f = singleton (f a) := rfl (singleton a).map f = singleton (f a) := rfl
@[simp] theorem map_comp (f : α → β) (g₁ g₂ : GGraph α) : @[simp] lemma map_comp (f : α → β) (g₁ g₂ : GGraph α) :
(g₁ ∙ g₂).map f = g₁.map f ∙ g₂.map f := by (g₁ ∙ g₂).map f = g₁.map f ∙ g₂.map f := by
rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩ rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
simp only [GGraph.map, GGraph.comp] simp only [GGraph.map, GGraph.comp]
@@ -112,7 +112,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) :=
funext i funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right] refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] theorem map_link (f : α → β) (g₁ g₂ : GGraph α) : @[simp] lemma map_link (f : α → β) (g₁ g₂ : GGraph α) :
(g₁ ⤳ g₂).map f = g₁.map f ⤳ g₂.map f := by (g₁ ⤳ g₂).map f = g₁.map f ⤳ g₂.map f := by
rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩ rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
simp only [GGraph.map, GGraph.link] simp only [GGraph.map, GGraph.link]
@@ -120,7 +120,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) :=
funext i funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right] refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] theorem map_loop (h : β → γ) (g : GGraph (List β)) : @[simp] lemma map_loop (h : β → γ) (g : GGraph (List β)) :
(loop g).map (List.map h) = loop (g.map (List.map h)) := by (loop g).map (List.map h) = loop (g.map (List.map h)) := by
rcases g with ⟨n, nd, e, i, o⟩ rcases g with ⟨n, nd, e, i, o⟩
simp only [GGraph.map, GGraph.loop] simp only [GGraph.map, GGraph.loop]
@@ -128,7 +128,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) :=
funext i funext i
refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right] refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
@[simp] theorem map_wrap (h : β → γ) (g : GGraph (List β)) : @[simp] lemma map_wrap (h : β → γ) (g : GGraph (List β)) :
(wrap g).map (List.map h) = wrap (g.map (List.map h)) := by (wrap g).map (List.map h) = wrap (g.map (List.map h)) := by
simp [GGraph.wrap, GGraph.map_link, GGraph.map_singleton] simp [GGraph.wrap, GGraph.map_link, GGraph.map_singleton]
@@ -136,20 +136,20 @@ variable (g : GGraph α)
def indices : List g.Index := List.finRange g.size def indices : List g.Index := List.finRange g.size
theorem mem_indices (idx : g.Index) : idx ∈ g.indices := lemma mem_indices (idx : g.Index) : idx ∈ g.indices :=
List.mem_finRange idx List.mem_finRange idx
theorem nodup_indices : g.indices.Nodup := lemma nodup_indices : g.indices.Nodup :=
List.nodup_finRange g.size List.nodup_finRange g.size
def predecessors (idx : g.Index) : List g.Index := def predecessors (idx : g.Index) : List g.Index :=
g.indices.filter (fun idx' => (idx', idx) ∈ g.edges) g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index} lemma mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
(h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ := (h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩ List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩
theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index} lemma edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
(h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by (h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
simpa using (List.mem_filter.mp h).2 simpa using (List.mem_filter.mp h).2

44
lean/Spa/Language/Properties.lean
View File

@@ -4,7 +4,7 @@ namespace Spa
open Graph open Graph
theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) : lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
Fin.castAdd m i ≠ Fin.natAdd n j := by Fin.castAdd m i ≠ Fin.natAdd n j := by
intro h intro h
have := congrArg Fin.val h have := congrArg Fin.val h
@@ -17,7 +17,7 @@ section Embeddings
variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
theorem Trace.comp_left {idx₁ idx₂ : g₁.Index} lemma Trace.comp_left {idx₁ idx₂ : g₁.Index}
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
induction tr with induction tr with
@@ -29,7 +29,7 @@ theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
· exact List.mem_append_left _ (List.mem_map_of_mem _ he) · exact List.mem_append_left _ (List.mem_map_of_mem _ he)
theorem Trace.comp_right {idx₁ idx₂ : g₂.Index} lemma Trace.comp_right {idx₁ idx₂ : g₂.Index}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
induction tr with induction tr with
@@ -41,7 +41,7 @@ theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right] · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
· exact List.mem_append_right _ (List.mem_map_of_mem _ he) · exact List.mem_append_right _ (List.mem_map_of_mem _ he)
theorem Trace.link_left {idx₁ idx₂ : g₁.Index} lemma Trace.link_left {idx₁ idx₂ : g₁.Index}
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
induction tr with induction tr with
@@ -53,7 +53,7 @@ theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
· rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
· exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)) · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
theorem Trace.link_right {idx₁ idx₂ : g₂.Index} lemma Trace.link_right {idx₁ idx₂ : g₂.Index}
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
induction tr with induction tr with
@@ -66,21 +66,21 @@ theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
· exact List.mem_append_left _ · exact List.mem_append_left _
(List.mem_append_right _ (List.mem_map_of_mem _ he)) (List.mem_append_right _ (List.mem_map_of_mem _ he))
theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) : lemma EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁), exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁),
i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂), i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
tr.comp_left⟩ tr.comp_left⟩
theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : lemma EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁), exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁),
i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂), i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
tr.comp_right⟩ tr.comp_right⟩
theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂) lemma EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
(etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂ obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
@@ -98,7 +98,7 @@ section Loop
variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) : lemma Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
induction tr with induction tr with
| single hbs => | single hbs =>
@@ -112,15 +112,15 @@ theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁
· exact List.mem_append_left _ (List.mem_append_left _ · exact List.mem_append_left _ (List.mem_append_left _
(List.mem_append_left _ (List.mem_map_of_mem _ he))) (List.mem_append_left _ (List.mem_map_of_mem _ he)))
private theorem loop_nodes_at_in : private lemma loop_nodes_at_in :
(Graph.loop g).nodes g.loopIn = [] := (Graph.loop g).nodes g.loopIn = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 0 Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
private theorem loop_nodes_at_out : private lemma loop_nodes_at_out :
(Graph.loop g).nodes g.loopOut = [] := (Graph.loop g).nodes g.loopOut = [] :=
Fin.append_left (fun _ : Fin 2 => []) g.nodes 1 Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) : lemma EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
-- the edge in → (2 ↑ʳ i₁), reached through the second edge group -- the edge in → (2 ↑ʳ i₁), reached through the second edge group
@@ -135,12 +135,12 @@ theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
(Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))) (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
private theorem loop_edge_out_in : private lemma loop_edge_out_in :
((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by ((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by
refine List.mem_append_right _ ?_ refine List.mem_append_right _ ?_
exact List.mem_cons_self _ _ exact List.mem_cons_self _ _
theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂) lemma EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
(etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) : (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
@@ -150,7 +150,7 @@ theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
Trace.concat tr₁ loop_edge_out_in tr₂⟩ Trace.concat tr₁ loop_edge_out_in tr₂⟩
theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by lemma EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges :=
List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _)) List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _))
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
@@ -161,16 +161,16 @@ end Loop
/-! ### Singletons, wrap, and the main result -/ /-! ### Singletons, wrap, and the main result -/
theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env} lemma EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
(h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ := (h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ :=
⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _, ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
Trace.single h⟩ Trace.single h⟩
theorem EndToEndTrace.singleton_nil (ρ : Env) : lemma EndToEndTrace.singleton_nil (ρ : Env) :
EndToEndTrace (Graph.singleton []) ρ ρ := EndToEndTrace (Graph.singleton []) ρ ρ :=
EndToEndTrace.singleton EvalBasicStmts.nil EndToEndTrace.singleton EvalBasicStmts.nil
theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env} lemma EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
(etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ := (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
(EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂)) (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
@@ -198,13 +198,13 @@ def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index := def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1))) Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
theorem Graph.wrap_inputs (g : Graph) : lemma Graph.wrap_inputs (g : Graph) :
(Graph.wrap g).inputs = [g.wrapInput] := rfl (Graph.wrap g).inputs = [g.wrapInput] := rfl
theorem Graph.wrap_outputs (g : Graph) : lemma Graph.wrap_outputs (g : Graph) :
(Graph.wrap g).outputs = [g.wrapOutput] := rfl (Graph.wrap g).outputs = [g.wrapOutput] := rfl
private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1) private lemma not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
(idx : (Graph.singleton [] ⤳ g₂).Index) : (idx : (Graph.singleton [] ⤳ g₂).Index) :
((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge) ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge)
∉ (Graph.singleton [] ⤳ g₂).edges := by ∉ (Graph.singleton [] ⤳ g₂).edges := by
@@ -221,7 +221,7 @@ private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
obtain ⟨j, -, heq⟩ := List.mem_map.mp hb obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
exact Fin.castAdd_ne_natAdd i j heq.symm exact Fin.castAdd_ne_natAdd i j heq.symm
theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index) lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
(h : idx ∈ (Graph.wrap g).inputs) : (h : idx ∈ (Graph.wrap g).inputs) :
(Graph.wrap g).predecessors idx = [] := by (Graph.wrap g).predecessors idx = [] := by
rw [Graph.wrap_inputs, List.mem_singleton] at h rw [Graph.wrap_inputs, List.mem_singleton] at h

2
lean/Spa/Language/Traces.lean
View File

@@ -10,7 +10,7 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges → EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃ Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} lemma Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂) {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
(he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) : (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
Trace g idx₁ idx₄ ρ₁ ρ₃ := by Trace g idx₁ idx₄ ρ₁ ρ₃ := by

10
lean/Spa/Lattice.lean
View File

@@ -11,7 +11,7 @@ section Folds
variable {α β : Type*} [Preorder α] [Preorder β] variable {α β : Type*} [Preorder α] [Preorder β]
theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β} lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂) (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
(hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) : (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
@@ -20,7 +20,7 @@ theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
| cons hxy _ ih => | cons hxy _ ih =>
exact le_trans (hf₁ _ hxy) (hf₂ _ ih) exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β} lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂) (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
(hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) : (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
@@ -30,7 +30,7 @@ theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy)) exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
omit [Preorder α] in omit [Preorder α] in
theorem foldr_mono' (l : List α) (f : α → β → β) lemma foldr_mono' (l : List α) (f : α → β → β)
(hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by (hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
intro b₁ b₂ hb intro b₁ b₂ hb
induction l with induction l with
@@ -38,7 +38,7 @@ theorem foldr_mono' (l : List α) (f : α → β → β)
| cons x xs ih => exact hf x ih | cons x xs ih => exact hf x ih
omit [Preorder α] in omit [Preorder α] in
theorem foldl_mono' (l : List α) (f : β → α → β) lemma foldl_mono' (l : List α) (f : β → α → β)
(hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by (hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
intro b₁ b₂ hb intro b₁ b₂ hb
induction l generalizing b₁ b₂ with induction l generalizing b₁ b₂ with
@@ -65,7 +65,7 @@ namespace FiniteHeightLattice
variable (α : Type*) [Lattice α] [FiniteHeightLattice α] variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
theorem bot_le (a : α) : (⊥ : α) ≤ a := by lemma bot_le (a : α) : (⊥ : α) ≤ a := by
by_cases heq : ⊥ ⊓ a = ⊥ by_cases heq : ⊥ ⊓ a = ⊥
· exact inf_eq_left.mp heq · exact inf_eq_left.mp heq
· exfalso · exfalso

58
lean/Spa/Lattice/AboveBelow.lean
View File

@@ -34,47 +34,47 @@ instance : Min (AboveBelow α) where
| mk _, bot => bot | mk _, bot => bot
| mk x, top => mk x | mk x, top => mk x
@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl @[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl @[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl @[simp] lemma sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl @[simp] lemma sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
@[simp] theorem mk_sup_mk (x y : α) : @[simp] lemma mk_sup_mk (x y : α) :
(mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl @[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl @[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl @[simp] lemma inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl @[simp] lemma inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
@[simp] theorem mk_inf_mk (x y : α) : @[simp] lemma mk_inf_mk (x y : α) :
(mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
[bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
split_ifs with h₁ h₂ h₂ <;> simp_all split_ifs with h₁ h₂ h₂ <;> simp_all
protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
split_ifs <;> simp_all split_ifs <;> simp_all
protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
[bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
split_ifs with h₁ h₂ h₂ <;> simp_all split_ifs with h₁ h₂ h₂ <;> simp_all
protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
split_ifs <;> simp_all split_ifs <;> simp_all
protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
try (split_ifs <;> simp_all) try (split_ifs <;> simp_all)
protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
@@ -85,24 +85,24 @@ instance : Lattice (AboveBelow α) :=
AboveBelow.inf_comm AboveBelow.inf_assoc AboveBelow.inf_comm AboveBelow.inf_assoc
AboveBelow.sup_inf_self AboveBelow.inf_sup_self AboveBelow.sup_inf_self AboveBelow.inf_sup_self
theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm lemma le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a := lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
le_iff.mpr (bot_sup a) le_iff.mpr (bot_sup a)
theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) := lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
le_iff.mpr (sup_top a) le_iff.mpr (sup_top a)
theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
lt_of_le_of_ne (bot_le' _) (by simp) lt_of_le_of_ne (bot_le' _) (by simp)
theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
lt_of_le_of_ne (le_top' _) (by simp) lt_of_le_of_ne (le_top' _) (by simp)
theorem bot_lt_top : (bot : AboveBelow α) < top := lemma bot_lt_top : (bot : AboveBelow α) < top :=
lt_of_le_of_ne (bot_le' _) (by simp) lt_of_le_of_ne (bot_le' _) (by simp)
theorem le_cases {a b : AboveBelow α} (h : a ≤ b) : lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
a = bot ∨ b = top ∨ a = b := by a = bot ∨ b = top ∨ a = b := by
have hsup := le_iff.mp h have hsup := le_iff.mp h
rcases a with _ | _ | x <;> rcases b with _ | _ | y rcases a with _ | _ | x <;> rcases b with _ | _ | y
@@ -125,7 +125,7 @@ theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
monotone in both arguments — regardless of its values on plain elements. monotone in both arguments — regardless of its values on plain elements.
`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these `Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
monotonicity facts for their `plus`/`minus`, all of which have this shape. -/ monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ] lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
(f : AboveBelow α → AboveBelow β → AboveBelow γ) (f : AboveBelow α → AboveBelow β → AboveBelow γ)
(hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot) (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
(htopl : ∀ y, y ≠ bot → f top y = top) (htopl : ∀ y, y ≠ bot → f top y = top)
@@ -154,7 +154,7 @@ section Interp
variable {V : Type*} {P : AboveBelow α → V → Prop} variable {V : Type*} {P : AboveBelow α → V → Prop}
theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v) lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
{s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
rcases s₁ with _ | _ | x rcases s₁ with _ | _ | x
· rw [bot_sup]; exact h.resolve_left (hbot v) · rw [bot_sup]; exact h.resolve_left (hbot v)
@@ -167,7 +167,7 @@ theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
· next heq => subst heq; exact h.elim id id · next heq => subst heq; exact h.elim id id
· exact htop v · exact htop v
theorem interp_inf_of lemma interp_inf_of
(hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v)) (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
{s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
rcases s₁ with _ | _ | x rcases s₁ with _ | _ | x
@@ -192,7 +192,7 @@ def rank : AboveBelow α → ℕ
/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and /-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/ `[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
intro h intro h
obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
have hsup := le_iff.mp hle have hsup := le_iff.mp hle
@@ -203,7 +203,7 @@ theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
· rw [if_neg hxy] at hsup · rw [if_neg hxy] at hsup
exact absurd hsup (by simp) exact absurd hsup (by simp)
theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
intro a b hab intro a b hab
rcases a with _ | _ | x <;> rcases b with _ | _ | y rcases a with _ | _ | x <;> rcases b with _ | _ | y
· exact absurd hab (lt_irrefl _) · exact absurd hab (lt_irrefl _)
@@ -216,7 +216,7 @@ theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
· simp [rank] · simp [rank]
· exact absurd hab (not_mk_lt_mk x y) · exact absurd hab (not_mk_lt_mk x y)
theorem boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono) have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank] have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]

4
lean/Spa/Lattice/Bool.lean
View File

@@ -17,11 +17,11 @@ def rank : Bool → ℕ
| false => 0 | false => 0
| true => 1 | true => 1
theorem rank_strictMono : StrictMono rank := by lemma rank_strictMono : StrictMono rank := by
intro a b hab intro a b hab
cases a <;> cases b <;> revert hab <;> decide cases a <;> cases b <;> revert hab <;> decide
theorem boundedChains : BoundedChains Bool 1 := fun c => by lemma boundedChains : BoundedChains Bool 1 := fun c => by
have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono) have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank] have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank]

30
lean/Spa/Lattice/FiniteMap.lean
View File

@@ -21,17 +21,17 @@ instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
instance : Membership (A × B) (FiniteMap A B ks) := instance : Membership (A × B) (FiniteMap A B ks) :=
⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩ ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
theorem mem_iff {fm : FiniteMap A B ks} {p : A × B} : lemma mem_iff {fm : FiniteMap A B ks} {p : A × B} :
p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks
theorem MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl lemma MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) := instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) :=
decidable_of_iff _ MemKey_iff.symm decidable_of_iff _ MemKey_iff.symm
theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks} lemma mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
(h : (k, v) ∈ fm) : MemKey k fm := by (h : (k, v) ∈ fm) : MemKey k fm := by
obtain ⟨i, hi, _⟩ := h obtain ⟨i, hi, _⟩ := h
have hik : ks.get i = k := hi have hik : ks.get i = k := hi
@@ -40,7 +40,7 @@ theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
def toList (fm : FiniteMap A B ks) : List (A × B) := def toList (fm : FiniteMap A B ks) : List (A × B) :=
(List.finRange ks.length).map fun i => (ks.get i, fm i) (List.finRange ks.length).map fun i => (ks.get i, fm i)
theorem le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} : lemma le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} :
fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
section Locate section Locate
@@ -57,7 +57,7 @@ end Locate
variable [Lattice B] variable [Lattice B]
theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks} lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
(hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B} (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
(h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
obtain ⟨i, hi, rfl⟩ := h₁ obtain ⟨i, hi, rfl⟩ := h₁
@@ -66,7 +66,7 @@ theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
subst hij subst hij
exact le_def.mp hle i exact le_def.mp hle i
theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B} lemma mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
(h : (k, v) ∈ fm₁ ⊔ fm₂) : (h : (k, v) ∈ fm₁ ⊔ fm₂) :
∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
@@ -80,7 +80,7 @@ def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A
fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
omit [Lattice B] in omit [Lattice B] in
theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} lemma eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
{ks' : List A} {g : A → B} (hk : k ∈ ks') {ks' : List A} {g : A → B} (hk : k ∈ ks')
(h : (k, v) ∈ updating fm ks' g) : v = g k := by (h : (k, v) ∈ updating fm ks' g) : v = g k := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
@@ -88,7 +88,7 @@ theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
rw [if_pos (by rw [hi]; exact hk), hi] rw [if_pos (by rw [hi]; exact hk), hi]
omit [Lattice B] in omit [Lattice B] in
theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} lemma mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
{ks' : List A} {g : A → B} (hk : k ∉ ks') {ks' : List A} {g : A → B} (hk : k ∉ ks')
(h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
@@ -96,7 +96,7 @@ theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i) show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
rw [if_neg (by rw [hi]; exact hk)] rw [if_neg (by rw [hi]; exact hk)]
theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A} lemma updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
{g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) : {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
rw [le_def] rw [le_def]
@@ -119,17 +119,17 @@ def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A} variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
theorem generalizedUpdate_monotone (hf : Monotone f) lemma generalizedUpdate_monotone (hf : Monotone f)
(hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') := (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl) fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
omit [Lattice B] [Lattice L] in omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks') lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
eq_of_mem_updating (g := fun k => g k l) hk h eq_of_mem_updating (g := fun k => g k l) hk h
omit [Lattice B] [Lattice L] in omit [Lattice B] [Lattice L] in
theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks') lemma generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
mem_of_mem_updating hk h mem_of_mem_updating hk h
@@ -148,7 +148,7 @@ def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
ks'.filterMap fm.lookup ks'.filterMap fm.lookup
omit [Lattice B] in omit [Lattice B] in
theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B} lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
{ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩ refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
@@ -161,7 +161,7 @@ theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
hks.get_inj_iff.mp (by rw [List.idxOf_get, hi]) hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
rw [this] rw [this]
private theorem lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) : private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) :
Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
show Option.Rel _ show Option.Rel _
(if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
@@ -170,7 +170,7 @@ private theorem lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm
· rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _) · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
· rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none
theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) lemma valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
(ks' : List A) : (ks' : List A) :
List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
induction ks' with induction ks' with

2
lean/Spa/Lattice/IterProd.lean
View File

@@ -37,7 +37,7 @@ def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) : instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
FiniteHeightLattice (IterProd A B k) := fixedHeight k FiniteHeightLattice (IterProd A B k) := fixedHeight k
theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] : lemma bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k ∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
| 0 => rfl | 0 => rfl
| k + 1 => by | k + 1 => by

2
lean/Spa/Lattice/Prod.lean
View File

@@ -6,7 +6,7 @@ section Unzip
variable {α β : Type*} [PartialOrder α] [PartialOrder β] variable {α β : Type*} [PartialOrder α] [PartialOrder β]
theorem LTSeries.exists_unzip (c : LTSeries (α × β)) : lemma LTSeries.exists_unzip (c : LTSeries (α × β)) :
∃ (c₁ : LTSeries α) (c₂ : LTSeries β), ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧ c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧ c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧

8
lean/Spa/Lattice/Tuple.lean
View File

@@ -17,14 +17,14 @@ private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B)
| 0, _ => Fin.elim0 | 0, _ => Fin.elim0
| _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2) | _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2)
private theorem funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B), private lemma funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B),
funOfIter (iterOfFun f) = f funOfIter (iterOfFun f) = f
| 0, _ => funext fun i => i.elim0 | 0, _ => funext fun i => i.elim0
| _ + 1, f => by | _ + 1, f => by
show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f
rw [funOfIter_iterOfFun (Fin.tail f), Fin.cons_self_tail] rw [funOfIter_iterOfFun (Fin.tail f), Fin.cons_self_tail]
private theorem iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n), private lemma iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n),
iterOfFun (funOfIter ip) = ip iterOfFun (funOfIter ip) = ip
| 0, PUnit.unit => rfl | 0, PUnit.unit => rfl
| _ + 1, ip => by | _ + 1, ip => by
@@ -34,7 +34,7 @@ private theorem iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n),
variable [Lattice B] variable [Lattice B]
private theorem funOfIter_mono {n : ℕ} : private lemma funOfIter_mono {n : ℕ} :
Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by
induction n with induction n with
| zero => intro _ _ _ i; exact i.elim0 | zero => intro _ _ _ i; exact i.elim0
@@ -47,7 +47,7 @@ private theorem funOfIter_mono {n : ℕ} :
| zero => rw [Fin.cons_zero, Fin.cons_zero]; exact h1 | zero => rw [Fin.cons_zero, Fin.cons_zero]; exact h1
| succ j => rw [Fin.cons_succ, Fin.cons_succ]; exact ih h2 j | succ j => rw [Fin.cons_succ, Fin.cons_succ]; exact ih h2 j
private theorem iterOfFun_mono {n : ℕ} : private lemma iterOfFun_mono {n : ℕ} :
Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by
induction n with induction n with
| zero => intro f g _; exact le_of_eq rfl | zero => intro f g _; exact le_of_eq rfl

2
lean/Spa/Lattice/Unit.lean
View File

@@ -2,7 +2,7 @@ import Spa.Lattice
namespace Spa namespace Spa
theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α] lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
(n : ℕ) : BoundedChains α n := fun c => by (n : ℕ) : BoundedChains α n := fun c => by
by_contra hc by_contra hc
push_neg at hc push_neg at hc