shhyou

#lang racket/base

(require racket/include
         racket/stxparam
         (for-syntax racket/base syntax/parse/pre))

(provide
 quote
 #%datum
 (rename-out [include |#include|]

shhyou

AGDA_FILES=$(wildcard *.agda)
TEX_FILES=${AGDA_FILES:.agda=.tex}
PDF_FILES=${AGDA_FILES:.agda=.pdf}
MONO_FONT=DejaVu Sans Mono # FreeMono is another choice
PYGMENTS_STYLE=tango

GRADED_XOPP_FILES=$(wildcard *-graded.xopp)
GRADED_PDF_FILES=${GRADED_XOPP_FILES:.xopp=.pdf}

.PHONY: all

shhyou

This pull request adds a set of combinators for equational reasoning about vector equality of the form cast eq xs ≡ ys and a few properties demonstrating its application. In particular, the new combinators deal with the threading of index equality proofs, greatly reducing the boilerplate that manipulates casts to make writing equational proofs about vectors more or less feasible.

(Sorry for the piles of PR and the mess of the commit history. I promise this is the last one I have in hand. The first commit is the content of #2041 and #2045. After these two PRs get in, I'll rebase to remove the first commit. To see the code of this PR, please check https://github.com/agda/agda-stdlib/commit/f8971193dce2620cdabf4c7f1d8319c2aa8fb0ed.)

Motivation

Index arithmetic is notably troublesome when it comes to proving vector properties (#942). Existing solutions include stating and proving cast-equality by induction, proving [pointwise equality](https://github.com/agda/agda-stdlib/blob/104125c62d88ebe91274ebd

shhyou

{-# OPTIONS --without-K --safe #-}

module VecCastReason where

open import Data.Nat.Base
open import Data.Nat.Properties using (+-comm; +-suc; +-assoc)
open import Data.List.Base as List using (List; []; _∷_)
import Data.List.Properties as Listₚ
open import Data.Vec.Base
open import Data.Vec.Properties hiding (reverse-++; cast-reverse)

shhyou

#!/usr/bin/env racket
#lang racket/base

(require racket/file)

(provide cleanup-pref-keys)

(define cleanup-pref-keys
  '((plt:framework-pref:drracket:recently-closed-tabs ())
    (plt:framework-pref:drracket:console-previous-exprs ())

shhyou

#lang racket

(module DynCtc racket
  ;; the blames of dyn1/c and dyn2/c are different
  (provide dyn1/c
           dyn2/c
           (struct-out RuntimeError))
  (struct RuntimeError (message) #:transparent)

  (define dyn1/c

shhyou

{-# OPTIONS --without-K --safe #-}

module MergeSort where

open import Data.Bool.Base using (Bool; true; false)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat
  using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≤?_)
open import Data.Nat.Properties
  using (≰⇒≥; ≤-reflexive; ≤-pred; m+n≤o⇒n≤o; m+n≤o⇒m≤o; +-comm; +-cancelˡ-≡; m≤m+n)

shhyou

Comparing PDF files in git diff commands

The typical approach to comparing PDF files in git diff outputs amounts to converting PDF files into texts through pdftotext and show the diff of conversion.

1. Install the utility pdftotext from the project poppler
2. Enable the handler pdffiles in diff for PDF files and instruct the handler to call the pdf-astextplain script:

shhyou

#lang racket/base

(require racket/list
         racket/vector
         racket/bytes
         racket/match)

(provide
 ;; plain implementation of the Burrows-Wheeler transformation
 (struct-out bwencode)

shhyou

{-# OPTIONS --safe --without-K #-}

-- using an inductive datatype (family) instead of El

module MutualRecData where

open import Agda.Primitive

open import Data.Nat.Base
  using (ℕ ; zero ; suc)