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

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

import Data.Int (Int32)
import Database.Record.Instances ()
import Database.Relational.Query

hello :: Relation () (Int32, String)
hello =  relation $ return (value 0 >< value "Hello")

world :: Relation () (Int32, String)
world =  relation $ return (value 0 >< value "World!")

khibino

foo :: Kleisli QuerySimple () (Projection Flat (Ex1, Maybe Ex1))
foo =  proc () -> do
  x <- query      -< ex1
  y <- queryMaybe -< ex1
  wheres -< just (x ! eid') .=. y ?! eid'
  returnA -< x >< y

khibino

Inductive Mod3' : nat -> Prop :=
| zero' : forall n k, n = 3 * k     -> Mod3' n
| one'  : forall n k, n = 3 * k + 1 -> Mod3' n
| two'  : forall n k, n = 3 * k + 2 -> Mod3' n
.


Lemma nat_mod3' : forall n, Mod3' n.
Proof.
  induction n as [| n1 IHn ].