Skip to content

Instantly share code, notes, and snippets.

Avatar

日比野 啓 (Kei Hibino) khibino

View GitHub Profile
@khibino
khibino / Session10.agda
Last active January 18, 2023 13:25
Conceptual Mathematics, Session 10, exercises
View Session10.agda
{- 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
khibino / div.agda
Last active November 16, 2022 08:25
View div.agda
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 (_×_; _,_)
View polySum.hs
{-# 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
View format.hs
-- 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 ++)
View ListMonad.agda
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
View set1.agda
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
View bin2.v
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 :=
View bin.v
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倍したものか,
View prunner.hs
{--# 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)
-----
View Language.hs
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