From e2df847139375f9ab4063d0dabcab70335d1a5bb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 13:59:08 -0500 Subject: [PATCH] Adopt lemma as the default keyword 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 --- lean/Spa/Analysis/Constant.lean | 12 ++--- lean/Spa/Analysis/Forward.lean | 26 +++++------ lean/Spa/Analysis/Forward/Adapters.lean | 4 +- lean/Spa/Analysis/Forward/Lattices.lean | 20 ++++----- lean/Spa/Analysis/Reaching.lean | 2 +- lean/Spa/Analysis/Sign.lean | 16 +++---- lean/Spa/Analysis/Utils.lean | 2 +- lean/Spa/Fixedpoint.lean | 2 +- lean/Spa/Language.lean | 10 ++--- lean/Spa/Language/Graphs.lean | 30 ++++++------- lean/Spa/Language/Properties.lean | 44 +++++++++---------- lean/Spa/Language/Traces.lean | 2 +- lean/Spa/Lattice.lean | 10 ++--- lean/Spa/Lattice/AboveBelow.lean | 58 ++++++++++++------------- lean/Spa/Lattice/Bool.lean | 4 +- lean/Spa/Lattice/FiniteMap.lean | 30 ++++++------- lean/Spa/Lattice/IterProd.lean | 2 +- lean/Spa/Lattice/Prod.lean | 2 +- lean/Spa/Lattice/Tuple.lean | 8 ++-- lean/Spa/Lattice/Unit.lean | 2 +- 20 files changed, 143 insertions(+), 143 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 6d9983b..62386de 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -27,13 +27,13 @@ def minus : ConstLattice → ConstLattice → ConstLattice | _, top => top | mk z₁, mk z₂ => mk (z₁ - z₂) -theorem plus_mono₂ : Monotone₂ plus := +lemma plus_mono₂ : Monotone₂ plus := AboveBelow.monotone₂_of_strict plus (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 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 (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl) (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl) @@ -44,7 +44,7 @@ def interpConst : ConstLattice → Value → Prop | .top, _ => True | .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 rintro ⟨h₁, 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 | .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 | add e₁ e₂ ih₁ ih₂ => intro vs₁ vs₂ h @@ -93,7 +93,7 @@ instance exprEvaluator : ExprEvaluator ConstLattice prog := def output : String := 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₂)) : ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by 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₂) 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₂)) : ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by rcases g₁ with _ | _ | c₁ diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index d6ce19e..726ad2d 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -13,7 +13,7 @@ def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) : VariableValues L prog := (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 => 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 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 -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) : vs = updateVariablesForState s sv := 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 := updateAll_mem_eq (variablesAt_mem s (updateAll sv)) @@ -38,7 +38,7 @@ variable [FiniteHeightLattice L] def analyze (sv : StateVariables L prog) : StateVariables L prog := 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) variable [DecidableEq L] @@ -48,10 +48,10 @@ def result : StateVariables L prog := Fixedpoint.aFix analyze analyze_mono 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 -theorem joinForKey_initialState : +lemma joinForKey_initialState : joinForKey prog.initialState (result L prog) = botV L prog := by rw [joinForKey, prog.incoming_initialState_eq_nil] rfl @@ -59,7 +59,7 @@ theorem joinForKey_initialState : variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog] 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} (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) : ⟦ 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) omit [FiniteHeightLattice L] [DecidableEq L] in -theorem updateVariablesForState_matches {s : prog.State} +lemma updateVariablesForState_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂) (hvs : ⟦ variablesAt s sv ⟧ ρ₁) : @@ -76,14 +76,14 @@ theorem updateVariablesForState_matches {s : prog.State} eval_fold_valid hbss hvs 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) ρ₂) (hvs : ⟦ variablesAt s sv ⟧ ρ₁) : ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by rw [variablesAt_updateAll] exact updateVariablesForState_matches hbss hvs -theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} +lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) : ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by @@ -92,7 +92,7 @@ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} rw [variablesAt_joinAll] exact hjoin -theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} +lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁) (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by @@ -108,7 +108,7 @@ theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} exact ih (interp_foldr hstep hmem) omit V in -theorem interp_joinForKey_initialState : +lemma interp_joinForKey_initialState : ⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by rw [joinForKey_initialState] exact interp_botV_nil diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean index d4e630d..8d0f9ca 100644 --- a/lean/Spa/Analysis/Forward/Adapters.lean +++ b/lean/Spa/Analysis/Forward/Adapters.lean @@ -10,7 +10,7 @@ def updateVariablesFromExpression (k : String) (e : Expr) (vs : VariableValues L prog) : VariableValues L prog := 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) := 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 | .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 cases bs with | assign k e => exact updateVariablesFromExpression_mono k e diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index 54bd62f..80b7e3b 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -18,7 +18,7 @@ def botV [FiniteHeightLattice L] : VariableValues L prog := variable {L prog} 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_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 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 := (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₂ := FiniteMap.le_of_mem_mem prog.states_nodup hle (variablesAt_mem s sv₁) (variablesAt_mem s sv₂) @@ -42,7 +42,7 @@ def joinForKey (k : prog.State) (sv : StateVariables L prog) : VariableValues 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 intro sv₁ sv₂ hle 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 := 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 -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) : vs = joinForKey s sv := 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 := 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 → ∀ (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 cases hmem 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 intro k l hmem v hv 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.inr (h _ _ h₂ _ hv)) -theorem interp_foldr {vs : VariableValues L prog} +lemma interp_foldr {vs : VariableValues L prog} {vss : List (VariableValues L prog)} {ρ : Env} (hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) : ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index 8a40e24..b34137f 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -23,7 +23,7 @@ def eval (s : prog.State) : FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] 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 cases bs with | assign k e => diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index bf841d3..24e43ac 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -55,7 +55,7 @@ def minus : SignLattice → SignLattice → SignLattice | mk .zero, mk .minus => mk .plus | mk .zero, mk .zero => mk .zero -theorem plus_mono₂ : Monotone₂ plus := +lemma plus_mono₂ : Monotone₂ plus := AboveBelow.monotone₂_of_strict plus (fun y => by cases y <;> 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 <;> first | exact absurd rfl hx | rfl | (cases s <;> rfl)) -theorem minus_mono₂ : Monotone₂ minus := +lemma minus_mono₂ : Monotone₂ minus := AboveBelow.monotone₂_of_strict minus (fun y => by cases y <;> 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 .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 rintro ⟨h₁, h₂⟩ rcases s₁ <;> rcases s₂ <;> try exact hne rfl @@ -125,7 +125,7 @@ def eval : Expr → VariableValues SignLattice prog → SignLattice | .num 0, _ => .mk .zero | .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 | add e₁ e₂ ih₁ ih₂ => intro vs₁ vs₂ h @@ -154,18 +154,18 @@ def output : String := show' (result SignLattice prog) /-- 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 · rintro ⟨n, rfl⟩; omega · intro h; exact ⟨(z - 1).toNat, by omega⟩ /-- 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 · rintro ⟨n, rfl⟩; 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₂)) : ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;> @@ -174,7 +174,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} at h₁ h₂ ⊢ <;> 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₂)) : ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;> diff --git a/lean/Spa/Analysis/Utils.lean b/lean/Spa/Analysis/Utils.lean index a950ee2..225b5da 100644 --- a/lean/Spa/Analysis/Utils.lean +++ b/lean/Spa/Analysis/Utils.lean @@ -2,7 +2,7 @@ import Spa.Lattice 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} (h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ := le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂) diff --git a/lean/Spa/Fixedpoint.lean b/lean/Spa/Fixedpoint.lean index f0ee408..8dc04ef 100644 --- a/lean/Spa/Fixedpoint.lean +++ b/lean/Spa/Fixedpoint.lean @@ -34,7 +34,7 @@ theorem aFix_eq (f : α → α) (hf : Monotone f) : aFix f hf = f (aFix f hf) := (fix f hf).2 -theorem doStep_le (f : α → α) (hf : Monotone f) +lemma doStep_le (f : α → α) (hf : Monotone f) {b : α} (hb : b = f b) : ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1) (hle : c.last ≤ f c.last), c.last ≤ b → diff --git a/lean/Spa/Language.lean b/lean/Spa/Language.lean index eebc152..69400ce 100644 --- a/lean/Spa/Language.lean +++ b/lean/Spa/Language.lean @@ -33,23 +33,23 @@ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : 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 -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 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 (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₂ := p.cfg.mem_predecessors_of_edge h diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index af0a6b2..7dc919f 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -41,10 +41,10 @@ def map (f : α → β) (g : GGraph α) : GGraph β where inputs := g.inputs outputs := g.outputs -@[simp] theorem 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] theorem 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_size (f : α → β) (g : GGraph α) : (g.map f).size = g.size := rfl +@[simp] lemma map_edges (f : α → β) (g : GGraph α) : (g.map f).edges = g.edges := rfl +@[simp] lemma map_inputs (f : α → β) (g : GGraph α) : (g.map f).inputs = g.inputs := rfl +@[simp] lemma map_outputs (f : α → β) (g : GGraph α) : (g.map f).outputs = g.outputs := rfl def comp (g₁ g₂ : GGraph α) : GGraph α where size := g₁.size + g₂.size @@ -79,9 +79,9 @@ def loop (g : GGraph (List β)) : GGraph (List β) where inputs := [g.loopIn] 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 size := g₁.size + g₂.size @@ -101,10 +101,10 @@ def singleton (a : α) : GGraph α where def wrap (g : GGraph (List β)) : GGraph (List β) := singleton [] ⤳ g ⤳ singleton [] -@[simp] theorem map_singleton (f : α → β) (a : α) : +@[simp] lemma map_singleton (f : α → β) (a : α) : (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 rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩ simp only [GGraph.map, GGraph.comp] @@ -112,7 +112,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) := funext i 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 rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩ simp only [GGraph.map, GGraph.link] @@ -120,7 +120,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) := funext i 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 rcases g with ⟨n, nd, e, i, o⟩ simp only [GGraph.map, GGraph.loop] @@ -128,7 +128,7 @@ def wrap (g : GGraph (List β)) : GGraph (List β) := funext i 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 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 -theorem mem_indices (idx : g.Index) : idx ∈ g.indices := +lemma mem_indices (idx : g.Index) : idx ∈ g.indices := List.mem_finRange idx -theorem nodup_indices : g.indices.Nodup := +lemma nodup_indices : g.indices.Nodup := List.nodup_finRange g.size def predecessors (idx : g.Index) : List g.Index := 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₂ := 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 simpa using (List.mem_filter.mp h).2 diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 9c7069e..ce57bf4 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -4,7 +4,7 @@ namespace Spa 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 intro h have := congrArg Fin.val h @@ -17,7 +17,7 @@ section Embeddings 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₂ ρ₁ ρ₂) : Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by 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] · 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₂ ρ₁ ρ₂) : Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by 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] · 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₂ ρ₁ ρ₂) : Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by 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] · 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₂ ρ₁ ρ₂) : Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by induction tr with @@ -66,21 +66,21 @@ theorem Trace.link_right {idx₁ idx₂ : g₂.Index} · exact List.mem_append_left _ (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 obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr 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₂), tr.comp_left⟩ -theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : +lemma EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr 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₂), tr.comp_right⟩ -theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂) +lemma EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂) (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂ @@ -98,7 +98,7 @@ section Loop 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 induction tr with | 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 _ (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 = [] := 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 = [] := 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 obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr -- 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 (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 refine List.mem_append_right _ ?_ 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) ρ₂ ρ₃) : EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by 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 _, 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 := 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 _, @@ -161,16 +161,16 @@ end Loop /-! ### 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) ρ₁ ρ₂ := ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _, Trace.single h⟩ -theorem EndToEndTrace.singleton_nil (ρ : Env) : +lemma EndToEndTrace.singleton_nil (ρ : Env) : EndToEndTrace (Graph.singleton []) ρ ρ := EndToEndTrace.singleton EvalBasicStmts.nil -theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env} +lemma EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env} (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ := (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 := 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 -theorem Graph.wrap_outputs (g : Graph) : +lemma Graph.wrap_outputs (g : Graph) : (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, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge) ∉ (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 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) : (Graph.wrap g).predecessors idx = [] := by rw [Graph.wrap_inputs, List.mem_singleton] at h diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 2568c0e..703b4f4 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -10,7 +10,7 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges → 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₂ ρ₁ ρ₂) (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) : Trace g idx₁ idx₄ ρ₁ ρ₃ := by diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index 3957f4a..d6ef43b 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -11,7 +11,7 @@ section Folds 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₂) (hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) : 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 => 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₂) (hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) : 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)) 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 intro b₁ b₂ hb induction l with @@ -38,7 +38,7 @@ theorem foldr_mono' (l : List α) (f : α → β → β) | cons x xs ih => exact hf x ih 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 intro b₁ b₂ hb induction l generalizing b₁ b₂ with @@ -65,7 +65,7 @@ namespace FiniteHeightLattice variable (α : Type*) [Lattice α] [FiniteHeightLattice α] -theorem bot_le (a : α) : (⊥ : α) ≤ a := by +lemma bot_le (a : α) : (⊥ : α) ≤ a := by by_cases heq : ⊥ ⊓ a = ⊥ · exact inf_eq_left.mp heq · exfalso diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 0448e4f..05bd6fe 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -34,47 +34,47 @@ instance : Min (AboveBelow α) where | mk _, bot => bot | mk x, top => mk x -@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl -@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl -@[simp] theorem 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] theorem mk_sup_mk (x y : α) : +@[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl +@[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl +@[simp] lemma sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl +@[simp] lemma sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl +@[simp] lemma mk_sup_mk (x y : α) : (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] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl -@[simp] theorem 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] theorem mk_inf_mk (x y : α) : +@[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl +@[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl +@[simp] lemma inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl +@[simp] lemma inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl +@[simp] lemma mk_inf_mk (x y : α) : (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 [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] 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 <;> simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] 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 [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] 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 <;> simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] 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 <;> simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> 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 <;> simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_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.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) -theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) := +lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) := 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) -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) -theorem bot_lt_top : (bot : AboveBelow α) < top := +lemma bot_lt_top : (bot : AboveBelow α) < top := 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 have hsup := le_iff.mp h 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. `Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these 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 γ) (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot) (htopl : ∀ y, y ≠ bot → f top y = top) @@ -154,7 +154,7 @@ section Interp 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 rcases s₁ with _ | _ | x · 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 · 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)) {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by rcases s₁ with _ | _ | x @@ -192,7 +192,7 @@ def rank : AboveBelow α → ℕ /-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and `[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 obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h 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 exact absurd hsup (by simp) -theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by +lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by intro a b hab rcases a with _ | _ | x <;> rcases b with _ | _ | y · exact absurd hab (lt_irrefl _) @@ -216,7 +216,7 @@ theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by · simp [rank] · 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) rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank] diff --git a/lean/Spa/Lattice/Bool.lean b/lean/Spa/Lattice/Bool.lean index fceea95..4f93174 100644 --- a/lean/Spa/Lattice/Bool.lean +++ b/lean/Spa/Lattice/Bool.lean @@ -17,11 +17,11 @@ def rank : Bool → ℕ | false => 0 | true => 1 -theorem rank_strictMono : StrictMono rank := by +lemma rank_strictMono : StrictMono rank := by intro a b hab 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) rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank] diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean index 3c476c0..24a1927 100644 --- a/lean/Spa/Lattice/FiniteMap.lean +++ b/lean/Spa/Lattice/FiniteMap.lean @@ -21,17 +21,17 @@ instance [DecidableEq B] : DecidableEq (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⟩ -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 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) := 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 obtain ⟨i, hi, _⟩ := h 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) := (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 section Locate @@ -57,7 +57,7 @@ end Locate 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} (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by 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 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₂) : ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by 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 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') (h : (k, v) ∈ updating fm ks' g) : v = g k := by 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] 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') (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by 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) 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) : updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by 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} -theorem generalizedUpdate_monotone (hf : Monotone f) +lemma generalizedUpdate_monotone (hf : Monotone f) (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') := fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl) 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 := eq_of_mem_updating (g := fun k => g k l) hk h 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 := 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 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 refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩ 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]) 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 show Option.Rel _ (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_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) : List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by induction ks' with diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean index 485f77f..d910735 100644 --- a/lean/Spa/Lattice/IterProd.lean +++ b/lean/Spa/Lattice/IterProd.lean @@ -37,7 +37,7 @@ def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] : instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (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 | 0 => rfl | k + 1 => by diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean index 2416b0b..a53a51b 100644 --- a/lean/Spa/Lattice/Prod.lean +++ b/lean/Spa/Lattice/Prod.lean @@ -6,7 +6,7 @@ section Unzip variable {α β : Type*} [PartialOrder α] [PartialOrder β] -theorem LTSeries.exists_unzip (c : LTSeries (α × β)) : +lemma LTSeries.exists_unzip (c : LTSeries (α × β)) : ∃ (c₁ : LTSeries α) (c₂ : LTSeries β), c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧ c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧ diff --git a/lean/Spa/Lattice/Tuple.lean b/lean/Spa/Lattice/Tuple.lean index ba1f964..ed37caa 100644 --- a/lean/Spa/Lattice/Tuple.lean +++ b/lean/Spa/Lattice/Tuple.lean @@ -17,14 +17,14 @@ private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B) | 0, _ => Fin.elim0 | _ + 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 | 0, _ => funext fun i => i.elim0 | _ + 1, f => by show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f 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 | 0, PUnit.unit => rfl | _ + 1, ip => by @@ -34,7 +34,7 @@ private theorem iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n), variable [Lattice B] -private theorem funOfIter_mono {n : ℕ} : +private lemma funOfIter_mono {n : ℕ} : Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by induction n with | 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 | 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 induction n with | zero => intro f g _; exact le_of_eq rfl diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean index a5763f6..4a3c537 100644 --- a/lean/Spa/Lattice/Unit.lean +++ b/lean/Spa/Lattice/Unit.lean @@ -2,7 +2,7 @@ import Spa.Lattice namespace Spa -theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α] +lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α] (n : ℕ) : BoundedChains α n := fun c => by by_contra hc push_neg at hc