C++で定理証明(C++ Advent Calendar 3日目)

本文ははてなが使えないすぎるので、まだテキストで張った方がマシでした
http://www.coins.tsukuba.ac.jp/~s0811425/adventc++3.txt

#include <iostream>
#include <typeinfo>
#include <cxxabi.h>
#include <type_traits>
#include <functional>
#include <boost/mpl/if.hpp>
using namespace std;

char* demangle(const char *ty)
{
    int status;
    return abi::__cxa_demangle(ty,0,0,&status);
}
template<typename T>T sucks(){}
template<typename T>
char* to_str()
{
    return demangle(typeid(sucks<T>()).name());
}


template<class L,class R>
struct eq
{
private:
    eq(){}
};

template<class T>
eq<T,T> eq_refl(T t){}
template<class L,class R>
eq<R,L> eq_symm(eq<L,R> obj){}
template<class A,class B,class C>
eq<A,C> eq_trans(eq<A,B> ab,eq<B,C> bc){}
template<class T>
eq<T,typename T::val> eq_unfold(T t){}
template<class A,class B,template<class>class F>
eq<F<A>,F<B> > f_equal(eq<A,B> ab){}

template<class T,class L,class R>
struct Rewrite
{
    typedef typename boost::mpl::if_<is_same<T,L>,R,T>::type type;
    static type rewrite(T obj,eq<L,R> lr){}
};
template<template<class>class F,class Arg,class L,class R>
struct Rewrite<F<Arg>,L,R>
{
    typedef typename boost::mpl::if_<is_same<Arg,L>,R,typename Rewrite<Arg,L,R>::type>::type Arg_;
    typedef F<Arg_> type;
    static type rewrite(F<Arg> obj,eq<L,R> lr){}
};
template<template<class,class>class F,class Arg1,class Arg2,class L,class R>
struct Rewrite<F<Arg1,Arg2>,L,R>
{
    typedef typename boost::mpl::if_<is_same<Arg1,L>,R,typename Rewrite<Arg1,L,R>::type>::type Arg1_;
    typedef typename boost::mpl::if_<is_same<Arg2,L>,R,typename Rewrite<Arg2,L,R>::type>::type Arg2_;
    typedef F<Arg1_,Arg2_> type;
    static type rewrite(F<Arg1,Arg2> obj,eq<L,R> lr){}
};
template<template<int,class>class C,int i,class Arg,class L,class R>
struct Rewrite<C<i,Arg>,L,R>
{
    typedef typename boost::mpl::if_<is_same<Arg,L>,R,typename Rewrite<Arg,L,R>::type>::type Arg_;
    typedef C<i,Arg_> type;
    static type rewrite(C<i,Arg> obj,eq<L,R> lr){}
};

template<class T,class L,class R>
typename Rewrite<T,L,R>::type rewrite_tactic(T obj,eq<L,R> lr){}

struct List{};
struct Nil : List{};
template<int i,class T>
struct Cons : List{
    static_assert(!is_same<List,T>::value,"T should be List's subtype");
    static_assert(is_base_of<List,T>::value,"T should be List's subtype");
};

template<template<class>class P>
struct list_ind
{
public:
    static const int i = int();
    struct SomeList : List{};
    struct X : List{};

    typedef typename P<SomeList>::type hypo;
    typedef typename P<Cons<i,SomeList> >::type self;
    typedef function<self (hypo)> ind;

    static typename P<X>::type build(typename P<Nil>::type basepr,ind pr){}
};

//append
template<class L,class R>struct app : List{
    typedef app<L,R> val;
};
//[] ++ y = y
template<class R>
struct app<Nil,R> : List
{
    typedef R val;
};
//(x :: xs) ++ y = x :: (xs ++ y)
template<int i,class L,class R>
struct app<Cons<i,L>,R> : List
{
    typedef Cons<i,typename app<L,R>::val> val;
};


//[] ++ l = l
template<typename V>
struct app_nil_l_aux
{
    typedef eq<app<Nil,V>,V> type;
};

struct app_nil_l2
{
    typedef typename list_ind<app_nil_l_aux>::X X;

    static eq<app<Nil,X>,X> proof(){
	eq<app<Nil,X>::val,X> tmp = eq_refl(X());
	eq<app<Nil,X>,app<Nil,X>::val> tmp2 = eq_unfold(app<Nil,X>());
	return eq_trans(tmp2,tmp);
    }
};
//l ++ [] = l
template<typename V>
struct app_l_nil_aux{
    typedef eq<app<V,Nil>,V> type;
};

