Agdaでかけ算の交換法則

Agdaでかけ算の交換法則をDay2-answer.agdaを参考に書きました。というかそのまんま。名前はProgramming Language Foundations in Agdaに合わせたつもりです。理解のためになるべくていねいに書こうと思ったんですが、*-sucと*-commをばらそうとするとエラーになってしまってめんどくさくなってしまいました。*-sucは先にlemmaが必要なんだろうな。*-commは「あっているはずなのに」と思うんですが通らない。基本がわかってないんですよね。reflはたんに計算するだけで、rewriteはsuc nをnにしたらいいのかと思うんですけど。まあ、いちおうC-c, C-lで通ります。

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

infixl 6  _+_
infixl 7  _*_

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
  
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎
  
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

*-identityʳ : ∀ n → n * zero ≡ zero
*-identityʳ zero =
  begin
    zero * zero
  ≡⟨⟩
    zero
  ∎
*-identityʳ (suc m) = *-identityʳ m

*-suc : ∀ m n → m * (suc n) ≡ m + m * n
*-suc zero n =
  begin
    zero * (suc n)
  ≡⟨⟩
    zero + zero * n
  ∎
*-suc (suc m) n rewrite *-suc m n =
  cong suc (
    begin
      n + (m + m * n)
    ≡⟨ sym (+-assoc n m _) ⟩
      n + m + m * n
    ≡⟨ cong (λ x → x + m * n) (+-comm n m) ⟩
      m + n + m * n
    ≡⟨ +-assoc m n _ ⟩
      m + (n + m * n)
    ∎
  )

*-comm : ∀ n m → n * m ≡ m * n
*-comm zero m = sym (*-identityʳ m)
*-comm (suc n) m rewrite *-suc m n = cong (_+_ m) (*-comm n m)
∨ Source markdown
Agdaでかけ算の交換法則

