Skip to content

Instantly share code, notes, and snippets.

@freeman42x
Created July 25, 2023 15:06
Show Gist options
  • Save freeman42x/ebe41f7651aaac457badce6e70cb8c07 to your computer and use it in GitHub Desktop.
Save freeman42x/ebe41f7651aaac457badce6e70cb8c07 to your computer and use it in GitHub Desktop.
How to formalise a concept in Agda

Agda is a dependently typed functional programming language that is also used as a proof assistant, meaning you can use it to construct and verify formal proofs. Formalizing a concept in Agda involves defining the concept in such a way that it is unambiguous, deterministic, and conforms to the principles of logic.

This can involve a number of steps, which I'll explain in more detail.

  1. Identify the Concept

    The first step is to identify the concept you wish to formalize. This could be anything from a simple mathematical operation, like addition, to more complex notions such as lists, trees, or even properties of more abstract structures.

  2. Define Data Types

    In Agda, you use data types to represent the various components of your concept. For instance, if you are formalizing the concept of natural numbers, you might define a data type Nat with constructors zero : Nat and suc : Nat -> Nat to represent zero and the successor function, respectively.

    data Nat : Set where
      zero : Nat
      suc  : Nat -> Nat
  3. Define Functions

    Once you've defined your data types, you'll need to define functions that operate on these types. For the case of natural numbers, you might define functions for addition and multiplication.

    _+_ : Nat -> Nat -> Nat
    zero  + n = n
    suc m + n = suc (m + n)
  4. State Properties

    With your data types and functions defined, you can begin to state properties of your functions. These properties are what you're actually interested in proving. For example, you might want to prove that addition of natural numbers is commutative, that is m + n = n + m.

    +-comm : (m n : Nat) -> m + n ≡ n + m
  5. Prove Properties

    Finally, you prove your properties using induction, case analysis, or other proof techniques. Agda's type system allows you to express these proofs as programs.

    +-comm : (m n : Nat) -> m + n ≡ n + m
    +-comm zero n = refl
    +-comm (suc m) n = cong suc (+-comm m n)

Here, refl stands for reflexivity, a property which says that every element is equal to itself. cong is a function that applies a function to both sides of an equality proof.

Remember, this is a high-level overview and each step may involve considerable thought and refinement to get right. The process of formalizing a concept also involves deep understanding of the concept you're formalizing, and the specific techniques for doing so can vary widely depending on the concept and context.

The Agda documentation and many online tutorials and guides can provide a deeper dive into these concepts and the specifics of implementing them in Agda.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment