Skip to content

Example Walkthrough

This walkthrough shows how to use a combination of DAMF-aware edge systems to verify and subsequently publish the following assertion:

Theorem. For \(n \in \mathbb{N}\), \(\kop{fib}(n) = n^2\) if and only if \(n \in \{0, 1, 12\}\), where \(\kop{fib}(n)\) stands for the \(n\)th Fibonacci number defined as: \(\kop{fib}(0) \triangleq 0\), \(\kop{fib}(1) \triangleq 1\), and \(\kop{fib}(n + 2) \triangleq \kop{fib}(n + 1) + \kop{fib}(n)\).

In the if direction, the assertion is fairly easy to prove in any system that can support inductive definitions such as \(\kop{fib}\) in the first place: one just has to compute \(\kop{fib}(0)\), \(\kop{fib}(1)\), and \(\kop{fib}(12)\) and verify that they are indeed \(0\), \(1\), and \(144\), respectively. The only if direction, on the other hand, requires the ability to reason about the growth of the Fibonacci function with respect to the quadratic function \(n \mapsto n^2\). In particular, one needs the following lemma:

Lemma. For \(n \in \mathbb{N}\), if \(n \ge 13\), then \(\kop{fib}(n) > n^2\).

This walkthrough will perform this verification task using the following heterogeneous collection of systems:

  • Abella DAMF for the overall theorem
  • Coq to prove the lemma
  • λProlog to illustrate how to incorporate logic programming

Setup

1. Local IPFS client

DAMF is built on top of IPFS and IPLD, so you will need an IPFS client. For this walkthrough we will use the Dispatch intermediary, which requires the Kubo desktop program accessed via the command ipfs.

You will also need to create your local IPFS repository, usually stored under $HOME/.ipfs or a similar folder. This is done by issuing the following command: ipfs init.

$ ipfs init
generating ED25519 keypair...done
peer identity: 12D3KooWNEsJFEp4FM14o9zedmFpBohUA4jPH77WYex75YP6mNHk
initializing IPFS node at /home/ExampleUser/.ipfs
to get started, enter:

    ipfs cat /ipfs/QmQPeNsJPyVWPFDVHb77w8G42Fvo15z4bG2X8D2GhfbSXc/readme

IPFS Daemon

Running the IPFS daemon is optional for this walkthrough. You only need the daemon if you want to disseminate the assertions you publish into the IPFS network so that other people may use them. If you leave the daemon off, you will only be able to share assertions between programs that can access your local IPFS repository.

2. Dispatch, agent profile

In DAMF, all assertions are signed by exactly one agent. Concretely, an agent is a public-private key pair; the name of the agent is just its public key.

The Dispatch intermediate tool can be used to create an agent profile, which is just a human-readable string that stands for an agent. Agent profile names are not globally shared using IPFS. Indeed, DAMF is completely unaware of agent profiles.

In this walkthrough, we will create an agent profile called exampleAgent. Install Dispatch by following the instructions. In the rest of this tutorial, we will use the command dispatch to stand for whichever Dispatch executable is relevant to your system. Next, run dispatch create-agent.

$ dispatch create-agent exampleAgent
Agent profile exampleAgent created successfully!

