proof.in

set(auto).
set(prolog_style_variables).

formulas(sos).
  % identities and composites

  % arrow(A,A,identity(A)).

  -arrow(A,B,F) | -arrow(B,C,G) | arrow(A,C,compose(G,F)).

  % products
  arrow(and(A,B),A,leftAnd(A,B)).
  arrow(and(A,B),B,rightAnd(A,B)).

  -arrow(C,A,F) | -arrow(C,B,G) | arrow(C,and(A,B),product(F,G)).

  % coproducts
  arrow(A,or(A,B),leftOr(A,B)).
  arrow(B,or(A,B),rightOr(A,B)).

  -arrow(A,C,F) | -arrow(B,C,G) | arrow(or(A,B),C,coproduct(F,G)).

  % exponentials
  arrow(and(if(B,C),B),C,eval(B,C)).

  -arrow(and(A,B),C,F) | arrow(A,if(B,C),curry(F)).

  % This is derivable, but it's hard to derive when we need it.  For 
  % term weighting, it might be preferable to simply use an `uncurry` 
  % function and rewrite it manually later.
  % -arrow(A,if(B,C),F) | arrow(and(A,B),C,uncurry(F)).
  % uncurry(F) = compose(eval(B,C),product(compose(F,leftAnd(A,B)),rightAnd(A,B))).


  %--------------------
  % provable results

  % -- unproduct arrows, finds "compose(leftAnd(b,c),f)"
  %
  % arrow(a,and(b,c),f). -arrow(a,b,G) # answer(G) .

  % -- uncoproduct arrows, finds "compose(f,leftOr(a,b))"
  %
  % arrow(or(a,b),c,f). -arrow(a,c,G) # answer(G).

  % -- uncurry arrows, finds "compose(eval(b,c),product(compose(f,leftAnd(a,b)),rightAnd(a,b)))" 
  %
  % arrow(a,if(b,c),f). -arrow(and(a,b),c,G) # answer(G).

  % -- commutativity
  %
  % -arrow(and(a,b),and(b,a),G) # answer(G) . % finds "product(rightAnd(a,b),leftAnd(a,b))"
  % -arrow(or(a,b),or(b,a),G) # answer(G) .   % finds "coproduct(rightOr(b,a),leftOr(b,a))"

  % -- distributivity
  %
  % dist2 and dist3 are easy, but dist1 is hard, and might not complete.
  %
  % -arrow(and(or(a,b),c),or(and(a,c),and(b,c)),F) # answer(F) # label("dist1").
  % -arrow(or(and(a,b),c),and(or(a,c),or(b,c)),F) # answer(F) # label("dist2").
  % -arrow(or(and(a,c),and(b,c)),and(or(a,b),c),coproduct(F,G)) # answer([F,G]) # label("dist3").

  % -- disjunction elimination
  %
  % de1 is hard, but de2 finishes in about 1500 steps.
  %
  % -arrow(or(a,b),if(and(if(a,c),if(b,c)),c),FG) # answer(FG) # label("de1").
  % -arrow(or(a,b),if(and(if(a,c),if(b,c)),c),coproduct(F,G)) # answer([F,G]) # label("de2").
  %
  % these are similar, but use more conditionals and fewer product arrows. de4 finishes
  % in under 700 steps, but de3 just keeps running.
  % 
  % -arrow(or(a,b),if(if(a,c),if(if(b,c),c)),FG) # answer(FG) # label("de3").
  % -arrow(or(a,b),if(if(a,c),if(if(b,c),c)),coproduct(F,G)) # answer([F,G]) # label("de4").
  %
  % de5 is the final result we want, but no luck yet.
  %
  % -arrow(t,if(if(a,c),if(if(b,c),if(or(a,b),c))),F) # answer(F) # label("de5").
end_of_list.