CoqのtacticとAgdaの対応

CoqAgdaCorrespond.agda

module CoqAgdaCorrespond where

import Data.Nat as Nat
import Data.Bool as Bool
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)

-- Moduleはmodule
-- Definitionは非再帰関数
-- Fixpointは再帰関数
-- Example/Theoremなどは関数の型
-- Proof ... Qed は関数

module MatchWith where
  -- match ... with ... end は 関数パターンマッチ
  open Nat hiding (pred)
  open Bool

  even : ℕ → Bool
  even 0 = true
  even 1 = false
  even (suc (suc n)) = even n

  -- あるいは，制約はあるがFunction.case_of_など
  open import Function
  even' : ℕ → Bool
  even' n = case n of λ
    { 0 → true
    ; 1 → false
    ; (suc (suc n)) → even n
    }


module ReflexivityTactic where
  -- reflexivityはRelation.Binary.PropositionalEquality.refl

  A≡A : ∀ {a} {A : Set a} → A ≡ A
  A≡A = refl


module SimplTactic where
  -- simplは特に対応が無く適宜挟まれる？
  open Nat

  0+0≡0 : 0 + 0 ≡ 0
  0+0≡0 = refl


module InductiveDataType where
  -- Inductiveは普通のデータ定義
  -- Type は Set/Set₀
  data Foo : Set₀ where
  data Bar : Set where
  data nat : Set where
    zero : nat
    suc : nat → nat


module EvalSimplCommand where
  -- Eval simpl in ~ は agda-mode の c-c c-n
  -- c-c c-n すると "Expression:   [∏]"と式の入力を促され，
  -- 入力してEnterで式の評価結果が表示される
  -- また，ゴール内で式を書いて c-c c-n すると，
  -- そのゴール内に書いた式が評価されて表示される．


module Admitted where
  -- Admittedはpostulate
  postulate
    -- 直観主義では証明できないパース
    peirce : (P Q : Set) → ((P → Q) → P) → P


module CheckCommand where
  -- Check は agda-mode の c-c c-d
  -- c-c c-d すると "Expression:   [∏]"と式の入力を促され，
  -- 入力してEnterで式の型が表示される
  -- また，ゴール内で式を書いて c-c c-d すると，
  -- そのゴール内に書いた式の型が表示される．


module Notation where
  -- Notationに相当する機能は無い．
  -- が，あえて何がコレに対応するかというと，
  -- prefix/suffix/mixfix operator とそれらの結合優先度


module IntrosTactic where
  -- intro/introsはゴールのλ抽象を1から数段外して仮定に加える
  open Nat

  0+n≡n : ∀ n → 0 + n ≡ n
  -- 0+n≡n = ?
  -- に対してゴールは (n : ℕ) → 0 + n ≡ n
  -- そのまま証明すると，証明オブジェクトは
  0+n≡n = λ n → refl

  -- 0+n≡n = ? に対し
  -- intros n 相当を挟むと以下のように
  -- 0+n≡n' n = ?
  -- で証明することになる．

  0+n≡n' : ∀ n → 0 + n ≡ n
  -- 0+n≡n' n = ?
  -- に対してゴールは 0 + n ≡ n
  -- そのまま証明すると，証明オブジェクトは
  0+n≡n' n = refl


module RewriteTactic where
  -- rewrite (→) H は rewrite H
  open Nat

  n≡m→n+n≡m+m : ∀ n m → n ≡ m → n + n ≡ m + m
  n≡m→n+n≡m+m n m n≡m
    rewrite n≡m
          = refl -- ゴールは m + m ≡ m + m


  -- rewrite ← H は rewrite Relation.Binary.PropositionalEquality.sym H
  open PropEq using (sym)
  n≡m→n+n≡m+m' : ∀ n m → n ≡ m → n + n ≡ m + m
  n≡m→n+n≡m+m' n m n≡m
    rewrite sym n≡m
          = refl -- ゴールは n + n ≡ n + n


module DestructTactic where
  -- destruct は agda-mode c-c c-c で，結局はパターンマッチになる．
  open Bool

  b∧c≡t→b≡t : ∀ b c → b ∧ c ≡ true → b ≡ true
  -- b∧c≡t→b≡t b c b∧c≡t = ? まで書いて c-c c-l
  -- b∧c≡t→b≡t b c b∧c≡t = { }0 となるので，このゴールの中で c-c c-c
  -- すると "pattern variables to case:   [∏]"となるので対象の変数bを入れEnter
  -- b∧c≡t→b≡t true c b∧c≡t = { }0
  -- b∧c≡t→b≡t false c b∧c≡t = { }1
  -- のようにbについて場合分けされる．
  -- b∧c≡t→b≡t true c b∧c≡t = { }0 のほうのゴールはtrue ≡ true なので refl
  b∧c≡t→b≡t true c b∧c≡t = refl
  -- b∧c≡t→b≡t false c b∧c≡t = { }1 のほうのゴールはfalse ≡ true なので ⊥ になるはず，
  -- このとき仮定b∧c≡tがもう成立していないハズなので．さらに c-c c-c で b∧c≡t すると．
  b∧c≡t→b≡t false c ()
  -- と仮定が空(⊥)にマッチして証明完了．

  -- ゴールに対象の変数を書いてから c-c c-c でもよい．
  -- また，複数の変数を同時に場合分けすることもできる．
  b∧c≡t→b≡t' : ∀ b c → b ∧ c ≡ true → b ≡ true
  -- b∧c≡t→b≡t' b c b∧c≡t = ? まで書いて c-c c-l
  -- b∧c≡t→b≡t' b c b∧c≡t = { }0 となるので，このゴールの中に次のように書き，
  -- b∧c≡t→b≡t' b c b∧c≡t = {b b∧c≡t }0 そして c-c c-lすると，
  -- b∧c≡t→b≡t' true .true refl = { }
  -- b∧c≡t→b≡t' false c ()
  -- と場合分けされ後者のケースは即終わる．前者はrefl入れて終わり．
  b∧c≡t→b≡t' true .true refl = refl
  b∧c≡t→b≡t' false c ()

  -- イントロパターンに相当するものは無くAgdaが適当に変数名を補完する．
  -- 気に入らなければ場合分け後に直す．


module InductionTactic where
  -- induction は destruct と同じくc-c c-c
  -- 証明オブジェクトは特定の引数に対する構造再帰関数となる．
  open Nat

  n+0≡n : ∀ n → n + 0 ≡ n
  -- c-c c-c で n について場合分け
  -- base case
  n+0≡n zero = refl
  -- step case
  n+0≡n (suc n)
    rewrite n+0≡n n -- nについて再帰したものは使ってOK(=使っても停止する)
          = refl


module AssertTactic where
  -- assert は where で補助関数として取り出すだけ
  -- イントロパターンに相当するものは無いが，
  -- どのみちwhereなので適当に名付けることになる．


module ReplaceTactic where
  -- replace t with u は rewrite (仮定等から t ≡ u を作る式) に対応