Agdaでかけ算の交換法則を[Day2-answer.agda](https://github.com/krtx/agda-handson/blob/master/Day2-answer.agda)を参考に書きました。
というかそのまんま。
名前は[Programming Language Foundations in Agda](https://plfa.github.io/Induction/)に合わせたつもりです。
理解のためになるべくていねいに書こうと思ったんですが、`*-suc`と`*-comm`をばらそうとするとエラーになってしまってめんどくさくなってしまいました。
`*-suc`は先にlemmaが必要なんだろうな。
`*-comm`は「あっているはずなのに」と思うんですが通らない。
基本がわかってないんですよね。
`refl`はたんに計算するだけで、`rewrite`は`suc n`を`n`にしたらいいのかと思うんですけど。
まあ、いちおう`C-c, C-l`で通ります。

```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

infixl 6  _+_
infixl 7  _*_

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
  
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎
  
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

*-identityʳ : ∀ n → n * zero ≡ zero
*-identityʳ zero =
  begin
    zero * zero
  ≡⟨⟩
    zero
  ∎
*-identityʳ (suc m) = *-identityʳ m

*-suc : ∀ m n → m * (suc n) ≡ m + m * n
*-suc zero n =
  begin
    zero * (suc n)
  ≡⟨⟩
    zero + zero * n
  ∎
*-suc (suc m) n rewrite *-suc m n =
  cong suc (
    begin
      n + (m + m * n)
    ≡⟨ sym (+-assoc n m _) ⟩
      n + m + m * n
    ≡⟨ cong (λ x → x + m * n) (+-comm n m) ⟩
      m + n + m * n
    ≡⟨ +-assoc m n _ ⟩
      m + (n + m * n)
    ∎
  )

*-comm : ∀ n m → n * m ≡ m * n
*-comm zero m = sym (*-identityʳ m)
*-comm (suc n) m rewrite *-suc m n = cong (_+_ m) (*-comm n m)
```
∨ Source code
# coding: utf-8
require 'optparse'
require 'open3'
require 'strscan'

$lib = ""

class Context
  attr_reader :state

  def initialize
    @block = Block.new
    @list = List.new
    @quote = Quote.new
    @paragraph = Paragraph.new
    @footnote = Footnote.new
    @normal = Normal.new
    @state = @normal
  end

  def change_state(state)
    if @state != state then
      @state.finish
      @state = state
      @state.start
    end
  end

  def block?
    @state.block?
  end

  def process(line)
    @state.process(line)
  end

  def block(end_str, header)
    @block.end_str = end_str
    @block.header = header
    change_state(@block)
  end

  def normal
    change_state(@normal)
  end

  def list(content)
    change_state(@list)
    printf "<li>" << parse_line(content) << "</li>"
  end

  def quote(content)
    change_state(@quote)
    puts parse_line(content)
  end

  def paragraph(line)
    change_state(@paragraph)
    @paragraph.add_line(parse_line(line))
  end

  def footnote(tag, content)
    change_state(@footnote)
    printf "<li><a id='footnote_#{tag}'>[#{tag}]</a>:" << parse_line(content) << "</li>"
  end
end

class State
  def start
    printf self.class::HEADER
  end

  def finish
    if self.class::FOOTER.length > 0 then
      printf "#{self.class::FOOTER}\n"
    end
  end

  def block?
    false
  end
end

class Block < State
  HEADER = ""
  FOOTER = ""

  attr_accessor :end_str
  attr_accessor :header
  attr_accessor :buffer

  def initialize
    @buffer = ""
  end

  def start
    initialize
  end

  def process(line)
    @buffer = @buffer << line << "\n"
  end

  def block?
    true
  end
end

class Normal < State
  HEADER = ""
  FOOTER = ""
end

class List < State
  HEADER = "<ul>"
  FOOTER = "</ul>"
end

class Quote < State
  HEADER = "<blockquote style='font-size: medium; text-align: left; border-left: 5px solid #DDDDDD; padding-left: 10px; background: #F0F0F0'>"
  FOOTER = "</blockquote>"
end

class Paragraph < State
  PARAGRAPH_HEADER = "<p>"
  PARAGRAPH_FOOTER = "</p>"
  DESCRIPTION_LIST_HEADER = "<dl>"
  DESCRIPTION_LIST_TERM_HEADER = "<dt>"
  DESCRIPTION_LIST_TERM_FOOTER = "</dt>"
  DESCRIPTION_LIST_VALUE_HEADER = "<dd>"
  DESCRIPTION_LIST_VALUE_FOOTER = "</dd>"
  DESCRIPTION_LIST_FOOTER = "</dl>"

  def initialize
    @lines = []
    @mode = :paragraph
  end

  def start
    initialize
  end

  def add_line(line)
    if md = line.match(/^: (.*)/) then
      @mode = :deflist
    end
    @lines.push(line)
  end

  def finish
    if @mode == :paragraph then
      print PARAGRAPH_HEADER
      @lines.each do |line|
        print line
      end
      puts PARAGRAPH_FOOTER
    else
      puts DESCRIPTION_LIST_HEADER
      @lines.each do |line|
        if md = line.match(/^: (.*)/) then
          print DESCRIPTION_LIST_VALUE_HEADER
          print md[1]
          puts DESCRIPTION_LIST_VALUE_FOOTER
        else
          print DESCRIPTION_LIST_TERM_HEADER
          print line
          puts DESCRIPTION_LIST_TERM_FOOTER
        end
      end
      puts DESCRIPTION_LIST_FOOTER
    end
  end
end

class Footnote < State
  HEADER = "<ul>"
  FOOTER = "</ul>"
end

mathjax = <<RUBY
<script>
  MathJax = {
    chtml: {
      displayAlign: "left",
    },
    tex: {
      inlineMath: [['$', '$']]
    }
  };
</script>
<script type="text/javascript" id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
</script>
RUBY

header = <<-RUBY
<!DOCTYPE html>
<html lang="ja">
  <head>
    <meta charset="utf-8">
    <script>
      MathJax = {
        chtml: {
          displayAlign: "left",
        },
        tex: {
          inlineMath: [['$', '$']]
        }
      };
    </script>
    <script type="text/javascript" id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
    </script>
    <title>TITLE</title>
  </head>
  <body>
    <h1>TITLE</h1>
RUBY
footer = <<RUBY
  </body>
  </html>
RUBY

opt = OptionParser.new
type = :html
opt.on('-b', '--blog', 'blog type output') do |v|
  type = :blog
end
filename = ""
opt.parse!(ARGV)

if ARGV.size > 1 then
  STDERR.puts "Too many argument: ARGV=#{ARGV}"
  exit 1
end
filename = ARGV[0]
if !File.exists?(filename) then
  STDERR.puts "File not exists: ARGV=#{ARGV}"
  exit 1
end

def parse_line(line)
  line.gsub!(/`([^`]*)`/) {
    s = $1
    s.gsub!('&', "&amp;")
    s.gsub!('<', "&lt;")
    s.gsub!('>', "&gt;")
    "<code style='padding: 2px 3px ; background: #FEFEFE; border: 1px solid #DDDDDD; border-radius: 5px'>#{s}</code>"
  }
  line.gsub!(/\[([^\]]*)\]\(([^\)]*)\)/) {
    "<a href='#{$2}'>#{$1}</a>"
  }
  line.gsub!(/\[\^([^\]]*)\]/) {
    "<a href='#footnote_#{$1}'><sup>[#{$1}]</sup></a>"
  }
  line
end

def parse_option(str)
  lang = nil
  name = nil
  options = {"echo"=>true, "eval"=>true, "include"=>true}
  s = StringScanner.new(str)
  lang = s.scan(/\w+/)
  s.scan(/\s+/)
  name = s.scan(/\w+/)
  while !s.eos?
    s.scan(/ *, */)
    option = s.scan(/\w+/)
    s.scan(/ *= */)
    value = s.scan(/\w+/)
    if value.casecmp("false") == 0 then
      options[option] = false
    end
  end
  return lang, name, options
end

def process_block(block)
  lang = nil
  name = nil
  options = {"echo"=>true, "eval"=>false, "include"=>true}
  if md = block.header.match(/^ *([^{: ]+)(:([^ ]*))?/) then
    lang = md[1]
    name = md[3]
    options = {"echo"=>true, "eval"=>false, "include"=>true}
  elsif md = block.header.match(/^ *{(.*)}/) then
    lang, name, options = parse_option(md[1])
  end

  if lang == "lib" then
    $lib = $lib << "\n" << block.buffer
  end

  if options["include"] then
    print '<div style="margin: 0 0 10px 0;">'
    if options["echo"] then
      if !name.nil? then
       printf "<div style=\"border: 1px solid black;padding-left: 3px;margin-bottom: 0;\">#{name}</div>"
      end
      print '<pre style="overflow-x: scroll;padding: 1px 1px 1px 3px;border:1px solid black;margin: 0;"><code>'
      buffer = block.buffer.gsub('&', "&amp;")
      buffer.gsub!('<', "&lt;")
      buffer.gsub!('>', "&gt;")
      puts buffer
      puts "</code></pre>"
    end

    if options["eval"] then
      print '<div style="overflow-x: scroll;padding: 1px 1px 1px 3px;border:1px solid black;margin-top: 0;">'
      if lang == "math" then
        print "$$"
        print block.buffer
        print "$$"
      elsif lang == "ruby" then
        print "<pre>"
        print eval($lib + block.buffer)
        print "</pre>"
      elsif lang == "PlantUML" then
        Open3.popen3("java -jar /mnt/d/app/plantuml.jar -pipe -svg -charset UTF-8") do |i, o, e, w|
          i.write block.buffer
          i.close
          o.each do |l| puts l end
          e.each do |l| printf("<!-- stderr: %s -->\n", l) end
          printf("<!-- thread: %s -->\n", w.value)
        end
      end
      print "</div>"
    end
    print '</div>'
  end
end

def print_script
  puts <<-RUBY
    <script>
      function toggleDisplay(e) {
        if (e.style.display === "none") {
          e.style.display = "block";
        } else {
          e.style.display = "none";
        }
      };
      function toggleDisplayMark(e) {
        str = e.innerText;
        c = str.substring(0, 1);
        if (c === "∨") {
          e.innerText = "∧" + str.substring(1, str.length);
        } else if (c === "∧") {
          e.innerText = "∨" + str.substring(1, str.length);
        }
      }
    </script>
  RUBY
end

def print_code(filename, title)
  puts %!<div onclick="toggleDisplayMark(this);toggleDisplay(this.nextElementSibling);" style="margin-top: 10px; border: 1px solid black;">∨ #{title}</div>!
  print '<pre style="display: none;overflow-x: scroll;padding: 1px 1px 1px 3px;border:1px solid black;margin: 0;"><code>'
  File.open(filename) do |f|
    f.each_line do |line|
      line.gsub!('&', "&amp;")
      line.gsub!('<', "&lt;")
      line.gsub!('>', "&gt;")
      puts line
    end
    puts "</code></pre>"
  end
end

File.open(filename, "r") do |i|
  context = Context.new
  i.each_line do |line|
    line.chomp!
    if i.lineno == 1 then
      if type == :html then
        puts header.gsub(/TITLE/, line)
      else
        puts line
        puts mathjax
      end
    elsif context.block? then
      re = Regexp.new("^#{context.state.end_str}")
      if line.match(re) then
        process_block(context.state)
        context.normal
      else
        context.process(line)
      end
    elsif md = line.match(/^(`{3,})(.*)/) then
      end_str = md[1]
      header = md[2]
      context.block(end_str, header)
    elsif md = line.match(/^(#+) *(.*)/) then
      level = md[1].length + 1
      printf("<h#{level}>%s</h#{level}>\n", md[2])
    elsif md = line.match(/^[ \t]*$/) then
      context.normal
    elsif md = line.match(/^> (.*)/) then
      context.quote(md[1])
    elsif md = line.match(/^- (.*)/) then
      context.list(md[1])
    elsif md = line.match(/^\[\^([^\]]*)\]:(.*)/) then
      context.footnote(md[1], md[2])
    elsif md = line.match(/^! *include +(.*)/) then
      context.normal
      file = File.open(md[1])
      puts file.read
    else
      context.paragraph(line)
    end
  end
  context.normal
end
print_script
print_code filename, "Source markdown"
print_code __FILE__, "Source code"
if type == :html then
  puts(footer)
end

コメント

コメントを投稿

このブログの人気の投稿

五十音配列付き新下駄配列

イメージ
keyboard layout editorデビューしました。ファイルが複数になると管理がめんどうなので、このブログの内容はSVGファイルに直接書いてますが、これでいいんだっけ？まあ、消えなければ後からなんとでもなるからいいか。 と思ったら、SVGは日本語に対応していないみたいです。しくしく。 レイアウトは新下駄配列に覚えやすい五十音配列を加えたものです。アルファベット自体をいじってますが、qtypをちょっと動かしただけです。bntyを親指で押すシステムなんですが、けっこう快適です。ErgoDox EZだと斜めになっているキーが親指に当たるので取ってしまっています。アルファベットの長押しに制御キーやレイヤーキーを割り当ててしまえば30%で十分なんですね。ほとんど手首を動かさずに入力できます。 日本語配列は新下駄配列の拗音以外はそのままなので、覚え直すことなく使えます。五十音部分は左手で行を指定して、右手で段か拗音を指定する方式です。新下駄配列で使用しているsdklはそのまま残してあるのでさ行、た行がありませんが、それは新下駄の方を使ってください。拗音は新下駄のものをそのまま使うこともできたのですが、左手で行を指定する方式なのを活かして、右手で拗音を指定する方式にしました。各行に拗音とくっつくのはひとつしかないんですね。不思議な感じです。 欠点はロールオーバーミスが起こりまくることです。「うんち」と入力しようとして「にち」になるようなことがよく起こります。新下駄配列でもsdklioがからむと起こるのですが、それ以外にもシフトキーを増やしたので大幅に起こりやすくなっています。そういう配列なのでそこはあきらめてください。スピードを犠牲にして脳の負荷を抑えた配列です。ただ、ローマ字テーブルからfj同時押しで「に」の項目を消してしまえばそうはならないので、いろいろカスタマイズできるかもしれません。この配列でスピードを目指すならステノワードのような方向になるでしょう。脳の負荷が増えてしまいますが。 良い点は、左手で行を指定する方式なので数字行にはみ出していたみゃ行等を30%の範囲に取り込めたことでしょうか。もう一つ、頻度の低い文字は五十音の方を使うことにすれば、空いた所にいろいろ突っ込めるところでしょうか。かなり気に入ってます。 ∨ Source mar...
続きを読む

WSLでの親指シフトはどうやらMozcで実現可能と気がつくまで

WindowsではAutoHotKeyを使って疑似親指シフトで日本語を入力しています。もともとかな打ちだったんですが、キーボードをErgoDox EZに変えたら「ろ」とかのキーが足りなくなって、どうしようか悩んで親指シフトを見つけてきました。疑似なのは同時押しではなくて、親指でファンクションキーを押しながらアルファベットキーを押すことで出しているからです。AutoHotKeyを使って同時押しを実現しているものがあるのは知っていますが、とりあえずNICOLA配列を試しつつ今まで引っ張ってきた感じです。 Windowsではそれで満足していたのですが、WSLを使うようになって困りました。AutoHotKey(以下AHK)ではIMEの状態を取ってきてオンの場合には出力を変えているのですが、WSLだとAutoHotKeyからMozcの情報を取ってこられる気がしません。WSL側で検知してWindows側から読める位置にファイルを置くような、トリッキーな方法を使えばできなくはないような気もしますが、そこまでしてAHKに頼るのも変な感じです。 ということで、WSL側で親指シフトを使えるようにしようとぐぐって出てきたのは oyainput というやつでした。しかし、これがWSLでは動かない。エラーコードから察するに、 /proc/bus/input/devices が空なのでキーボードの情報が取れないのでだめみたいです。まあ、WSLですし。 しかたがないので、今度はWSLのEmacsでWindows側のIMEが使えるという「 emacs-mozc を動かすための設定（WSL 設定編） 」のmozc_emacs_helperというのを試してみました。で、苦労して動かしてみたものの、Windows側の辞書を使って変換はしているようですが、AHKがIMEの状態を把握できないので親指シフトモードに切り替わらないのは同じでした。残念。 いったんは諦めてMinGW版のEmacsを使うことにしたのですが、ぐぐってみたら「 [Question] Possible to (properly) implement simultaneous (custom) Kana-input layout? #512 」というMozcに新下駄配列を実装する話が出てきました。 新下駄配列は知らなかったのでぐぐ...
続きを読む

親指シフト新下駄配列の可能性

Google日本語入力の「シフトキーでの入力切り替え」をオフにして、ローマ字テーブルに大文字で登録すると、登録されたとおりに出力されます。当たり前ですが。これで「L」に「l」とは別に「じ」や「しかし、」や「𝕏」を割り当てることができます。 NICOLAなどの親指シフトとは違って、たんに大文字かどうかを見ているだけなのでシフトキーの左右を区別はできませんが、いろいろな使い方が考えられそうです。例えば、「X」に「𝕏」を割り当てるとか、「A」に「∀」とか。「L」に「しかし、」とかの接続詞を割り当てて入力時間の短縮もできるかもしれません。「L」に「じ」を割り当てて、「じ」に割り当てられている場所に別の文字なども考えられそうです。左右を混ぜて、シフトキーを押している間だけ全く別のマップでアルペジオとかも考えられます。覚えるのが大変ですけど。数字キーに割り当てられている文字をアルファベットに割り当てれば40%キーボードでも3点押しなしに入力することもできます。 このように、いろいろな可能性がありますが、実はまだ使っていません。まだ新下駄配列に慣れていないので、それどころじゃないんですよね。まずは新下駄配列に慣れて、その中で困ったことが起きたら解決に使う感じかな？
続きを読む