diff --git a/lean/Main.lean b/lean/Main.lean index 298a365..ede1ffd 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -1,20 +1,14 @@ -/- -Port of `Main.agda`. Prints the constant- and sign-analysis results for the -test program (Agda: `putStrLn (output-Const ++ "\n" ++ output-Sign)`). --/ import Spa.Analysis.Sign import Spa.Analysis.Constant namespace Spa -/-- Agda: `testCode`. -/ def testCode : Stmt := .andThen (.basic (.assign "zero" (.num 0))) (.andThen (.basic (.assign "pos" (.add (.var "zero") (.num 1)))) (.andThen (.basic (.assign "neg" (.sub (.var "zero") (.num 1)))) (.basic (.assign "unknown" (.add (.var "pos") (.var "neg")))))) -/-- Agda: `testCodeCond₁`. -/ def testCodeCond₁ : Stmt := .andThen (.basic (.assign "var" (.num 1))) (.ifElse (.var "var") @@ -22,19 +16,16 @@ def testCodeCond₁ : Stmt := (.andThen (.basic (.assign "var" (.sub (.var "var") (.num 1)))) (.basic (.assign "var" (.num 1))))) -/-- Agda: `testCodeCond₂`. -/ def testCodeCond₂ : Stmt := .andThen (.basic (.assign "var" (.num 1))) (.ifElse (.var "var") (.basic (.assign "x" (.num 1))) (.basic .noop)) -/-- Agda: `testProgram`. -/ def testProgram : Program := ⟨testCode⟩ end Spa -/-- Agda: `main`. -/ def main : IO Unit := IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++ Spa.SignAnalysis.output Spa.testProgram) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 9ec3707..7aa6542 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -1,29 +1,3 @@ -/- -Port of `Analysis/Constant.agda`. - -Correspondence: - showable, ≡-equiv, ≡-Decidable-ℤ ↦ (mathlib/derived instances) - ConstLattice (AboveBelow ℤ) ↦ ConstLattice - AB.Plain (+ 0) ↦ the AboveBelow FiniteHeightLattice instance, - seeded by `Inhabited ℤ` (default `0`) - plus, minus ↦ plus, minus - plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!) - ↦ plus_mono_left/right, minus_mono_left/right - — now actually proved, via - AboveBelow.monotone₂_of_strict - plus-Mono₂, minus-Mono₂ ↦ plus_mono₂, minus_mono₂ - ⟦_⟧ᶜ ↦ interpConst - ⟦⟧ᶜ-respects-≈ᶜ ↦ (trivial with `=`) - ⟦⟧ᶜ-⊔ᶜ-∨, ⟦⟧ᶜ-⊓ᶜ-∧ ↦ interpConst_sup, interpConst_inf - s₁≢s₂⇒¬s₁∧s₂ ↦ interpConst_mk_disjoint - latticeInterpretationᶜ ↦ constInterpretation - WithProg.eval, eval-Monoʳ ↦ ConstAnalysis.eval, eval_mono - ConstEval ↦ ConstAnalysis.exprEvaluator - plus-valid, minus-valid ↦ plus_valid, minus_valid - eval-valid, ConstEvalValid ↦ eval_valid - output ↦ ConstAnalysis.output - analyze-correct ↦ ConstAnalysis.analyze_correct --/ import Spa.Analysis.Forward import Spa.Analysis.Utils import Spa.Interp @@ -36,7 +10,6 @@ abbrev ConstLattice : Type := AboveBelow ℤ namespace ConstAnalysis open AboveBelow in -/-- Agda: `plus`. -/ def plus : ConstLattice → ConstLattice → ConstLattice | bot, _ => bot | _, bot => bot @@ -45,7 +18,6 @@ def plus : ConstLattice → ConstLattice → ConstLattice | mk z₁, mk z₂ => mk (z₁ + z₂) open AboveBelow in -/-- Agda: `minus`. -/ def minus : ConstLattice → ConstLattice → ConstLattice | bot, _ => bot | _, bot => bot @@ -53,44 +25,33 @@ def minus : ConstLattice → ConstLattice → ConstLattice | _, top => top | mk z₁, mk z₂ => mk (z₁ - z₂) -/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a -strict operation on the flat lattice, so monotonicity holds regardless of the -constant table). -/ theorem 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) -/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/ theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂ -/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/ theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁ -/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/ theorem 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) (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl) -/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/ theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂ -/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/ theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁ -/-- Agda: `⟦_⟧ᶜ`. -/ def interpConst : ConstLattice → Value → Prop | .bot, _ => False | .top, _ => True | .mk z, v => v = .int z -/-- Agda: `⟦_⟧ᶜ` is registered for the `⟦_⟧` interpretation notation. -/ instance : Interp ConstLattice (Value → Prop) := ⟨interpConst⟩ -/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} : ¬(⟦(.mk z₁ : ConstLattice)⟧ v ∧ ⟦(.mk z₂ : ConstLattice)⟧ v) := by rintro ⟨h₁, h₂⟩ @@ -98,17 +59,14 @@ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Val injection h₂ with hz exact hne hz -/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨` (via the factored flat-lattice lemma). -/ theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value) (h : ⟦s₁⟧ v ∨ ⟦s₂⟧ v) : ⟦s₁ ⊔ s₂⟧ v := AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h -/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧` (via the factored flat-lattice lemma). -/ theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value) (h : ⟦s₁⟧ v ∧ ⟦s₂⟧ v) : ⟦s₁ ⊓ s₂⟧ v := AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h -/-- Agda: `latticeInterpretationᶜ` (an instance there too). -/ instance constInterpretation : LatticeInterpretation ConstLattice where interp := interpConst interp_sup := fun {l₁ l₂} v h => interpConst_sup (s₁ := l₁) (s₂ := l₂) v h @@ -116,7 +74,6 @@ instance constInterpretation : LatticeInterpretation ConstLattice where variable (prog : Program) -/-- Agda: `WithProg.eval`. -/ def eval : Expr → VariableValues ConstLattice prog → ConstLattice | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs) | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs) @@ -124,7 +81,6 @@ def eval : Expr → VariableValues ConstLattice prog → ConstLattice if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top | .num n, _ => .mk n -/-- Agda: `WithProg.eval-Monoʳ`. -/ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by induction e with | add e₁ e₂ ih₁ ih₂ => @@ -147,15 +103,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by intro vs₁ vs₂ _ exact le_refl _ -/-- Agda: the `ConstEval` instance. -/ instance exprEvaluator : ExprEvaluator ConstLattice prog := ⟨eval prog, eval_mono prog⟩ -/-- Agda: `WithProg.result`/`output`. -/ def output : String := show' (result ConstLattice prog) -/-- Agda: `plus-valid`. -/ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by @@ -173,7 +126,6 @@ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} show Value.int (z₁ + z₂) = Value.int (c₁ + c₂) rw [hz₁, hz₂] -/-- Agda: `minus-valid`. -/ theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by @@ -191,7 +143,6 @@ theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} show Value.int (z₁ - z₂) = Value.int (c₁ - c₂) rw [hz₁, hz₂] -/-- Agda: `eval-valid` / the `ConstEvalValid` instance. -/ instance eval_valid : ValidExprEvaluator ConstLattice prog := by constructor intro vs ρ e v hev @@ -222,7 +173,6 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂)) exact minus_valid h₁ h₂ -/-- Agda: `WithProg.analyze-correct`. -/ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : interpV (variablesAt prog.finalState (result ConstLattice prog)) ρ := Spa.analyze_correct ConstLattice prog hrun diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean index 9e24abb..07225d6 100644 --- a/lean/Spa/Analysis/Forward/Adapters.lean +++ b/lean/Spa/Analysis/Forward/Adapters.lean @@ -1,53 +1,32 @@ -/- -Port of `Analysis/Forward/Adapters.agda` (`ExprToStmtAdapter`). - -Correspondence: - updateVariablesFromExpression ↦ updateVariablesFromExpression - updateVariablesFromExpression-Mono ↦ updateVariablesFromExpression_mono - (the -k∈ks-≡ / -k∉ks-backward renames ↦ used directly from FiniteMap) - evalᵇ, evalᵇ-Monoʳ ↦ evalB, evalB_mono - stmtEvaluator (instance) ↦ instance StmtEvaluator L prog - evalᵇ-valid, validStmtEvaluator ↦ instance ValidStmtEvaluator L prog - (the Agda `k ≟ˢ k'` case split is - subsumed by `cases` on `Env.Mem`, - whose `here` case forces `k' = k`) --/ import Spa.Analysis.Forward.Evaluation namespace Spa variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog] -/-- Agda: `updateVariablesFromExpression` — set the single key `k` to the -value of `e` (the `GeneralizedUpdate` with `ks = [k]`). -/ def updateVariablesFromExpression (k : String) (e : Expr) (vs : VariableValues L prog) : VariableValues L prog := FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs -/-- Agda: `updateVariablesFromExpression-Mono`. -/ theorem updateVariablesFromExpression_mono (k : String) (e : Expr) : Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) := FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e) -/-- Agda: `evalᵇ`. -/ def evalB (_ : prog.State) (bs : BasicStmt) (vs : VariableValues L prog) : VariableValues L prog := match bs with | .assign k e => updateVariablesFromExpression k e vs | .noop => vs -/-- Agda: `evalᵇ-Monoʳ`. -/ theorem evalB_mono (s : prog.State) (bs : BasicStmt) : Monotone (evalB (L := L) (prog := prog) s bs) := by cases bs with | assign k e => exact updateVariablesFromExpression_mono k e | noop => exact monotone_id -/-- Agda: the `stmtEvaluator` instance of `ExprToStmtAdapter`. -/ instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog := ⟨evalB, evalB_mono⟩ -/-- Agda: `evalᵇ-valid` / the `validStmtEvaluator` instance. -/ instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L] [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by constructor diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index 8dd465d..818ff04 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -1,39 +1,22 @@ -/- -Port of `Analysis/Forward/Evaluation.agda`. - -All four records were consumed through Agda instance arguments (`{{evaluator : -StmtEvaluator}}`, `{{validEvaluator : ValidStmtEvaluator …}}`), so they are -typeclasses here as well. - -Correspondence: - StmtEvaluator (eval, eval-Monoʳ) ↦ StmtEvaluator (eval, eval_mono) - ExprEvaluator (eval, eval-Monoʳ) ↦ ExprEvaluator (eval, eval_mono) - ValidExprEvaluator ↦ ValidExprEvaluator (valid) - ValidStmtEvaluator ↦ ValidStmtEvaluator (valid) --/ import Spa.Analysis.Forward.Lattices namespace Spa variable (L : Type) [Lattice L] (prog : Program) -/-- Agda: `StmtEvaluator`. -/ class StmtEvaluator where eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog eval_mono : ∀ s bs, Monotone (eval s bs) -/-- Agda: `ExprEvaluator`. -/ class ExprEvaluator where eval : Expr → VariableValues L prog → L eval_mono : ∀ e, Monotone (eval e) -/-- Agda: `ValidExprEvaluator`. -/ class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] : Prop where valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value}, EvalExpr ρ e v → interpV vs ρ → I.interp (ExprEvaluator.eval e vs) v -/-- Agda: `ValidStmtEvaluator`. -/ class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] : Prop where valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index 4b1180c..bd3d36a 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -1,32 +1,3 @@ -/- -Port of `Analysis/Forward/Lattices.agda`. - -The Agda module instantiates `Lattice.FiniteMap` twice (variables ↦ abstract -values, states ↦ variable maps) and re-exports everything with ᵛ/ᵐ suffixes. -In Lean the two instantiations are `abbrev`s and the FiniteMap API is used -directly; the module parameters (the finite-height lattice `L`, the program) -become section variables, with the finite-height structure and the lattice -interpretation arriving by instance resolution as in Agda. - -Correspondence: - VariableValues, StateVariables ↦ VariableValues, StateVariables - isLatticeᵛ/isLatticeᵐ, ⊔ᵛ, ≼ᵛ … ↦ (the FiniteMap Lattice instances) - fixedHeightᵛ, fixedHeightᵐ ↦ (the FiniteMap FiniteHeightLattice instance) - ⊥ᵛ, ⊥ᵛ-contains-bottoms ↦ botV, FiniteMap.bot_contains_bots - states-in-Map ↦ states_memKey - variablesAt ↦ variablesAt - variablesAt-∈ ↦ variablesAt_mem - variablesAt-≈ ↦ (congruence, trivial with `=`) - joinForKey, joinForKey-Mono ↦ joinForKey, joinForKey_mono - joinAll, joinAll-Mono, - joinAll-k∈ks-≡ ↦ joinAll, joinAll_mono, joinAll_mem_eq - variablesAt-joinAll ↦ variablesAt_joinAll - ⟦_⟧ᵛ ↦ interpV - ⟦⊥ᵛ⟧ᵛ∅ ↦ interpV_botV_nil - ⟦⟧ᵛ-respects-≈ᵛ ↦ (trivial with `=`) - ⟦⟧ᵛ-⊔ᵛ-∨ ↦ interpV_sup - ⟦⟧ᵛ-foldr ↦ interpV_foldr --/ import Spa.Language import Spa.Lattice.FiniteMap @@ -34,36 +5,29 @@ namespace Spa variable (L : Type) [Lattice L] (prog : Program) -/-- Agda: `VariableValues`. -/ abbrev VariableValues : Type := FiniteMap String L prog.vars -/-- Agda: `StateVariables`. -/ abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states -/-- Agda: `⊥ᵛ` (the bottom of `fixedHeightᵛ`, now found by instance search). -/ def botV [FiniteHeightLattice L] : VariableValues L prog := (⊥ : VariableValues L prog) variable {L prog} omit [Lattice L] in -/-- Agda: `states-in-Map`. -/ theorem states_memKey (s : prog.State) (sv : StateVariables L prog) : FiniteMap.MemKey s sv := FiniteMap.memKey_iff.mpr (prog.states_complete s) -/-- Agda: `variablesAt`. -/ def variablesAt (s : prog.State) (sv : StateVariables L prog) : VariableValues L prog := (FiniteMap.locate (states_memKey s sv)).1 omit [Lattice L] in -/-- Agda: `variablesAt-∈`. -/ theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) : (s, variablesAt s sv) ∈ sv := (FiniteMap.locate (states_memKey s sv)).2 -/-- Agda: `m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ`, specialized the way `Forward.agda` uses it. -/ theorem 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 @@ -71,12 +35,10 @@ theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv variable [FiniteHeightLattice L] -/-- Agda: `joinForKey`. -/ def joinForKey (k : prog.State) (sv : StateVariables L prog) : VariableValues L prog := (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog) -/-- Agda: `joinForKey-Mono`. -/ theorem joinForKey_mono (k : prog.State) : Monotone (joinForKey (L := L) k) := by intro sv₁ sv₂ hle @@ -84,21 +46,17 @@ theorem joinForKey_mono (k : prog.State) : (fun b _ _ hab => sup_le_sup_right hab b) (fun a _ _ hab => sup_le_sup_left hab a) -/-- Agda: `joinAll` (the "Exercise 4.26" generalized update with `f = id`). -/ def joinAll (sv : StateVariables L prog) : StateVariables L prog := FiniteMap.generalizedUpdate id joinForKey prog.states sv -/-- Agda: `joinAll-Mono`. -/ theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) := FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono -/-- Agda: `joinAll-k∈ks-≡`. -/ theorem 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 -/-- Agda: `variablesAt-joinAll`. -/ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : variablesAt s (joinAll sv) = joinForKey s sv := joinAll_mem_eq (variablesAt_mem s (joinAll sv)) @@ -108,18 +66,15 @@ theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) : variable [I : LatticeInterpretation L] omit [FiniteHeightLattice L] in -/-- Agda: `⟦_⟧ᵛ`. -/ def interpV (vs : VariableValues L prog) (ρ : Env) : Prop := ∀ (k : String) (l : L), (k, l) ∈ vs → ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v -/-- Agda: `⟦⊥ᵛ⟧ᵛ∅`. -/ theorem interpV_botV_nil : interpV (botV L prog) [] := by intro k l _ v hmem cases hmem omit [FiniteHeightLattice L] in -/-- Agda: `⟦⟧ᵛ-⊔ᵛ-∨`. -/ theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env} (h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by intro k l hmem v hv @@ -128,7 +83,6 @@ theorem interpV_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)) -/-- Agda: `⟦⟧ᵛ-foldr`. -/ theorem interpV_foldr {vs : VariableValues L prog} {vss : List (VariableValues L prog)} {ρ : Env} (hvs : interpV vs ρ) (hmem : vs ∈ vss) : diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 0629c09..842ba23 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -86,7 +86,6 @@ def interpSign : SignLattice → Value → Prop | .mk .zero, v => v = .int 0 | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1)) -/-- Agda: `⟦_⟧ᵍ` is registered for the `⟦_⟧` interpretation notation. -/ instance signInterp : Interp SignLattice (Value → Prop) := ⟨interpSign⟩ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} : diff --git a/lean/Spa/Analysis/Utils.lean b/lean/Spa/Analysis/Utils.lean index bb9d5e3..a950ee2 100644 --- a/lean/Spa/Analysis/Utils.lean +++ b/lean/Spa/Analysis/Utils.lean @@ -1,12 +1,7 @@ -/- -Port of `Analysis/Utils.agda`. The `≼ᴼ-trans` module parameter lifts into the -`Preorder` instance. --/ import Spa.Lattice namespace Spa -/-- Agda: `eval-combine₂`. -/ theorem 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₄ := diff --git a/lean/Spa/Isomorphism.lean b/lean/Spa/Isomorphism.lean index ed15ba8..ce900f8 100644 --- a/lean/Spa/Isomorphism.lean +++ b/lean/Spa/Isomorphism.lean @@ -2,9 +2,6 @@ import Spa.Lattice namespace Spa -/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. Transport a -`FiniteHeightLattice` structure along a monotone inverse pair `f : α → β`, -`g : β → α`. -/ def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β] [I : FiniteHeightLattice α] (f : α → β) (g : β → α) (hf : Monotone f) (hg : Monotone g) diff --git a/lean/Spa/Language.lean b/lean/Spa/Language.lean index e1596c1..b7947ba 100644 --- a/lean/Spa/Language.lean +++ b/lean/Spa/Language.lean @@ -1,24 +1,3 @@ -/- -Port of `Language.agda` (the `Program` record and re-exports). - -Correspondence: - Program record ↦ structure Program (defs in the `Program` namespace) - graph ↦ Program.graph - State ↦ Program.State - initialState ↦ Program.initialState - finalState ↦ Program.finalState - trace ↦ Program.trace - vars, vars-Unique ↦ Program.vars, Program.vars_nodup - (Finset.toList + Finset.nodup_toList replace - `to-Listˢ` and the intrinsic MapSet uniqueness) - states, states-complete, states-Unique - ↦ Program.states, .states_complete, .states_nodup - code ↦ Program.code - _≟_, _≟ᵉ_ ↦ (instances, automatic for Fin/products) - incoming ↦ Program.incoming - initialState-pred-∅ ↦ Program.incoming_initialState_eq_nil - edge⇒incoming ↦ Program.mem_incoming_of_edge --/ import Spa.Language.Base import Spa.Language.Semantics import Spa.Language.Graphs @@ -44,7 +23,6 @@ def initialState : p.State := (buildCfg p.rootStmt).wrapInput def finalState : p.State := (buildCfg p.rootStmt).wrapOutput -/-- Agda: `Program.trace`. -/ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : Trace p.graph p.initialState p.finalState [] ρ := by obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_sufficient h) @@ -53,34 +31,24 @@ theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) : subst h₁; subst h₂ exact tr -/-- Agda: `vars` (via `vars-Set = Stmt-vars rootStmt`). `Finset.toList` is -noncomputable, so the variables are listed in sorted order instead — this is -the computable stand-in for MapSet's `to-List`. -/ def vars : List String := p.rootStmt.vars.sort (· ≤ ·) -/-- Agda: `vars-Unique`. -/ theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _ def states : List p.State := p.graph.indices -/-- Agda: `states-complete`. -/ theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s -/-- Agda: `states-Unique`. -/ theorem states_nodup : p.states.Nodup := p.graph.nodup_indices -/-- Agda: `code`. -/ def code (st : p.State) : List BasicStmt := p.graph.nodes st -/-- Agda: `incoming`. -/ def incoming (s : p.State) : List p.State := p.graph.predecessors s -/-- Agda: `initialState-pred-∅`. -/ theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] := Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _) -/-- Agda: `edge⇒incoming`. -/ theorem mem_incoming_of_edge {s₁ s₂ : p.State} (h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ := p.graph.mem_predecessors_of_edge h diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean index 2c596d5..1228cc3 100644 --- a/lean/Spa/Language/Base.lean +++ b/lean/Spa/Language/Base.lean @@ -1,21 +1,3 @@ -/- -Port of `Language/Base.agda`. - -`StringSet` (built on `Lattice/MapSet.agda`, itself on `Lattice/Map.agda`) is -lifted to mathlib's `Finset String`: `insertˢ ↦ insert`, `emptyˢ ↦ ∅`, -`singletonˢ ↦ {·}`, `_⊔ˢ_ ↦ ∪`, `to-List ↦ Finset.toList` (with -`Finset.nodup_toList` standing in for the intrinsic `Unique` proof). - -Constructor renaming (Agda mixfix has no direct Lean counterpart): - _+_ ↦ Expr.add _-_ ↦ Expr.sub `_ ↦ Expr.var #_ ↦ Expr.num - _←_ ↦ BasicStmt.assign noop ↦ BasicStmt.noop - ⟨_⟩ ↦ Stmt.basic _then_ ↦ Stmt.andThen - if_then_else_ ↦ Stmt.ifElse while_repeat_ ↦ Stmt.whileLoop - -The `_∈ᵉ_` / `_∈ᵇ_` variable-occurrence relations are ported as -`Expr.HasVar` / `BasicStmt.HasVar`; the commented-out lemmas relating them to -`Expr-vars` remain unported (they were commented out in the Agda, too). --/ import Mathlib.Data.Finset.Basic namespace Spa @@ -39,7 +21,6 @@ inductive Stmt where | whileLoop (e : Expr) (s : Stmt) deriving DecidableEq -/-- Agda: `_∈ᵉ_`. -/ inductive Expr.HasVar : String → Expr → Prop | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂) | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂) @@ -47,31 +28,26 @@ inductive Expr.HasVar : String → Expr → Prop | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂) | here {k} : Expr.HasVar k (.var k) -/-- Agda: `_∈ᵇ_`. -/ inductive BasicStmt.HasVar : String → BasicStmt → Prop | assignLeft {k e} : BasicStmt.HasVar k (.assign k e) | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e) -/-- Agda: `Expr-vars`. -/ def Expr.vars : Expr → Finset String | .add l r => l.vars ∪ r.vars | .sub l r => l.vars ∪ r.vars | .var s => {s} | .num _ => ∅ -/-- Agda: `BasicStmt-vars`. -/ def BasicStmt.vars : BasicStmt → Finset String | .assign x e => {x} ∪ e.vars | .noop => ∅ -/-- Agda: `Stmt-vars`. -/ def Stmt.vars : Stmt → Finset String | .basic bs => bs.vars | .andThen s₁ s₂ => s₁.vars ∪ s₂.vars | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars | .whileLoop e s => e.vars ∪ s.vars -/-- Agda: `Stmts-vars`. -/ def Stmt.varsList (ss : List Stmt) : Finset String := ss.foldr (fun s acc => s.vars ∪ acc) ∅ diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index c7756b3..7b89631 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -1,29 +1,3 @@ -/- -Port of `Language/Graphs.agda`. - -Representation note: `nodes : Vec (List BasicStmt) size` becomes -`nodes : Fin size → List BasicStmt`. With that, the `Data.Vec` lookup/append -lemma stack (`lookup-++ˡ/ʳ`, `cast-is-id`, …) lifts into mathlib's -`Fin.append` with `Fin.append_left` / `Fin.append_right`. - -Correspondence: - _↑ˡ_/_↑ʳ_ (on Fin) ↦ Fin.castAdd / Fin.natAdd (mathlib) - _↑ˡⁱ_/_↑ʳⁱ_ ↦ liftIdxL / liftIdxR - _↑ˡᵉ_/_↑ʳᵉ_ ↦ liftEdgeL / liftEdgeR - _∙_ ↦ Graph.comp (scoped notation ∙) - _↦_ ↦ Graph.link (scoped notation ⤳) - loop ↦ Graph.loop - _skipto_ ↦ Graph.skipto - _[_] ↦ Graph.nodes (plain application) - singleton, wrap ↦ Graph.singleton, Graph.wrap - buildCfg ↦ buildCfg - indices ↦ List.finRange (mathlib; `fins` from Utils.agda) - indices-complete ↦ List.mem_finRange - indices-Unique ↦ List.nodup_finRange - predecessors ↦ Graph.predecessors - edge⇒predecessor ↦ Graph.mem_predecessors_of_edge - predecessor⇒edge ↦ Graph.edge_of_mem_predecessors --/ import Spa.Language.Base import Mathlib.Data.Fin.Tuple.Basic import Mathlib.Data.List.ProdSigma @@ -44,25 +18,20 @@ abbrev Index (g : Graph) : Type := Fin g.size abbrev Edge (g : Graph) : Type := g.Index × g.Index -/-- Agda: `_↑ˡⁱ_`. -/ def liftIdxL {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) := l.map (Fin.castAdd m) -/-- Agda: `_↑ʳⁱ_`. -/ def liftIdxR (n : ℕ) {m : ℕ} (l : List (Fin m)) : List (Fin (n + m)) := l.map (Fin.natAdd n) -/-- Agda: `_↑ˡᵉ_` (with `_↑ˡ_` on pairs inlined). -/ def liftEdgeL {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) : List (Fin (n + m) × Fin (n + m)) := l.map (fun e => (e.1.castAdd m, e.2.castAdd m)) -/-- Agda: `_↑ʳᵉ_` (with `_↑ʳ_` on pairs inlined). -/ def liftEdgeR (n : ℕ) {m : ℕ} (l : List (Fin m × Fin m)) : List (Fin (n + m) × Fin (n + m)) := l.map (fun e => (e.1.natAdd n, e.2.natAdd n)) -/-- Agda: `_∙_` — disjoint union. -/ def comp (g₁ g₂ : Graph) : Graph where size := g₁.size + g₂.size nodes := Fin.append g₁.nodes g₂.nodes @@ -72,7 +41,6 @@ def comp (g₁ g₂ : Graph) : Graph where @[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp -/-- Agda: `_↦_` — sequencing: all outputs of `g₁` feed all inputs of `g₂`. -/ def link (g₁ g₂ : Graph) : Graph where size := g₁.size + g₂.size nodes := Fin.append g₁.nodes g₂.nodes @@ -89,7 +57,6 @@ def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size /-- The exit node of a `loop` graph. -/ def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size -/-- Agda: `loop`. -/ def loop (g : Graph) : Graph where size := 2 + g.size nodes := Fin.append (fun _ : Fin 2 => []) g.nodes @@ -104,7 +71,6 @@ def loop (g : Graph) : Graph where @[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl -/-- Agda: `_skipto_` (unused by `buildCfg`, ported for parity). -/ def skipto (g₁ g₂ : Graph) : Graph where size := g₁.size + g₂.size nodes := Fin.append g₁.nodes g₂.nodes @@ -113,7 +79,6 @@ def skipto (g₁ g₂ : Graph) : Graph where inputs := liftIdxL g₁.inputs g₂.size outputs := liftIdxR g₁.size g₂.inputs -/-- Agda: `singleton`. -/ def singleton (bss : List BasicStmt) : Graph where size := 1 nodes := fun _ => bss @@ -121,14 +86,12 @@ def singleton (bss : List BasicStmt) : Graph where inputs := [0] outputs := [0] -/-- Agda: `wrap`. -/ def wrap (g : Graph) : Graph := singleton [] ⤳ g ⤳ singleton [] end Graph open Graph in -/-- Agda: `buildCfg`. -/ def buildCfg : Stmt → Graph | .basic bs => Graph.singleton [bs] | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂ @@ -139,27 +102,21 @@ namespace Graph variable (g : Graph) -/-- Agda: `indices` (`fins` is mathlib's `List.finRange`). -/ def indices : List g.Index := List.finRange g.size -/-- Agda: `indices-complete`. -/ theorem mem_indices (idx : g.Index) : idx ∈ g.indices := List.mem_finRange idx -/-- Agda: `indices-Unique`. -/ theorem nodup_indices : g.indices.Nodup := List.nodup_finRange g.size -/-- Agda: `predecessors`. -/ def predecessors (idx : g.Index) : List g.Index := g.indices.filter (fun idx' => (idx', idx) ∈ g.edges) -/-- Agda: `edge⇒predecessor`. -/ theorem 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⟩ -/-- Agda: `predecessor⇒edge`. -/ theorem 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 c67983d..ab4b2b0 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -1,36 +1,9 @@ -/- -Port of `Language/Properties.agda`. - -Correspondence: - ↑-≢ (and the whole "ugly" Fin-disjointness block: - idx→f∉↑ʳᵉ, idx→f∉pair, idx→f∉cart, help, helpAll) - ↦ Fin.castAdd_ne_natAdd + not_mem_edges_castAdd_link - (mathlib `List.mem_append`/`mem_map`/`mem_product` - replace the hand-rolled membership eliminations) - wrap-preds-∅ ↦ wrap_predecessors_eq_nil - wrap-input, wrap-output ↦ Graph.wrapInput/wrapOutput + wrap_inputs/wrap_outputs - Trace-∙ˡ/ʳ ↦ Trace.comp_left / Trace.comp_right - Trace-↦ˡ/ʳ ↦ Trace.link_left / Trace.link_right - Trace-loop ↦ Trace.loop - EndToEndTrace-∙ˡ/ʳ ↦ EndToEndTrace.comp_left / .comp_right - loop-edge-groups, - loop-edge-help ↦ (inlined: the four edge groups are reached through - `List.mem_append` directly) - EndToEndTrace-loop ↦ EndToEndTrace.loop - EndToEndTrace-loop² ↦ EndToEndTrace.loop_concat - EndToEndTrace-loop⁰ ↦ EndToEndTrace.loop_empty - _++_ ↦ EndToEndTrace.concat - EndToEndTrace-singleton ↦ EndToEndTrace.singleton (+ .singleton_nil) - EndToEndTrace-wrap ↦ EndToEndTrace.wrap - buildCfg-sufficient ↦ buildCfg_sufficient --/ import Spa.Language.Traces namespace Spa open Graph -/-- Agda: `↑-≢`. -/ theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) : Fin.castAdd m i ≠ Fin.natAdd n j := by intro h @@ -44,7 +17,6 @@ section Embeddings variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} -/-- Agda: `Trace-∙ˡ`. -/ theorem Trace.comp_left {idx₁ idx₂ : g₁.Index} (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by @@ -57,7 +29,6 @@ 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) -/-- Agda: `Trace-∙ʳ`. -/ theorem Trace.comp_right {idx₁ idx₂ : g₂.Index} (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by @@ -70,7 +41,6 @@ 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) -/-- Agda: `Trace-↦ˡ`. -/ theorem Trace.link_left {idx₁ idx₂ : g₁.Index} (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by @@ -83,7 +53,6 @@ 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)) -/-- Agda: `Trace-↦ʳ`. -/ theorem Trace.link_right {idx₁ idx₂ : g₂.Index} (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by @@ -97,7 +66,6 @@ theorem Trace.link_right {idx₁ idx₂ : g₂.Index} · exact List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he)) -/-- Agda: `EndToEndTrace-∙ˡ`. -/ theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) : EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr @@ -105,7 +73,6 @@ theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) : i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂), tr.comp_left⟩ -/-- Agda: `EndToEndTrace-∙ʳ`. -/ theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr @@ -113,7 +80,6 @@ theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) : i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂), tr.comp_right⟩ -/-- Agda: `_++_` — sequencing end-to-end traces over `⤳`. -/ theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂) (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁ @@ -132,7 +98,6 @@ section Loop variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} -/-- Agda: `Trace-loop`. -/ theorem 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 @@ -155,7 +120,6 @@ private theorem loop_nodes_at_out : (Graph.loop g).nodes g.loopOut = [] := Fin.append_left (fun _ : Fin 2 => []) g.nodes 1 -/-- Agda: `EndToEndTrace-loop`. -/ theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr @@ -176,7 +140,6 @@ private theorem loop_edge_out_in : refine List.mem_append_right _ ?_ exact List.mem_cons_self _ _ -/-- Agda: `EndToEndTrace-loop²`. -/ theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂) (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) : EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by @@ -187,7 +150,6 @@ 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₂⟩ -/-- Agda: `EndToEndTrace-loop⁰`. -/ theorem 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 _ _)) @@ -199,24 +161,19 @@ end Loop /-! ### Singletons, wrap, and the main result -/ -/-- Agda: `EndToEndTrace-singleton`. -/ theorem 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⟩ -/-- Agda: `EndToEndTrace-singleton[]`. -/ theorem EndToEndTrace.singleton_nil (ρ : Env) : EndToEndTrace (Graph.singleton []) ρ ρ := EndToEndTrace.singleton EvalBasicStmts.nil -/-- Agda: `EndToEndTrace-wrap`. -/ theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env} (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ := (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂)) -/-- Agda: `buildCfg-sufficient` — every terminating execution is witnessed by -an end-to-end trace through the control-flow graph. -/ theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env} (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by induction h with @@ -235,11 +192,9 @@ theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env} /-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/ -/-- The input of `wrap g` (Agda: `wrap-input`). -/ def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index := (0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size) -/-- The output of `wrap g` (Agda: `wrap-output`). -/ def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index := Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1))) @@ -249,8 +204,6 @@ theorem Graph.wrap_inputs (g : Graph) : theorem Graph.wrap_outputs (g : Graph) : (Graph.wrap g).outputs = [g.wrapOutput] := rfl -/-- Agda: `help`/`helpAll` — no edge of `singleton [] ⤳ g₂` ends at a -`castAdd`-injected node (all edge targets are `natAdd`s). -/ private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1) (idx : (Graph.singleton [] ⤳ g₂).Index) : ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge) @@ -268,8 +221,6 @@ 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 -/-- Agda: `wrap-preds-∅` — the entry node of a wrapped graph has no -incoming edges. -/ theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index) (h : idx ∈ (Graph.wrap g).inputs) : (Graph.wrap g).predecessors idx = [] := by diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean index f849885..848c7fd 100644 --- a/lean/Spa/Language/Semantics.lean +++ b/lean/Spa/Language/Semantics.lean @@ -1,21 +1,3 @@ -/- -Port of `Language/Semantics.agda`. - -Correspondence: - Value (↑ᶻ) ↦ Value.int - Env ↦ Env (= List (String × Value)) - _∈_ (env lookup) ↦ Env.Mem - _,_⇒ᵉ_ ↦ EvalExpr - _,_⇒ᵇ_ ↦ EvalBasicStmt - _,_⇒ᵇˢ_ ↦ EvalBasicStmts - _,_⇒ˢ_ ↦ EvalStmt - LatticeInterpretation: - ⟦_⟧ ↦ interp - ⟦⟧-respects-≈ ↦ (trivial with `=`; field dropped) - ⟦⟧-⊔-∨ ↦ interp_sup - ⟦⟧-⊓-∧ ↦ interp_inf - (the `Utils` combinators `_⇒_`, `_∨_`, `_∧_` are inlined as plain logic) --/ import Spa.Language.Base import Spa.Lattice @@ -27,13 +9,11 @@ inductive Value where def Env : Type := List (String × Value) -/-- Agda: `_∈_` on environments — lookup respecting shadowing. -/ inductive Env.Mem : String × Value → Env → Prop | here (s : String) (v : Value) (ρ : Env) : Env.Mem (s, v) ((s, v) :: ρ) | there (s s' : String) (v v' : Value) (ρ : Env) : ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ) -/-- Agda: `_,_⇒ᵉ_`. -/ inductive EvalExpr : Env → Expr → Value → Prop | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n) | var (ρ : Env) (x : String) (v : Value) : @@ -45,20 +25,17 @@ inductive EvalExpr : Env → Expr → Value → Prop EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) → EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂)) -/-- Agda: `_,_⇒ᵇ_`. -/ inductive EvalBasicStmt : Env → BasicStmt → Env → Prop | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ | assign (ρ : Env) (x : String) (e : Expr) (v : Value) : EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ) -/-- Agda: `_,_⇒ᵇˢ_`. -/ inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop | nil {ρ : Env} : EvalBasicStmts ρ [] ρ | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} : EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ → EvalBasicStmts ρ₁ (bs :: bss) ρ₃ -/-- Agda: `_,_⇒ˢ_`. -/ inductive EvalStmt : Env → Stmt → Env → Prop | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) : EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂ @@ -79,8 +56,6 @@ inductive EvalStmt : Env → Stmt → Env → Prop EvalExpr ρ e (.int 0) → EvalStmt ρ (.whileLoop e s) ρ -/-- Agda: `LatticeInterpretation` (used there as an instance argument `⦃·⦄`, -hence a typeclass here). -/ class LatticeInterpretation (L : Type*) [Lattice L] where interp : L → Value → Prop interp_sup : ∀ {l₁ l₂ : L} (v : Value), diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 92019d1..2568c0e 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -1,18 +1,8 @@ -/- -Port of `Language/Traces.agda`. - -Correspondence: - Trace ↦ Trace (a `Prop`-valued inductive; only used in proofs) - _++⟨_⟩_ ↦ Trace.concat - EndToEndTrace ↦ EndToEndTrace (a `Prop`-valued structure, like `∃`; its - fields are accessed by destructuring inside proofs) --/ import Spa.Language.Semantics import Spa.Language.Graphs namespace Spa -/-- Agda: `Trace`. -/ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop | single {ρ₁ ρ₂ : Env} {idx : g.Index} : EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂ @@ -20,7 +10,6 @@ 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₃ ρ₁ ρ₃ -/-- Agda: `_++⟨_⟩_`. -/ theorem 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₄ ρ₂ ρ₃) : @@ -29,7 +18,6 @@ theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} | single hbs => exact Trace.edge hbs he tr₂ | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂) -/-- Agda: `EndToEndTrace` (an existential package, destructured in proofs). -/ inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs) (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs) diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 737bfd8..0448e4f 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -1,25 +1,7 @@ -/- -Port of `Lattice/AboveBelow.agda`: the flat lattice obtained by adjoining a -top and bottom element to an (unordered, decidable-equality) type. - -With propositional equality the `_≈_` data type and its equivalence/decidability -proofs disappear (`deriving DecidableEq`). The lattice itself cannot be lifted: -mathlib has no "flat lattice on a discrete type". The `Lattice` instance is -built with `Lattice.mk'`, which — exactly like the Agda module — consumes the -two semilattices (comm/assoc, idempotence derived) plus the absorption laws, -and defines `a ≤ b ↔ a ⊔ b = b` (Agda's `_≼_`). - -The Agda module's `Plain x` submodule (the witness `x` seeds the longest chain -`⊥ ≺ [x] ≺ ⊤`) becomes `plainFixedHeight x`; the boundedness proof `isLongest` -is restated through a rank function since chains are mathlib `LTSeries` rather -than a pattern-matchable inductive (the `¬-Chain-⊤`-style case analysis lives -in `rank_strictMono`). --/ import Spa.Lattice namespace Spa -/-- Agda: `AboveBelow` with constructors `⊥`, `⊤`, `[_]`. -/ inductive AboveBelow (α : Type*) where | bot | top @@ -28,7 +10,6 @@ inductive AboveBelow (α : Type*) where namespace AboveBelow -/-- Agda: the `Showable` instance. -/ instance {α : Type*} [ToString α] : ToString (AboveBelow α) where toString | bot => "⊥" @@ -53,9 +34,6 @@ instance : Min (AboveBelow α) where | mk _, bot => bot | mk x, top => mk x -/-! Agda: `⊥⊔x≡x`, `⊤⊔x≡⊤`, `x⊔⊥≡x`, `x⊔⊤≡⊤`, and the `[x]⊔[y]` reductions -(`x≈y⇒[x]⊔[y]≡[x]` / `x̷≈y⇒[x]⊔[y]≡⊤` are the two branches of `mk_sup_mk`). -/ - @[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 @@ -70,46 +48,38 @@ instance : Min (AboveBelow α) where @[simp] theorem mk_inf_mk (x y : α) : (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl -/-- Agda: `⊔-comm`. -/ protected theorem 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 -/-- Agda: `⊔-assoc`. -/ protected theorem 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 -/-- Agda: `⊓-comm`. -/ protected theorem 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 -/-- Agda: `⊓-assoc`. -/ protected theorem 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 -/-- Agda: `absorb-⊔-⊓`. -/ protected theorem 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) -/-- Agda: `absorb-⊓-⊔`. -/ protected theorem 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] <;> try (split_ifs <;> simp_all) -/-- Agda: `isLattice` (via the two semilattices + absorption, like the Agda -record; `Lattice.mk'` derives idempotence and sets `a ≤ b ↔ a ⊔ b = b`). -/ instance : Lattice (AboveBelow α) := Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc AboveBelow.inf_comm AboveBelow.inf_assoc @@ -117,11 +87,9 @@ instance : Lattice (AboveBelow α) := theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm -/-- Agda: `⊥≺[x]` (the `≤` part; `⊥` is least). -/ theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a := le_iff.mpr (bot_sup a) -/-- Agda: `[x]≺⊤` (the `≤` part; `⊤` is greatest). -/ theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) := le_iff.mpr (sup_top a) @@ -134,9 +102,6 @@ theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top := theorem bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp) -/-- The order of the flat lattice, by cases (used to discharge the -monotonicity obligations that were `postulate`d in `Analysis/Sign.agda` and -`Analysis/Constant.agda`). -/ theorem le_cases {a b : AboveBelow α} (h : a ≤ b) : a = bot ∨ b = top ∨ a = b := by have hsup := le_iff.mp h @@ -183,18 +148,12 @@ theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ] · rw [htopr x hx]; exact le_top' _ · exact le_rfl -/-! ### Interpretations of flat lattices - -The `⟦⟧-⊔-∨` / `⟦⟧-⊓-∧` proofs of `Analysis/Sign.agda` and -`Analysis/Constant.agda` are the same case analysis; only the meaning of the -plain elements differs. Factored here, they need just `P ⊥ ↦ False`, -`P ⊤ ↦ True`, and (for `⊓`) disjointness of distinct plain elements. -/ +/-! ### Interpretations of flat lattices -/ section Interp variable {V : Type*} {P : AboveBelow α → V → Prop} -/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` / `⟦⟧ᶜ-⊔ᶜ-∨`, generalized. -/ theorem 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 @@ -208,7 +167,6 @@ 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 -/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` / `⟦⟧ᶜ-⊓ᶜ-∧`, generalized. -/ theorem 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 @@ -258,17 +216,12 @@ theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by · simp [rank] · exact absurd hab (not_mk_lt_mk x y) -/-- Agda: `isLongest` — no chain is longer than 2. -/ theorem 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] omega -/-- Agda: `Plain.longestChain`/`Plain.fixedHeight` and -`Plain.isFiniteHeightLattice`/`Plain.finiteHeightLattice` — the witness -(`default`, playing the role of the Agda module parameter `x`) seeds the chain -`⊥ ≺ [x] ≺ ⊤` of length 2. -/ instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where bot := bot top := top diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean index cffa120..e60a76b 100644 --- a/lean/Spa/Lattice/IterProd.lean +++ b/lean/Spa/Lattice/IterProd.lean @@ -1,21 +1,3 @@ -/- -Port of `Lattice/IterProd.agda`: the `k`-fold product `A × (A × ⋯ × B)`. - -With propositional equality and typeclasses, the Agda `Everything` record -(which threaded the lattice operations and the conditional fixed-height proof -through one recursion, so that the operations built by separate recursions -would agree) is no longer needed: the `Lattice` instance is one recursive -definition, and the fixed-height structure is another recursion over it. - -Correspondence: - IterProd ↦ Spa.IterProd - build ↦ Spa.IterProd.build - isLattice/lattice ↦ instance Spa.IterProd.instLattice - fixedHeight, - isFiniteHeightLattice, - finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ instFiniteHeight instance) - ⊥-built ↦ Spa.IterProd.bot_fixedHeight --/ import Spa.Lattice.Prod import Spa.Lattice.Unit @@ -23,8 +5,6 @@ namespace Spa universe u -/-- Agda: `IterProd k = iterate k (A × ·) B`. (As in the Agda module, `A` and -`B` are constrained to the same universe to keep the recursion simple.) -/ def IterProd (A B : Type u) : ℕ → Type u | 0 => B | k + 1 => A × IterProd A B k @@ -43,7 +23,6 @@ instance instDecidableEq [DecidableEq A] [DecidableEq B] : | 0 => inferInstanceAs (DecidableEq B) | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k) -/-- Agda: `build`. -/ def build (a : A) (b : B) : (k : ℕ) → IterProd A B k | 0 => b | k + 1 => (a, build a b k) diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean index 8567c2f..5959fba 100644 --- a/lean/Spa/Lattice/Unit.lean +++ b/lean/Spa/Lattice/Unit.lean @@ -1,23 +1,13 @@ -/- -Port of `Lattice/Unit.agda`. - -The lattice structure itself (`_⊔_`, `_⊓_`, all semilattice/lattice laws) is -lifted into mathlib: `PUnit.instLinearOrder` provides `Lattice PUnit`. -What remains is the fixed-height structure: the unit lattice has height 0. --/ import Spa.Lattice namespace Spa -/-- Chains in a subsingleton order are bounded by any `n` (Agda: the `bounded` -field of `Lattice/Unit.agda`'s `fixedHeight`, generalized). -/ theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α] (n : ℕ) : BoundedChains α n := fun c => by by_contra hc push_neg at hc exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _) -/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`. -/ instance : FiniteHeightLattice PUnit where bot := PUnit.unit top := PUnit.unit diff --git a/lean/Spa/Showable.lean b/lean/Spa/Showable.lean index 55d0e16..b4dd2ca 100644 --- a/lean/Spa/Showable.lean +++ b/lean/Spa/Showable.lean @@ -1,16 +1,8 @@ -/- -Port of `Showable.agda` (plus the `Showable` instances that lived on -`Lattice/Map.agda` and `Lattice/AboveBelow.agda`). - -Lean has `ToString`, but its `String` instance does not quote (the Agda one -does), so to reproduce the Agda output exactly we port the class as-is. --/ import Spa.Lattice.FiniteMap import Spa.Lattice.AboveBelow namespace Spa -/-- Agda: `Showable` (`show` is a Lean keyword, hence `show'`). -/ class Showable (α : Type*) where show' : α → String @@ -29,15 +21,12 @@ instance {α β : Type*} [Showable α] [Showable β] : Showable (α × β) := instance : Showable PUnit := ⟨fun _ => "()"⟩ -/-- Agda: the `Showable` instance of `Lattice/AboveBelow.agda`. -/ instance {α : Type*} [Showable α] : Showable (AboveBelow α) := ⟨fun | .bot => "⊥" | .top => "⊤" | .mk x => show' x⟩ -/-- Agda: the `Showable` instance of `Lattice/Map.agda` (inherited by -`FiniteMap`). -/ instance {α β : Type*} {ks : List α} [Showable α] [Showable β] : Showable (FiniteMap α β ks) := ⟨fun fm =>