Skip to content

Reuse a proof by identity

Prove a new theorem by citing an accepted one through bindings, then point the same source at a second implementation.

By the end of this tutorial your store will hold two theorems built from one source file: one about implA, and one about a second implementation, implB. Both use the accepted twice_id by its ID, and neither proves it again.

You need:

  • Publish your first proof done: twice_id, implA and implA_law accepted, and their aliases saved in ~/lema-tutorial/found.json;
  • the server running on $SOCK;
  • a terminal at the root of your checkout, with ~/.lema/env and ~/lema-tutorial/env loaded.

Read the new theorem

lean/examples/reuse/Parametric.lean
set_option autoImplicit false
namespace LemaDraft
namespace Reuse

theorem par_twice : ∀ x, Received.f (Received.f x) = x :=
  Received.twice_id Received.f Received.f_law

end Reuse
end LemaDraft

The source uses Received.twice_id, Received.f and Received.f_law but never defines them. Your request will bind each of these names to an accepted object, by its ID. The server installs those objects from the store, and each Received.* name then stands for the stored declaration itself, not a copy.

The proof applies twice_id to f and its law. It uses nothing about the body of f, so the same text works for any implementation that comes with the law.

Bind it to implA

Build the request from the IDs that you saved with find in the last tutorial. The bindings field maps each Received.* name to an ID. (--slurpfile reads found.json as an array, hence $found[0].)

Shell
jq -n --rawfile source lean/examples/reuse/Parametric.lean \
  --slurpfile found ~/lema-tutorial/found.json '$found[0] as $f | {
  source: $source,
  prefix: "LemaDraft",
  bindings: {
    "Received.twice_id": {id: $f["LemaDraft.Reuse.twice_id"].id},
    "Received.f": {id: $f["LemaDraft.Reuse.implA"].id},
    "Received.f_law": {id: $f["LemaDraft.Reuse.implA_law"].id}
  },
  aliases: {"LemaDraft.Reuse.par_twice": {expect: null}}
}' > ~/lema-tutorial/par-a.json
jq .bindings ~/lema-tutorial/par-a.json
Output
{
  "Received.twice_id": {
    "id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"
  },
  "Received.f": {
    "id": "04527d69167ff540b7d50f8af18411221932906bc87d292ac9cd7a6541e5ec1c"
  },
  "Received.f_law": {
    "id": "3f1c38da391932e571280fff4f0266471abd03b6fb4251eba060668c22909167"
  }
}

The server checks every binding before it makes any native call: each target must be an object this store has accepted.

Publish and see what is new

Publish the request and save the answer, since you will need the new ID:

Shell
lema --socket $SOCK call publish --params-file ~/lema-tutorial/par-a.json > ~/lema-tutorial/par-a-published.json
jq '{names, stored}' ~/lema-tutorial/par-a-published.json
Output
{
  "names": {
    "LemaDraft.Reuse.par_twice": {
      "id": "b28938636f8618bdedb9d4e51654bce4e9452f18533ebd246f0367e8bcefcbff"
    }
  },
  "stored": 5
}

The store wrote five new objects: the new theorem’s statement, template, proof, satisfaction and declaration. The draft held none of the objects of twice_id, implA or implA_law, because a draft never repeats what it receives. Kernel replay checked one declaration, par_twice, with the pinned Lean 4.34.1 kernel. The Lean module it was checked in imports the modules that already hold the three received declarations.

See which declarations it uses

The new theorem’s satisfaction records which declarations it uses. The satisfaction’s ID is the declaration’s binding, so read that first:

Shell
lema --socket $SOCK call show --params '{"id": "b28938636f8618bdedb9d4e51654bce4e9452f18533ebd246f0367e8bcefcbff"}' | jq -r .object.binding
Output
f79ddde898c0938cafbb0ddc07837574c1afcec862d29ab6afd3781edb5bbd0d

Then show the satisfaction’s realizations:

Shell
lema --socket $SOCK call show --params '{"id": "f79ddde898c0938cafbb0ddc07837574c1afcec862d29ab6afd3781edb5bbd0d"}' | jq .object.realizations
Output
[
  {
    "declaration": "04527d69167ff540b7d50f8af18411221932906bc87d292ac9cd7a6541e5ec1c",
    "of": "00c081105265b84f5b4cd009dcce10fb0e2f71f0594fc7a7943ecbbb71814d53"
  },
  {
    "declaration": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc",
    "of": "07d8af57d41afa499cbca43fe58da14ec7c75389263148d91543967c3707097a"
  },
  {
    "declaration": "3f1c38da391932e571280fff4f0266471abd03b6fb4251eba060668c22909167",
    "of": "72b9342dc5a08579b5b4aa10276e6310e9261dfc34b448fca0475e8b3a7e7c87"
  }
]

