Publish your first proof

Publish a generic theorem and an implementation with its law, then read back what the store accepted.

By the end of this tutorial your store will hold three accepted declarations, each with an alias: a theorem, twice_id, a function, implA, and a theorem about that function, implA_law. You will also look at what the store recorded for them.

You need:

• Start a store and a server done, with the server still running on $SOCK;
• a terminal at the root of your lema-lang checkout, with ~/.lema/env and ~/lema-tutorial/env loaded.

Read the theorem

The example files are in lean/examples/reuse/. Here is the first one, without its header comment:

set_option autoImplicit false
namespace LemaDraft
namespace Reuse

/-- An `f` that is the identity pointwise is the identity twice over. -/
theorem twice_id : ∀ (f : Nat → Nat), (∀ x, f x = x) → ∀ x, f (f x) = x :=
  fun f law x => (congrArg f (law x)).trans (law x)

end Reuse
end LemaDraft

It says: take any function f on natural numbers that obeys the law ∀ x, f x = x. Then applying f twice also gives back x. The proof is a term: congrArg f (law x) shows f (f x) = f x, and .trans (law x) chains that with f x = x.

This is restricted Lean, the subset of Lean the server accepts. The source imports nothing, because the server writes the header, and everything sits under namespace LemaDraft. Restricted Lean lists the rules.

Write the publish request

The publish method takes its parameters as a JSON object. Build them with jq, which puts the file’s exact text in source:

jq -n --rawfile source lean/examples/reuse/Generic.lean '{
  source: $source,
  prefix: "LemaDraft",
  aliases: {"LemaDraft.Reuse.twice_id": {expect: null}}
}' > ~/lema-tutorial/generic.json

• source is the Lean text.
• prefix says which constants become objects: every one under LemaDraft.
• aliases lists the names that should get an alias in the store, each with what you expect the alias to hold now. expect: null means the alias must not exist yet. If an expectation is missing or out of date, the server refuses the request before it makes any native call.

Publish it

Send the request:

lema --socket $SOCK call publish --params-file ~/lema-tutorial/generic.json | jq .

{
  "aliases": {
    "LemaDraft.Reuse.twice_id": {
      "changed": true,
      "generation": 1,
      "id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"
    }
  },
  "names": {
    "LemaDraft.Reuse.twice_id": {
      "id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"
    }
  },
  "receipts": 5,
  "roots": [
    "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"
  ],
  "stored": 9
}

publish did two things inside the server:

1. It elaborated the source. The pinned lean ran it in the sandbox, and Lema turned each constant under the prefix into canonical objects. The result is a draft, which nothing trusts yet.
2. It submitted the draft. In kernel replay, the decoder module from the last tutorial turned the objects back into Lean declarations, and the pinned Lean 4.34.1 kernel added each one, without the source text. The kernel accepted them, so the store saved the objects, wrote a receipt for each declaration and created the alias.

So twice_id is now checked: the kernel accepted it within the store’s axiom policy. stored is 9. The theorem itself is five objects, and four more are external objects for the Lean constants it uses: Nat, Eq, congrArg and Eq.trans. receipts is 5, one for the theorem and one for each external this replay checked. The alias starts at generation 1.

Nothing reaches the store unless both steps pass. If a proof does not prove its statement, elaboration fails with Lean’s own error and no draft is made; you will see that happen in the next tutorial. If the kernel refuses a draft, the whole submission is refused: no object is stored and no alias moves. How acceptance works explains both steps.

Publish the implementation and its law

The second file defines a function and proves that it obeys the same law:

set_option autoImplicit false
namespace LemaDraft
namespace Reuse

def implA : Nat → Nat := fun x => x

theorem implA_law : ∀ x, implA x = x := fun _ => rfl

end Reuse
end LemaDraft

implA is an implementation of the law ∀ x, f x = x, and implA_law is the proof that it obeys it. Publish both, with an alias for each:

jq -n --rawfile source lean/examples/reuse/ImplA.lean '{
  source: $source,
  prefix: "LemaDraft",
  aliases: {
    "LemaDraft.Reuse.implA": {expect: null},
    "LemaDraft.Reuse.implA_law": {expect: null}
  }
}' > ~/lema-tutorial/impl-a.json
lema --socket $SOCK call publish --params-file ~/lema-tutorial/impl-a.json | jq '{names, stored}'

