a0b719e170
A new Lake project with path dependencies on the three sibling kernels
(golang-lean, octive-lean, tsm-lean). Provides typeclass abstractions
that capture what's structurally shared.
Common/ — three files:
Lang.lean — two typeclasses:
BigStepLang: Term, Value, State, Eval, deterministic.
Captures TGC's and TOC's big-step shape.
SmallStepLang: State, step.
Captures TSM's small-step shape (determinism is
automatic from `step` being a function).
Generic theorems exported once:
BigStepLang.unique_value, BigStepLang.unique_state
SmallStepLang.step_deterministic
Plus a `CompileCorrect` structure for substrate-projection
theorems (the categorical kernel of CompCert-style results).
Instances.lean — three instances:
TGCLang : BigStepLang (State := Heap × Env)
TOCLang : BigStepLang (State := Env)
TSMLang : SmallStepLang (State := TSM.State)
Each instance bridges the local kernel's existing
`BigStep`/`step` + `deterministic` proof into the typeclass.
Demo.lean — three application examples:
The SAME `BigStepLang.unique_value` theorem applied to TGC and
TOC; `SmallStepLang.step_deterministic` to TSM. One abstract
definition, three concrete payoffs.
The factoring is real: any new theorem stated over the typeclasses
applies to all instances. Future theorems (compilation correctness,
type soundness, simulation) can be expressed abstractly and proved
once.
Zero sorries / axioms / admits across all four projects.
56 lines
1.9 KiB
Text
56 lines
1.9 KiB
Text
import Common.Instances
|
||
|
||
namespace Common.Demo
|
||
|
||
open Common
|
||
|
||
/-! # Cross-language abstraction demonstration.
|
||
|
||
The same generic theorem `BigStepLang.unique_value` is here applied
|
||
to TGC and TOC. The `SmallStepLang.step_deterministic` is applied
|
||
to TSM. One abstract definition, multiple concrete payoffs. -/
|
||
|
||
/-! ## Generic theorem statement (in `Common.Lang`):
|
||
|
||
`BigStepLang.unique_value : Eval s t v₁ s₁ → Eval s t v₂ s₂ → v₁ = v₂`
|
||
|
||
Below are direct applications. -/
|
||
|
||
/-! ### TGC (golang-lean) — the `Heap × Env`-stateful instance. -/
|
||
|
||
example
|
||
(h : GolangLean.Core.Heap) (env : GolangLean.Core.Env)
|
||
(t : GolangLean.Core.Term)
|
||
(v₁ v₂ : GolangLean.Core.Value) (h₁ h₂ : GolangLean.Core.Heap)
|
||
(D₁ : GolangLean.Core.BigStep h env t v₁ h₁)
|
||
(D₂ : GolangLean.Core.BigStep h env t v₂ h₂) :
|
||
v₁ = v₂ := by
|
||
-- Package the existing TGC theorem as a Common.BigStepLang application:
|
||
exact BigStepLang.unique_value
|
||
(L := TGCLang) (s := (h, env)) (s₁ := (h₁, env)) (s₂ := (h₂, env))
|
||
⟨D₁, rfl⟩ ⟨D₂, rfl⟩
|
||
|
||
/-! ### TOC (octive-lean) — the env-mutating instance. -/
|
||
|
||
example
|
||
(env : OctiveLean.Core.Env)
|
||
(t : OctiveLean.Core.Term)
|
||
(v₁ v₂ : OctiveLean.Core.Value) (env₁ env₂ : OctiveLean.Core.Env)
|
||
(D₁ : OctiveLean.Core.BigStep env t v₁ env₁)
|
||
(D₂ : OctiveLean.Core.BigStep env t v₂ env₂) :
|
||
v₁ = v₂ :=
|
||
BigStepLang.unique_value (L := TOCLang) D₁ D₂
|
||
|
||
/-! ### TSM (tsm-lean) — the small-step instance. -/
|
||
|
||
example
|
||
(s s₁ s₂ : TsmLean.Core.State)
|
||
(h₁ : TsmLean.Core.step s = some s₁) (h₂ : TsmLean.Core.step s = some s₂) :
|
||
s₁ = s₂ :=
|
||
SmallStepLang.step_deterministic (L := TSMLang) h₁ h₂
|
||
|
||
/-! ## Observation: with three instances now exhibiting `BigStepLang`/
|
||
`SmallStepLang`, any new theorem stated abstractly applies to all
|
||
of them. The factoring is real. -/
|
||
|
||
end Common.Demo
|