Logics.(Problems and Answer, includes a template which judge the given logic express is a tautology)

logics.d

// ¬P
bool not(bool p) {
  return !p;
}

// P ∧Q
bool and(bool p, bool q) {
  return p && q;
}

// P | Q
bool nand(bool p, bool q) {
  return not(p.and(q));
}

// P ∨Q
bool or(bool p, bool q) {
  return p || q;
}

// P ▽Q ⇔¬(P ∧Q) ∧(P ∨Q)
bool xor(bool p, bool q) {
  return not(p.and(q)).and(p.or(q));
}

// P ⇒Q (⇔¬(P ∧¬Q))
bool imp(bool p, bool q) {
  return not(p.and(not(q)));
}

// P ≡Q 
bool eq(bool p, bool q) {
  return (p.and(q)).or(not(p).and(not(q)));
}

// ---------------------------------

// p ∨¬p
bool excludedMiddle(bool p) {
  return p | !p;
}

// ((P ⇒Q) ∧P) ⇒Q
bool moduesPonens(bool p, bool q) {
  return ((p.imp(q)).and(p)).imp(q);
}

// (P ⇒Q) ⇒(¬Q ⇒¬P)
bool cont(bool p, bool q) {
  return (p.imp(q)).imp(not(q).imp(not(p)));
}

//------------------------------------

import std.algorithm,
       std.typecons,
       std.string,
       std.traits,
       std.range,
       std.meta;

// copy from phobos std.meta, for my machine's phobos doesn't contain this template
template Repeat(size_t n, TList...) if (n > 0)
{
    static if (n == 1)
    {
        alias Repeat = AliasSeq!TList;
    }
    else static if (n == 2)
    {
        alias Repeat = AliasSeq!(TList, TList);
    }
    else
    {
        alias R = Repeat!((n - 1) / 2, TList);
        static if ((n - 1) % 2 == 0)
        {
            alias Repeat = AliasSeq!(TList, R, R);
        }
        else
        {
            alias Repeat = AliasSeq!(TList, TList, R, R);
        }
    }
}

// returns whether the logic expression is a tautology
bool isTautology(alias expr)()
  if (
      isCallable!expr
   && arity!expr > 0
   && is(Parameters!(expr) == Repeat!(arity!expr, bool))
   && is(ReturnType!expr == bool)
    ) {
  enum N = arity!expr;

  static if (N > 1) {
    mixin("return cartesianProduct(tuple(" ~ 
            "[true, false]".repeat(N).join(",")
            ~ ").expand).all!(tup => expr(tup.expand));");
  } else {
    return [true, false].all!(b => expr(b));
  }
}

unittest {
  // not
  assert(not(true)  == false);
  assert(not(false) == true);

  // or
  assert (true.or(true)   == true);
  assert (true.or(false)  == true);
  assert (false.or(true)  == true);
  assert (false.or(false) == false);

  // xor
  assert (true.xor(true)   == false);
  assert (true.xor(false)  == true);
  assert (false.xor(true)  == true);
  assert (false.xor(false) == false);

  // and
  assert (true.and(true)   == true);
  assert (true.and(false)  == false);
  assert (false.and(true)  == false);
  assert (false.and(false) == false);

  // nand
  assert (true.nand(true) == false);
  assert (true.nand(false) == true);
  assert (false.nand(true) == true);
  assert (false.nand(false) == true);

  // imp
  assert (true.imp(true)   == true);
  assert (true.imp(false)  == false);
  assert (false.imp(true)  == true);
  assert (false.imp(false) == true);

  // eq
  assert (true.eq(true)   == true);
  assert (true.eq(false)  == false);
  assert (false.eq(true)  == false);
  assert (false.eq(false) == true);


}

import std.stdio;