$ dispatch list-config | grep exampleAgent # (1)!
  exampleAgent: {
    name: 'exampleAgent',
  1. Just to verify that it worked.

Lemma in Coq

In order to follow along with this walkthrough, you should install Coq version 8.16.1.

3. Full proof

We begin with a traditional (autarkic) mode of usage of Coq, unmodified, without any connection to DAMF assertions.

As usual, we begin with importing the Arith module to fix the interpretation of numerals using the nat type, and then capture \(\kop{fib}\) as the recursive fixed point function fib.

FibLemma.v
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
Require Import Arith.

Fixpoint fib (n: nat): nat :=
  match n with
  | 0 => 0
  | S j =>
      match j with
      | 0 => 1
      | S k => fib j + fib k
      end
  end.

We will prove our lemma of interest using the lia tactic of Coq, which is enabled by the Lia module. We will also pervasively use rewriting modulo linear arithmetic identities, so we define a Ltac named liarw for convenience.

FibLemma.v
12
13
14
15
16
Require Import Lia.

Ltac liarw F :=
  let h := fresh "H" in
  assert (h: F) by (simpl; lia); rewrite h in *; clear h.

Finally, here is our full proof of the lemma, which is named fib_square_above here. This lemma itself makes use of a different lemma called fib_square_lemma.

FibLemma.v
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
Lemma fib_square_lemma: forall n, 2 * n + 27 <= fib (n + 12).
Proof.
  induction n.
  - simpl; lia.
  - liarw (n + 12 = S (n + 11)).
    liarw (S n + 12 = S (S (n + 11))).
    assert (Hl: 2 <= fib (n + 11)).
      clear IHn; induction n; [simpl; lia | ].
      liarw (n + 11 = S (n + 10)).
      liarw (S n + 11 = S (S (n + 10))).
      assert (H: fib (S (S (n + 10)))
                 = fib (S (n + 10)) + fib (n + 10)) by auto.
      lia.
    assert (fib (S (S (n + 11)))
            = fib (S (n + 11)) + fib (n + 11)) by auto.
    lia.
Qed.

Theorem fib_square_above: forall n, 13 <= n -> n ^ 2 < fib n.
Proof.
  intros n Hle; pose (k := n - 13); liarw (n = k + 13); clear Hle.
  induction k.
  - simpl; lia.
  - liarw (k + 13 = S (k + 12)).
    liarw (S k + 13 = S (S (k + 12))).
    assert (fib (S (S (k + 12)))
            = fib (S (k + 12)) + fib (k + 12)) by auto.
    liarw (S (S (k + 12)) ^ 2
           = S (k + 12) ^ 2 + 2 * k + 27).
    specialize (fib_square_lemma k).
    lia.
Qed.

4. Language and Tool objects

Let’s move on to representng fib_square_lemma and fib_square_above as DAMF assertions.

To get there, we first have to turn Coq propositions into DAMF formula objects, for which we will need to supply a suitable language field. As there isn’t (yet!) a universally agreed upon DAMF object to represent this language, we will create one for the purposes of this walkthrough.

We start by creating a JSON object to represent the content of what a “Coq version 8.16.1” language object might contain. Here we could in principle link to the reference manual that is distributed as part of the Coq 8.16.1 release. We could alternatively, or in addition, place the source or exceutable code of a Coq parser. In this walkthrough, to simplify matters, we will represent this language as the following JSON object that just links to the Coq website.

Coq.language.content.json
1
2
3
4
5
{
  "name": "Coq",
  "version": "8.16.1",
  "url": "https://coq.inria.fr"
}

We can then use dispatch create-language to make the DAMF language object and simultaneously give it a local human-readable name, coq-8.16.1.

$ dispatch create-language coq-8.16.1 json Coq.language.content.json
Language record coq-8.16.1 created successfully!

If we want to see the DAMF object that was created by Dispatch, we can read its languages.json configuration file to get its CID, and then use ipfs dag get to explore the contents of the linked objects in IPLD starting from that CID.

$ cat $HOME/.config/dispatch/languages.json
{"coq-8.16.1":{"name":"coq-8.16.1","language":"bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy"}}

$ ipfs dag get bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy # (1)!
{"content":{"/":"bafyreidmf3nxeigvi7mfklzu2wr7oapa7fodqdeajbxtngy5ax7cccmj5u"},"format":"language"}

$ ipfs dag get bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy/content # (2)!
{"name":"Coq","url":"https://coq.inria.fr","version":"8.16.1"}
  1. This is the CID found in languages.json.
  2. This is isomorphic to our Coq.language.content.json object.

We can record that we used Coq v.8.16.1 to verify our proofs of the assertions by referencing a DAMF tool object in the mode field of the corresponding production. Like with the language object above, there isn’t currently a standard DAMF tool object to represent this version of the Coq implementation. Therefore, like with languages above, we will create the content of such a tool object ourselves for the purposes of this walkthrough.

coq-8.16.1.tool.content.json
1
2
3
4
5
6
{
  "name": "Coq",
  "version": "8.16.1",
  "url": "https://github.com/coq/coq/archive/refs/tags/V8.16.1.tar.gz",
  "sha256": "583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b"
}

To create the DAMF tool object, we use dispatch create-tool.

$ dispatch create-tool coq-8.16.1 json coq-8.16.1.tool.content.json
Tool profile coq-8.16.1 created successfully!

5. The DAMF assertions

There is currently no software that can transform the theorems we have just proved in Coq into DAMF assertions. We will do this manually. To cause the least breakage, we will reuse the text of the Coq development as much as possible.

Consider the first lemma, fib_square_lemma. The formula content of this lemma is the string "forall n, 2 * n + 27 <= fib (n + 12)". This string, however, only makes sense in a context where the symbols *, +, <=, fib, etc. are defined. These symbols come from the Coq standard prelude with some additional support from the Arith module, except fib which we defined ourselves. Thus, the DAMF context object for this formula can be built with the following input for Dispatch:

1
2
3
4
5
6
7
8
{
  "format": "context",
  "language": "coq-8.16.1", // (1)!
  "content": [
    "Require Arith",
    "Fixpoint fib (n: nat): nat := match … end" // (2)!
  ]
}
  1. This is the local name we picked using dispatch create-language in step 4.
  2. Lines 3–11 of FibLemma.v.

In order to build the assertion that corresponds to fib_square_lemma, Dispatch expects the formulas and contexts to be laid out using local names. Here, we can use the name fib_square_lemma as the local name of the formula, and fib_square_lemma!context as the local name of its context. Then, in the production underlying the assertion we use the local name coq-8.16.1 for the mode field, which is the local name of the DAMF tool object we created in step 4. The complete assertion is as follows, again as a Dispatch input.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
{
  "format": "assertion",
  "agent": "exampleAgent", // (1)!
  "claim": {
    "format": "annotated-production",
    "annotation": { "name": "fib_square_lemma" }, // (2)!
    "production": {
      "mode": "coq-8.16.1", // (3)!
      "sequent": {
        "conclusion": "fib_square_lemma", // (4)!
        "dependencies": [ ]
      }
    }
  },
  "formulas": {
    "fib_square_lemma": {
      "language": "coq-8.16.1",
      "context": "fib_square_lemma!context", // (5)!
      "content": "forall n, 2 * n + 27 <= fib (n + 12)"
    }
  },
  "contexts": {
    "fib_square_lemma!context": {
      "language": "coq-8.16.1",
      "content": [
        "Require Arith",
        "Fixpoint fib (n: nat): nat := match … end"
      ]
    }
  }
}
  1. We made this with dispatch create-agent in step 2.
  2. This defines a possible name for the assertion, but it only serves as a hint for consumers. The actual global name is the CID of the DAMF assertion object that Dispatch will create. This annotation object can have other metadata besides this name himt, such as the Coq proof script. Its structure is not prescribed by DAMF.
  3. This is the local name we picked using dispatch create-tool in step 4.
  4. This points to the formula object defined in the "formulas" section below (lines 16–20).
  5. This points to the context object defined in the "contexts" section below (lines 23–29).

We can of course ask Dispatch to publish only this assertion. However, since we have two assertions in this file, it is more convenient for Dispatch to publish both assertions together as a DAMF collection. Here is what it looks like:

FibLemma.v.assertions.json
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
{
  "format": "collection",
  "name": "FibLemma.v",
  "elements": [
    {
      "format": "assertion",
      "element": {
        "agent": "exampleAgent",
        "claim": {
          "format": "annotated-production",
          "annotation": { "name": "fib_square_lemma" },
          "production": {
            "mode": "coq-8.16.1",
            "sequent": {
              "conclusion": "fib_square_lemma",
              "dependencies": [ ]
            }
          }
        }
      }
    },
    {
      "format": "assertion",
      "element": {
        "agent": "exampleAgent",
        "claim": {
          "format": "annotated-production",
          "annotation": { "name": "fib_square_above" },
          "production": {
            "mode": "coq-8.16.1",
            "sequent": {
              "conclusion": "fib_square_above",
              "dependencies": [ "fib_square_lemma" ]
            }
          }
        }
      }
    }
  ],
  "formulas": {
    "fib_square_lemma": {
      "language": "coq-8.16.1",
      "context": [ "fib_square!context" ],
      "content": "forall n, 2 * n + 27 <= fib (n + 12)"
    },
    "fib_square_above": {
      "language": "coq-8.16.1",
      "context": [ "fib_square!context" ],
      "content": "forall n, 13 <= n -> n ^ 2 < fib n"
    }
  },
  "contexts": {
    "fib_square!context": {
      "language": "coq-8.16.1",
      "content": [
        "Require Import Arith",
        "Fixpoint fib (n: nat): nat := match n with | 0 => 0 | S j => match j with | 0 => 1 | S k => fib j + fib k end end"
      ]
    }
  }
}

We can now use Dispatch to publish the entire collection at once.

$ dispatch publish FibLemma.v.assertions.json local # (1)!
Published DAMF collection object to local with cid: bafyreigdthmeok6gwsdulovqrgvzz4tbad2ifjxpa74dlpbfbt7ehnkyha
  1. local means that it is being published to the local IPFS repository we set up in step 1.

This CID can be explored in IPLD explorer. It can also be locally explored with ipfs dag get:

$ ipfs dag get bafyreigdthmeok6gwsdulovqrgvzz4tbad2ifjxpa74dlpbfbt7ehnkyha | python -m json.tool # (1)!
{
    "elements": [
        {
            "/": "bafyreicpwpxl3xe4nefsqc3f2rdxiedxjbmekh25m5cgqkriwp3qsivope"
        },
        {
            "/": "bafyreigscd65tb2rabcpjxbep7h4lklbyfenmj32ioond7ouhh7qpvkh7a"
        }
    ],
    "format": "collection",
    "name": "FibLemma.v"
}

$ ipfs dag get bafyreic53degjxdfn7e2l3spleevftr5pxemr7ydspkvwimr4smhjqjzuy/elements/0/claim/production/sequent/conclusion/content
"forall n, 2 * n + 27 <= fib (n + 12)"
  1. python -m json.tool is being used to pretty-print the JSON

Computations with λProlog

Another way of building assertions is by means of a computational engine. Here we will give the example of using λProlog to perform computations on natural numbers. Coq is of course more than capable of doing these computations by itself, so the purpose of this section is mainly to illustrate how we can incorporate assertions from different sources.

6. Logic programming

Like with Coq earlier, let us quickly sketch how we are going to represent and compute with natural numbers in λProlog. We declare nat as a new type with the kind keyword in the signature, then declare two constants z and s as the constructors of nat. Note that λProlog operates under the open world assumption, so there is no way to declare that these are the only two constructors for nat. The signature also declares three predicates, which are constants with target type o, which is the type of λProlog formulas. Here are the signature (fib.sig) and module (fib.mod) files.

fib.sig
1
2
3
4
5
6
7
sig fib.
kind nat    type.
type z      nat.
type s      nat -> nat.
type plus   nat -> nat -> nat -> o.
type times  nat -> nat -> nat -> o.
type fib    nat -> nat -> o.
fib.mod
1
2
3
4
5
6
7
8
module fib.
plus z X X.
plus (s X) Y (s Z) :- plus X Y Z.
times z X z.
times (s X) Y Z :- times X Y U, plus Y U Z.
fib z z.
fib (s z) (s z).
fib (s (s X)) Y :- fib (s X) U, fib X V, plus U V Y.

We will use the Teyjus implementation of λProlog, which compiles a module (a .sig/.mod pair) to bytecode that can be executed using a bytecode interpreter. To compile the above module fib, we run:

$ tjcc fib && tjlink fib

Then, we can execute queries against fib by using tjsim.

$ tjsim fib
Welcome to Teyjus
⋮
[fib] ?- fib (s (s (s (s (s (s z)))))) X.

The answer substitution:
X = s (s (s (s (s (s (s (s z)))))))

More solutions (y/n)? n

yes

[fib] ?-

It is also possible to run tjsim in batch (non-interactive) mode, where the query is specified in the command line.

$ tjsim -b -m 1 -s 'fib (s (s (s (s (s (s z)))))) X.' fib # (1)!

The answer substitution:
X = s (s (s (s (s (s (s (s z)))))))
  1. batch mode, maximum one solution, solve query

7. Exporting to DAMF

We use the following language and tool descriptions for λProlog and Teyjus (version 2.1.1):

lprolog.language.content.json
1
2
3
4
{
  "name": "λProlog",
  "url": "https://www.lix.polytechnique.fr/~dale/lProlog/"
}
teyjus-2.1.1.tool.content.json
1
2
3
4
5
6
{
  "name": "Teyjus",
  "version": "2.1.1",
  "url": "https://github.com/teyjus/teyjus/archive/refs/tags/v2.1.1.tar.gz",
  "sha256": "a8fafe8ab7cd857a3f46ab8e4a7f76f9f3fac2169fdb72f95b84d1d0bcdf66f9"
}

$ dispatch create-language lprolog json lprolog.language.content.json
Language record lprolog created successfully!

$ dispatch create-tool teyjus-2.1.1 json teyjus-2.1.1.tool.content.json
Tool profile teyjus-2.1.1 created successfully!

To build the DAMF assertions, we can use the following harness module: harness.sig and harness.mod. The purpose of the harness module is to turn a sequence of goals for a module FILE, written in a file FILE.goals, into a JSON file FILE.json that can be given to dispatch publish. Note that the agent, language, and tool names that we chose with dispath create-agent, dispatch create-language, and dispatch create-tool respectively, are directly written in the harness module.

To use the harness, we define a module main that accumulates and compiles the fib and harness modules.

main.sig
1
2
3
4
sig main.
accum_sig fib.
accum_sig harness.
type damf_export o.
main.mod
1
2
3
4
module main.
accumulate fib.
accumulate harness.
damf_export :- json "fib".

The file fib.goals is a list of goals, with each goal wrapped in a name using the name predicate. For our purposes, we can just list goals that compute \(\kop{fib}(n)\) and \(n^2\) for \(n\) between 1 and 13.

fib.goals
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
name "sq1" (times (s z) (s z) X).
name "sq2" (times (s (s z)) (s (s z)) X).
name "sq3" (times (s (s (s z))) (s (s (s z))) X).
name "sq4" (times (s (s (s (s z)))) (s (s (s (s z)))) X).
name "sq5" (times (s (s (s (s (s z))))) (s (s (s (s (s z))))) X).
name "sq6" (times (s (s (s (s (s (s z)))))) (s (s (s (s (s (s z)))))) X).
name "sq7" (times (s (s (s (s (s (s (s z))))))) (s (s (s (s (s (s (s z))))))) X).
name "sq8" (times (s (s (s (s (s (s (s (s z)))))))) (s (s (s (s (s (s (s (s z)))))))) X).
name "sq9" (times (s (s (s (s (s (s (s (s (s z))))))))) (s (s (s (s (s (s (s (s (s z))))))))) X).
name "sq10" (times (s (s (s (s (s (s (s (s (s (s z)))))))))) (s (s (s (s (s (s (s (s (s (s z)))))))))) X).
name "sq11" (times (s (s (s (s (s (s (s (s (s (s (s z))))))))))) (s (s (s (s (s (s (s (s (s (s (s z))))))))))) X).
name "sq12" (times (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))) (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))) X).
name "sq13" (times (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))) (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))) X).
name "fib1" (fib (s z) X).
name "fib2" (fib (s (s z)) X).
name "fib3" (fib (s (s (s z))) X).
name "fib4" (fib (s (s (s (s z)))) X).
name "fib5" (fib (s (s (s (s (s z))))) X).
name "fib6" (fib (s (s (s (s (s (s z)))))) X).
name "fib7" (fib (s (s (s (s (s (s (s z))))))) X).
name "fib8" (fib (s (s (s (s (s (s (s (s z)))))))) X).
name "fib9" (fib (s (s (s (s (s (s (s (s (s z))))))))) X).
name "fib10" (fib (s (s (s (s (s (s (s (s (s (s z)))))))))) X).
name "fib11" (fib (s (s (s (s (s (s (s (s (s (s (s z))))))))))) X).
name "fib12" (fib (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))) X).
name "fib13" (fib (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))) X).

