shuhung 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

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.

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

	#lang racket/base

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

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

	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

	{-# 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)

	#!/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 ())

	#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

	{-# 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)

	#lang racket/base

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

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

	{-# 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)

shuhung shhyou

Motivation

Comparing PDF files in git diff commands

Comparing PDF files in `git diff` commands