314maro

import Control.Applicative
import Control.Monad.State
import Data.Char

data Op = Add | Sub | Mul | Div | LParens
  deriving (Show)
priority :: Op -> Int
priority Add = 2
priority Sub = 2
priority Mul = 3

314maro

Module Q0_2.
  Theorem tautology : forall P : Prop, P -> P.
  Proof.
    intros P H.
    assumption.
  Qed.
  (*
  Theorem wrong : forall P : Prop, P.
  Proof.
    intros P.

314maro

Module Q6.
  Require Import Arith.

  Goal forall x y, x < y -> x + 10 < y + 10.
  Proof.
    intros.
    apply plus_lt_compat_r.
    assumption.
  Qed.
End Q6.

314maro

Module Q11.
  Require Import Arith.
  Fixpoint sum_odd(n:nat) : nat :=
    match n with
    | O => O
    | S m => 1 + m + m + sum_odd m
    end.

  Goal forall n, sum_odd n = n * n.
  Proof.

314maro

#include <iostream>
#include <vector>
#include "vm.hpp"

int main() {
  const unsigned char offset = 0x03, loopend = 0x27;
  // 0x00:ptr, 0x01:pc, 0x02:len
  std::vector<unsigned char> inst =
    { 0x02, 0x00, 0x02, 0x00, 0x10 // store
    , 0x02, 0x01, 0x02, offset, 0x10 // store

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

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

#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

Haskellでは厳しそう...

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

Templの定義面倒くさそう

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.