Finally, here’s how we can run harness, and subsequently Dispatch:

$ tjcc fib && tjcc harness && tjcc main && tjlink main

$ tjsim -b -s 'damf_export.' -m 1 main
Wrote fib.json.

$ dispatch publish fib.json local # (1)!
Published DAMF collection object to local with cid: bafyreickai4hsl3aht53hz3veen5xlzvx7njy7sudsfpns3ikxtnuzpjha
  1. Can take a few dozen seconds to finish.

This CID can be explored on IPLD explorer or locally with ipfs dag get.

Theorem in Abella DAMF

The assertions generated by Coq and λProlog will be used to prove the main theorem in Abella DAMF, which is a variant of the Abella theorem prover that can accept and publish DAMF assertions.

Abella is simply typed and its type system does not have any reasoning principles that yield theorems. Reasoning in Abella is done with its reasoning logic known as \(\mathcal{G}\), which is an extension of first-order intuitionistic logic over \(\lambda\)-terms that supports inductive and co-inductive definitions, generic quantification (using \(\nabla\)), and nominal abstraction (a generalization of \(\alpha\beta\eta\) equality on \(\lambda\)-terms).

8. Setting the stage

We will write the overall theorem in the Abella file FibTheorem.thm. It begins by defining the type nat of natural numbers, its constructors z and s, and then some comparison relations and computations. Note that all definitions in Abella are relational: unlike Coq, we don’t define + as a binary function on natural numbers but as a ternary relation plus that relates its first two arguments to its third.

