4bf2dd38cd
git-subtree-dir: common-lean git-subtree-mainline:bd2e14214dgit-subtree-split:a0b719e170
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
|