khibino

Theorem plus_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)    +  reflexivity.
  (* Case "n = S n'". *) +  simpl. rewrite -> IHn'. reflexivity.  Qed.

(** **** 練習問題: ★★★★, recommended (binary) *)
(** これまでとは異なる、通常表記の自然数ではなく2進のシステムで、自然数のより効率的な表現を考えなさい。それは自然数をゼロとゼロに1を加える加算器からなるものを定義する代わりに、以下のような2進の形で表すものです。2進数とは、
      - ゼロであるか,
      - 2進数を2倍したものか,

khibino

{--# OPTIONS_GHC -Wno-name-shadowing #-}

import Control.Concurrent (forkIO)
import Control.Concurrent (threadDelay)
import Control.Concurrent.Chan (Chan, newChan, readChan, writeChan)
import Control.Monad (void, replicateM, replicateM_)
import System.IO (BufferMode (LineBuffering), hSetBuffering, stdout)

-----

khibino

module Language where
import Utils

import Prelude hiding (seq)

data Expr a
   = EVar Name               -- ^ Variables
   | ENum Int                -- ^ Numbers
   | EConstr Int Int         -- ^ Constructor tag arity
   | EAp (Expr a) (Expr a)   -- ^ Applications

khibino

-- Example implementation for Meta-Theory à la Carte

-- data Fix (f : Set -> Set) : Set where
--   inF : f (Fix f) -> Fix f

open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat

khibino

f1029 = [7, 123229502148636]

f1030 = [2, 7]

f1031 = [4, 21855]

f1032 = [7, 560803991675135]

f1034 = [5, 33554431]

khibino

import Numeric.Natural (Natural)

type Nat = Natural

data NatListF a = Nil | Cons (Nat, a) deriving Show
newtype NatList = In (NatListF NatList) deriving Show

out :: NatList -> NatListF NatList
out (In x) = x

khibino

module CoYoneda where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Data.Product using (_×_; proj₁; proj₂; ∃; _,_)


pattern _⊢_⊗_ a k x = (a , k , x) --  ∃ (λ a → (a → r) × f a)

module CovariantMap

khibino

module Yoneda where

open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

{- specialized Morphism to Haskell function,
   specialized Functor to Haskell Functor,
   Proof of Yoneda Lemma -}
{- 射を Haskell の関数に、
   関手を Haskell の Functor に限定した場合の

khibino

{-# LANGUAGE FlexibleInstances #-}

import Data.DList
import Control.Monad.Trans.Writer (Writer)
import Data.Functor.ProductIsomorphic

data PH a = PH

newtype WithPhT r a =
  WithPhT { runWithPhT :: Writer (DList Int) (r a)  }

khibino

open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import RSC

-- Basic data-types