FibTheorem.thm
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
Kind nat type.
Type z nat.
Type s nat -> nat.

Define nat: nat -> prop by
; nat z
; nat (s X) := nat X.

Define lt: nat -> nat -> prop by
; lt z (s X)
; lt (s X) (s Y) := lt X Y.

Define leq: nat -> nat -> prop by
; leq z X
; leq (s X) (s Y) := leq X Y.

Define plus: nat -> nat -> nat -> prop by
; plus z X X
; plus (s X) Y (s Z) := plus X Y Z.

Define times: nat -> nat -> nat -> prop by
; times z X z
; times (s X) Y Z := exists U, times X Y U /\ plus U Y Z.

Define fib: nat -> nat -> prop by
; fib z z
; fib (s z) (s z)
; fib (s (s X)) K :=
    exists M N, fib X M /\ fib (s X) N /\ plus M N K.

Because all inductive definitions are relational in Abella, we often need additional lemmas to establish that the relations behave like functions. In our theorem we will need the following lemmas of this kind.

FibTheorem.thm
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
Theorem plus_deterministic: forall x y u v, plus x y u -> plus x y v -> u = v.
induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to *H3 *H4. search.

Theorem times_deterministic: forall x y u v, times x y u -> times x y v -> u = v.
induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to *H3 *H5. apply plus_deterministic to *H4 *H6. search.

