Skip to content

Instantly share code, notes, and snippets.

@srghma

srghma/1 WF.lean

Last active April 28, 2026 17:51
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save srghma/82b592a3788cceb75eb75f263ffd2d61 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save srghma/82b592a3788cceb75eb75f263ffd2d61 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
1 WF.lean
-- 1. The raw data structure
inductive BinderImplementation (e : Type) where
| Op : BinderImplementation e → Array (BinderImplementation e) → BinderImplementation e
-- 2. The validation predicate
def BinderImplementation.isWF {e : Type} : BinderImplementation e → Prop
| .Op what whatElse =>
what.isWF ∧ whatElse.size > 0 ∧ (∀ x ∈ whatElse, x.isWF)
-- 3. The actual Type
def Binder (e : Type) := { b : BinderImplementation e // b.isWF }
-------
namespace List
def keys (pairs : List (α × β)) : List α := pairs.map (·.1)
end List
-- 1. The raw data structure
inductive TermImplementation : Type where
| var : String → TermImplementation
| app : TermImplementation → TermImplementation → TermImplementation
| lam : String → TermImplementation → TermImplementation
| record : List (String × TermImplementation) → TermImplementation
-- 2. The validation predicate
def TermImplementation.isWF : TermImplementation → Prop
| .var _ => True
| .app f a => f.isWF ∧ a.isWF
| .lam _ b => b.isWF
| .record entries =>
entries.keys.Nodup ∧ allWF entries
where
allWF : List (String × TermImplementation) → Prop
| [] => True
| (_, t) :: rest => t.isWF ∧ allWF rest
-- 3. The actual Type
def Term := { t : TermImplementation // t.isWF }
Raw
2 Correct-by-Construction.lean
mutual
inductive Binder (e : Type) where
| Op : Binder e → NonEmptyBinderArray e → Binder e
inductive NonEmptyBinderArray (e : Type) where
| head : Binder e → Array (Binder e) → NonEmptyBinderArray e
end
-- Now you can define a helper to get the full array back
def NonEmptyBinderArray.toArray {e} : NonEmptyBinderArray e → Array (Binder e)
| .head b bs => #[b] ++ bs
-- modular: The proof 'size > 0' is built into the structure of 'head'
--------------
mutual
inductive Term : Type where
| var : String → Term
| app : Term → Term → Term
| lam : String → Term → Term
-- {ks : List String} allows the record to hold ANY valid list of keys
| record : {ks : List String} → TermEntries ks → Term
inductive TermEntries : List String → Type where
| nil : TermEntries []
| cons : (key : String) → (val : Term) → {ks : List String}
→ (tail : TermEntries ks)
→ (h : key ∉ ks) -- Proof key is not in the tail
→ TermEntries (key :: ks)
end
-- Example of constructing a valid record:
def myTerm : Term :=
.record (
.cons "age" (.var "x") (
.cons "name" (.var "y")
.nil
(by simp) -- proof "name" ∉ []
)
(by simp) -- proof "age" ∉ ["name"]
)
Raw
3 Fixed Point.lean
-- Modular: Define this once in your library
structure NonEmptyArray (α : Type) where
head : α
tail : Array α
-- array : Array α -- doesnt work
-- isNonEmpty : array.size > 0
-- Modular: The "Shape" of your binder
structure BinderF (e α : Type) where
what : α
whatElse : NonEmptyArray α
-- The Actual Inductive: You must define the recursion explicitly
-- to satisfy the kernel's positivity check.
inductive Binder (e : Type) where
| mk : BinderF e (Binder e) → Binder e
-- Convenience helper
def Binder.op {e} (w : Binder e) (h : Binder e) (t : Array (Binder e)) : Binder e :=
.mk ⟨w, ⟨h, t⟩⟩
---------
-- 1. Shape (One level of the tree, no recursion)
inductive TermF (α : Type) where
| var : String → TermF α
| app : α → α → TermF α
| lam : String → α → TermF α
| record : List (String × α) → TermF α
-- 2. Validation Logic (Standard function)
def TermF.IsLocalWF : TermF α → Prop
| .record entries => (entries.map (·.1)).Nodup
| _ => True
inductive Term where
| mk : TermF Term → Term
-- 4. Full Recursive Validation
mutual
def Term.IsWF : Term → Prop
| .mk shape =>
TermF.IsLocalWF shape ∧
match shape with
| .var _ => True
| .app a b => a.IsWF ∧ b.IsWF
| .lam _ b => b.IsWF
| .record entries => allWF entries
def Term.allWF : List (String × Term) → Prop
| [] => True
| (_, t) :: rest => t.IsWF ∧ allWF rest
end
-- 5. The Verified Type
def VerifiedTerm := { t : Term // t.IsWF }
-- 6. Helper for construction
def mkRecord (entries : List (String × VerifiedTerm)) (h_nodup : (entries.map (·.1)).Nodup) : VerifiedTerm :=
let rawEntries := entries.map (fun (s, v) => (s, v.val))
let t := Term.mk (.record rawEntries)
have h_wf : t.IsWF := by
-- 1. Unfold the main IsWF definition
rw [Term.IsWF]
-- 2. Prove TermF.IsLocalWF (.record rawEntries)
constructor
· simp [TermF.IsLocalWF]
-- Prove that keys of rawEntries are the same as keys of entries
have h_keys : (rawEntries.map (·.1)) = (entries.map (·.1)) := by
induction entries <;> simp_all
grind only [= List.map_nil]
rw [h_keys]
exact h_nodup
· -- 3. Prove Term.allWF rawEntries
induction entries with
| nil => grind only [= List.map_nil, Term.allWF]
| cons entry rest ih =>
-- Expand one step of Term.allWF
grind only [= List.map_cons, = List.nodup_cons, Term.allWF, usr Subtype.property]
⟨t, h_wf⟩
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment