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.