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

Delete more LLM-generated comments from the migration

Browse Source
This commit is contained in:
Danila Fedorin
2026-06-23 12:29:46 -05:00
parent 21b2e3dd98
commit 7f753a4f38
18 changed files with 1 additions and 427 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -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

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

@@ -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

17
lean/Spa/Analysis/Forward/Evaluation.lean
View File

@@ -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}

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

@@ -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) :

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

@@ -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} :

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

@@ -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₄ :=

3
lean/Spa/Isomorphism.lean
View File

@@ -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)

32
lean/Spa/Language.lean
View File

@@ -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

24
lean/Spa/Language/Base.lean
View File

@@ -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) ∅

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

@@ -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

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

@@ -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

25
lean/Spa/Language/Semantics.lean
View File

@@ -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),

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

@@ -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)

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

@@ -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

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

@@ -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)

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

@@ -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

11
lean/Spa/Showable.lean
View File

@@ -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 =>