314maro

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (succ)

newtype Church = Church (forall t. (t -> t) -> (t -> t))

zero :: Church
zero = Church $ \_ z -> z
succ :: Church -> Church
succ (Church cn) = Church $ \f -> f . cn f

314maro

Module Q21.
Require Import Classical.
Lemma ABC_iff_iff : forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
intros.
pose (HA := classic A). pose (HB := classic B). pose (HC := classic C).
destruct HA; destruct HB; destruct HC; tauto.
Qed.

Goal

314maro

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

i :: Int -> Int
i = id

puti :: Int -> Stack -> Stack
puti i (Stack os vs) = Stack os (i : vs)

putop :: (Int -> Int -> Int) -> Stack -> Stack
putop op (Stack os vs) = Stack (op : os) vs

314maro

Lensについて

自分用のメモという感じ

Lensの定義を見てみよう.

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

Lensを作ってみよう. sがforall f.の外にあっても問題ないので外に出しておこう. その方が今は都合がいい. つまりs t a b はそれぞれなんらかの型として,

314maro

Section SupInf.
Variable S : Type.
Variable R : S -> S -> Prop.
Infix ">=" := R.
Infix "<=" := (fun x y => y >= x).
Definition subset : Type := S -> Prop.
Definition element (X : subset) (x : S) : Prop := X x.
Definition upper_bound (X : subset) (u : S) : Prop :=
  forall x, element X x -> u >= x.
Definition lower_bound (X : subset) (u : S) : Prop :=

314maro

Module Wau_san.
Require Import ZArith.
Theorem wau_san : (forall m n, (m > 1) -> ~ ((m | n) /\ (m | n+1)))%Z.
Proof.
intros m n Hm H.
destruct H as [Hmn Hm1n].
assert (H : (m | n+1 - n)%Z) by (apply Z.divide_sub_r; assumption).
replace (n+1 - n)%Z with 1%Z in H by ring.
apply Z.divide_1_r in H.
destruct H as [H|H]; subst; inversion Hm.

314maro

Haskellでは厳しそう...

対象の文字列全体の集合の部分集合、射はその間の関数
`string -> bool` と `forall (x y : string -> bool) (s : string), x s = true -> exists t : string, y t = true`

Templの定義面倒くさそう

314maro

#include <stdio.h>

int main(void) {
  int x, a, b;
  scanf("%x",&x);
  if (x < 0x20 || 0xDF < x) {
    printf("error: %d\n", x);
    return -1;
  }
  a = (x & 0xE0) >> 5;

314maro

Module Q16.
Definition tautology : forall P : Prop, P -> P
  := fun _ p => p.

Definition Modus_tollens : forall P Q : Prop, ~Q /¥ (P -> Q) -> ~P
  := fun _ _ h p => let (q,f) := h in q (f p).

Definition Disjunctive_syllogism : forall P Q : Prop, (P ¥/ Q) -> ~P -> Q
  := fun _ _ pq np => match pq with
  | or_introl p => match np p with end

314maro

import Control.Applicative
import Data.List (stripPrefix, intercalate)

sub :: Eq a => [a] -> [a] -> [a] -> Maybe [a]
sub from to s = (to ++) <$> stripPrefix from s <|> rec s
  where
    rec [] = Nothing
    rec (x:xs) = (x :) <$> sub from to xs

step :: [(String,String)] -> String -> Maybe String