Objects never cite a declaration directly. A statement, template or proof cites a definition by its template and a theorem by its statement. Each realization then says which declaration one citation means: of is the cited object, and declaration is the declaration it resolves to. Here the new theorem cites implA by its template, and twice_id and implA_law by their statements (#07d8…097a is the statement of twice_id you saw in the last tutorial). The three declarations are the ones you published there, by ID.

Publish a second implementation

lean/examples/reuse/ImplB.lean
set_option autoImplicit false
namespace LemaDraft
namespace Reuse

def implB : Nat → Nat := fun x => 0 + x

theorem implB_law : ∀ x, implB x = x := fun x => Nat.zero_add x

end Reuse
end LemaDraft

implB has a different body and the same law. 0 + x does not reduce to x when x is a variable, so the law needs a real proof, Nat.zero_add. Publish it, then save found.json again so that it includes the new aliases:

Shell
jq -n --rawfile source lean/examples/reuse/ImplB.lean '{
  source: $source,
  prefix: "LemaDraft",
  aliases: {
    "LemaDraft.Reuse.implB": {expect: null},
    "LemaDraft.Reuse.implB_law": {expect: null}
  }
}' > ~/lema-tutorial/impl-b.json
lema --socket $SOCK call publish --params-file ~/lema-tutorial/impl-b.json | jq .names
lema --socket $SOCK call find --params '{"prefix": "LemaDraft.Reuse."}' > ~/lema-tutorial/found.json
Output
{
  "LemaDraft.Reuse.implB": {
    "id": "ef20c6e6b2e2db5517ff27a429e67a688ae3036e965a781f9a110ac8bb612658"
  },
  "LemaDraft.Reuse.implB_law": {
    "id": "c12172915e599fe70b908278e6e6c376b836b0de470d0ff411af71e7d9b276fd"
  }
}

Bind the same source to implB

Make the second request from the first. Change only the bindings of Received.f and Received.f_law, and keep the source as it is. Drop the alias as well: LemaDraft.Reuse.par_twice already names the first theorem, so expect: null would be refused.

Shell
jq --slurpfile found ~/lema-tutorial/found.json '$found[0] as $f
  | .bindings["Received.f"].id = $f["LemaDraft.Reuse.implB"].id
  | .bindings["Received.f_law"].id = $f["LemaDraft.Reuse.implB_law"].id
  | del(.aliases)' ~/lema-tutorial/par-a.json > ~/lema-tutorial/par-b.json
lema --socket $SOCK call publish --params-file ~/lema-tutorial/par-b.json > ~/lema-tutorial/par-b-published.json
jq '{names, stored}' ~/lema-tutorial/par-b-published.json
Output
{
  "names": {
    "LemaDraft.Reuse.par_twice": {
      "id": "099fdcb4c82f03fb1f2405aa3976f5a09fe18345973924e21d93f87a6c28096a"
    }
  },
  "stored": 5
}

The same source now gives a theorem with another ID. The dependents method lists the stored objects that link to an ID. Ask it about twice_id:

Shell
lema --socket $SOCK call dependents --params '{"id": "c6535c1bba1f55f46b635aa85bba04cb42d1f728745b9b16c8cfe3908512e8dc"}'
Output
["d8c20ba40aeccbd5bf9cd084809d88bc2d74c3222360c8b8daead49523ad9c42","f79ddde898c0938cafbb0ddc07837574c1afcec862d29ab6afd3781edb5bbd0d"]

The two objects are the satisfactions of the two par_twice theorems. Both point at the one accepted twice_id, which was proved and checked once, in the last tutorial.

Compare the two theorems

Render both theorems with view. The alias LemaDraft.Reuse.par_twice still names the first one, so for the second you pass the name together with its ID, taken from its publish result:

Shell
lema --socket $SOCK call view --params '{"render": ["LemaDraft.Reuse.par_twice"]}' | jq -r '.[].text'
jq '{render: ["LemaDraft.Reuse.par_twice"], names: .names}' ~/lema-tutorial/par-b-published.json > ~/lema-tutorial/view-b.json
lema --socket $SOCK call view --params-file ~/lema-tutorial/view-b.json | jq -r '.[].text'
Output
law Reuse.par_twice (x : Nat) :
  (Reuse.implA (Reuse.implA x)) = x
law Reuse.par_twice (x : Nat) :
  (Reuse.implB (Reuse.implB x)) = x

The second theorem is about implB, so its statement, template, proof and satisfaction are all new objects. What carried over is twice_id: changing the implementation took new bindings, not a new proof. The alias still names the first theorem, because nothing moves an alias by itself. Move an alias safely shows how to move one.

Try a proof that depends on the body

lean/examples/reuse/Concrete.lean proves the same kind of statement another way, by unfolding the body of f:

lean/examples/reuse/Concrete.lean (the theorem)
theorem con_twice : ∀ x, Received.f (Received.f x) = x := fun _ => rfl

With implA, f (f x) reduces to x, so rfl holds. Bind it to implB instead and send it to the elaborate method, which runs only the first step of publish:

Shell
jq -n --rawfile source lean/examples/reuse/Concrete.lean \
  --slurpfile found ~/lema-tutorial/found.json '{
  source: $source,
  prefix: "LemaDraft",
  bindings: {"Received.f": {id: $found[0]["LemaDraft.Reuse.implB"].id}}
}' > ~/lema-tutorial/concrete-b.json
lema --socket $SOCK call elaborate --params-file ~/lema-tutorial/concrete-b.json
Output (shortened)
lema: export failed (exit Some(1)): …

The message goes on with Lean’s log, which reports a Type mismatch: rfl cannot prove implB (implB x) = x, because 0 + (0 + x) does not reduce to x. In the log, implB appears under its stored kernel name, LemaStored.h followed by its ID. No draft was made and nothing was stored. A proof that relies on a body has to be written again for each body, while the one through twice_id did not. Contracts, implementations and proofs explains why Lema is built around that difference.

Next

Go on to build and run a program from accepted code.

Written against lema-lang at commit 5a94951, 17 Oct 2026.