Compare commits
20 Commits
dag-lattic
...
f23705a93e
| Author | SHA1 | Date | |
|---|---|---|---|
| f23705a93e | |||
| b1dc725ced | |||
| ed88f4ce94 | |||
| 8ce6e5e4e4 | |||
| 6afa7df444 | |||
| 7f753a4f38 | |||
| 21b2e3dd98 | |||
| 5e0c002fd5 | |||
| 20daf817e4 | |||
| 2044d4b2b6 | |||
| 8c37a4c049 | |||
| 2ee32580a2 | |||
| b16f14fdfd | |||
| b26d6b5acd | |||
| a82d54666a | |||
| 739fbb503c | |||
| 2cfd0a2fb7 | |||
| 781d7947e0 | |||
| 4c337afa9c | |||
| ae030386b4 |
9
.claude/settings.json
Normal file
9
.claude/settings.json
Normal file
@@ -0,0 +1,9 @@
|
|||||||
|
{
|
||||||
|
"permissions": {
|
||||||
|
"allow": [
|
||||||
|
"Bash(lake build)",
|
||||||
|
"Bash(lake build *)",
|
||||||
|
"Bash(export PATH=\"$HOME/.elan/bin:$PATH\")"
|
||||||
|
]
|
||||||
|
}
|
||||||
|
}
|
||||||
117
LEAN_MIGRATION.md
Normal file
117
LEAN_MIGRATION.md
Normal file
@@ -0,0 +1,117 @@
|
|||||||
|
# Agda → Lean 4 (mathlib) migration plan
|
||||||
|
|
||||||
|
Goal: port the static-analysis framework to Lean 4 + mathlib, preserving the
|
||||||
|
overall structure and **the same theorems/lemmas** (modulo language details),
|
||||||
|
while lifting custom machinery into mathlib wherever a standard counterpart
|
||||||
|
exists. Per discussion, the setoid equality (`_≈_`) is **dropped in favor of
|
||||||
|
propositional `=`** — it existed mainly so that unordered key-value maps could
|
||||||
|
be "equal"; representations below are chosen to be canonical so `=` works.
|
||||||
|
|
||||||
|
The Lean project lives in `lean/` (library root `Spa`). Each phase ends with a
|
||||||
|
green `lake build` and a correspondence table appended to this file, so you can
|
||||||
|
validate phase by phase.
|
||||||
|
|
||||||
|
## Design mapping
|
||||||
|
|
||||||
|
| Agda | Lean | Notes |
|
||||||
|
|---|---|---|
|
||||||
|
| `Equivalence.agda` | *lifted*: `Eq`, `Equivalence` | module disappears |
|
||||||
|
| `IsDecidable` | *lifted*: `DecidableEq` / `DecidableRel` | mathlib is classical; decidability kept only where functions compute (e.g. the fixpoint iteration) |
|
||||||
|
| `Showable.agda` | *lifted*: `ToString` | |
|
||||||
|
| `Lattice.agda` `IsSemilattice` (`⊔-assoc/comm/idemp`, `≼`, `≼-refl/trans/antisym`, `x≼x⊔y`, `⊔-Monotonicˡ/ʳ`) | *lifted*: `SemilatticeSup` (`sup_assoc`, `sup_comm`, `sup_idem`, `≤` with `sup_eq_right`, `le_refl`, `le_trans`, `le_antisymm`, `le_sup_left`, `sup_le_sup_left/right`) | `a ≼ b := a ⊔ b ≈ b` becomes `a ≤ b` with bridge lemma `sup_eq_right` |
|
||||||
|
| `IsLattice` (`absorb-⊔-⊓`, `absorb-⊓-⊔`) | *lifted*: `Lattice` (`sup_inf_self`, `inf_sup_self`) | |
|
||||||
|
| `Monotonic`, `Monotonicˡ/ʳ/₂` | *lifted*: `Monotone` (+ tiny aliases) | |
|
||||||
|
| `foldr-Mono`, `foldl-Mono`, `foldr-Mono'`, `foldl-Mono'` | custom, `Spa/Lattice.lean` | stated with `List.Forall₂` (≙ `Utils.Pairwise`) |
|
||||||
|
| `Chain.agda` (`Chain`, `concat`, `Chain-map` in `ChainMapping`) | *lifted*: `LTSeries` (`RelSeries.smash`, `LTSeries.map` + `Monotone.strictMono_of_injective`) | with `=`, the ≈-congruence steps in chains vanish |
|
||||||
|
| `Chain.Height`, `Bounded`, `Bounded-suc-n` | custom: `Spa.FixedHeight` structure (`⊥`, `⊤`, longest `LTSeries`, `bounded`) | |
|
||||||
|
| `IsFiniteHeightLattice`, `FiniteHeightLattice` | custom class `Spa.FiniteHeightLattice` | |
|
||||||
|
| `⊥≼` (chain bottom is least, given decidable eq) | custom, same proof shape (prepend `⊥⊓a ≺ ⊥` to longest chain) | decidability hypothesis dropped (classical) |
|
||||||
|
| `Fixedpoint.agda` (`doStep` with gas, `aᶠ`, `aᶠ≈faᶠ`, `aᶠ≼`) | custom, `Spa/Fixedpoint.lean`, same gas-based algorithm | **not** replaced by mathlib `lfp` (would change the proof approach and lose computability) |
|
||||||
|
| `Isomorphism.agda` (`TransportFiniteHeight`) | custom, `Spa/Isomorphism.lean` | much smaller: with `=`, f/g monotone inverse pair transports `FixedHeight` via `LTSeries.map` |
|
||||||
|
| `Lattice/Unit.agda` | *lifted*: mathlib `Lattice PUnit`; custom `FixedHeight PUnit 0` | |
|
||||||
|
| `Lattice/Nat.agda` (max/min lattice) | *lifted*: mathlib `Lattice ℕ` (`Nat.instLattice`) | kept only as a remark; file had no fixed-height content |
|
||||||
|
| `Lattice/Prod.agda` | instance *lifted* (`Prod.instLattice`); custom: `unzip` + `FixedHeight (A×B) (h₁+h₂)` | same proof: split a product chain into component chains |
|
||||||
|
| `Lattice/AboveBelow.agda` (flat lattice ⊥/[x]/⊤) | custom, same datatype; `Plain` module ⇒ `FixedHeight 2` | mathlib has no flat-lattice-on-discrete-type |
|
||||||
|
| `Lattice/ExtendBelow.agda` | *lifted*: `WithBot A` lattice instance; custom `FixedHeight (h+1)` | unused by the pipeline; ported for parity (optional) |
|
||||||
|
| `Lattice/IterProd.agda` | custom, same induction (`IterProd k = A × … × B`), lattice + height-sum by recursion | the `Everything` record trick survives as a recursive definition of bundled instances |
|
||||||
|
| `Lattice/Map.agda` (assoc list with `Unique` keys, setoid) | **deleted**: only existed to support setoid map equality | its consumers move to `Finset` / spine-fixed `FiniteMap` |
|
||||||
|
| `Lattice/MapSet.agda` (`StringSet`) | *lifted*: `Finset String` (`∪`, `{·}`, `∅`, `.toList`, `nodup_toList`) | |
|
||||||
|
| `Lattice/FiniteMap.agda` | custom: `{ l : List (A × B) // l.map Prod.fst = ks }` — key spine fixed ⇒ `=` is pointwise value equality | same API: `locate`, `_[_]`, `GeneralizedUpdate` (`f'`, `f'-Monotonic`, `f'-k∈ks-≡`, `f'-k∉ks-backward`), `m₁≼m₂⇒m₁[k]≼m₂[k]`, `Provenance-union` analog; fixed height **still via isomorphism to `IterProd`** (same approach) |
|
||||||
|
| `Lattice/Builder.agda` | **skipped** — not imported by anything in the repo | flag if you want it |
|
||||||
|
| `Utils.agda` | *lifted*: `Unique`→`List.Nodup`, `Pairwise`→`List.Forall₂`, `fins`→`List.finRange`, `∈-cartesianProduct`→`List.product`/`pair_mem_product`, `x∈xs⇒fx∈fxs`→`List.mem_map_of_mem`, `filter-++`→`List.filter_append`, `iterate`→`f^[n]`, `concat-∈`→`List.mem_join`, `All¬-¬Any` etc. → `List.All`/`Any` API | leftovers (if any) in `Spa/Utils.lean` |
|
||||||
|
| `Language/Base.agda` | custom; `Expr-vars`/`Stmt-vars : Finset String` | commented-out `∈-vars` lemmas stay omitted |
|
||||||
|
| `Language/Semantics.agda` | custom, same big-step relations; `Value`, `Env = List (String × Value)`, custom `∈` | `ℤ` → `Int` |
|
||||||
|
| `Language/Graphs.agda` | custom; `Vec` → `Vector` (mathlib `List.Vector`), `Fin._↑ˡ/_↑ʳ` → `Fin.castAdd`/`Fin.natAdd` | same `Graph` record, `∙`/`↦`/`loop`/`skipto`/`singleton`/`wrap`/`buildCfg`, `predecessors` + edge lemmas |
|
||||||
|
| `Language/Traces.agda` | custom, same `Trace`/`EndToEndTrace`/`++⟨_⟩` | |
|
||||||
|
| `Language/Properties.agda` | custom, same lemma inventory (`Trace-∙ˡ/ʳ`, `Trace-↦ˡ/ʳ`, `Trace-loop`, `EndToEndTrace-*`, `wrap-preds-∅`, `buildCfg-sufficient`) | the "ugly" `↑-≢` Fin-disjointness block should shrink via `Fin.castAdd_ne_natAdd`-style mathlib lemmas |
|
||||||
|
| `Language.agda` (`Program` record) | custom, same fields/lemmas (`trace`, `vars`, `states`, `incoming`, `initialState-pred-∅`, …) | |
|
||||||
|
| `Analysis/Forward/{Lattices,Evaluation,Adapters}.agda`, `Analysis/Forward.agda` | custom, same structure: `VariableValues`, `StateVariables`, `joinForKey`/`joinAll`, `StmtEvaluator`/`ExprEvaluator` + validity, expr→stmt adapter, `analyze`, `result`, `analyze-correct` | section variables instead of parameterized modules; everything Agda passed as an instance argument (`IsFiniteHeightLattice`, the evaluators, `LatticeInterpretation`, the validity records) is a typeclass resolved by instance search |
|
||||||
|
| `Analysis/Sign.agda`, `Analysis/Constant.agda` | custom, same definitions | the four monotonicity **postulates** become real proofs (any `⊥`-strict/`⊤`-dominating operation on a flat lattice is monotone: `AboveBelow.monotone₂_of_strict`) |
|
||||||
|
| `Main.agda` | `lake exe spa` | same test programs, same printed output |
|
||||||
|
|
||||||
|
## Phases & checkpoints
|
||||||
|
|
||||||
|
- **Phase 0 — scaffold.** `lean/` lake project, mathlib pinned to toolchain
|
||||||
|
v4.17.0 (already installed). ✅ checkpoint: `lake build` green on empty lib.
|
||||||
|
- **Phase 1 — core order theory.** `Spa/Lattice.lean` (Monotone aliases, fold
|
||||||
|
monotonicity, `FixedHeight`, `Bounded`, `FiniteHeightLattice`, chain-bottom-
|
||||||
|
is-least). ✅ checkpoint: build + table below.
|
||||||
|
- **Phase 2 — fixpoint & transport.** `Spa/Fixedpoint.lean`,
|
||||||
|
`Spa/Isomorphism.lean`. ✅ checkpoint: `fix`, `fix_eq`, `fix_le`,
|
||||||
|
`TransportFiniteHeight`.
|
||||||
|
- **Phase 3 — basic lattice instances.** Unit, Prod (+height), AboveBelow
|
||||||
|
(+`Plain`, height 2), ExtendBelow. ✅ checkpoint.
|
||||||
|
- **Phase 4 — map lattices.** IterProd, FiniteMap (+fixed height via IterProd
|
||||||
|
isomorphism), MapSet→`Finset` shims. ✅ checkpoint.
|
||||||
|
- **Phase 5 — language.** Base, Semantics, Graphs, Traces, Properties,
|
||||||
|
`Program`. ✅ checkpoint: `buildCfg_sufficient`, `Program.trace`.
|
||||||
|
- **Phase 6 — forward analysis framework.** Lattices/Evaluation/Adapters/
|
||||||
|
Forward. ✅ checkpoint: `analyze_correct`.
|
||||||
|
- **Phase 7 — concrete analyses + executable.** Sign, Constant, Main.
|
||||||
|
✅ checkpoint: `lake exe spa` output vs Agda `Main` output; postulates now
|
||||||
|
proved.
|
||||||
|
|
||||||
|
## Status
|
||||||
|
|
||||||
|
- [x] Phase 0
|
||||||
|
- [x] Phase 1
|
||||||
|
- [x] Phase 2
|
||||||
|
- [x] Phase 3
|
||||||
|
- [x] Phase 4
|
||||||
|
- [x] Phase 5
|
||||||
|
- [x] Phase 6
|
||||||
|
- [x] Phase 7
|
||||||
|
|
||||||
|
All phases complete: `lake build` is green with zero warnings, zero `sorry`s
|
||||||
|
and zero axioms, and `lake exe spa` prints output **byte-for-byte identical**
|
||||||
|
to the compiled Agda `Main` (verified with `diff`). Per-file `Agda ↦ Lean`
|
||||||
|
correspondence tables live in the header comment of each Lean file.
|
||||||
|
|
||||||
|
## Wins from the migration
|
||||||
|
|
||||||
|
- The four monotonicity **postulates** in `Analysis/Sign.agda` and
|
||||||
|
`Analysis/Constant.agda` are now proved theorems (via
|
||||||
|
`AboveBelow.monotone₂_of_strict`: any operation on the flat lattice that
|
||||||
|
is strict in `⊥` and dominated by `⊤` is monotone, whatever its table),
|
||||||
|
so the Lean development is postulate-free.
|
||||||
|
- ~2200 lines of map machinery (`Lattice/Map.agda`, `Lattice/MapSet.agda`,
|
||||||
|
much of `Lattice/FiniteMap.agda`) collapse into the spine-pinned
|
||||||
|
`FiniteMap` + `Finset`; the `IterProd` isomorphism no longer needs
|
||||||
|
`Unique ks` (the representation is canonical).
|
||||||
|
- `Equivalence.agda`, `Chain.agda`, the `IsSemilattice`/`IsLattice`
|
||||||
|
hierarchy, and most of `Utils.agda` lift into mathlib.
|
||||||
|
|
||||||
|
## Deviations & deferred items
|
||||||
|
|
||||||
|
- `Lattice/Builder.agda`: not ported (nothing in the repo imports it).
|
||||||
|
- `Lattice/ExtendBelow.agda`, `Lattice/Nat.agda`: not ported (unused by the
|
||||||
|
pipeline; `Nat`'s lattice is mathlib's, `ExtendBelow` would be `WithBot` +
|
||||||
|
a small height proof). Say the word if you want them for parity.
|
||||||
|
- `Program.vars` lists variables in **sorted** order (`Finset.sort`, since
|
||||||
|
`Finset.toList` is noncomputable). For the test program this coincides
|
||||||
|
with the Agda MapSet order.
|
||||||
|
- Chains are mathlib `LTSeries`, so chain-manipulating proofs
|
||||||
|
(`Prod` `unzip`, `AboveBelow`'s `isLongest` → a `rank`-based bound) are
|
||||||
|
restated against that API rather than pattern-matching a custom `Chain`
|
||||||
|
inductive.
|
||||||
|
- `Trace`/`EndToEndTrace` are `Prop`-valued and destructured in proofs.
|
||||||
1
lean/.gitignore
vendored
Normal file
1
lean/.gitignore
vendored
Normal file
@@ -0,0 +1 @@
|
|||||||
|
.lake/
|
||||||
35
lean/Main.lean
Normal file
35
lean/Main.lean
Normal file
@@ -0,0 +1,35 @@
|
|||||||
|
import Spa.Analysis.Sign
|
||||||
|
import Spa.Analysis.Constant
|
||||||
|
import Spa.Language.Notation
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
def testCode : Stmt := [obj_stmt|
|
||||||
|
zero := 0;
|
||||||
|
pos := zero + 1;
|
||||||
|
neg := zero - 1;
|
||||||
|
unknown := pos + neg
|
||||||
|
]
|
||||||
|
|
||||||
|
def testCodeCond₁ : Stmt := [obj_stmt|
|
||||||
|
var := 1;
|
||||||
|
if var {
|
||||||
|
var := var + 1
|
||||||
|
} else {
|
||||||
|
var := var - 1;
|
||||||
|
var := 1
|
||||||
|
}
|
||||||
|
]
|
||||||
|
|
||||||
|
def testCodeCond₂ : Stmt := [obj_stmt|
|
||||||
|
var := 1;
|
||||||
|
if var { x := 1 } else { noop }
|
||||||
|
]
|
||||||
|
|
||||||
|
def testProgram : Program := ⟨testCode⟩
|
||||||
|
|
||||||
|
end Spa
|
||||||
|
|
||||||
|
def main : IO Unit :=
|
||||||
|
IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
|
||||||
|
Spa.SignAnalysis.output Spa.testProgram)
|
||||||
23
lean/Spa.lean
Normal file
23
lean/Spa.lean
Normal file
@@ -0,0 +1,23 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
import Spa.Fixedpoint
|
||||||
|
import Spa.Isomorphism
|
||||||
|
import Spa.Lattice.Unit
|
||||||
|
import Spa.Lattice.Prod
|
||||||
|
import Spa.Lattice.AboveBelow
|
||||||
|
import Spa.Lattice.IterProd
|
||||||
|
import Spa.Lattice.FiniteMap
|
||||||
|
import Spa.Language.Base
|
||||||
|
import Spa.Language.Notation
|
||||||
|
import Spa.Language.Semantics
|
||||||
|
import Spa.Language.Graphs
|
||||||
|
import Spa.Language.Traces
|
||||||
|
import Spa.Language.Properties
|
||||||
|
import Spa.Language
|
||||||
|
import Spa.Analysis.Forward.Lattices
|
||||||
|
import Spa.Analysis.Forward.Evaluation
|
||||||
|
import Spa.Analysis.Forward.Adapters
|
||||||
|
import Spa.Analysis.Forward
|
||||||
|
import Spa.Showable
|
||||||
|
import Spa.Analysis.Utils
|
||||||
|
import Spa.Analysis.Sign
|
||||||
|
import Spa.Analysis.Constant
|
||||||
164
lean/Spa/Analysis/Constant.lean
Normal file
164
lean/Spa/Analysis/Constant.lean
Normal file
@@ -0,0 +1,164 @@
|
|||||||
|
import Spa.Analysis.Forward
|
||||||
|
import Spa.Analysis.Utils
|
||||||
|
import Spa.Interp
|
||||||
|
import Spa.Showable
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
abbrev ConstLattice : Type := AboveBelow ℤ
|
||||||
|
|
||||||
|
namespace ConstAnalysis
|
||||||
|
|
||||||
|
open AboveBelow in
|
||||||
|
def plus : ConstLattice → ConstLattice → ConstLattice
|
||||||
|
| bot, _ => bot
|
||||||
|
| _, bot => bot
|
||||||
|
| top, _ => top
|
||||||
|
| _, top => top
|
||||||
|
| mk z₁, mk z₂ => mk (z₁ + z₂)
|
||||||
|
|
||||||
|
open AboveBelow in
|
||||||
|
def minus : ConstLattice → ConstLattice → ConstLattice
|
||||||
|
| bot, _ => bot
|
||||||
|
| _, bot => bot
|
||||||
|
| top, _ => top
|
||||||
|
| _, top => top
|
||||||
|
| mk z₁, mk z₂ => mk (z₁ - z₂)
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
def interpConst : ConstLattice → Value → Prop
|
||||||
|
| .bot, _ => False
|
||||||
|
| .top, _ => True
|
||||||
|
| .mk z, v => v = .int z
|
||||||
|
|
||||||
|
theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
|
||||||
|
¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
|
||||||
|
rintro ⟨h₁, h₂⟩
|
||||||
|
rw [h₁] at h₂
|
||||||
|
injection h₂ with hz
|
||||||
|
exact hne hz
|
||||||
|
|
||||||
|
instance constInterpretation : LatticeInterpretation ConstLattice where
|
||||||
|
interp := interpConst
|
||||||
|
interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
|
||||||
|
interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
|
||||||
|
|
||||||
|
variable (prog : Program)
|
||||||
|
|
||||||
|
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)
|
||||||
|
| .var k, vs =>
|
||||||
|
if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
|
||||||
|
| .num n, _ => .mk n
|
||||||
|
|
||||||
|
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
|
||||||
|
induction e with
|
||||||
|
| add e₁ e₂ ih₁ ih₂ =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h)
|
||||||
|
| sub e₁ e₂ ih₁ ih₂ =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h)
|
||||||
|
| var k =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
simp only [eval]
|
||||||
|
by_cases hk : k ∈ prog.vars
|
||||||
|
· rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
|
||||||
|
dif_pos (FiniteMap.memKey_iff.mpr hk)]
|
||||||
|
exact FiniteMap.le_of_mem_mem prog.vars_nodup h
|
||||||
|
(FiniteMap.locate _).2 (FiniteMap.locate _).2
|
||||||
|
· rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
|
||||||
|
dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
|
||||||
|
| num n =>
|
||||||
|
intro vs₁ vs₂ _
|
||||||
|
exact le_refl _
|
||||||
|
|
||||||
|
instance exprEvaluator : ExprEvaluator ConstLattice prog :=
|
||||||
|
⟨eval prog, eval_mono prog⟩
|
||||||
|
|
||||||
|
def output : String :=
|
||||||
|
show' (result ConstLattice prog)
|
||||||
|
|
||||||
|
theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
|
||||||
|
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
|
||||||
|
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
|
||||||
|
rcases g₁ with _ | _ | c₁
|
||||||
|
· exact h₁.elim
|
||||||
|
· rcases g₂ with _ | _ | c₂
|
||||||
|
· exact h₂.elim
|
||||||
|
· exact trivial
|
||||||
|
· exact trivial
|
||||||
|
· rcases g₂ with _ | _ | c₂
|
||||||
|
· exact h₂.elim
|
||||||
|
· exact trivial
|
||||||
|
· injection h₁ with hz₁
|
||||||
|
injection h₂ with hz₂
|
||||||
|
show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
|
||||||
|
rw [hz₁, hz₂]
|
||||||
|
|
||||||
|
theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
|
||||||
|
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
|
||||||
|
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
|
||||||
|
rcases g₁ with _ | _ | c₁
|
||||||
|
· exact h₁.elim
|
||||||
|
· rcases g₂ with _ | _ | c₂
|
||||||
|
· exact h₂.elim
|
||||||
|
· exact trivial
|
||||||
|
· exact trivial
|
||||||
|
· rcases g₂ with _ | _ | c₂
|
||||||
|
· exact h₂.elim
|
||||||
|
· exact trivial
|
||||||
|
· injection h₁ with hz₁
|
||||||
|
injection h₂ with hz₂
|
||||||
|
show Value.int (z₁ - z₂) = Value.int (c₁ - c₂)
|
||||||
|
rw [hz₁, hz₂]
|
||||||
|
|
||||||
|
instance eval_valid : ValidExprEvaluator ConstLattice prog := by
|
||||||
|
constructor
|
||||||
|
intro vs ρ e v hev
|
||||||
|
induction hev with
|
||||||
|
| num n =>
|
||||||
|
intro _
|
||||||
|
show ⟦eval prog (.num n) vs⟧ (.int n)
|
||||||
|
rfl
|
||||||
|
| var x v hxv =>
|
||||||
|
intro hvs
|
||||||
|
show ⟦eval prog (.var x) vs⟧ v
|
||||||
|
simp only [eval]
|
||||||
|
by_cases hk : FiniteMap.MemKey x vs
|
||||||
|
· rw [dif_pos hk]
|
||||||
|
exact hvs _ _ (FiniteMap.locate hk).2 _ hxv
|
||||||
|
· rw [dif_neg hk]
|
||||||
|
exact trivial
|
||||||
|
| add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
|
||||||
|
intro hvs
|
||||||
|
have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
|
||||||
|
have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
|
||||||
|
show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
|
||||||
|
exact plus_valid h₁ h₂
|
||||||
|
| sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
|
||||||
|
intro hvs
|
||||||
|
have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
|
||||||
|
have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
|
||||||
|
show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
|
||||||
|
exact minus_valid h₁ h₂
|
||||||
|
|
||||||
|
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
|
||||||
|
⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
|
||||||
|
Spa.analyze_correct ConstLattice prog hrun
|
||||||
|
|
||||||
|
end ConstAnalysis
|
||||||
|
|
||||||
|
end Spa
|
||||||
119
lean/Spa/Analysis/Forward.lean
Normal file
119
lean/Spa/Analysis/Forward.lean
Normal file
@@ -0,0 +1,119 @@
|
|||||||
|
import Spa.Analysis.Forward.Lattices
|
||||||
|
import Spa.Analysis.Forward.Evaluation
|
||||||
|
import Spa.Analysis.Forward.Adapters
|
||||||
|
import Spa.Fixedpoint
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
|
||||||
|
|
||||||
|
def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
|
||||||
|
VariableValues L prog :=
|
||||||
|
(prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
|
||||||
|
|
||||||
|
theorem updateVariablesForState_mono (s : prog.State) :
|
||||||
|
Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
|
||||||
|
foldl_mono' (prog.code s) _ (E.eval_mono s ·) (variablesAt_le hle s)
|
||||||
|
|
||||||
|
def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
|
||||||
|
FiniteMap.generalizedUpdate id updateVariablesForState
|
||||||
|
prog.states sv
|
||||||
|
|
||||||
|
theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
|
||||||
|
FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
|
||||||
|
|
||||||
|
theorem updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
|
||||||
|
{sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) :
|
||||||
|
vs = updateVariablesForState s sv :=
|
||||||
|
FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem
|
||||||
|
|
||||||
|
theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
|
||||||
|
variablesAt s (updateAll sv) = updateVariablesForState s sv :=
|
||||||
|
updateAll_mem_eq (variablesAt_mem s (updateAll sv))
|
||||||
|
|
||||||
|
variable [FiniteHeightLattice L]
|
||||||
|
|
||||||
|
def analyze (sv : StateVariables L prog) : StateVariables L prog :=
|
||||||
|
updateAll (joinAll sv)
|
||||||
|
|
||||||
|
theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
|
||||||
|
updateAll_mono (joinAll_mono hle)
|
||||||
|
|
||||||
|
variable [DecidableEq L]
|
||||||
|
|
||||||
|
variable (L prog) in
|
||||||
|
def result : StateVariables L prog :=
|
||||||
|
Fixedpoint.aFix analyze analyze_mono
|
||||||
|
|
||||||
|
variable (L prog) in
|
||||||
|
theorem result_eq : result L prog = analyze (result L prog) :=
|
||||||
|
Fixedpoint.aFix_eq analyze analyze_mono
|
||||||
|
|
||||||
|
theorem joinForKey_initialState :
|
||||||
|
joinForKey prog.initialState (result L prog) = botV L prog := by
|
||||||
|
rw [joinForKey, prog.incoming_initialState_eq_nil]
|
||||||
|
rfl
|
||||||
|
|
||||||
|
variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
|
||||||
|
|
||||||
|
omit [FiniteHeightLattice L] [DecidableEq L] in
|
||||||
|
theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
|
||||||
|
{vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
|
||||||
|
(hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : ⟦ vs ⟧ ρ₁) :
|
||||||
|
⟦ bss.foldl (fun vs bs => E.eval s bs vs) vs ⟧ ρ₂ := by
|
||||||
|
induction hbss generalizing vs with
|
||||||
|
| nil => exact hvs
|
||||||
|
| cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)
|
||||||
|
|
||||||
|
omit [FiniteHeightLattice L] [DecidableEq L] in
|
||||||
|
theorem updateVariablesForState_matches {s : prog.State}
|
||||||
|
{sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
|
||||||
|
(hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
|
||||||
|
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
|
||||||
|
⟦ updateVariablesForState s sv ⟧ ρ₂ :=
|
||||||
|
eval_fold_valid hbss hvs
|
||||||
|
|
||||||
|
omit [FiniteHeightLattice L] [DecidableEq L] in
|
||||||
|
theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
|
||||||
|
{ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
|
||||||
|
(hvs : ⟦ variablesAt s sv ⟧ ρ₁) :
|
||||||
|
⟦ variablesAt s (updateAll sv) ⟧ ρ₂ := by
|
||||||
|
rw [variablesAt_updateAll]
|
||||||
|
exact updateVariablesForState_matches hbss hvs
|
||||||
|
|
||||||
|
theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
|
||||||
|
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
|
||||||
|
(hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
|
||||||
|
⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ := by
|
||||||
|
rw [result_eq L prog]
|
||||||
|
refine updateAll_matches hbss ?_
|
||||||
|
rw [variablesAt_joinAll]
|
||||||
|
exact hjoin
|
||||||
|
|
||||||
|
theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
|
||||||
|
(hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
|
||||||
|
(tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
|
||||||
|
⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
|
||||||
|
induction tr with
|
||||||
|
| single hbss => exact stepTrace hjoin hbss
|
||||||
|
| @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
|
||||||
|
have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' :=
|
||||||
|
stepTrace hjoin hbss
|
||||||
|
have hmem : variablesAt i₁ (result L prog)
|
||||||
|
∈ (result L prog).valuesAt (prog.incoming i₂) :=
|
||||||
|
FiniteMap.mem_valuesAt prog.states_nodup
|
||||||
|
(prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
|
||||||
|
exact ih (interp_foldr hstep hmem)
|
||||||
|
|
||||||
|
omit V in
|
||||||
|
theorem interp_joinForKey_initialState :
|
||||||
|
⟦ joinForKey prog.initialState (result L prog) ⟧ [] := by
|
||||||
|
rw [joinForKey_initialState]
|
||||||
|
exact interp_botV_nil
|
||||||
|
|
||||||
|
variable (L prog) in
|
||||||
|
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
|
||||||
|
⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
|
||||||
|
walkTrace interp_joinForKey_initialState (prog.trace hrun)
|
||||||
|
|
||||||
|
end Spa
|
||||||
54
lean/Spa/Analysis/Forward/Adapters.lean
Normal file
54
lean/Spa/Analysis/Forward/Adapters.lean
Normal file
@@ -0,0 +1,54 @@
|
|||||||
|
import Spa.Analysis.Forward.Evaluation
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
|
||||||
|
|
||||||
|
def updateVariablesFromExpression (k : String) (e : Expr)
|
||||||
|
(vs : VariableValues L prog) : VariableValues L prog :=
|
||||||
|
FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
|
||||||
|
|
||||||
|
theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
|
||||||
|
Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
|
||||||
|
FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
|
||||||
|
⟨evalB, evalB_mono⟩
|
||||||
|
|
||||||
|
instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
|
||||||
|
[ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
|
||||||
|
constructor
|
||||||
|
intro s vs ρ₁ ρ₂ bs hbs hvs
|
||||||
|
cases hbs with
|
||||||
|
| noop => exact hvs
|
||||||
|
| assign k e v hev =>
|
||||||
|
intro k' l hk'l v' hv'
|
||||||
|
cases hv' with
|
||||||
|
| here =>
|
||||||
|
have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
|
||||||
|
(fun _ vs => E.eval e vs) [k] vs := hk'l
|
||||||
|
have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
|
||||||
|
(g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
|
||||||
|
rw [hl]
|
||||||
|
exact ValidExprEvaluator.valid hev hvs
|
||||||
|
| there _ _ _ _ _ hne hmem' =>
|
||||||
|
have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
|
||||||
|
(fun _ vs => E.eval e vs) [k] vs := hk'l
|
||||||
|
have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
|
||||||
|
FiniteMap.generalizedUpdate_not_mem_backward
|
||||||
|
(fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
|
||||||
|
exact hvs _ _ hk'l' _ hmem'
|
||||||
|
|
||||||
|
end Spa
|
||||||
26
lean/Spa/Analysis/Forward/Evaluation.lean
Normal file
26
lean/Spa/Analysis/Forward/Evaluation.lean
Normal file
@@ -0,0 +1,26 @@
|
|||||||
|
import Spa.Analysis.Forward.Lattices
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
variable (L : Type) [Lattice L] (prog : Program)
|
||||||
|
|
||||||
|
class StmtEvaluator where
|
||||||
|
eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
|
||||||
|
eval_mono : ∀ s bs, Monotone (eval s bs)
|
||||||
|
|
||||||
|
class ExprEvaluator where
|
||||||
|
eval : Expr → VariableValues L prog → L
|
||||||
|
eval_mono : ∀ e, Monotone (eval e)
|
||||||
|
|
||||||
|
class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
|
||||||
|
Prop where
|
||||||
|
valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
|
||||||
|
EvalExpr ρ e v → ⟦ vs ⟧ ρ → I.interp (ExprEvaluator.eval e vs) v
|
||||||
|
|
||||||
|
class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
|
||||||
|
Prop where
|
||||||
|
valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
|
||||||
|
{bs : BasicStmt},
|
||||||
|
EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s bs vs ⟧ ρ₂
|
||||||
|
|
||||||
|
end Spa
|
||||||
99
lean/Spa/Analysis/Forward/Lattices.lean
Normal file
99
lean/Spa/Analysis/Forward/Lattices.lean
Normal file
@@ -0,0 +1,99 @@
|
|||||||
|
import Spa.Language
|
||||||
|
import Spa.Lattice.FiniteMap
|
||||||
|
import Spa.Interp
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
variable (L : Type) [Lattice L] (prog : Program)
|
||||||
|
|
||||||
|
abbrev VariableValues : Type := FiniteMap String L prog.vars
|
||||||
|
|
||||||
|
abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states
|
||||||
|
|
||||||
|
def botV [FiniteHeightLattice L] : VariableValues L prog :=
|
||||||
|
(⊥ : VariableValues L prog)
|
||||||
|
|
||||||
|
variable {L prog}
|
||||||
|
|
||||||
|
omit [Lattice L] in
|
||||||
|
theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
|
||||||
|
FiniteMap.MemKey s sv :=
|
||||||
|
FiniteMap.memKey_iff.mpr (prog.states_complete s)
|
||||||
|
|
||||||
|
def variablesAt (s : prog.State) (sv : StateVariables L prog) :
|
||||||
|
VariableValues L prog :=
|
||||||
|
(FiniteMap.locate (states_memKey s sv)).1
|
||||||
|
|
||||||
|
omit [Lattice L] in
|
||||||
|
theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
|
||||||
|
(s, variablesAt s sv) ∈ sv :=
|
||||||
|
(FiniteMap.locate (states_memKey s sv)).2
|
||||||
|
|
||||||
|
theorem variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
|
||||||
|
(s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
|
||||||
|
FiniteMap.le_of_mem_mem prog.states_nodup hle
|
||||||
|
(variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
|
||||||
|
|
||||||
|
variable [FiniteHeightLattice L]
|
||||||
|
|
||||||
|
def joinForKey (k : prog.State) (sv : StateVariables L prog) :
|
||||||
|
VariableValues L prog :=
|
||||||
|
(sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
|
||||||
|
|
||||||
|
theorem joinForKey_mono (k : prog.State) :
|
||||||
|
Monotone (joinForKey (L := L) k) := by
|
||||||
|
intro sv₁ sv₂ hle
|
||||||
|
exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
|
||||||
|
(fun b _ _ hab => sup_le_sup_right hab b)
|
||||||
|
(fun a _ _ hab => sup_le_sup_left hab a)
|
||||||
|
|
||||||
|
def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
|
||||||
|
FiniteMap.generalizedUpdate id joinForKey prog.states sv
|
||||||
|
|
||||||
|
theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
|
||||||
|
FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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))
|
||||||
|
|
||||||
|
/-! ### Lifting an interpretation to variable maps -/
|
||||||
|
|
||||||
|
variable [I : LatticeInterpretation L]
|
||||||
|
|
||||||
|
omit [FiniteHeightLattice L] in
|
||||||
|
instance : Interp (VariableValues L prog) (Env → Prop) where
|
||||||
|
interp (vs : VariableValues L prog) (ρ : Env) : Prop :=
|
||||||
|
∀ (k : String) (l : L), (k, l) ∈ vs →
|
||||||
|
∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
|
||||||
|
|
||||||
|
theorem interp_botV_nil : ⟦ botV L prog ⟧ [] := by
|
||||||
|
intro k l _ v hmem
|
||||||
|
cases hmem
|
||||||
|
|
||||||
|
omit [FiniteHeightLattice L] in
|
||||||
|
theorem interp_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
|
||||||
|
(h : ⟦ vs₁⟧ ρ ∨ ⟦ vs₂ ⟧ ρ) : ⟦ vs₁ ⊔ vs₂ ⟧ ρ := by
|
||||||
|
intro k l hmem v hv
|
||||||
|
obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
|
||||||
|
rcases h with h | h
|
||||||
|
· exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
|
||||||
|
· exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv))
|
||||||
|
|
||||||
|
theorem interp_foldr {vs : VariableValues L prog}
|
||||||
|
{vss : List (VariableValues L prog)} {ρ : Env}
|
||||||
|
(hvs : ⟦ vs ⟧ ρ) (hmem : vs ∈ vss) :
|
||||||
|
⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ := by
|
||||||
|
induction vss with
|
||||||
|
| nil => cases hmem
|
||||||
|
| cons vs' vss' ih =>
|
||||||
|
rcases List.mem_cons.mp hmem with rfl | hmem'
|
||||||
|
· exact interp_sup (Or.inl hvs)
|
||||||
|
· exact interp_sup (Or.inr (ih hmem'))
|
||||||
|
|
||||||
|
end Spa
|
||||||
222
lean/Spa/Analysis/Sign.lean
Normal file
222
lean/Spa/Analysis/Sign.lean
Normal file
@@ -0,0 +1,222 @@
|
|||||||
|
import Spa.Analysis.Forward
|
||||||
|
import Spa.Analysis.Utils
|
||||||
|
import Spa.Interp
|
||||||
|
import Spa.Showable
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
inductive Sign where
|
||||||
|
| plus
|
||||||
|
| minus
|
||||||
|
| zero
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
instance : Showable Sign :=
|
||||||
|
⟨fun
|
||||||
|
| .plus => "+"
|
||||||
|
| .minus => "-"
|
||||||
|
| .zero => "0"⟩
|
||||||
|
|
||||||
|
instance : Inhabited Sign := ⟨.zero⟩
|
||||||
|
|
||||||
|
abbrev SignLattice : Type := AboveBelow Sign
|
||||||
|
|
||||||
|
open AboveBelow in
|
||||||
|
def plus : SignLattice → SignLattice → SignLattice
|
||||||
|
| bot, _ => bot
|
||||||
|
| _, bot => bot
|
||||||
|
| top, _ => top
|
||||||
|
| _, top => top
|
||||||
|
| mk .plus, mk .plus => mk .plus
|
||||||
|
| mk .plus, mk .minus => top
|
||||||
|
| mk .plus, mk .zero => mk .plus
|
||||||
|
| mk .minus, mk .plus => top
|
||||||
|
| mk .minus, mk .minus => mk .minus
|
||||||
|
| mk .minus, mk .zero => mk .minus
|
||||||
|
| mk .zero, mk .plus => mk .plus
|
||||||
|
| mk .zero, mk .minus => mk .minus
|
||||||
|
| mk .zero, mk .zero => mk .zero
|
||||||
|
|
||||||
|
open AboveBelow in
|
||||||
|
def minus : SignLattice → SignLattice → SignLattice
|
||||||
|
| bot, _ => bot
|
||||||
|
| _, bot => bot
|
||||||
|
| top, _ => top
|
||||||
|
| _, top => top
|
||||||
|
| mk .plus, mk .plus => top
|
||||||
|
| mk .plus, mk .minus => mk .plus
|
||||||
|
| mk .plus, mk .zero => mk .plus
|
||||||
|
| mk .minus, mk .plus => mk .minus
|
||||||
|
| mk .minus, mk .minus => top
|
||||||
|
| mk .minus, mk .zero => mk .minus
|
||||||
|
| mk .zero, mk .plus => mk .minus
|
||||||
|
| mk .zero, mk .minus => mk .plus
|
||||||
|
| mk .zero, mk .zero => mk .zero
|
||||||
|
|
||||||
|
theorem plus_mono₂ : Monotone₂ plus :=
|
||||||
|
AboveBelow.monotone₂_of_strict plus
|
||||||
|
(fun y => by cases y <;> rfl)
|
||||||
|
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
|
||||||
|
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
|
||||||
|
(fun x hx => by
|
||||||
|
rcases x with _ | _ | s <;>
|
||||||
|
first | exact absurd rfl hx | rfl | (cases s <;> rfl))
|
||||||
|
|
||||||
|
theorem minus_mono₂ : Monotone₂ minus :=
|
||||||
|
AboveBelow.monotone₂_of_strict minus
|
||||||
|
(fun y => by cases y <;> rfl)
|
||||||
|
(fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
|
||||||
|
(fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
|
||||||
|
(fun x hx => by
|
||||||
|
rcases x with _ | _ | s <;>
|
||||||
|
first | exact absurd rfl hx | rfl | (cases s <;> rfl))
|
||||||
|
|
||||||
|
def interpSign : SignLattice → Value → Prop
|
||||||
|
| .bot, _ => False
|
||||||
|
| .top, _ => True
|
||||||
|
| .mk .plus, v => ∃ n : ℕ, v = .int (n + 1)
|
||||||
|
| .mk .zero, v => v = .int 0
|
||||||
|
| .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
|
||||||
|
|
||||||
|
theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
|
||||||
|
¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
|
||||||
|
rintro ⟨h₁, h₂⟩
|
||||||
|
rcases s₁ <;> rcases s₂ <;> try exact hne rfl
|
||||||
|
all_goals simp only [interpSign] at h₁ h₂
|
||||||
|
· obtain ⟨n₁, rfl⟩ := h₁
|
||||||
|
obtain ⟨n₂, hv⟩ := h₂
|
||||||
|
injection hv with hz
|
||||||
|
omega
|
||||||
|
· obtain ⟨n₁, rfl⟩ := h₁
|
||||||
|
injection h₂ with hz
|
||||||
|
omega
|
||||||
|
· obtain ⟨n₁, rfl⟩ := h₁
|
||||||
|
obtain ⟨n₂, hv⟩ := h₂
|
||||||
|
injection hv with hz
|
||||||
|
omega
|
||||||
|
· obtain ⟨n₁, rfl⟩ := h₁
|
||||||
|
injection h₂ with hz
|
||||||
|
omega
|
||||||
|
· subst h₁
|
||||||
|
obtain ⟨n₂, hv⟩ := h₂
|
||||||
|
injection hv with hz
|
||||||
|
omega
|
||||||
|
· subst h₁
|
||||||
|
obtain ⟨n₂, hv⟩ := h₂
|
||||||
|
injection hv with hz
|
||||||
|
omega
|
||||||
|
|
||||||
|
instance signInterpretation : LatticeInterpretation SignLattice where
|
||||||
|
interp := interpSign
|
||||||
|
interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
|
||||||
|
interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
|
||||||
|
|
||||||
|
namespace SignAnalysis
|
||||||
|
|
||||||
|
variable (prog : Program)
|
||||||
|
|
||||||
|
def eval : Expr → VariableValues SignLattice prog → SignLattice
|
||||||
|
| .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
|
||||||
|
| .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
|
||||||
|
| .var k, vs =>
|
||||||
|
if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
|
||||||
|
| .num 0, _ => .mk .zero
|
||||||
|
| .num (_ + 1), _ => .mk .plus
|
||||||
|
|
||||||
|
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
|
||||||
|
induction e with
|
||||||
|
| add e₁ e₂ ih₁ ih₂ =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h)
|
||||||
|
| sub e₁ e₂ ih₁ ih₂ =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h)
|
||||||
|
| var k =>
|
||||||
|
intro vs₁ vs₂ h
|
||||||
|
simp only [eval]
|
||||||
|
by_cases hk : k ∈ prog.vars
|
||||||
|
· rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
|
||||||
|
dif_pos (FiniteMap.memKey_iff.mpr hk)]
|
||||||
|
exact FiniteMap.le_of_mem_mem prog.vars_nodup h
|
||||||
|
(FiniteMap.locate _).2 (FiniteMap.locate _).2
|
||||||
|
· rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
|
||||||
|
dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
|
||||||
|
| num n =>
|
||||||
|
intro vs₁ vs₂ _
|
||||||
|
cases n <;> exact le_refl _
|
||||||
|
|
||||||
|
instance exprEvaluator : ExprEvaluator SignLattice prog :=
|
||||||
|
⟨eval prog, eval_mono prog⟩
|
||||||
|
|
||||||
|
def output : String :=
|
||||||
|
show' (result SignLattice prog)
|
||||||
|
|
||||||
|
/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
|
||||||
|
private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
|
||||||
|
constructor
|
||||||
|
· rintro ⟨n, rfl⟩; omega
|
||||||
|
· intro h; exact ⟨(z - 1).toNat, by omega⟩
|
||||||
|
|
||||||
|
/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
|
||||||
|
private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
|
||||||
|
constructor
|
||||||
|
· rintro ⟨n, rfl⟩; omega
|
||||||
|
· intro h; exact ⟨(-z - 1).toNat, by omega⟩
|
||||||
|
|
||||||
|
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
|
||||||
|
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
|
||||||
|
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
|
||||||
|
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
|
||||||
|
(try rcases s₁) <;> (try rcases s₂) <;>
|
||||||
|
simp only [plus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
|
||||||
|
at h₁ h₂ ⊢ <;>
|
||||||
|
omega
|
||||||
|
|
||||||
|
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
|
||||||
|
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
|
||||||
|
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
|
||||||
|
rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
|
||||||
|
(try rcases s₁) <;> (try rcases s₂) <;>
|
||||||
|
simp only [minus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
|
||||||
|
at h₁ h₂ ⊢ <;>
|
||||||
|
omega
|
||||||
|
|
||||||
|
instance eval_valid : ValidExprEvaluator SignLattice prog := by
|
||||||
|
constructor
|
||||||
|
intro vs ρ e v hev
|
||||||
|
induction hev with
|
||||||
|
| num n =>
|
||||||
|
intro _
|
||||||
|
show ⟦eval prog (.num n) vs⟧ (.int n)
|
||||||
|
cases n with
|
||||||
|
| zero => rfl
|
||||||
|
| succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
|
||||||
|
| var x v hxv =>
|
||||||
|
intro hvs
|
||||||
|
show ⟦eval prog (.var x) vs⟧ v
|
||||||
|
simp only [eval]
|
||||||
|
by_cases hk : FiniteMap.MemKey x vs
|
||||||
|
· rw [dif_pos hk]
|
||||||
|
exact hvs _ _ (FiniteMap.locate hk).2 _ hxv
|
||||||
|
· rw [dif_neg hk]
|
||||||
|
exact trivial
|
||||||
|
| add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
|
||||||
|
intro hvs
|
||||||
|
have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
|
||||||
|
have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
|
||||||
|
show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
|
||||||
|
exact plus_valid h₁ h₂
|
||||||
|
| sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
|
||||||
|
intro hvs
|
||||||
|
have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
|
||||||
|
have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
|
||||||
|
show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
|
||||||
|
exact minus_valid h₁ h₂
|
||||||
|
|
||||||
|
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
|
||||||
|
⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
|
||||||
|
Spa.analyze_correct SignLattice prog hrun
|
||||||
|
|
||||||
|
end SignAnalysis
|
||||||
|
|
||||||
|
end Spa
|
||||||
10
lean/Spa/Analysis/Utils.lean
Normal file
10
lean/Spa/Analysis/Utils.lean
Normal file
@@ -0,0 +1,10 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
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₄ :=
|
||||||
|
le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂)
|
||||||
|
|
||||||
|
end Spa
|
||||||
52
lean/Spa/Fixedpoint.lean
Normal file
52
lean/Spa/Fixedpoint.lean
Normal file
@@ -0,0 +1,52 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa.Fixedpoint
|
||||||
|
|
||||||
|
open FiniteHeightLattice (height)
|
||||||
|
|
||||||
|
variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
|
||||||
|
|
||||||
|
def doStep (f : α → α) (hf : Monotone f) :
|
||||||
|
∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
|
||||||
|
c.last ≤ f c.last → {a : α // a = f a}
|
||||||
|
| 0, c, hlen, _ =>
|
||||||
|
absurd (FiniteHeightLattice.chains_bounded c) (by omega)
|
||||||
|
| g + 1, c, hlen, hle =>
|
||||||
|
if heq : c.last = f c.last then
|
||||||
|
⟨c.last, heq⟩
|
||||||
|
else
|
||||||
|
doStep f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq))
|
||||||
|
(by simp [RelSeries.snoc]; omega)
|
||||||
|
(by rw [RelSeries.last_snoc]; exact hf hle)
|
||||||
|
|
||||||
|
def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
|
||||||
|
doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
|
||||||
|
(by simp)
|
||||||
|
(by simpa [RelSeries.last_singleton]
|
||||||
|
using FiniteHeightLattice.bot_le α (f ⊥))
|
||||||
|
|
||||||
|
def aFix (f : α → α) (hf : Monotone f) : α :=
|
||||||
|
(fix f hf).1
|
||||||
|
|
||||||
|
theorem aFix_eq (f : α → α) (hf : Monotone f) :
|
||||||
|
aFix f hf = f (aFix f hf) :=
|
||||||
|
(fix f hf).2
|
||||||
|
|
||||||
|
theorem doStep_le (f : α → α) (hf : Monotone f)
|
||||||
|
{b : α} (hb : b = f b) :
|
||||||
|
∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
|
||||||
|
(hle : c.last ≤ f c.last), c.last ≤ b →
|
||||||
|
(doStep f hf g c hlen hle : α) ≤ b
|
||||||
|
| 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
|
||||||
|
| g + 1, c, hlen, hle => fun hcb => by
|
||||||
|
rw [doStep]
|
||||||
|
split
|
||||||
|
· exact hcb
|
||||||
|
· exact doStep_le f hf hb g _ _ _
|
||||||
|
(by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)
|
||||||
|
|
||||||
|
theorem aFix_le (f : α → α) (hf : Monotone f)
|
||||||
|
{a : α} (ha : a = f a) : aFix f hf ≤ a :=
|
||||||
|
doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
|
||||||
|
|
||||||
|
end Spa.Fixedpoint
|
||||||
10
lean/Spa/Interp.lean
Normal file
10
lean/Spa/Interp.lean
Normal file
@@ -0,0 +1,10 @@
|
|||||||
|
import Mathlib.Tactic.TypeStar
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
class Interp (α : Type*) (dom : outParam Type*) where
|
||||||
|
interp : α → dom
|
||||||
|
|
||||||
|
notation:max (priority := high) "⟦" v "⟧" => Interp.interp v
|
||||||
|
|
||||||
|
end Spa
|
||||||
24
lean/Spa/Isomorphism.lean
Normal file
24
lean/Spa/Isomorphism.lean
Normal file
@@ -0,0 +1,24 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
|
||||||
|
[I : FiniteHeightLattice α] (f : α → β) (g : β → α)
|
||||||
|
(hf : Monotone f) (hg : Monotone g)
|
||||||
|
(hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
|
||||||
|
FiniteHeightLattice β where
|
||||||
|
bot := f ⊥
|
||||||
|
top := f ⊤
|
||||||
|
height := I.height
|
||||||
|
longestChain :=
|
||||||
|
{ series :=
|
||||||
|
I.longestChain.series.map f
|
||||||
|
(hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
|
||||||
|
head_series := congrArg f I.longestChain.head_series
|
||||||
|
last_series := congrArg f I.longestChain.last_series
|
||||||
|
length_series := I.longestChain.length_series }
|
||||||
|
chains_bounded := fun c =>
|
||||||
|
I.chains_bounded
|
||||||
|
(c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
|
||||||
|
|
||||||
|
end Spa
|
||||||
58
lean/Spa/Language.lean
Normal file
58
lean/Spa/Language.lean
Normal file
@@ -0,0 +1,58 @@
|
|||||||
|
import Spa.Language.Base
|
||||||
|
import Spa.Language.Semantics
|
||||||
|
import Spa.Language.Graphs
|
||||||
|
import Spa.Language.Traces
|
||||||
|
import Spa.Language.Properties
|
||||||
|
import Mathlib.Data.Finset.Sort
|
||||||
|
import Mathlib.Data.String.Basic
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
structure Program where
|
||||||
|
rootStmt : Stmt
|
||||||
|
|
||||||
|
namespace Program
|
||||||
|
|
||||||
|
variable (p : Program)
|
||||||
|
|
||||||
|
def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
|
||||||
|
|
||||||
|
abbrev State : Type := p.graph.Index
|
||||||
|
|
||||||
|
def initialState : p.State := (buildCfg p.rootStmt).wrapInput
|
||||||
|
|
||||||
|
def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
|
||||||
|
|
||||||
|
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)
|
||||||
|
rw [Graph.wrap_inputs, List.mem_singleton] at h₁
|
||||||
|
rw [Graph.wrap_outputs, List.mem_singleton] at h₂
|
||||||
|
subst h₁; subst h₂
|
||||||
|
exact tr
|
||||||
|
|
||||||
|
def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
|
||||||
|
|
||||||
|
theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
|
||||||
|
|
||||||
|
def states : List p.State := p.graph.indices
|
||||||
|
|
||||||
|
theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
|
||||||
|
|
||||||
|
theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
|
||||||
|
|
||||||
|
def code (st : p.State) : List BasicStmt := p.graph.nodes st
|
||||||
|
|
||||||
|
def incoming (s : p.State) : List p.State := p.graph.predecessors s
|
||||||
|
|
||||||
|
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 _)
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
end Program
|
||||||
|
|
||||||
|
end Spa
|
||||||
54
lean/Spa/Language/Base.lean
Normal file
54
lean/Spa/Language/Base.lean
Normal file
@@ -0,0 +1,54 @@
|
|||||||
|
import Mathlib.Data.Finset.Basic
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
inductive Expr where
|
||||||
|
| add (e₁ e₂ : Expr)
|
||||||
|
| sub (e₁ e₂ : Expr)
|
||||||
|
| var (x : String)
|
||||||
|
| num (n : ℕ)
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
inductive BasicStmt where
|
||||||
|
| assign (x : String) (e : Expr)
|
||||||
|
| noop
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
inductive Stmt where
|
||||||
|
| basic (bs : BasicStmt)
|
||||||
|
| andThen (s₁ s₂ : Stmt)
|
||||||
|
| ifElse (e : Expr) (s₁ s₂ : Stmt)
|
||||||
|
| whileLoop (e : Expr) (s : Stmt)
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
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₂)
|
||||||
|
| subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂)
|
||||||
|
| subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
|
||||||
|
| here {k} : Expr.HasVar k (.var k)
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
def Expr.vars : Expr → Finset String
|
||||||
|
| .add l r => l.vars ∪ r.vars
|
||||||
|
| .sub l r => l.vars ∪ r.vars
|
||||||
|
| .var s => {s}
|
||||||
|
| .num _ => ∅
|
||||||
|
|
||||||
|
def BasicStmt.vars : BasicStmt → Finset String
|
||||||
|
| .assign x e => {x} ∪ e.vars
|
||||||
|
| .noop => ∅
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
def Stmt.varsList (ss : List Stmt) : Finset String :=
|
||||||
|
ss.foldr (fun s acc => s.vars ∪ acc) ∅
|
||||||
|
|
||||||
|
end Spa
|
||||||
126
lean/Spa/Language/Graphs.lean
Normal file
126
lean/Spa/Language/Graphs.lean
Normal file
@@ -0,0 +1,126 @@
|
|||||||
|
import Spa.Language.Base
|
||||||
|
import Mathlib.Data.Fin.Tuple.Basic
|
||||||
|
import Mathlib.Data.List.ProdSigma
|
||||||
|
import Mathlib.Data.List.FinRange
|
||||||
|
|
||||||
|
def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
|
||||||
|
l.map (Fin.castAdd m)
|
||||||
|
|
||||||
|
def List.finNatAdd {m : ℕ} (l : List (Fin m)) (n : ℕ) : List (Fin (n + m)) :=
|
||||||
|
l.map (Fin.natAdd n)
|
||||||
|
|
||||||
|
def List.finCastAddProd {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))
|
||||||
|
|
||||||
|
def List.finNatAddProd {m : ℕ} (l : List (Fin m × Fin m)) (n : ℕ) :
|
||||||
|
List (Fin (n + m) × Fin (n + m)) :=
|
||||||
|
l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
structure Graph where
|
||||||
|
size : ℕ
|
||||||
|
nodes : Fin size → List BasicStmt
|
||||||
|
edges : List (Fin size × Fin size)
|
||||||
|
inputs : List (Fin size)
|
||||||
|
outputs : List (Fin size)
|
||||||
|
|
||||||
|
namespace Graph
|
||||||
|
|
||||||
|
abbrev Index (g : Graph) : Type := Fin g.size
|
||||||
|
|
||||||
|
abbrev Edge (g : Graph) : Type := g.Index × g.Index
|
||||||
|
|
||||||
|
def comp (g₁ g₂ : Graph) : Graph where
|
||||||
|
size := g₁.size + g₂.size
|
||||||
|
nodes := Fin.append g₁.nodes g₂.nodes
|
||||||
|
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size
|
||||||
|
inputs := g₁.inputs.finCastAdd g₂.size ++ g₂.inputs.finNatAdd g₁.size
|
||||||
|
outputs := g₁.outputs.finCastAdd g₂.size ++ g₂.outputs.finNatAdd g₁.size
|
||||||
|
|
||||||
|
@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp
|
||||||
|
|
||||||
|
def link (g₁ g₂ : Graph) : Graph where
|
||||||
|
size := g₁.size + g₂.size
|
||||||
|
nodes := Fin.append g₁.nodes g₂.nodes
|
||||||
|
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
|
||||||
|
(g₁.outputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
|
||||||
|
inputs := g₁.inputs.finCastAdd g₂.size
|
||||||
|
outputs := g₂.outputs.finNatAdd g₁.size
|
||||||
|
|
||||||
|
@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link
|
||||||
|
|
||||||
|
/-- The entry node of a `loop` graph. -/
|
||||||
|
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
|
||||||
|
|
||||||
|
def loop (g : Graph) : Graph where
|
||||||
|
size := 2 + g.size
|
||||||
|
nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
|
||||||
|
edges := g.edges.finNatAddProd 2 ++
|
||||||
|
(g.inputs.finNatAdd 2).map (g.loopIn, ·) ++
|
||||||
|
(g.outputs.finNatAdd 2).map (·, g.loopOut) ++
|
||||||
|
[(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
|
||||||
|
inputs := [g.loopIn]
|
||||||
|
outputs := [g.loopOut]
|
||||||
|
|
||||||
|
@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
|
||||||
|
|
||||||
|
@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
|
||||||
|
|
||||||
|
def skipto (g₁ g₂ : Graph) : Graph where
|
||||||
|
size := g₁.size + g₂.size
|
||||||
|
nodes := Fin.append g₁.nodes g₂.nodes
|
||||||
|
edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
|
||||||
|
(g₁.inputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
|
||||||
|
inputs := g₁.inputs.finCastAdd g₂.size
|
||||||
|
outputs := g₂.inputs.finNatAdd g₁.size
|
||||||
|
|
||||||
|
def singleton (bss : List BasicStmt) : Graph where
|
||||||
|
size := 1
|
||||||
|
nodes := fun _ => bss
|
||||||
|
edges := []
|
||||||
|
inputs := [0]
|
||||||
|
outputs := [0]
|
||||||
|
|
||||||
|
def wrap (g : Graph) : Graph :=
|
||||||
|
singleton [] ⤳ g ⤳ singleton []
|
||||||
|
|
||||||
|
end Graph
|
||||||
|
|
||||||
|
open Graph in
|
||||||
|
def buildCfg : Stmt → Graph
|
||||||
|
| .basic bs => Graph.singleton [bs]
|
||||||
|
| .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
|
||||||
|
| .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
|
||||||
|
| .whileLoop _ s => Graph.loop (buildCfg s)
|
||||||
|
|
||||||
|
namespace Graph
|
||||||
|
|
||||||
|
variable (g : Graph)
|
||||||
|
|
||||||
|
def indices : List g.Index := List.finRange g.size
|
||||||
|
|
||||||
|
theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
|
||||||
|
List.mem_finRange idx
|
||||||
|
|
||||||
|
theorem nodup_indices : g.indices.Nodup :=
|
||||||
|
List.nodup_finRange g.size
|
||||||
|
|
||||||
|
def predecessors (idx : g.Index) : List g.Index :=
|
||||||
|
g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
|
||||||
|
|
||||||
|
theorem mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
|
||||||
|
(h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
|
||||||
|
List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩
|
||||||
|
|
||||||
|
theorem edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
|
||||||
|
(h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
|
||||||
|
simpa using (List.mem_filter.mp h).2
|
||||||
|
|
||||||
|
end Graph
|
||||||
|
|
||||||
|
end Spa
|
||||||
60
lean/Spa/Language/Notation.lean
Normal file
60
lean/Spa/Language/Notation.lean
Normal file
@@ -0,0 +1,60 @@
|
|||||||
|
import Spa.Language.Base
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
/-!
|
||||||
|
Scoped quotation syntax for writing object-language programs.
|
||||||
|
|
||||||
|
`[obj_expr| … ]` builds an `Expr`, `[obj_stmt| … ]` builds a `Stmt`.
|
||||||
|
|
||||||
|
Example:
|
||||||
|
```
|
||||||
|
[obj_stmt|
|
||||||
|
zero := 0;
|
||||||
|
pos := zero + 1;
|
||||||
|
if pos { x := 1 } else { noop };
|
||||||
|
while x { x := x - 1 }
|
||||||
|
]
|
||||||
|
```
|
||||||
|
-/
|
||||||
|
|
||||||
|
/-- Expressions of the object language. -/
|
||||||
|
declare_syntax_cat obj_expr
|
||||||
|
|
||||||
|
syntax num : obj_expr
|
||||||
|
syntax ident : obj_expr
|
||||||
|
syntax:65 obj_expr:65 " + " obj_expr:66 : obj_expr
|
||||||
|
syntax:65 obj_expr:65 " - " obj_expr:66 : obj_expr
|
||||||
|
syntax "(" obj_expr ")" : obj_expr
|
||||||
|
|
||||||
|
/-- Statements of the object language. -/
|
||||||
|
declare_syntax_cat obj_stmt
|
||||||
|
|
||||||
|
syntax "noop" : obj_stmt
|
||||||
|
syntax ident " := " obj_expr : obj_stmt
|
||||||
|
syntax "if " obj_expr " { " obj_stmt " } " "else" " { " obj_stmt " } " : obj_stmt
|
||||||
|
syntax "while " obj_expr " { " obj_stmt " } " : obj_stmt
|
||||||
|
syntax:50 obj_stmt:51 "; " obj_stmt:50 : obj_stmt
|
||||||
|
syntax "(" obj_stmt ")" : obj_stmt
|
||||||
|
|
||||||
|
scoped syntax "[obj_expr| " obj_expr " ]" : term
|
||||||
|
scoped syntax "[obj_stmt| " obj_stmt " ]" : term
|
||||||
|
|
||||||
|
scoped macro_rules
|
||||||
|
| `([obj_expr| $n:num]) => `(Expr.num $n)
|
||||||
|
| `([obj_expr| $x:ident]) => `(Expr.var $(Lean.quote x.getId.toString))
|
||||||
|
| `([obj_expr| $a + $b]) => `(Expr.add [obj_expr| $a] [obj_expr| $b])
|
||||||
|
| `([obj_expr| $a - $b]) => `(Expr.sub [obj_expr| $a] [obj_expr| $b])
|
||||||
|
| `([obj_expr| ($e:obj_expr)]) => `([obj_expr| $e])
|
||||||
|
|
||||||
|
scoped macro_rules
|
||||||
|
| `([obj_stmt| noop]) => `(Stmt.basic .noop)
|
||||||
|
| `([obj_stmt| $x:ident := $e]) =>
|
||||||
|
`(Stmt.basic (.assign $(Lean.quote x.getId.toString) [obj_expr| $e]))
|
||||||
|
| `([obj_stmt| $s₁ ; $s₂]) => `(Stmt.andThen [obj_stmt| $s₁] [obj_stmt| $s₂])
|
||||||
|
| `([obj_stmt| if $e { $s₁ } else { $s₂ }]) =>
|
||||||
|
`(Stmt.ifElse [obj_expr| $e] [obj_stmt| $s₁] [obj_stmt| $s₂])
|
||||||
|
| `([obj_stmt| while $e { $s }]) => `(Stmt.whileLoop [obj_expr| $e] [obj_stmt| $s])
|
||||||
|
| `([obj_stmt| ($s:obj_stmt)]) => `([obj_stmt| $s])
|
||||||
|
|
||||||
|
end Spa
|
||||||
233
lean/Spa/Language/Properties.lean
Normal file
233
lean/Spa/Language/Properties.lean
Normal file
@@ -0,0 +1,233 @@
|
|||||||
|
import Spa.Language.Traces
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
open Graph
|
||||||
|
|
||||||
|
theorem Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
|
||||||
|
Fin.castAdd m i ≠ Fin.natAdd n j := by
|
||||||
|
intro h
|
||||||
|
have := congrArg Fin.val h
|
||||||
|
simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
|
||||||
|
omega
|
||||||
|
|
||||||
|
/-! ### Trace embeddings -/
|
||||||
|
|
||||||
|
section Embeddings
|
||||||
|
|
||||||
|
variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
|
||||||
|
|
||||||
|
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
|
||||||
|
induction tr with
|
||||||
|
| single hbs =>
|
||||||
|
exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
|
||||||
|
Fin.append_left])
|
||||||
|
| edge hbs he _ ih =>
|
||||||
|
refine Trace.edge ?_ ?_ ih
|
||||||
|
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
|
||||||
|
· exact List.mem_append_left _ (List.mem_map_of_mem _ he)
|
||||||
|
|
||||||
|
theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
|
||||||
|
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
|
||||||
|
Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
|
||||||
|
induction tr with
|
||||||
|
| single hbs =>
|
||||||
|
exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
|
||||||
|
Fin.append_right])
|
||||||
|
| edge hbs he _ ih =>
|
||||||
|
refine Trace.edge ?_ ?_ ih
|
||||||
|
· rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
|
||||||
|
· exact List.mem_append_right _ (List.mem_map_of_mem _ he)
|
||||||
|
|
||||||
|
theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
|
||||||
|
(tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
|
||||||
|
Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
|
||||||
|
induction tr with
|
||||||
|
| single hbs =>
|
||||||
|
exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
|
||||||
|
Fin.append_left])
|
||||||
|
| edge hbs he _ ih =>
|
||||||
|
refine Trace.edge ?_ ?_ ih
|
||||||
|
· rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
|
||||||
|
· exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
|
||||||
|
|
||||||
|
theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
|
||||||
|
(tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
|
||||||
|
Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
|
||||||
|
induction tr with
|
||||||
|
| single hbs =>
|
||||||
|
exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
|
||||||
|
Fin.append_right])
|
||||||
|
| edge hbs he _ ih =>
|
||||||
|
refine Trace.edge ?_ ?_ ih
|
||||||
|
· rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
|
||||||
|
· exact List.mem_append_left _
|
||||||
|
(List.mem_append_right _ (List.mem_map_of_mem _ he))
|
||||||
|
|
||||||
|
theorem EndToEndTrace.comp_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
|
||||||
|
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
|
||||||
|
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
|
||||||
|
exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁),
|
||||||
|
i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
|
||||||
|
tr.comp_left⟩
|
||||||
|
|
||||||
|
theorem EndToEndTrace.comp_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
|
||||||
|
EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
|
||||||
|
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
|
||||||
|
exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁),
|
||||||
|
i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
|
||||||
|
tr.comp_right⟩
|
||||||
|
|
||||||
|
theorem EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
|
||||||
|
(etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
|
||||||
|
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
|
||||||
|
obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
|
||||||
|
refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁,
|
||||||
|
j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂,
|
||||||
|
Trace.concat tr₁.link_left ?_ tr₂.link_right⟩
|
||||||
|
exact List.mem_append_right _
|
||||||
|
(List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
|
||||||
|
|
||||||
|
end Embeddings
|
||||||
|
|
||||||
|
/-! ### Loops -/
|
||||||
|
|
||||||
|
section Loop
|
||||||
|
|
||||||
|
variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
|
||||||
|
|
||||||
|
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
|
||||||
|
| single hbs =>
|
||||||
|
exact Trace.single (by
|
||||||
|
rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
|
||||||
|
Fin.append_right])
|
||||||
|
| edge hbs he _ ih =>
|
||||||
|
refine Trace.edge ?_ ?_ ih
|
||||||
|
· rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
|
||||||
|
Fin.append_right]
|
||||||
|
· exact List.mem_append_left _ (List.mem_append_left _
|
||||||
|
(List.mem_append_left _ (List.mem_map_of_mem _ he)))
|
||||||
|
|
||||||
|
private theorem loop_nodes_at_in :
|
||||||
|
(Graph.loop g).nodes g.loopIn = [] :=
|
||||||
|
Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
|
||||||
|
|
||||||
|
private theorem loop_nodes_at_out :
|
||||||
|
(Graph.loop g).nodes g.loopOut = [] :=
|
||||||
|
Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
|
||||||
|
|
||||||
|
theorem EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
|
||||||
|
EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
|
||||||
|
obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
|
||||||
|
-- the edge in → (2 ↑ʳ i₁), reached through the second edge group
|
||||||
|
have hin : (g.loopIn, i₁.natAdd 2) ∈ (Graph.loop g).edges := by
|
||||||
|
refine List.mem_append_left _ (List.mem_append_left _ (List.mem_append_right _ ?_))
|
||||||
|
exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₁)
|
||||||
|
-- the edge (2 ↑ʳ i₂) → out, reached through the third edge group
|
||||||
|
have hout : (i₂.natAdd 2, g.loopOut) ∈ (Graph.loop g).edges := by
|
||||||
|
refine List.mem_append_left _ (List.mem_append_right _ ?_)
|
||||||
|
exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂)
|
||||||
|
refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩
|
||||||
|
exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
|
||||||
|
(Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
|
||||||
|
|
||||||
|
private theorem loop_edge_out_in :
|
||||||
|
((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by
|
||||||
|
refine List.mem_append_right _ ?_
|
||||||
|
exact List.mem_cons_self _ _
|
||||||
|
|
||||||
|
theorem EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
|
||||||
|
(etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
|
||||||
|
EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
|
||||||
|
obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
|
||||||
|
obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
|
||||||
|
simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂
|
||||||
|
subst h₁; subst h₂; subst k₁; subst k₂
|
||||||
|
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
|
||||||
|
Trace.concat tr₁ loop_edge_out_in tr₂⟩
|
||||||
|
|
||||||
|
theorem EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
|
||||||
|
have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges :=
|
||||||
|
List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _))
|
||||||
|
exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
|
||||||
|
Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hedge
|
||||||
|
(Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))⟩
|
||||||
|
|
||||||
|
end Loop
|
||||||
|
|
||||||
|
/-! ### Singletons, wrap, and the main result -/
|
||||||
|
|
||||||
|
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⟩
|
||||||
|
|
||||||
|
theorem EndToEndTrace.singleton_nil (ρ : Env) :
|
||||||
|
EndToEndTrace (Graph.singleton []) ρ ρ :=
|
||||||
|
EndToEndTrace.singleton EvalBasicStmts.nil
|
||||||
|
|
||||||
|
theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
|
||||||
|
(etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
|
||||||
|
(EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
|
||||||
|
|
||||||
|
theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
|
||||||
|
(h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
|
||||||
|
induction h with
|
||||||
|
| basic ρ₁ ρ₂ bs hbs =>
|
||||||
|
exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)
|
||||||
|
| andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
|
||||||
|
exact ih₁.concat ih₂
|
||||||
|
| ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
|
||||||
|
exact ih.comp_left
|
||||||
|
| ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
|
||||||
|
exact ih.comp_right
|
||||||
|
| whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
|
||||||
|
exact (ih₁.loop).loop_concat ih₂
|
||||||
|
| whileFalse ρ e s _ =>
|
||||||
|
exact EndToEndTrace.loop_empty
|
||||||
|
|
||||||
|
/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
|
||||||
|
|
||||||
|
def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
|
||||||
|
(0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size)
|
||||||
|
|
||||||
|
def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
|
||||||
|
Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
|
||||||
|
|
||||||
|
theorem Graph.wrap_inputs (g : Graph) :
|
||||||
|
(Graph.wrap g).inputs = [g.wrapInput] := rfl
|
||||||
|
|
||||||
|
theorem Graph.wrap_outputs (g : Graph) :
|
||||||
|
(Graph.wrap g).outputs = [g.wrapOutput] := rfl
|
||||||
|
|
||||||
|
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)
|
||||||
|
∉ (Graph.singleton [] ⤳ g₂).edges := by
|
||||||
|
intro h
|
||||||
|
rcases List.mem_append.mp h with h' | h'
|
||||||
|
· rcases List.mem_append.mp h' with h'' | h''
|
||||||
|
· -- lifted edges of `singleton []`: there are none
|
||||||
|
simp [Graph.singleton, List.finCastAddProd] at h''
|
||||||
|
· -- lifted edges of g₂: targets are natAdd
|
||||||
|
obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
|
||||||
|
exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
|
||||||
|
· -- product edges: targets are natAdd'd inputs of g₂
|
||||||
|
obtain ⟨-, hb⟩ := List.mem_product.mp h'
|
||||||
|
obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
|
||||||
|
exact Fin.castAdd_ne_natAdd i j heq.symm
|
||||||
|
|
||||||
|
theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
|
||||||
|
(h : idx ∈ (Graph.wrap g).inputs) :
|
||||||
|
(Graph.wrap g).predecessors idx = [] := by
|
||||||
|
rw [Graph.wrap_inputs, List.mem_singleton] at h
|
||||||
|
subst h
|
||||||
|
rw [Graph.predecessors, List.filter_eq_nil_iff]
|
||||||
|
intro idx' _
|
||||||
|
simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx'
|
||||||
|
|
||||||
|
end Spa
|
||||||
66
lean/Spa/Language/Semantics.lean
Normal file
66
lean/Spa/Language/Semantics.lean
Normal file
@@ -0,0 +1,66 @@
|
|||||||
|
import Spa.Language.Base
|
||||||
|
import Spa.Lattice
|
||||||
|
import Spa.Interp
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
inductive Value where
|
||||||
|
| int (z : ℤ)
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
def Env : Type := List (String × Value)
|
||||||
|
|
||||||
|
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') :: ρ)
|
||||||
|
|
||||||
|
inductive EvalExpr : Env → Expr → Value → Prop
|
||||||
|
| num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
|
||||||
|
| var (ρ : Env) (x : String) (v : Value) :
|
||||||
|
Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v
|
||||||
|
| add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :
|
||||||
|
EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
|
||||||
|
EvalExpr ρ (.add e₁ e₂) (.int (z₁ + z₂))
|
||||||
|
| sub (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :
|
||||||
|
EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
|
||||||
|
EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
|
||||||
|
|
||||||
|
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) :: ρ)
|
||||||
|
|
||||||
|
inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
|
||||||
|
| nil {ρ : Env} : EvalBasicStmts ρ [] ρ
|
||||||
|
| cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
|
||||||
|
EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
|
||||||
|
EvalBasicStmts ρ₁ (bs :: bss) ρ₃
|
||||||
|
|
||||||
|
inductive EvalStmt : Env → Stmt → Env → Prop
|
||||||
|
| basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
|
||||||
|
EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
|
||||||
|
| andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) :
|
||||||
|
EvalStmt ρ₁ s₁ ρ₂ → EvalStmt ρ₂ s₂ ρ₃ →
|
||||||
|
EvalStmt ρ₁ (.andThen s₁ s₂) ρ₃
|
||||||
|
| ifTrue (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) :
|
||||||
|
EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s₁ ρ₂ →
|
||||||
|
EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂
|
||||||
|
| ifFalse (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) :
|
||||||
|
EvalExpr ρ₁ e (.int 0) → EvalStmt ρ₁ s₂ ρ₂ →
|
||||||
|
EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂
|
||||||
|
| whileTrue (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) :
|
||||||
|
EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s ρ₂ →
|
||||||
|
EvalStmt ρ₂ (.whileLoop e s) ρ₃ →
|
||||||
|
EvalStmt ρ₁ (.whileLoop e s) ρ₃
|
||||||
|
| whileFalse (ρ : Env) (e : Expr) (s : Stmt) :
|
||||||
|
EvalExpr ρ e (.int 0) →
|
||||||
|
EvalStmt ρ (.whileLoop e s) ρ
|
||||||
|
|
||||||
|
class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
|
||||||
|
interp_sup : ∀ {l₁ l₂ : L} (v : Value),
|
||||||
|
interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v
|
||||||
|
interp_inf : ∀ {l₁ l₂ : L} (v : Value),
|
||||||
|
interp l₁ v ∧ interp l₂ v → interp (l₁ ⊓ l₂) v
|
||||||
|
|
||||||
|
end Spa
|
||||||
26
lean/Spa/Language/Traces.lean
Normal file
26
lean/Spa/Language/Traces.lean
Normal file
@@ -0,0 +1,26 @@
|
|||||||
|
import Spa.Language.Semantics
|
||||||
|
import Spa.Language.Graphs
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
|
||||||
|
| single {ρ₁ ρ₂ : Env} {idx : g.Index} :
|
||||||
|
EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
|
||||||
|
| edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
|
||||||
|
EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
|
||||||
|
Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
|
||||||
|
|
||||||
|
theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
|
||||||
|
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
|
||||||
|
(he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
|
||||||
|
Trace g idx₁ idx₄ ρ₁ ρ₃ := by
|
||||||
|
induction tr₁ with
|
||||||
|
| single hbs => exact Trace.edge hbs he tr₂
|
||||||
|
| edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
|
||||||
|
|
||||||
|
inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
|
||||||
|
| intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
|
||||||
|
(idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
|
||||||
|
(trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂
|
||||||
|
|
||||||
|
end Spa
|
||||||
91
lean/Spa/Lattice.lean
Normal file
91
lean/Spa/Lattice.lean
Normal file
@@ -0,0 +1,91 @@
|
|||||||
|
import Mathlib.Order.Lattice
|
||||||
|
import Mathlib.Order.RelSeries
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
|
||||||
|
(f : α → β → γ) : Prop :=
|
||||||
|
(∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))
|
||||||
|
|
||||||
|
section Folds
|
||||||
|
|
||||||
|
variable {α β : Type*} [Preorder α] [Preorder β]
|
||||||
|
|
||||||
|
theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
|
||||||
|
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
|
||||||
|
(hf₁ : ∀ b, Monotone fun a => f a b) (hf₂ : ∀ a, Monotone (f a)) :
|
||||||
|
l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
|
||||||
|
induction hl with
|
||||||
|
| nil => exact hb
|
||||||
|
| cons hxy _ ih =>
|
||||||
|
exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
|
||||||
|
|
||||||
|
theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
|
||||||
|
(hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
|
||||||
|
(hf₁ : ∀ a, Monotone fun b => f b a) (hf₂ : ∀ b, Monotone (f b)) :
|
||||||
|
l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
|
||||||
|
induction hl generalizing b₁ b₂ with
|
||||||
|
| nil => exact hb
|
||||||
|
| cons hxy _ ih =>
|
||||||
|
exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
|
||||||
|
|
||||||
|
omit [Preorder α] in
|
||||||
|
theorem foldr_mono' (l : List α) (f : α → β → β)
|
||||||
|
(hf : ∀ a, Monotone (f a ·)) : Monotone fun b => l.foldr f b := by
|
||||||
|
intro b₁ b₂ hb
|
||||||
|
induction l with
|
||||||
|
| nil => exact hb
|
||||||
|
| cons x xs ih => exact hf x ih
|
||||||
|
|
||||||
|
omit [Preorder α] in
|
||||||
|
theorem foldl_mono' (l : List α) (f : β → α → β)
|
||||||
|
(hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
|
||||||
|
intro b₁ b₂ hb
|
||||||
|
induction l generalizing b₁ b₂ with
|
||||||
|
| nil => exact hb
|
||||||
|
| cons x xs ih => exact ih (hf x hb)
|
||||||
|
|
||||||
|
end Folds
|
||||||
|
|
||||||
|
def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
|
||||||
|
∀ c : LTSeries α, c.length ≤ n
|
||||||
|
|
||||||
|
structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
|
||||||
|
series : LTSeries α
|
||||||
|
head_series : series.head = f
|
||||||
|
last_series : series.last = t
|
||||||
|
length_series : series.length = n
|
||||||
|
|
||||||
|
class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
|
||||||
|
height : ℕ
|
||||||
|
longestChain : PointedLTSeries α ⊥ ⊤ height
|
||||||
|
chains_bounded : BoundedChains α height
|
||||||
|
|
||||||
|
namespace FixedHeight
|
||||||
|
|
||||||
|
variable {α : Type*} [Lattice α] {h : ℕ}
|
||||||
|
|
||||||
|
theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
|
||||||
|
intro a
|
||||||
|
by_cases heq : ⊥ ⊓ a = ⊥
|
||||||
|
· exact inf_eq_left.mp heq
|
||||||
|
· exfalso
|
||||||
|
have lc := FiniteHeightLattice.longestChain (α := α)
|
||||||
|
have hlt : ⊥ ⊓ a < lc.series.head := by
|
||||||
|
rw [lc.head_series]
|
||||||
|
exact lt_of_le_of_ne inf_le_left heq
|
||||||
|
have hbound := FiniteHeightLattice.chains_bounded (lc.series.cons (⊥ ⊓ a) hlt)
|
||||||
|
rw [RelSeries.cons_length, lc.length_series] at hbound
|
||||||
|
omega
|
||||||
|
|
||||||
|
end FixedHeight
|
||||||
|
|
||||||
|
namespace FiniteHeightLattice
|
||||||
|
|
||||||
|
variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
|
||||||
|
|
||||||
|
theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
|
||||||
|
|
||||||
|
end FiniteHeightLattice
|
||||||
|
|
||||||
|
end Spa
|
||||||
241
lean/Spa/Lattice/AboveBelow.lean
Normal file
241
lean/Spa/Lattice/AboveBelow.lean
Normal file
@@ -0,0 +1,241 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
inductive AboveBelow (α : Type*) where
|
||||||
|
| bot
|
||||||
|
| top
|
||||||
|
| mk (x : α)
|
||||||
|
deriving DecidableEq
|
||||||
|
|
||||||
|
namespace AboveBelow
|
||||||
|
|
||||||
|
instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
|
||||||
|
toString
|
||||||
|
| bot => "⊥"
|
||||||
|
| top => "⊤"
|
||||||
|
| mk x => toString x
|
||||||
|
|
||||||
|
variable {α : Type*} [DecidableEq α]
|
||||||
|
|
||||||
|
instance : Max (AboveBelow α) where
|
||||||
|
max
|
||||||
|
| bot, x => x
|
||||||
|
| top, _ => top
|
||||||
|
| mk x, mk y => if x = y then mk x else top
|
||||||
|
| mk x, bot => mk x
|
||||||
|
| mk _, top => top
|
||||||
|
|
||||||
|
instance : Min (AboveBelow α) where
|
||||||
|
min
|
||||||
|
| bot, _ => bot
|
||||||
|
| top, x => x
|
||||||
|
| mk x, mk y => if x = y then mk x else bot
|
||||||
|
| mk _, bot => bot
|
||||||
|
| mk x, top => mk x
|
||||||
|
|
||||||
|
@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
|
||||||
|
@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
|
||||||
|
@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
|
||||||
|
@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
|
||||||
|
@[simp] theorem mk_sup_mk (x y : α) :
|
||||||
|
(mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
|
||||||
|
|
||||||
|
@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
|
||||||
|
@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
|
||||||
|
@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
|
||||||
|
@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
|
||||||
|
@[simp] theorem mk_inf_mk (x y : α) :
|
||||||
|
(mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
|
||||||
|
|
||||||
|
protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
|
||||||
|
[bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
|
||||||
|
split_ifs with h₁ h₂ h₂ <;> simp_all
|
||||||
|
|
||||||
|
protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
|
||||||
|
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
|
||||||
|
split_ifs <;> simp_all
|
||||||
|
|
||||||
|
protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
|
||||||
|
[bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
|
||||||
|
split_ifs with h₁ h₂ h₂ <;> simp_all
|
||||||
|
|
||||||
|
protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
|
||||||
|
simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
|
||||||
|
split_ifs <;> simp_all
|
||||||
|
|
||||||
|
protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
|
||||||
|
simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
|
||||||
|
bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
|
||||||
|
try (split_ifs <;> simp_all)
|
||||||
|
|
||||||
|
protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
|
||||||
|
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)
|
||||||
|
|
||||||
|
instance : Lattice (AboveBelow α) :=
|
||||||
|
Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
|
||||||
|
AboveBelow.inf_comm AboveBelow.inf_assoc
|
||||||
|
AboveBelow.sup_inf_self AboveBelow.inf_sup_self
|
||||||
|
|
||||||
|
theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
|
||||||
|
|
||||||
|
theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
|
||||||
|
le_iff.mpr (bot_sup a)
|
||||||
|
|
||||||
|
theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
|
||||||
|
le_iff.mpr (sup_top a)
|
||||||
|
|
||||||
|
theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
|
||||||
|
lt_of_le_of_ne (bot_le' _) (by simp)
|
||||||
|
|
||||||
|
theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
|
||||||
|
lt_of_le_of_ne (le_top' _) (by simp)
|
||||||
|
|
||||||
|
theorem bot_lt_top : (bot : AboveBelow α) < top :=
|
||||||
|
lt_of_le_of_ne (bot_le' _) (by simp)
|
||||||
|
|
||||||
|
theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
|
||||||
|
a = bot ∨ b = top ∨ a = b := by
|
||||||
|
have hsup := le_iff.mp h
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y
|
||||||
|
· exact Or.inl rfl
|
||||||
|
· exact Or.inr (Or.inl rfl)
|
||||||
|
· exact Or.inl rfl
|
||||||
|
· exact absurd hsup (by simp)
|
||||||
|
· exact Or.inr (Or.inl rfl)
|
||||||
|
· exact absurd hsup (by simp)
|
||||||
|
· exact absurd hsup (by simp)
|
||||||
|
· exact Or.inr (Or.inl rfl)
|
||||||
|
· rw [mk_sup_mk] at hsup
|
||||||
|
by_cases hxy : x = y
|
||||||
|
· exact Or.inr (Or.inr (by rw [hxy]))
|
||||||
|
· rw [if_neg hxy] at hsup
|
||||||
|
exact absurd hsup (by simp)
|
||||||
|
|
||||||
|
/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
|
||||||
|
`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
|
||||||
|
monotone in both arguments — regardless of its values on plain elements.
|
||||||
|
`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
|
||||||
|
monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
|
||||||
|
theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
|
||||||
|
(f : AboveBelow α → AboveBelow β → AboveBelow γ)
|
||||||
|
(hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
|
||||||
|
(htopl : ∀ y, y ≠ bot → f top y = top)
|
||||||
|
(htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
|
||||||
|
constructor
|
||||||
|
· intro y a b hab
|
||||||
|
show f a y ≤ f b y
|
||||||
|
rcases le_cases hab with rfl | rfl | rfl
|
||||||
|
· rw [hbotl]; exact bot_le' _
|
||||||
|
· rcases eq_or_ne y bot with rfl | hy
|
||||||
|
· rw [hbotr, hbotr]
|
||||||
|
· rw [htopl y hy]; exact le_top' _
|
||||||
|
· exact le_rfl
|
||||||
|
· intro x a b hab
|
||||||
|
show f x a ≤ f x b
|
||||||
|
rcases le_cases hab with rfl | rfl | rfl
|
||||||
|
· rw [hbotr]; exact bot_le' _
|
||||||
|
· rcases eq_or_ne x bot with rfl | hx
|
||||||
|
· rw [hbotl, hbotl]
|
||||||
|
· rw [htopr x hx]; exact le_top' _
|
||||||
|
· exact le_rfl
|
||||||
|
|
||||||
|
/-! ### Interpretations of flat lattices -/
|
||||||
|
|
||||||
|
section Interp
|
||||||
|
|
||||||
|
variable {V : Type*} {P : AboveBelow α → V → Prop}
|
||||||
|
|
||||||
|
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
|
||||||
|
· rw [bot_sup]; exact h.resolve_left (hbot v)
|
||||||
|
· rw [top_sup]; exact htop v
|
||||||
|
· rcases s₂ with _ | _ | y
|
||||||
|
· rw [sup_bot]; exact h.resolve_right (hbot v)
|
||||||
|
· rw [sup_top]; exact htop v
|
||||||
|
· rw [mk_sup_mk]
|
||||||
|
split
|
||||||
|
· next heq => subst heq; exact h.elim id id
|
||||||
|
· exact htop v
|
||||||
|
|
||||||
|
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
|
||||||
|
rcases s₁ with _ | _ | x
|
||||||
|
· rw [bot_inf]; exact h.1
|
||||||
|
· rw [top_inf]; exact h.2
|
||||||
|
· rcases s₂ with _ | _ | y
|
||||||
|
· rw [inf_bot]; exact h.2
|
||||||
|
· rw [inf_top]; exact h.1
|
||||||
|
· rw [mk_inf_mk]
|
||||||
|
split
|
||||||
|
· next heq => subst heq; exact h.1
|
||||||
|
· next hne => exact absurd h (hdisj hne v)
|
||||||
|
|
||||||
|
end Interp
|
||||||
|
|
||||||
|
/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
|
||||||
|
(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
|
||||||
|
def rank : AboveBelow α → ℕ
|
||||||
|
| bot => 0
|
||||||
|
| mk _ => 1
|
||||||
|
| top => 2
|
||||||
|
|
||||||
|
/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
|
||||||
|
`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
|
||||||
|
theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
|
||||||
|
intro h
|
||||||
|
obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
|
||||||
|
have hsup := le_iff.mp hle
|
||||||
|
rw [mk_sup_mk] at hsup
|
||||||
|
by_cases hxy : x = y
|
||||||
|
· rw [if_pos hxy] at hsup
|
||||||
|
exact hne hsup
|
||||||
|
· rw [if_neg hxy] at hsup
|
||||||
|
exact absurd hsup (by simp)
|
||||||
|
|
||||||
|
theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
|
||||||
|
intro a b hab
|
||||||
|
rcases a with _ | _ | x <;> rcases b with _ | _ | y
|
||||||
|
· exact absurd hab (lt_irrefl _)
|
||||||
|
· simp [rank]
|
||||||
|
· simp [rank]
|
||||||
|
· exact absurd hab (bot_le' _).not_lt
|
||||||
|
· exact absurd hab (lt_irrefl _)
|
||||||
|
· exact absurd hab (le_top' _).not_lt
|
||||||
|
· exact absurd hab (bot_le' _).not_lt
|
||||||
|
· simp [rank]
|
||||||
|
· exact absurd hab (not_mk_lt_mk x y)
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
|
||||||
|
bot := bot
|
||||||
|
top := top
|
||||||
|
height := 2
|
||||||
|
longestChain :=
|
||||||
|
{ series :=
|
||||||
|
((RelSeries.singleton _ bot).snoc (mk default)
|
||||||
|
(by rw [RelSeries.last_singleton]; exact bot_lt_mk default)).snoc top
|
||||||
|
(by rw [RelSeries.last_snoc]; exact mk_lt_top default)
|
||||||
|
head_series := by simp
|
||||||
|
last_series := by simp
|
||||||
|
length_series := by simp [RelSeries.snoc, RelSeries.append] }
|
||||||
|
chains_bounded := boundedChains
|
||||||
|
|
||||||
|
end AboveBelow
|
||||||
|
|
||||||
|
end Spa
|
||||||
546
lean/Spa/Lattice/FiniteMap.lean
Normal file
546
lean/Spa/Lattice/FiniteMap.lean
Normal file
@@ -0,0 +1,546 @@
|
|||||||
|
import Spa.Lattice.IterProd
|
||||||
|
import Spa.Isomorphism
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
|
||||||
|
{ l : List (A × B) // l.map Prod.fst = ks }
|
||||||
|
|
||||||
|
namespace FiniteMap
|
||||||
|
|
||||||
|
variable {A B : Type*} {ks : List A}
|
||||||
|
|
||||||
|
instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
|
||||||
|
fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
|
||||||
|
|
||||||
|
theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
|
||||||
|
fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
|
||||||
|
fm₁.property.trans fm₂.property.symm
|
||||||
|
|
||||||
|
def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
|
||||||
|
List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
|
||||||
|
|
||||||
|
theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
|
||||||
|
l₁.map Prod.fst = l₂.map Prod.fst →
|
||||||
|
(combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
|
||||||
|
| [], [], _ => rfl
|
||||||
|
| p :: l₁, q :: l₂, h => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h
|
||||||
|
simp only [combine, List.zipWith_cons_cons, List.map_cons]
|
||||||
|
exact congrArg _ (combine_spine f h.2)
|
||||||
|
| [], _ :: _, h => by simp at h
|
||||||
|
| _ :: _, [], h => by simp at h
|
||||||
|
|
||||||
|
theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
|
||||||
|
∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
|
||||||
|
combine f l₁ l₂ = combine f l₂ l₁
|
||||||
|
| [], [], _ => rfl
|
||||||
|
| p :: l₁, q :: l₂, h => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h
|
||||||
|
simp only [combine, List.zipWith_cons_cons]
|
||||||
|
rw [h.1, hf]
|
||||||
|
exact congrArg _ (combine_comm f hf h.2)
|
||||||
|
| [], _ :: _, h => by simp at h
|
||||||
|
| _ :: _, [], h => by simp at h
|
||||||
|
|
||||||
|
theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
|
||||||
|
∀ {l₁ l₂ l₃ : List (A × B)},
|
||||||
|
l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
|
||||||
|
combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
|
||||||
|
| [], [], [], _, _ => rfl
|
||||||
|
| p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
|
||||||
|
simp only [combine, List.zipWith_cons_cons]
|
||||||
|
rw [hf]
|
||||||
|
exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
|
||||||
|
| [], [], _ :: _, _, h => by simp at h
|
||||||
|
| [], _ :: _, _, h, _ => by simp at h
|
||||||
|
| _ :: _, [], _, h, _ => by simp at h
|
||||||
|
| _ :: _, _ :: _, [], _, h => by simp at h
|
||||||
|
|
||||||
|
theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
|
||||||
|
∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
|
||||||
|
combine f l₁ (combine g l₁ l₂) = l₁
|
||||||
|
| [], [], _ => rfl
|
||||||
|
| p :: l₁, q :: l₂, h => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h
|
||||||
|
simp only [combine, List.zipWith_cons_cons, hfg]
|
||||||
|
exact congrArg _ (combine_absorb f g hfg h.2)
|
||||||
|
| [], _ :: _, h => by simp at h
|
||||||
|
| _ :: _, [], h => by simp at h
|
||||||
|
|
||||||
|
variable [Lattice B]
|
||||||
|
|
||||||
|
instance : Max (FiniteMap A B ks) where
|
||||||
|
max fm₁ fm₂ :=
|
||||||
|
⟨combine (· ⊔ ·) fm₁.val fm₂.val,
|
||||||
|
(combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
|
||||||
|
|
||||||
|
instance : Min (FiniteMap A B ks) where
|
||||||
|
min fm₁ fm₂ :=
|
||||||
|
⟨combine (· ⊓ ·) fm₁.val fm₂.val,
|
||||||
|
(combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
|
||||||
|
|
||||||
|
@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
|
||||||
|
(fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
|
||||||
|
|
||||||
|
@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
|
||||||
|
(fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
|
||||||
|
|
||||||
|
instance : Lattice (FiniteMap A B ks) :=
|
||||||
|
Lattice.mk'
|
||||||
|
(fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
|
||||||
|
(fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
|
||||||
|
(fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
|
||||||
|
(fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
|
||||||
|
(fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
|
||||||
|
(fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
|
||||||
|
|
||||||
|
instance : Membership (A × B) (FiniteMap A B ks) :=
|
||||||
|
⟨fun fm p => p ∈ fm.val⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
|
||||||
|
Iff.rfl
|
||||||
|
|
||||||
|
def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
|
||||||
|
k ∈ fm.val.map Prod.fst
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
|
||||||
|
rw [MemKey, fm.property]
|
||||||
|
|
||||||
|
instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
|
||||||
|
Decidable (MemKey k fm) :=
|
||||||
|
decidable_of_iff _ memKey_iff.symm
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
|
||||||
|
(h : (k, v) ∈ fm) : MemKey k fm :=
|
||||||
|
List.mem_map_of_mem _ h
|
||||||
|
|
||||||
|
section Locate
|
||||||
|
|
||||||
|
variable [DecidableEq A]
|
||||||
|
|
||||||
|
private def locateList (k : A) :
|
||||||
|
(l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
|
||||||
|
| [], h => absurd h (by simp)
|
||||||
|
| p :: l', h =>
|
||||||
|
if heq : p.1 = k then
|
||||||
|
⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
|
||||||
|
else
|
||||||
|
let ⟨v, hv⟩ := locateList k l' (by
|
||||||
|
rcases List.mem_cons.mp h with h' | h'
|
||||||
|
· exact absurd h'.symm heq
|
||||||
|
· exact h')
|
||||||
|
⟨v, List.mem_cons_of_mem _ hv⟩
|
||||||
|
|
||||||
|
def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
|
||||||
|
{v : B // (k, v) ∈ fm} :=
|
||||||
|
locateList k fm.val h
|
||||||
|
|
||||||
|
end Locate
|
||||||
|
|
||||||
|
theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
|
||||||
|
l₁.map Prod.fst = l₂.map Prod.fst →
|
||||||
|
(combine (· ⊔ ·) l₁ l₂ = l₂ ↔
|
||||||
|
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
|
||||||
|
| [], [], _ => by simp [combine]
|
||||||
|
| p :: l₁, q :: l₂, h => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h
|
||||||
|
simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
|
||||||
|
List.forall₂_cons, Prod.ext_iff]
|
||||||
|
rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
|
||||||
|
= combine (· ⊔ ·) l₁ l₂ from rfl,
|
||||||
|
combine_eq_right_iff h.2]
|
||||||
|
constructor
|
||||||
|
· rintro ⟨⟨hk, hv⟩, hrest⟩
|
||||||
|
exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
|
||||||
|
· rintro ⟨⟨hk, hv⟩, hrest⟩
|
||||||
|
exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
|
||||||
|
| [], _ :: _, h => by simp at h
|
||||||
|
| _ :: _, [], h => by simp at h
|
||||||
|
|
||||||
|
theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
|
||||||
|
fm₁ ≤ fm₂ ↔
|
||||||
|
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
|
||||||
|
rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
|
||||||
|
sup_val]
|
||||||
|
|
||||||
|
private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
|
||||||
|
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
|
||||||
|
l₁.map Prod.fst = l₂.map Prod.fst
|
||||||
|
| _, _, List.Forall₂.nil => rfl
|
||||||
|
| _, _, List.Forall₂.cons hpq hrest => by
|
||||||
|
simp [List.map_cons, hpq.1, forall₂_spine hrest]
|
||||||
|
|
||||||
|
private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
|
||||||
|
(hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
|
||||||
|
(l₁.map Prod.fst).Nodup →
|
||||||
|
∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
|
||||||
|
induction hf with
|
||||||
|
| nil =>
|
||||||
|
intro _ k v₁ v₂ h₁ _
|
||||||
|
simp at h₁
|
||||||
|
| @cons p q l₁' l₂' hpq hrest ih =>
|
||||||
|
intro hnd k v₁ v₂ h₁ h₂
|
||||||
|
simp only [List.map_cons, List.nodup_cons] at hnd
|
||||||
|
have hspine := forall₂_spine hrest
|
||||||
|
rcases List.mem_cons.mp h₁ with heq₁ | h₁'
|
||||||
|
· rcases List.mem_cons.mp h₂ with heq₂ | h₂'
|
||||||
|
· rw [← heq₁, ← heq₂] at hpq
|
||||||
|
exact hpq.2
|
||||||
|
· exfalso
|
||||||
|
apply hnd.1
|
||||||
|
rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
|
||||||
|
exact List.mem_map_of_mem _ h₂'
|
||||||
|
· rcases List.mem_cons.mp h₂ with heq₂ | h₂'
|
||||||
|
· exfalso
|
||||||
|
apply hnd.1
|
||||||
|
rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
|
||||||
|
exact List.mem_map_of_mem _ h₁'
|
||||||
|
· exact ih hnd.2 h₁' h₂'
|
||||||
|
|
||||||
|
theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
|
||||||
|
(hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
|
||||||
|
(h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
|
||||||
|
forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
|
||||||
|
l₁.map Prod.fst = l₂.map Prod.fst →
|
||||||
|
(k, v) ∈ combine f l₁ l₂ →
|
||||||
|
∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
|
||||||
|
| [], [], _, _, _, h => by simp [combine] at h
|
||||||
|
| p :: l₁, q :: l₂, k, v, hsp, h => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at hsp
|
||||||
|
simp only [combine, List.zipWith_cons_cons] at h
|
||||||
|
rcases List.mem_cons.mp h with heq | h'
|
||||||
|
· injection heq with hk hv
|
||||||
|
exact ⟨p.2, q.2, hv,
|
||||||
|
by rw [hk]; simp,
|
||||||
|
by rw [hk, hsp.1]; simp⟩
|
||||||
|
· obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
|
||||||
|
exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
|
||||||
|
|
||||||
|
theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
|
||||||
|
(h : (k, v) ∈ fm₁ ⊔ fm₂) :
|
||||||
|
∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
|
||||||
|
mem_combine _ (spine_eq fm₁ fm₂) h
|
||||||
|
|
||||||
|
section Updating
|
||||||
|
|
||||||
|
variable [DecidableEq A]
|
||||||
|
|
||||||
|
def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
|
||||||
|
FiniteMap A B ks :=
|
||||||
|
⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
|
||||||
|
rw [List.map_map,
|
||||||
|
show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
|
||||||
|
= Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
|
||||||
|
exact fm.property⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
|
||||||
|
(updating fm ks' g).val
|
||||||
|
= fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
|
||||||
|
MemKey k (updating fm ks' g) ↔ MemKey k fm := by
|
||||||
|
rw [memKey_iff, memKey_iff]
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
|
||||||
|
{ks' : List A} {g : A → B} (hk : k ∈ ks')
|
||||||
|
(h : (k, v) ∈ updating fm ks' g) : v = g k := by
|
||||||
|
obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
|
||||||
|
by_cases hmem : p.1 ∈ ks'
|
||||||
|
· rw [if_pos hmem] at heq
|
||||||
|
injection heq with h1 h2
|
||||||
|
rw [← h2, h1]
|
||||||
|
· rw [if_neg hmem] at heq
|
||||||
|
rw [heq] at hmem
|
||||||
|
exact absurd hk hmem
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
|
||||||
|
(hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
|
||||||
|
obtain ⟨v, hv⟩ := locate hmem
|
||||||
|
exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
|
||||||
|
{ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
|
||||||
|
(k, v) ∈ updating fm ks' g :=
|
||||||
|
List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
|
||||||
|
{ks' : List A} {g : A → B} (hk : k ∉ ks')
|
||||||
|
(h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
|
||||||
|
obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
|
||||||
|
by_cases hmem : p.1 ∈ ks'
|
||||||
|
· rw [if_pos hmem] at heq
|
||||||
|
injection heq with h1 _
|
||||||
|
rw [← h1] at hk
|
||||||
|
exact absurd hmem hk
|
||||||
|
· rw [if_neg hmem] at heq
|
||||||
|
exact heq ▸ hp
|
||||||
|
|
||||||
|
private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
|
||||||
|
(hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
|
||||||
|
(hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
|
||||||
|
List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
|
||||||
|
(l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
|
||||||
|
(l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
|
||||||
|
induction hl with
|
||||||
|
| nil => exact List.Forall₂.nil
|
||||||
|
| @cons x y l₁' l₂' hpq hrest ih =>
|
||||||
|
simp only [List.map_cons]
|
||||||
|
refine List.Forall₂.cons ?_ ih
|
||||||
|
obtain ⟨hk, hv⟩ := hpq
|
||||||
|
by_cases h : x.1 ∈ ks'
|
||||||
|
· rw [if_pos h, if_pos (hk ▸ h)]
|
||||||
|
exact ⟨hk, hk ▸ hg x.1⟩
|
||||||
|
· rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
|
||||||
|
exact ⟨hk, hv⟩
|
||||||
|
|
||||||
|
theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
|
||||||
|
{g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
|
||||||
|
updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
|
||||||
|
rw [le_iff] at hfm ⊢
|
||||||
|
simp only [updating_val]
|
||||||
|
exact updating_mono_list hg hfm
|
||||||
|
|
||||||
|
end Updating
|
||||||
|
|
||||||
|
section GeneralizedUpdate
|
||||||
|
|
||||||
|
variable [DecidableEq A] {L : Type*} [Lattice L]
|
||||||
|
|
||||||
|
def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
|
||||||
|
(ks' : List A) (l : L) : FiniteMap A B ks :=
|
||||||
|
(f l).updating ks' (fun k => g k l)
|
||||||
|
|
||||||
|
variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
|
||||||
|
|
||||||
|
theorem generalizedUpdate_monotone (hf : Monotone f)
|
||||||
|
(hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
|
||||||
|
fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
|
||||||
|
|
||||||
|
omit [Lattice B] [Lattice L] in
|
||||||
|
theorem generalizedUpdate_memKey {k : A} {l : L}
|
||||||
|
(h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
|
||||||
|
unfold generalizedUpdate
|
||||||
|
exact memKey_updating.mpr h
|
||||||
|
|
||||||
|
omit [Lattice B] [Lattice L] in
|
||||||
|
theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
|
||||||
|
(h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
|
||||||
|
unfold generalizedUpdate
|
||||||
|
exact mem_updating hk h
|
||||||
|
|
||||||
|
omit [Lattice B] [Lattice L] in
|
||||||
|
theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
|
||||||
|
(h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
|
||||||
|
unfold generalizedUpdate at h
|
||||||
|
exact eq_of_mem_updating (g := fun k => g k l) hk h
|
||||||
|
|
||||||
|
omit [Lattice B] [Lattice L] in
|
||||||
|
theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
|
||||||
|
(h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
|
||||||
|
unfold generalizedUpdate
|
||||||
|
exact mem_updating_of_not_mem hk h
|
||||||
|
|
||||||
|
omit [Lattice B] [Lattice L] in
|
||||||
|
theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
|
||||||
|
(h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
|
||||||
|
unfold generalizedUpdate at h
|
||||||
|
exact mem_of_mem_updating hk h
|
||||||
|
|
||||||
|
end GeneralizedUpdate
|
||||||
|
|
||||||
|
section ValuesAt
|
||||||
|
|
||||||
|
variable [DecidableEq A]
|
||||||
|
|
||||||
|
private def lookup? (k : A) : List (A × B) → Option B
|
||||||
|
| [] => none
|
||||||
|
| p :: l' => if p.1 = k then some p.2 else lookup? k l'
|
||||||
|
|
||||||
|
def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
|
||||||
|
ks'.filterMap (fun k => lookup? k fm.val)
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
|
||||||
|
(l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
|
||||||
|
lookup? k l = some v
|
||||||
|
| [], _, _, _, h => by simp at h
|
||||||
|
| p :: l', hnd, k, v, h => by
|
||||||
|
simp only [List.map_cons, List.nodup_cons] at hnd
|
||||||
|
rcases List.mem_cons.mp h with heq | h'
|
||||||
|
· rw [← heq]
|
||||||
|
simp [lookup?]
|
||||||
|
· rw [lookup?, if_neg ?_]
|
||||||
|
· exact lookup?_eq_some_of_mem hnd.2 h'
|
||||||
|
· intro hpk
|
||||||
|
subst hpk
|
||||||
|
have := List.mem_map_of_mem Prod.fst h'
|
||||||
|
exact hnd.1 this
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
|
||||||
|
{ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
|
||||||
|
List.mem_filterMap.mpr
|
||||||
|
⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
|
||||||
|
|
||||||
|
private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
|
||||||
|
(h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
|
||||||
|
Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
|
||||||
|
induction h with
|
||||||
|
| nil => exact Option.Rel.none
|
||||||
|
| @cons p q l₁ l₂ hpq hrest ih =>
|
||||||
|
rw [lookup?, lookup?]
|
||||||
|
by_cases hc : q.1 = k
|
||||||
|
· rw [if_pos hc, if_pos (hpq.1.trans hc)]
|
||||||
|
exact Option.Rel.some hpq.2
|
||||||
|
· rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
|
||||||
|
exact ih
|
||||||
|
|
||||||
|
theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
|
||||||
|
(ks' : List A) :
|
||||||
|
List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
|
||||||
|
induction ks' with
|
||||||
|
| nil => exact List.Forall₂.nil
|
||||||
|
| cons k ks'' ih =>
|
||||||
|
have hrel := lookup?_forall₂ (le_iff.mp hle) k
|
||||||
|
rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
|
||||||
|
revert hrel
|
||||||
|
generalize lookup? k fm₁.val = o₁
|
||||||
|
generalize lookup? k fm₂.val = o₂
|
||||||
|
intro hrel
|
||||||
|
cases hrel with
|
||||||
|
| none => simpa [valuesAt] using ih
|
||||||
|
| some hv => exact List.Forall₂.cons hv (by simpa [valuesAt] using ih)
|
||||||
|
|
||||||
|
end ValuesAt
|
||||||
|
|
||||||
|
section Iso
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
|
||||||
|
fm.val ≠ [] := fun h => by
|
||||||
|
have hp := fm.property
|
||||||
|
rw [h] at hp
|
||||||
|
simp at hp
|
||||||
|
|
||||||
|
def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
|
||||||
|
| ⟨[], h⟩ => absurd h (by simp)
|
||||||
|
| ⟨p :: _, _⟩ => p.2
|
||||||
|
|
||||||
|
def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
|
||||||
|
| ⟨[], h⟩ => absurd h (by simp)
|
||||||
|
| ⟨_ :: l, h⟩ =>
|
||||||
|
⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem val_eq_cons {k : A} {ks' : List A} :
|
||||||
|
∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
|
||||||
|
| ⟨[], h⟩ => absurd h (by simp)
|
||||||
|
| ⟨p :: l, h⟩ => by
|
||||||
|
simp only [List.map_cons, List.cons.injEq] at h
|
||||||
|
simp [headVal, pop, ← h.1]
|
||||||
|
|
||||||
|
def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
|
||||||
|
| [], _ => PUnit.unit
|
||||||
|
| _ :: _, fm => (fm.headVal, toIter fm.pop)
|
||||||
|
|
||||||
|
def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
|
||||||
|
| [], _ => ⟨[], rfl⟩
|
||||||
|
| k :: ks', ip =>
|
||||||
|
⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
|
||||||
|
simp [(ofIter ks' ip.2).property]⟩
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
|
||||||
|
ofIter ks (toIter fm) = fm
|
||||||
|
| [], fm => by
|
||||||
|
obtain ⟨val, hprop⟩ := fm
|
||||||
|
cases val with
|
||||||
|
| nil => rfl
|
||||||
|
| cons p l => exact absurd hprop (by simp)
|
||||||
|
| k :: ks', fm => Subtype.ext (by
|
||||||
|
show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
|
||||||
|
rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
|
||||||
|
toIter (ofIter ks ip) = ip
|
||||||
|
| [], _ => rfl
|
||||||
|
| k :: ks', ip => by
|
||||||
|
show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
|
||||||
|
rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
|
||||||
|
toIter_ofIter ks' ip.2]
|
||||||
|
rfl
|
||||||
|
|
||||||
|
theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
|
||||||
|
(h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
|
||||||
|
have h' := le_iff.mp h
|
||||||
|
rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
|
||||||
|
exact (List.forall₂_cons.mp h').1.2
|
||||||
|
|
||||||
|
theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
|
||||||
|
(h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
|
||||||
|
rw [le_iff]
|
||||||
|
have h' := le_iff.mp h
|
||||||
|
rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
|
||||||
|
exact (List.forall₂_cons.mp h').2
|
||||||
|
|
||||||
|
theorem toIter_monotone : ∀ {ks : List A},
|
||||||
|
Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
|
||||||
|
| [] => fun _ _ _ => le_refl _
|
||||||
|
| _ :: _ => fun _ _ h =>
|
||||||
|
Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
|
||||||
|
|
||||||
|
theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
|
||||||
|
| [] => fun _ _ _ => le_refl _
|
||||||
|
| k :: ks' => fun ip₁ ip₂ h => by
|
||||||
|
rw [le_iff]
|
||||||
|
show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
|
||||||
|
((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
|
||||||
|
exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
|
||||||
|
|
||||||
|
def fixedHeight [FiniteHeightLattice B] (ks : List A) :
|
||||||
|
FiniteHeightLattice (FiniteMap A B ks) :=
|
||||||
|
FiniteHeightLattice.transport
|
||||||
|
(ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
|
||||||
|
(toIter_ofIter ks) (fun fm => ofIter_toIter fm)
|
||||||
|
|
||||||
|
instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
|
||||||
|
fixedHeight ks
|
||||||
|
|
||||||
|
omit [Lattice B] in
|
||||||
|
theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
|
||||||
|
(k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
|
||||||
|
| [], _, _, h => by simp [ofIter, mem_def] at h
|
||||||
|
| k' :: ks', k, v, h => by
|
||||||
|
rcases List.mem_cons.mp h with heq | h'
|
||||||
|
· exact (Prod.ext_iff.mp heq).2
|
||||||
|
· exact mem_ofIter_build h'
|
||||||
|
|
||||||
|
theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B}
|
||||||
|
(h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by
|
||||||
|
have hbot : (fixedHeight ks).bot
|
||||||
|
= ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by
|
||||||
|
show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _
|
||||||
|
rw [IterProd.bot_fixedHeight]
|
||||||
|
rw [hbot] at h
|
||||||
|
exact mem_ofIter_build h
|
||||||
|
|
||||||
|
end Iso
|
||||||
|
|
||||||
|
end FiniteMap
|
||||||
|
|
||||||
|
end Spa
|
||||||
50
lean/Spa/Lattice/IterProd.lean
Normal file
50
lean/Spa/Lattice/IterProd.lean
Normal file
@@ -0,0 +1,50 @@
|
|||||||
|
import Spa.Lattice.Prod
|
||||||
|
import Spa.Lattice.Unit
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
universe u
|
||||||
|
|
||||||
|
def IterProd (A B : Type u) : ℕ → Type u
|
||||||
|
| 0 => B
|
||||||
|
| k + 1 => A × IterProd A B k
|
||||||
|
|
||||||
|
namespace IterProd
|
||||||
|
|
||||||
|
variable {A B : Type u}
|
||||||
|
|
||||||
|
instance instLattice [Lattice A] [Lattice B] :
|
||||||
|
∀ k, Lattice (IterProd A B k)
|
||||||
|
| 0 => inferInstanceAs (Lattice B)
|
||||||
|
| k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
|
||||||
|
|
||||||
|
instance instDecidableEq [DecidableEq A] [DecidableEq B] :
|
||||||
|
∀ k, DecidableEq (IterProd A B k)
|
||||||
|
| 0 => inferInstanceAs (DecidableEq B)
|
||||||
|
| k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
|
||||||
|
|
||||||
|
def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
|
||||||
|
| 0 => b
|
||||||
|
| k + 1 => (a, build a b k)
|
||||||
|
|
||||||
|
variable [Lattice A] [Lattice B]
|
||||||
|
|
||||||
|
def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
|
||||||
|
∀ k, FiniteHeightLattice (IterProd A B k)
|
||||||
|
| 0 => inferInstanceAs (FiniteHeightLattice B)
|
||||||
|
| k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)
|
||||||
|
|
||||||
|
instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
|
||||||
|
FiniteHeightLattice (IterProd A B k) := fixedHeight k
|
||||||
|
|
||||||
|
theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
|
||||||
|
∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
|
||||||
|
| 0 => rfl
|
||||||
|
| k + 1 => by
|
||||||
|
show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
|
||||||
|
= ((⊥ : A), build (⊥ : A) (⊥ : B) k)
|
||||||
|
rw [bot_fixedHeight k]
|
||||||
|
|
||||||
|
end IterProd
|
||||||
|
|
||||||
|
end Spa
|
||||||
98
lean/Spa/Lattice/Prod.lean
Normal file
98
lean/Spa/Lattice/Prod.lean
Normal file
@@ -0,0 +1,98 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
section Unzip
|
||||||
|
|
||||||
|
variable {α β : Type*} [PartialOrder α] [PartialOrder β]
|
||||||
|
|
||||||
|
theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
|
||||||
|
∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
|
||||||
|
c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
|
||||||
|
c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
|
||||||
|
c.length ≤ c₁.length + c₂.length := by
|
||||||
|
suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
|
||||||
|
∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
|
||||||
|
c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
|
||||||
|
c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
|
||||||
|
c.length ≤ c₁.length + c₂.length from H c.length c rfl
|
||||||
|
intro n
|
||||||
|
induction n with
|
||||||
|
| zero =>
|
||||||
|
intro c hn
|
||||||
|
refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
|
||||||
|
rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
|
||||||
|
· have hlast : Fin.last c.length = 0 := by ext; simp [hn]
|
||||||
|
simp [RelSeries.last, RelSeries.head, hlast]
|
||||||
|
| succ n ih =>
|
||||||
|
intro c hn
|
||||||
|
have h0 : c.length ≠ 0 := by omega
|
||||||
|
obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
|
||||||
|
ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
|
||||||
|
rw [RelSeries.last_tail] at hl₁ hl₂
|
||||||
|
rw [RelSeries.head_tail] at hh₁ hh₂
|
||||||
|
rw [RelSeries.tail_length] at hlen
|
||||||
|
have hstep : c.head < c 1 := by
|
||||||
|
have h := c.step ⟨0, by omega⟩
|
||||||
|
have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
|
||||||
|
ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
|
||||||
|
rwa [h1] at h
|
||||||
|
obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
|
||||||
|
rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
|
||||||
|
rcases eq_or_lt_of_le hle2 with heq2 | hlt2
|
||||||
|
· exact absurd (Prod.ext heq1 heq2) hstep.ne
|
||||||
|
· refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
|
||||||
|
hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
|
||||||
|
rw [RelSeries.last_cons]; exact hl₂, by
|
||||||
|
simp only [RelSeries.cons_length]; omega⟩
|
||||||
|
· refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
|
||||||
|
RelSeries.head_cons .., by
|
||||||
|
rw [RelSeries.last_cons]; exact hl₁,
|
||||||
|
hh₂.trans heq2.symm, hl₂, by
|
||||||
|
simp only [RelSeries.cons_length]; omega⟩
|
||||||
|
· refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
|
||||||
|
RelSeries.head_cons .., by
|
||||||
|
rw [RelSeries.last_cons]; exact hl₁,
|
||||||
|
RelSeries.head_cons .., by
|
||||||
|
rw [RelSeries.last_cons]; exact hl₂, by
|
||||||
|
simp only [RelSeries.cons_length]; omega⟩
|
||||||
|
|
||||||
|
end Unzip
|
||||||
|
|
||||||
|
section FixedHeight
|
||||||
|
|
||||||
|
variable {α β : Type*} [Lattice α] [Lattice β]
|
||||||
|
|
||||||
|
instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
|
||||||
|
FiniteHeightLattice (α × β) where
|
||||||
|
bot := ((⊥ : α), (⊥ : β))
|
||||||
|
top := ((⊤ : α), (⊤ : β))
|
||||||
|
height := A.height + B.height
|
||||||
|
longestChain :=
|
||||||
|
{ series :=
|
||||||
|
RelSeries.smash
|
||||||
|
(A.longestChain.series.map (fun a => (a, (⊥ : β)))
|
||||||
|
(fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
|
||||||
|
(B.longestChain.series.map (fun b => ((⊤ : α), b))
|
||||||
|
(fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
|
||||||
|
(by simp [A.longestChain.last_series, B.longestChain.head_series])
|
||||||
|
head_series :=
|
||||||
|
(RelSeries.head_smash _).trans
|
||||||
|
((LTSeries.head_map _ _ _).trans
|
||||||
|
(congrArg (·, (⊥ : β)) A.longestChain.head_series))
|
||||||
|
last_series :=
|
||||||
|
(RelSeries.last_smash _).trans
|
||||||
|
((LTSeries.last_map _ _ _).trans
|
||||||
|
(congrArg ((⊤ : α), ·) B.longestChain.last_series))
|
||||||
|
length_series := by
|
||||||
|
show A.longestChain.series.length + B.longestChain.series.length = _
|
||||||
|
rw [A.longestChain.length_series, B.longestChain.length_series] }
|
||||||
|
chains_bounded := fun c => by
|
||||||
|
obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
|
||||||
|
have h₁ := A.chains_bounded c₁
|
||||||
|
have h₂ := B.chains_bounded c₂
|
||||||
|
omega
|
||||||
|
|
||||||
|
end FixedHeight
|
||||||
|
|
||||||
|
end Spa
|
||||||
18
lean/Spa/Lattice/Unit.lean
Normal file
18
lean/Spa/Lattice/Unit.lean
Normal file
@@ -0,0 +1,18 @@
|
|||||||
|
import Spa.Lattice
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
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 _ _)
|
||||||
|
|
||||||
|
instance : FiniteHeightLattice PUnit where
|
||||||
|
bot := PUnit.unit
|
||||||
|
top := PUnit.unit
|
||||||
|
height := 0
|
||||||
|
longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
|
||||||
|
chains_bounded := boundedChains_of_subsingleton PUnit 0
|
||||||
|
|
||||||
|
end Spa
|
||||||
36
lean/Spa/Showable.lean
Normal file
36
lean/Spa/Showable.lean
Normal file
@@ -0,0 +1,36 @@
|
|||||||
|
import Spa.Lattice.FiniteMap
|
||||||
|
import Spa.Lattice.AboveBelow
|
||||||
|
|
||||||
|
namespace Spa
|
||||||
|
|
||||||
|
class Showable (α : Type*) where
|
||||||
|
show' : α → String
|
||||||
|
|
||||||
|
export Showable (show')
|
||||||
|
|
||||||
|
instance : Showable String := ⟨fun s => "\"" ++ s ++ "\""⟩
|
||||||
|
|
||||||
|
instance : Showable ℕ := ⟨toString⟩
|
||||||
|
|
||||||
|
instance : Showable ℤ := ⟨toString⟩
|
||||||
|
|
||||||
|
instance {n : ℕ} : Showable (Fin n) := ⟨fun i => toString i.val⟩
|
||||||
|
|
||||||
|
instance {α β : Type*} [Showable α] [Showable β] : Showable (α × β) :=
|
||||||
|
⟨fun p => "(" ++ show' p.1 ++ ", " ++ show' p.2 ++ ")"⟩
|
||||||
|
|
||||||
|
instance : Showable PUnit := ⟨fun _ => "()"⟩
|
||||||
|
|
||||||
|
instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
|
||||||
|
⟨fun
|
||||||
|
| .bot => "⊥"
|
||||||
|
| .top => "⊤"
|
||||||
|
| .mk x => show' x⟩
|
||||||
|
|
||||||
|
instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
|
||||||
|
Showable (FiniteMap α β ks) :=
|
||||||
|
⟨fun fm =>
|
||||||
|
"{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
|
||||||
|
++ "}"⟩
|
||||||
|
|
||||||
|
end Spa
|
||||||
95
lean/lake-manifest.json
Normal file
95
lean/lake-manifest.json
Normal file
@@ -0,0 +1,95 @@
|
|||||||
|
{"version": "1.1.0",
|
||||||
|
"packagesDir": ".lake/packages",
|
||||||
|
"packages":
|
||||||
|
[{"url": "https://github.com/leanprover-community/mathlib4",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "",
|
||||||
|
"rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
|
||||||
|
"name": "mathlib",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "v4.17.0",
|
||||||
|
"inherited": false,
|
||||||
|
"configFile": "lakefile.lean"},
|
||||||
|
{"url": "https://github.com/leanprover-community/plausible",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
|
||||||
|
"name": "plausible",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover-community/LeanSearchClient",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
|
||||||
|
"name": "LeanSearchClient",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover-community/import-graph",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
|
||||||
|
"name": "importGraph",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover-community/ProofWidgets4",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
|
||||||
|
"name": "proofwidgets",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "v0.0.52",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.lean"},
|
||||||
|
{"url": "https://github.com/leanprover-community/aesop",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
|
||||||
|
"name": "aesop",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "master",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover-community/quote4",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
|
||||||
|
"name": "Qq",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "master",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover-community/batteries",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover-community",
|
||||||
|
"rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
|
||||||
|
"name": "batteries",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"},
|
||||||
|
{"url": "https://github.com/leanprover/lean4-cli",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"scope": "leanprover",
|
||||||
|
"rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
|
||||||
|
"name": "Cli",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.toml"}],
|
||||||
|
"name": "spa",
|
||||||
|
"lakeDir": ".lake"}
|
||||||
14
lean/lakefile.toml
Normal file
14
lean/lakefile.toml
Normal file
@@ -0,0 +1,14 @@
|
|||||||
|
name = "spa"
|
||||||
|
defaultTargets = ["Spa"]
|
||||||
|
|
||||||
|
[[require]]
|
||||||
|
name = "mathlib"
|
||||||
|
git = "https://github.com/leanprover-community/mathlib4"
|
||||||
|
rev = "v4.17.0"
|
||||||
|
|
||||||
|
[[lean_lib]]
|
||||||
|
name = "Spa"
|
||||||
|
|
||||||
|
[[lean_exe]]
|
||||||
|
name = "spa"
|
||||||
|
root = "Main"
|
||||||
1
lean/lean-toolchain
Normal file
1
lean/lean-toolchain
Normal file
@@ -0,0 +1 @@
|
|||||||
|
leanprover/lean4:v4.17.0
|
||||||
Reference in New Issue
Block a user