struct app_l_nil
{
    typedef list_ind<app_l_nil_aux>::SomeList X;
    typedef list_ind<app_l_nil_aux>::X L;

    static list_ind<app_l_nil_aux>::self step(list_ind<app_l_nil_aux>::hypo hyp){
	const int i = list_ind<app_l_nil_aux>::i;
	
	//(X ++ []) = X
	eq<app<X,Nil>,X> x = hyp;
	
	//((i :: X) ++ []) = i :: (X ++ [])
	eq<app<Cons<i,X>,Nil>::val,Cons<i,app<X,Nil>::val> > simpled = eq_refl( app<Cons<i,X>,Nil>::val() );
    
    //(X ++ []) = (X ++ []) fold - unfold
    eq<app<X,Nil>::val,app<X,Nil> > tmp1 = eq_refl(app<X,Nil>());
    
    //simpledの型に出現する app<X,Nil>::val を、app<X,Nil>で置き換え!!
    //((i :: X) ++ []) = i :: (X ++ [])    
    eq<app<Cons<i,X>,Nil>::val,Cons<i,app<X,Nil> > > tmp2 = rewrite_tactic(simpled,tmp1);
    //((i :: X) ++ []) = i :: (X ++ [])
    eq<app<Cons<i,X>,Nil>,Cons<i,app<X,Nil> > > tmp3 = eq_trans(eq_unfold(app<Cons<i,X>,Nil>()),tmp2);
    //((i :: X) ++ []) = i :: X
    eq<app<Cons<i,X>,Nil>,Cons<i,X> > goal = rewrite_tactic(tmp3,hyp);
    return goal;
    }

    static eq<app<Nil,Nil>,Nil> base(){
	eq<app<Nil,Nil>::val,Nil> app_nil_nil = eq_refl(Nil());
	eq<app<Nil,Nil>,app<Nil,Nil>::val> unfolded = eq_unfold(app<Nil,Nil>());
	eq<app<Nil,Nil>,Nil> pr = eq_trans(unfolded,app_nil_nil);
	return pr;
    }

    static eq<app<L,Nil>,L> proof(){
	list_ind<app_l_nil_aux>::ind f = &step;
	
	app_l_nil_aux<L>::type pr = list_ind<app_l_nil_aux>::build(base(),step);
	return pr;
    }
};

template<class L,template<class>class P>
static typename P<L>::type subst(typename P<typename list_ind<P>::X>::type pr){}

int main()
{
    typedef Cons<1,Cons<2,Cons<3,Cons<4,Nil> > > > l;
    eq<app<l,Nil>,l> inst1 = subst<l,app_l_nil_aux>(app_l_nil::proof());
    eq<app<Nil,l>,l> inst2 = subst<l,app_nil_l_aux>(app_nil_l2::proof());
}
Inductive IList : Set :=
  | nil : IList
  | cons : nat -> IList -> IList.

Fixpoint app (l r : IList) : IList :=
  match l with
    | nil => r
    | cons v rest => cons v (app rest r)
  end.

(*
app_nil_l < intros.
1 subgoal
  
  l : IList
  ============================
   app nil l = l

app_nil_l < simpl.
1 subgoal
  
  l : IList
  ============================
   l = l

app_nil_l < trivial.
Proof completed.

app_nil_l < Qed.
intros.
simpl.
trivial.

app_nil_l is defined
*)
Theorem app_nil_l : forall (l : IList) , app nil l = l.
Proof.
intros.
simpl.
trivial.
Qed.

(*
app_l_nil < Show.
1 subgoal
  
  ============================
   forall l : IList, app l nil = l

app_l_nil < intro.
1 subgoal
  
  l : IList
  ============================
   app l nil = l

app_l_nil < induction l.
2 subgoals
  
  ============================
   app nil nil = nil

subgoal 2 is:
 app (cons n l) nil = cons n l

app_l_nil < trivial.
1 subgoal
  
  n : nat
  l : IList
  IHl : app l nil = l
  ============================
   app (cons n l) nil = cons n l

app_l_nil < simpl.
1 subgoal
  
  n : nat
  l : IList
  IHl : app l nil = l
  ============================
   cons n (app l nil) = cons n l

app_l_nil < Check f_equal.
f_equal
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

app_l_nil < apply f_equal.
1 subgoal
  
  n : nat
  l : IList
  IHl : app l nil = l
  ============================
   app l nil = l

app_l_nil < trivial.
Proof completed.
*)
Theorem app_l_nil : forall (l : IList) , app l nil = l.
Proof.
intro.
induction l.
 trivial.
 
 simpl.
 apply f_equal.
 trivial.
Qed.