void main() {
  // 問. シェファーの棒(|, nand)を用いて
  // - 否定(¬, not)
  // - 連言(∧, and)
  // - 両立的選言(∨, or)
  // - 排他的選言(▽, xor)
  // - 条件法(⇒, imp)
  // - 同値(⇔, eq)
  // を構成せよ。

  // ¬P ⇔P|P
  assert (
      isTautology!((bool p) => (not(p)).eq(
        p.nand(p)
      ))
    );

  // P ∧Q ⇔(P|Q)|(P | Q) 連言
  assert (
      isTautology!((bool p, bool q) => (p.and(q)).eq(
        (p.nand(q)).nand(p.nand(q))
      ))
    );

  // P ∨Q ⇔(P|P)|(Q|Q) : 両立的選言
  assert (
      isTautology!((bool p, bool q) => (p.or(q)).eq(
        (p.nand(p)).nand(q.nand(q))
      ))
    );

  // P ▽Q ⇔((P|Q)|((P|P)|(Q|Q)))|(P|Q)|((P|P)|(Q|Q)) : 排他的選言
  assert (
      isTautology!((bool p, bool q) => (p.xor(q)).eq(
        (
         (p.nand(q)).nand((p.nand(p)).nand(q.nand(q)))
        ).nand(
         (p.nand(q)).nand((p.nand(p)).nand(q.nand(q)))
        )
      ))
    );

  // P ⇒Q ⇔P|(Q|Q) : 条件法
  assert (
      isTautology!((bool p, bool q) => (p.imp(q)).eq(
        p.nand(q.nand(q))
      ))
    );

  // P ≡Q ⇔(P|Q)|((P|P)|(Q|Q)): 同値
  assert (
      isTautology!((bool p, bool q) => (p.eq(q)).eq(
        (p.nand(q)).nand((p.nand(p)).nand(q.nand(q)))
      ))
    );


  //問. 否定¬(not)と両立的選言∨(or)を用いて
  // - 連言(∧, and)
  // - 排他的選言(▽, xor)
  // - 条件法(⇒, imp)
  // - 同値(⇔, eq)
  //を構成せよ

  // P ∧Q ⇔¬(¬P ∨¬Q) 連言
  assert (
      isTautology!((bool p, bool q) => (p.and(q)).eq(
        not(not(p).or(not(q)))
      ))
    );

  // P ▽Q ⇔¬(¬(¬P ∨¬Q) ∨(¬P ∨Q)) : 排他的選言
  assert (
      isTautology!((bool p, bool q) => (p.xor(q)).eq(
        not(not(not(p).or(not(q))).or(not(p.or(q))))
      ))
    );

  // P ⇒Q ⇔¬P ∨Q : 条件法
  assert (
      isTautology!((bool p, bool q) => (p.imp(q)).eq(
        not(p).or(q)
      ))
    );


  // P ≡Q ⇔¬(¬P ∨¬Q) ∨(¬(P ∨Q)) : 同値
  assert (
      isTautology!((bool p, bool q) => (p.eq(q)).eq(
        not(not(p).or(not(q))).or(not(p.or(q)))
      ))
    );


  //問. 否定¬(not)と条件法⇒(imp)を用いて
  // - 両立的選言(∨, or)
  // - 排他的選言(▽, xor)
  // - 連言(∧, and)
  // - 同値(⇔, eq)
  //を構成せよ

  // P ∨Q ⇔¬P ⇒Q : 両立的選言
  assert (
      isTautology!((bool p, bool q) => (p.or(q)).eq(
        not(p).imp(q)
      ))
    );

  // P ▽Q ⇔¬(P ⇒¬Q) ⇒¬(¬P ⇒Q) : 排他的選言
  assert (
      isTautology!((bool p, bool q) => (p.xor(q)).eq(
        not(p.imp(not(q)).imp(not(not(p).imp(q))))
      ))
    );

  // P ∧Q ⇔¬(P ⇒¬Q) : 連言
  assert (
      isTautology!((bool p, bool q) => (p.and(q)).eq(
        not(p.imp(not(q)))
      ))
    );

  // P ≡Q ⇔(P ⇒¬Q) ⇒¬(¬P ⇒ Q) : 同値
  assert (
      isTautology!((bool p, bool q) => (p.eq(q)).eq(
        (p.imp(not(q))).imp(not(not(p).imp(q)))
      ))
    );

  //問. 否定¬(not)と連言∧(and)を用いて
  // - 両立的選言(∨, or)
  // - 排他的選言(▽, xor)
  // - 条件法(⇒, imp)
  // - 同値(⇔, eq)
  //を構成せよ

  // P ∨Q ⇔¬(¬P ∧¬Q) : 両立的選言
  assert (
      isTautology!((bool p, bool q) => (p.or(q)).eq(
        not(not(p).and(not(q)))
      ))
    );

  // P ▽Q ⇔¬(P ∧Q) ∧¬(¬P ∧¬Q): 排他的選言
  assert (
      isTautology!((bool p, bool q) => (p.xor(q)).eq(
        not(p.and(q)).and(not(not(p).and(not(q))))
      ))
    );

  // P ⇒Q ⇔¬(P ∧¬Q): 条件法
  assert (
      isTautology!((bool p, bool q) => (p.imp(q)).eq(
        not(p.and(not(q)))
      ))
    );

  // P ≡Q ⇔¬(¬(P ∧Q) ∧¬(¬P ∧¬Q)): 同値
  assert (
      isTautology!((bool p, bool q) => (p.eq(q)).eq(
        not(not(p.and(q)).and(not(not(p).and(not(q)))))
      ))
    );
}