{
  "names": {
    "LemaDraft.Reuse.implA": {
      "id": "04527d69167ff540b7d50f8af18411221932906bc87d292ac9cd7a6541e5ec1c"
    },
    "LemaDraft.Reuse.implA_law": {
      "id": "3f1c38da391932e571280fff4f0266471abd03b6fb4251eba060668c22909167"
    }
  },
  "stored": 10
}

The draft held twelve objects, but the store wrote ten. Nat and Eq were already there from the first publication. The same content always has the same ID, so it is stored once.

Find them by name

The find method lists the aliases that start with a prefix. Save its answer, because the next tutorial reads the IDs from it:

lema --socket $SOCK call find --params '{"prefix": "LemaDraft.Reuse."}' > ~/lema-tutorial/found.json
jq . ~/lema-tutorial/found.json

{
  "LemaDraft.Reuse.implA": {
    "generation": 1,
    "id": "04527d69167ff540b7d50f8af18411221932906bc87d292ac9cd7a6541e5ec1c"
  },
  "LemaDraft.Reuse.implA_law": {
    "generation": 1,
    "id": "3f1c38da391932e571280fff4f0266471abd03b6fb4251eba060668c22909167"
  },
  "LemaDraft.Reuse.twice_id": {
    "generation": 1,
    "id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"
  }
}

Your IDs are the same as the ones shown here. An ID is the SHA-256 of the object’s canonical form, so the same source under the same pinned Lean gives the same objects on every machine. Code stored by identity explains what follows from that.

Look inside the declaration

The show method returns one stored object with its receipt and names. Ask for twice_id by its ID, and save the answer:

lema --socket $SOCK call show --params '{"id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"}' > ~/lema-tutorial/twice_id.json
jq .object ~/lema-tutorial/twice_id.json

{
  "binding": "a6553280b13f5f396decc471d6e955037c60fc488b9d2cdbb9d68751ce5670a9",
  "flavor": "theorem",
  "hints": null,
  "kind": "declaration",
  "namespace": "4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a",
  "proofs": [
    "32f786cce2d57a1f6b1d2f9f0983ec7ba8335eab7bd602b45b6d6376590f9f29"
  ],
  "schema": "lema.core/v3",
  "statement": "07d8af57d41afa499cbca43fe58da14ec7c75389263148d91543967c3707097a",
  "template": "9500cf36ed781f1c9a5e0dce7083429b22c069a864c4f1f695295e76a59d6751"
}

The declaration is one of the five objects that make up the theorem, and its fields name the other four:

Objects and identity describes every kind of object.

Now read the rest of the show answer, the receipt and the names:

jq '.receipt.axioms, .names' ~/lema-tutorial/twice_id.json

[]
[
  "LemaDraft.Reuse.twice_id"
]

The receipt is this store’s record that the kernel accepted the declaration. It names the checker (the Lean version, the distribution and the host pins), the call that replayed it, the module it is installed in, the time, and the axioms the declaration depends on. twice_id depends on none, so the list is empty.

Render it

The view method prints stored declarations in the contract syntax, a small subset of Lean’s term syntax:

lema --socket $SOCK call view --params '{"render": ["LemaDraft.Reuse.implA", "LemaDraft.Reuse.implA_law", "LemaDraft.Reuse.twice_id"]}' | jq -r '.[].text'

def Reuse.implA :
  Nat → Nat :=
  fun (x : Nat) => x
law Reuse.implA_law (x : Nat) :
  (Reuse.implA x) = x
law Reuse.twice_id (x : Nat → Nat) (h : ∀ (y : Nat), (x y) = y) (y : Nat) :
  (x (x y)) = y

In this syntax a theorem appears as a law, which shows its statement only. The proof is not shown; the receipt records that the kernel accepted it. The renderer drops the LemaDraft. prefix and makes up the binder names (x, h, y), because binder names are not part of any object. Each result also lists what every name in the text refers to: a stored object by its ID, or a Lean constant by its Lean name. view does not check what it prints; the project’s round-trip tests do, by parsing the text back to the same objects. Contract syntax has the full grammar.

Next

Keep the server running and reuse twice_id by its identity.