Theorem fib_deterministic: forall x y u, fib x y -> fib x u -> y = u.
induction on 1. intros. case H1.
  case H2. search.
  case H2. search.
  case H2.
    apply IH to *H3 *H6.
    apply IH to *H4 *H7.
    apply plus_deterministic to *H5 *H8. search.

Theorem lt_irreflexive: forall x, nat x -> lt x x -> false.
induction on 1. intros. case H1.
  case H2.
  case H2. apply IH to *H3 *H4.

Theorem plus_result_nat: forall x y k, nat x -> nat y -> plus x y k -> nat k.
induction on 3. intros. case H3.
  search.
  case H1. apply IH to *H5 *H2 *H4. search.

Theorem times_result_nat: forall x y k, nat x -> nat y -> times x y k -> nat k.
induction on 3. intros. case H3.
  search.
  case H1. apply IH to *H6 H2 *H4. apply plus_result_nat to *H7 *H2 *H5. search.

9. Importing DAMF assertions

Abella can import any DAMF assertion using the following statement:

Import "damf:<cid>".

Here, <cid> can be the CID of an individual DAMF assertion object or a DAMF collection object containing assertions. If these assertion objects are in Abella’s own language, they can be used as is. For reference, Abella’s DAMF language object has the following CID:

bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy

