khibino

{- Conceptual Mathematics, Session 10, exercises -}

module Session10 where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; _≢_)
open import Data.Product using (∃; _,_; _×_)
open import Relation.Nullary using (¬_)

-- contraposition : ∀ {l} -> ∀ {A B : Set l} -> (A -> B) -> ¬ B -> ¬ A
-- contraposition f nb a = nb (f a)

khibino

open import Agda.Builtin.Equality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.Core using (sym; trans; _≢_)
-- open import Data.Nat.Base
open import Data.Nat.Base
  using (ℕ; zero; suc; _+_; _*_; s≤s; z≤n; _≤_; _<_; _>_;
        Ordering; less; equal; greater; compare)
open import Data.Nat.Properties using (+-identityʳ; +-assoc; ≤-trans; m≤m+n; m≢1+m+n; *-cancelˡ-≡)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; _,_)

khibino

{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses,
             FunctionalDependencies, FlexibleInstances, FlexibleContexts,
             OverloadedLabels, ScopedTypeVariables #-}

import GHC.OverloadedLabels (IsLabel(..))
import GHC.TypeLits (Symbol)

data Label (l :: Symbol) = Put

class Belongs a l b | l b -> a where

khibino

-- printf like function, formatting package method

newtype Format r a = Format ((ShowS -> r) -> a)

string :: Format r (String -> r)
string = Format $ \k s -> k (s ++)

int :: Format r (Int -> r)
int = Format $ \k i -> k (show i ++)

khibino

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

----------
-- List の定義

infixr 50 _∷_

data List (A : Set) : Set where
  [] : List A

khibino

open import Agda.Primitive using (lsuc)
open import Data.Bool using (Bool)

Fix : ∀{l} -> (Set l → Set l) → Set (lsuc l)
Fix f = ∀ k → (f k → k) → k

T : ∀{l} → Set l → Set l
T a = (a → Bool) → Bool

X : Set1

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) *)

(* (a) *)
Inductive bin : Type :=

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