wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

wenkokke

{-# LANGUAGE TemplateHaskell, QuasiQuotes, FlexibleInstances, FlexibleContexts,
             TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds, RankNTypes,
             KindSignatures, UndecidableInstances, StandaloneDeriving,
             RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable  #-}
module AB where


import           Prelude hiding (lookup, lex)
import           Control.Applicative ((<|>),empty)
import           Data.Maybe (maybeToList)

wenkokke

-- This file contains the code from the paper "Formalising
-- type-logical grammars in Agda", and was directly extracted from the
-- paper's source.
--
-- Note: because the symbol customarily used for the "left difference"
-- is unavailable in the Unicode character set, and the backslash used
-- for implication is often a reserved symbol, the source file uses a
-- different notation for the connectives: the left and right
-- implications are represented by the double arrows "⇐" and "⇒", and

wenkokke

#!/bin/bash
set -eo pipefail

# 1. Build GHC with JavaScript backend
# https://gitlab.haskell.org/ghc/ghc/-/wikis/javascript-backend/building

# 2. Get Agda source
git clone --depth=1 git@github.com:agda/agda.git agda
cd agda

wenkokke

from contextlib import contextmanager
from curses.ascii import isalpha
from dataclasses import dataclass
from pathlib import Path
import ast
import re
from typing import Any, Optional, Sequence, Set


@dataclass

wenkokke

open import Level                                      using (_⊔_)
open import Function                                   using (_∘_)
open import Data.Vec                                   using (Vec; []; _∷_; foldr)
open import Data.Nat                                   using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties.Simple                 using (+-right-identity; +-suc)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Data.Product                               using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty                                 using (⊥-elim)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Relation.Binary                            using (module DecTotalOrder; DecTotalOrder; Rel)

wenkokke

cheatsheet.tex
*.aux
*.fls
*.log
*.synctex.gz
*.fdb_latexmk
*.lot

wenkokke

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes   #-}

module Lib where

data Nat = Z
         | S Nat

-- There's something really wonky going on with closed type families: if both

wenkokke

%if False
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% linear.fmt
%
% Format -> as a period when part of a lambda abstraction,
% as a lolli when used as part of a linear function arrow,
% and as an arrow otherwise.
%
% Wen Kokke, February 2021, version 1.0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

wenkokke

{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}

module lecture1 where

module sum-and-product-types where

{--------------------------------------------------------------------------------}
-- so Coq and Agda are kinda the same, yet very different

-- * it's said Coq looks like ML and Agda looks like Haskell