Devices are graphs

Part E, lesson E1. You need Parts A-D of this tutorial: sites, junctions, rails, shuttles, gates and the rules, as the studio shows them. You do not need to know Lean; this lesson teaches the Lean it uses.

In the studio a device is a drawing: traps on rails, rails meeting at junctions. Underneath the drawing is a document, a list of nodes and a list of segments (the rails), and every tool on this site works from that document: the studio, the rules, the compiler, and, through facts read out of it, the proved checker of Part F. This lesson writes three of the site's devices as Lean data and computes from them what the rules and the checker read off a device: who is next to whom, how many rails meet at a node, which nodes are junctions, and which moves the machine allows.

Part E goes on the same way: programmes as data (E2), the rules as statements Lean can decide (E3), and rule sets (E4). Everything below runs in this page. Edit any of it.

1. A device document

Here is one node, one segment and one zone type of the device chain4, from its document (chain4.arch.json; ... marks fields left out):

{ "id": "C1", "pos": [1.0, 0.0], "kind": "site", "capacity": 2, "zone_type": "trap", ..., "degree": 2, ... }
{ "id": "E0", "ends": ["C0", "C1"], "length": 1.0, "capacity": 1, ... }
"zone_types": { "trap": { "capacity": 2, "gate": true, "spam": true, "cool": true, ... } }

A node's kind is site (a trap, where ions rest) or junction. Its capacity is how many ions it holds; a junction's entry gives none, which the platform reads as 0. Whether a site can gate is said by its zone type: trap has "gate": true. We keep four facts per node and two per segment.

An inductive type lists its values; Kind has exactly two. deriving DecidableEq, Repr asks Lean to write two things for us: a way to compare two kinds, and a way to print one.

A structure is a record: named fields, each with its type. String is text, Nat a whole number 0, 1, 2, ..., Bool is true or false.

A segment joins two nodes. String × String is the type of a pair of strings, written ("C0", "C1"); s.ends.1 and s.ends.2 are its two halves. List Node is a list of nodes, written [a, b, c].

2. Three devices

def gives a name to a value. ⟨"C0", .site, 2, true⟩ builds a Node from its fields in order (id, kind, capacity, gate); .site is short for Kind.site, since Lean knows the type it wants there. chain4 is four traps in a row, C0 - C1 - C2 - C3, each holding two ions and able to gate, joined by three segments.

grid2x3 is a lattice: six nodes its document calls junctions, J0_0 to J1_2, and seven traps, each on a rail between two of them (T0_1h lies between J0_1 and J1_1). Each trap has two segments, .a and .b, one to each of its junctions. The lists are in the document's order.

ring6d is a closed loop of six sites, S0 to S5, that cannot gate (their zone type is data, with "gate": false), and two docks that can: A0 off S0 and A3 off S3.

A function is a def with parameters. fun n => ... is a function written in place; filter keeps the elements of a list for which it says true, and map applies it to every element. == compares two values and answers a Bool. So sites d is the names of the nodes of d whose kind is site, in the document's order.

#eval runs an expression and shows the result. It proves nothing; it computes.

The page draws any value with two fields, arch (a device of the site) and src (a programme in the studio's language), in the studio. Lesson E2 is about programmes; here a programme only places ions, with one p.init statement. ionsAt k ns names one ion per node, q0, q1, ...; initSrc writes the statement. ("\"" is a string holding one double quote; ++ joins strings and lists.)

Here is chain4 with an ion in every site, computed from the definitions above: edit chain4 (drop a node) and the figure follows.

A theorem is a statement with a proof. rfl ("reflexivity") proves an equation whose two sides compute to the same thing; ∧ is "and", and ⟨p, q⟩ proves it from two proofs.

Exercise 1 ★ grid_size open

Prove that grid2x3 has 13 nodes and 14 segments.

3. Neighbours and degree

The rails at a node n: every segment with n at one end, paired with the node at its other end. flatMap maps each segment to a list (here of zero, one or two entries) and joins the lists. A node's neighbours are the other ends; its degree is how many rails meet at it. A rail from a node to itself would count twice, as it does in the platform's Device.degree (no device here has one).

The document records a "degree" for every node (C0 1, C1 2, J0_1 3, J0_0 2, S0 3); the values computed here agree with it, node for node, on all three devices.

For statements that compute with strings this lesson uses decide +kernel. It proves a statement by having Lean's kernel, the small trusted core that checks every proof, compute it to true. It is the strongest kind of proof by computation: the kernel is the only thing trusted.

Exercise 2 ★ c1_neighbours open

Prove that the neighbours of C1 on chain4 are C0 then C2.

4. Junctions are a matter of degree (R18)

Rule R18, as the platform's rule checker states it, says: "a node is a junction only if three or more trap axes meet at it". The rule language says it more bluntly: "Whatever a node is called, it is a junction exactly when three or more rails meet at it." The platform's device keeps its junctions that way, as the nodes of degree at least three, and the junction rule R2 and the cost of crossing a junction both read that degree, never the node's kind.

Both directions of R18 show here. grid2x3's document calls six nodes junctions, but at the four corners (J0_0, J0_2, J1_0, J1_2) only two rails meet: they are bends, crossed as plain transport. And ring6d's document calls S0 and S3 sites, but three rails meet at each (two of the loop and the dock's): they are junctions that are also traps.

Exercise 3 ★ junctions_by_degree open

Prove which nodes are junctions on grid2x3 and on ring6d.

The rest of this section is about every device, not one. { d with segments := s :: d.segments } is d with one more segment s in front of its list (:: puts an element in front of a list).

simp rewrites a goal with the definitions and facts you give it, and with a large set of facts it knows, until it is solved or stuck. omega proves statements of linear arithmetic about whole numbers (a ≤ b + a, and the like), whatever the numbers stand for.

Exercise 4 ★★ degree_more open

Prove that adding a segment never lowers the degree of a node. (simp [degree, railsAt] turns both degrees into sums; omega finishes.)

The platform's device module says why R18 is written this way: drawing a spur onto a rail makes the rail node degree 3, and it becomes a junction (that is how S0 and S3 became junctions on ring6d). Prove it, for every device.

Exercise 5 ★★ spur_makes_junction open

A node of degree 2 that gains a segment at one of its ends is a junction. (simp [isJunction, degree, railsAt, hs] at * and omega.)

5. Hops: what the checker is told about a device

Part F's checker decides whether a compiler's account of a programme holds. It never takes the compiler's word for what the machine can do: the moves a device allows, its hops, are read out of the device document by a short Python function, trap_hops, in the builder of the checker's device facts (mk_qcheck_input). A hop is an ordered pair of sites one machine cycle apart. In the function's own words: an ion never rests on a junction, so a hop leaves a trap, crosses only junctions, and lands on a trap — where a junction is what R18 says it is, a bare junction node or a site where three or more rails meet.

The function walks the rails out of every site. It may cross a node that is not a site (a bare junction, or a bend like J0_0) or a site where three or more rails meet; it never uses a rail twice; it crosses at most three nodes (max_transit = 3); and every site it reaches, other than the start, is a hop. Here is the same walk in Lean.

A function can be defined by pattern matching: one line per shape of its arguments. The first argument of walk is its fuel; | 0, _, _ => [] says that with no fuel left the walk finds nothing, and the second line handles fuel k + 1 and calls walk again with k. Lean accepts a function that calls itself only when it can see the calls end, as here, where the fuel goes down by one each time. used.contains seg asks whether a rail was used already; ! is "not", && "and", || "or".

A site reached by two routes is one hop: fresh keeps the first time each name appears, which is the order the Python function records them in. The walk starts with fuel 4: it looks along the rails of the start and of at most three crossed nodes, as the Python does, whose walk stops when depth > max_transit.

The Bell pair that lesson F1 proves was compiled for chain4, and its certificate carries the device's hops in the field hops. Here is that list, copied from the certificate (bell.qcheck.json, and bell in lesson F1).

Exercise 6 ★ chain4_hops open

Prove that the walk computes exactly the hops of the Bell certificate.

On grid2x3 every hop crosses a junction or a bend, and from T0_1h, which lies between the two real junctions, there are four. The figure puts q0 in T0_1h and one ion in each trap a hop away, computed by hopsFrom.

On ring6d the walk crosses sites: from the dock A3 it reaches S3 and, through S3, which is a junction, S2 and S4. The SWAP compiled for ring6d on the Compilation page uses exactly such a hop: its first move takes q1 from A3 to S4 in one cycle, through S3.

The published certificates of the CX on grid2x3 and the SWAP on ring6d carry these hop lists (cx.qcheck.json and swap.qcheck.json), copied here.

Exercise 7 ★ published_hops open

Prove that the walk computes exactly the hops of both published certificates. Those lists were written by the Python trap_hops, so this proves the Lean walk agrees with it on both devices.

6. Facts about every device

The theorems so far were about one device each. These two hold for every device there will ever be, and their proofs are about the definitions, not about any list.

∈ is membership in a list. A hypothesis h : m ∈ neighbours d n is a proof you may use; simp only [...] at * rewrites the goal and every hypothesis with exactly the facts listed (List.mem_map, List.mem_flatMap: what membership in a map and a flatMap means); obtain ⟨a, b⟩ := h takes a proof of "there is an a with b" apart; by_cases h : p splits the proof in two, with p and with ¬ p ("not p"); <;> runs the next tactic on every goal the last one left; simp_all simplifies everything with everything.

Exercise 8 ★★★ neighbours_symm open

A rail runs both ways: if m is a neighbour of n, then n is a neighbour of m. Hints: unfold neighbours and railsAt with simp only [neighbours, railsAt, List.mem_map, List.mem_flatMap] at *; h then says some segment s of d lists m as the other end of a rail at n; use the same s (refine ⟨(n, s.id), ⟨s, hs, ?_⟩, rfl⟩), and finish by cases on which end of s is n.

The checker relies on every hop going from a site to a different site. That is a fact about walk, for any fuel: whatever it reports is a site and is not where it started. A statement about every amount of fuel is proved by induction: prove it for fuel 0, then prove it for fuel k + 1 assuming it for k (the assumption is called ih). split at hx splits a proof on the if inside the hypothesis hx, one goal per branch.

Exercise 9 ★★★ walk_sites open

Prove it. Hints: intro fuel; induction fuel with | zero => ... | succ k ih => ...; at fuel 0 the walk is empty (simp [walk] at hx); at k + 1, unfold one step of walk and List.mem_flatMap, take the rail apart, and follow split at hx through the three ifs: a reported r.1 comes with isSite d r.1 && r.1 != src, and a name from deeper in the walk is ih's business.

7. What comes next

A device is now a value you can compute with and prove things about. Lesson E2 does the same for programmes: the studio's statements as Lean data, and the replay that says where every ion is after every step. Lesson E3 then states the rules of Part R as propositions about that replay, and has Lean decide them.