What about the case of DAMF assertions in a different language? In this case, Abella will need to use an adapter sequent as explained in the DAMF technical design paper. In the future, such adapter sequents will be built using language translation tools. For now, we will write the adapter sequents ourselves and sign the resulting assertions using a mode field of null, which stands for an assertion for which the signing agent is wholly responsible.

To create such adapter sequents, Abella has a modified form of the Import ... as statement that allows the user to restate the theorem in Abella’s own language. For example, the theorem fib_square_above from Coq that was exported in step 5 can be imported in Abella as follows:

FibTheorem.thm
63
64
65
66
67
Import "damf:bafyreigscd65tb2rabcpjxbep7h4lklbyfenmj32ioond7ouhh7qpvkh7a" as
Theorem fib_square_above: forall x, nat x ->
  leq (s^13 z) x ->
  forall y, times x x y ->
  forall u, fib x u -> lt y u.

The statement of this theorem needs to be comprehensible in the local context of the Abella development, using the type nat, constants s and z, and the relations times, fib, lt, etc. defined in lines 1–29 of FibTheorem.thm.

Iterated application notation

The term s^13 z stands for the term (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))), which is 13 in the unary representation of nat. For any unary term constant k and literal number n (\(\ge 0\)), the notation (k^n t) stands for the n-times iterated application of k to t.

After type-checking the statement of the theorem, Abella uses this Import ... as statement first to build the adapter sequent that has the following DAMF structure:

{ "format": "assertion",
  "claim": {
    "format": "annotated-production",
    "annotation": {
      "name": "fib_square_above!adapter"
      "generator": "damf:bafyreiegwjyj5f2lpw3ck35pqeqt45bwl57c7n7xfpbtxm6ym3sfsixixq" // (1)!
    },
    "production": {
      "mode": null,
      "sequent": {
        "conclusion": "fib_square_above",
        "dependencies": [
          "damf:bafyreigscd65tb2rabcpjxbep7h4lklbyfenmj32ioond7ouhh7qpvkh7a/claim/production/sequent/conclusion" // (2)!
        ] } }
  "formulas": {
    "fib_square_above": {
      "language": "damf:bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy", // (3)!
      "content": "forall x, nat x -> … -> lt y u",
      "context": "fib_square_above!context"
    } },
  "contexts": {
    "fib_square_above!context": {
      "language": "damf:bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy",
      "content": [
        "Kind nat type", "Type z nat", "Type s nat -> nat",
        "Define nat : …", "Define leq : …", "Define lt : …",
        "Define times : …", "Define fib : …"
      ] } } }
  1. This field links to the DAMF tool object for this version of Abella. Because it is part of an annotation, DAMF prescribes no particular meaning to the "generator" key or its value. Its purpose in this walkthrough is purely documentary in nature.
  2. This uses IPLD paths to refer to the CID of the conclusion of the assertion object that was imported. It corresponds to the theorem named fib_square_above that we proved in Coq.
  3. This is the Abella language’s identifier

This adapter sequent, which has a dependency on an external formula in a different language (Coq) to the conclusion (Abella), will be published using Dispatch. For the rest of the file, Abella then continues as if fib_square_lemma was indeed stated and proved in Abella.

The assertions produced using λProlog in step 7 are similarly imported using a sequence of Import ... as statements.

FibTheorem.thm
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
Import "damf:bafyreibdhpzggdkox2tq2i5jj47lbigdjen6szhtdl5hpqdiokmxzpupby" as
Theorem sq1: times (s^1 z) (s^1 z) (s^1 z).

Import "damf:bafyreib2cj3s46kalezk352bhxagw57rmb35klldgxdwvpfovikuafbkwa" as
Theorem sq2: times (s^2 z) (s^2 z) (s^4 z).

Import "damf:bafyreieo4vvpuk75qzvuesotzebtsq6skvenvkpyfxoibkgrtpfhlktcza" as
Theorem sq3: times (s^3 z) (s^3 z) (s^9 z).

Import "damf:bafyreic3tflezeagl3plwwffuu3j4ggop7cogkafxiktmkcwhkzzqrbv7i" as
Theorem sq4: times (s^4 z) (s^4 z) (s^16 z).

Import "damf:bafyreih6g3sddcnb57mlhr735pzw7wnqmuix5657ppnirwdeamhiq6sfpq" as
Theorem sq5: times (s^5 z) (s^5 z) (s^25 z).

Import "damf:bafyreiehmglxz2qegqvkeom32ew53rii64ibiypeyrr6opwiu22vt6v6aq" as
Theorem sq6: times (s^6 z) (s^6 z) (s^36 z).

Import "damf:bafyreiappmrptuwvdju5zwltx4v57zpy244kc2v72g7bu63vwoisqbnf3m" as
Theorem sq7: times (s^7 z) (s^7 z) (s^49 z).

Import "damf:bafyreibestkx33qyvk6frpcv5sahdoz6igkkpeqjfkkzdxaktn6tyxm7xe" as
Theorem sq8: times (s^8 z) (s^8 z) (s^64 z).

Import "damf:bafyreia7o42fqa7f65su4mbdkiliayzom3acmsc3cwmwqs6o4csklo7jau" as
Theorem sq9: times (s^9 z) (s^9 z) (s^81 z).

Import "damf:bafyreibbgfbqp3xgvlznp2lpdlaptpt2cfg47ymkol6bjpbutgi3plr24m" as
Theorem sq10: times (s^10 z) (s^10 z) (s^100 z).

Import "damf:bafyreighquu5d7vgndlnewbhhslqbfq6koaqjo2k4lzp2fpthq45kmrtvq" as
Theorem sq11: times (s^11 z) (s^11 z) (s^121 z).

Import "damf:bafyreicolq7bcvn47aqhtddofca2crbkvjchpgfa24jz2t2ikfn3i4bzde" as
Theorem sq12: times (s^12 z) (s^12 z) (s^144 z).

Import "damf:bafyreigetyik2x3dzsjk2e2fdthg54fnqwdbhpmnm7ohcoddm6lsvyrgfe" as
Theorem sq13: times (s^13 z) (s^13 z) (s^169 z).

Import "damf:bafyreiadisiqi67dohxfrwsrau2r4a2n3p5546zydr7zg246yby2gwkl2i" as
Theorem fib2: fib (s^2 z) (s^1 z).

Import "damf:bafyreihmjaelmx56ir63myuym7rrcct3prm2hgkk2thkvumlg3q62peywa" as
Theorem fib3: fib (s^3 z) (s^2 z).

Import "damf:bafyreihcxdyl5wqvravu7nh42p6jczegay5l3bq6m7i76ytwugaythui7u" as
Theorem fib4: fib (s^4 z) (s^3 z).

Import "damf:bafyreihk2eyjeer63e7axrookccyl6k45pn2ah4zmgqtqjmgdv5lniw3li" as
Theorem fib5: fib (s^5 z) (s^5 z).

Import "damf:bafyreibehq6b5d2npqrwkd3nzzyekteq7ttzoa75gmjtrxsvumcab22wie" as
Theorem fib6: fib (s^6 z) (s^8 z).

Import "damf:bafyreibtg4hqlzvxx4vh7buj2wn7fjhuolbwlchvnc3qzzgr7ev32vlcre" as
Theorem fib7: fib (s^7 z) (s^13 z).

Import "damf:bafyreifijsv4n2kvlyvk4b3hwg47sla2s4cizfdcndya5qdnkxdsc3acyi" as
Theorem fib8: fib (s^8 z) (s^21 z).

Import "damf:bafyreid3yqc2q5eefuo6snea5s2l5tog4kzikfyi67s7rbzkdvunqzujty" as
Theorem fib9: fib (s^9 z) (s^34 z).

Import "damf:bafyreieskqtqvyavgywf6ooytykfwyqeilodcfhxmzc5glmagaqrjngmhi" as
Theorem fib10: fib (s^10 z) (s^55 z).

Import "damf:bafyreiekhrslzuhdt3pvjcnmfmvnlomsntvqnqt6vqrq6egygxrncy3vmy" as
Theorem fib11: fib (s^11 z) (s^89 z).

Import "damf:bafyreifp67qkkvc7r3ng4hu7uoxnekooucaiv4kanqzocij2kiu2ragowi" as
Theorem fib12: fib (s^12 z) (s^144 z).

Import "damf:bafyreiggvc5wz7tcmouywkchh7tvdqrtvvwj35oc7jylka3nxic4gjtq6q" as
Theorem fib13: fib (s^13 z) (s^233 z).

10. Finishing the theorem

Assembling the final theorem in Abella is now straightforward. In the only if direction (forward), we repeatedly make use of the computation assertions from λProlog for \(n \in 0..12\), and then the fib_square_above assertion for \(n \ge 13\). In the if direction, we just verify that the computations (again, pulled from λProlog) have the right values.

FibTheorem.thm
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
Theorem fib_squares: forall x x2, nat x -> times x x x2 ->
  (fib x x2 -> x = z \/ x = s z \/ x = s^12 z) /\
  (x = z \/ x = s z \/ x = s^12 z -> fib x x2).
intros Hnat Hsquare. split.
%% ->
intros Hfib.
Hcs: assert x = s^0 z \/ x = s^1 z \/ x = s^2 z \/ x = s^3 z
         \/ x = s^4 z \/ x = s^5 z \/ x = s^6 z \/ x = s^7 z
         \/ x = s^8 z \/ x = s^9 z \/ x = s^10 z \/ x = s^11 z
         \/ x = s^12 z \/ leq (s^13 z) x.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  Hnat: case Hnat. search.
  right. search 14.
Hcs: case Hcs.
  search. % case of x = z
  search. % case of x = s z
  % case of x = 2
  apply fib_deterministic to fib2 Hfib.
  apply times_deterministic to sq2 Hsquare.
  % case of x = 3
  apply fib_deterministic to fib3 Hfib.
  apply times_deterministic to sq3 Hsquare.
  % case of x = 4
  apply fib_deterministic to fib4 Hfib.
  apply times_deterministic to sq4 Hsquare.
  % case of x = 5
  apply fib_deterministic to fib5 Hfib.
  apply times_deterministic to sq5 Hsquare.
  % case of x = 6
  apply fib_deterministic to fib6 Hfib.
  apply times_deterministic to sq6 Hsquare.
  % case of x = 7
  apply fib_deterministic to fib7 Hfib.
  apply times_deterministic to sq7 Hsquare.
  % case of x = 8
  apply fib_deterministic to fib8 Hfib.
  apply times_deterministic to sq8 Hsquare.
  % case of x = 9
  apply fib_deterministic to fib9 Hfib.
  apply times_deterministic to sq9 Hsquare.
  % case of x = 10
  apply fib_deterministic to fib10 Hfib.
  apply times_deterministic to sq10 Hsquare.
  % case of x = 11
  apply fib_deterministic to fib11 Hfib.
  apply times_deterministic to sq11 Hsquare.
  % case of x = 12
  search.
  % case of x >= 13
  H: apply fib_square_above to Hnat Hcs.
  H: apply *H to Hsquare.
  H: apply *H to Hfib.
  Hnat2: apply times_result_nat to Hnat Hnat Hsquare.
  apply lt_irreflexive to Hnat2 H.

%% <-
intros Hcs.
Hcs: case Hcs.
  case Hsquare. search.
  apply times_deterministic to sq1 Hsquare. search.
  apply times_deterministic to sq12 Hsquare. backchain fib12.

Verifying this in Abella requires the --damf-imports command line flag. Publishing the assertions also requires the --damf-publish <location> flag, where <location> is either local or cloud.

$ abella --damf-imports --damf-publish local FibTheorem.thm
Published as damf:bafyreifg3cosrvpidfmepwsjjt6kwvrlb2iobe5wo27sqsbu5uzbrdlvhm

As usual, this can be browsed in IPLD explorer.