(* Coq printing functions for model-checking justifications.
   Copyright (C) 2003, 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "coq_fun_h";
open "coq_term_h";
open "coq_model_h";
open "coq_kw_h";
open "gensym_h";
open "sort_h";

(*
fun coq_print_and_type (f as |[put, ...]|, and_prefix, n : int) =
    let fun pind () =
	    (put and_prefix; print f (pack n))
	val delimr = ref "["
	val ir = ref 0
    in
	put "\nInductive "; pind ();
	if n<>0
	    then (iterate
		    (put (!delimr);
		     delimr := ",";
		     put "H";
		     inc ir; print f (pack (!ir)))
		  |while !ir<n
		  end;
		    put ":Prop]")
	else ();
	    put " : Prop :=\n    "; put and_prefix; put "_intro : ";
	    ir := 0;
	    iterate
	      (put "H"; print f (pack (!ir)); put " -> ")
	    |while !ir<n
	    end;
	    if n<>0
		then (delimr := "("; ir := 0;
		      iterate
			(put (!delimr); delimr := " H";
			 print f (pack (!ir)))
		      |while !ir<n
		      end;
		      put ")")
	    else pind ();
		put ".\n"
    end;
*)

fun coq_print_or_type (ver, f as |[put, ...]|, or_prefix) =
    let val |[param_prolog, param_epilog, var_delim, ...]| =
	coq_keywords ver
	val pfvars = coq_print_f_vars (f, "")
	val pvars = coq_print_vars f
	memofun portype (n : int) =
		let val or_n = let val g as |[convert, ...]| =
				       outstring or_prefix
			       in
				   print g (pack n);
				   convert ()
			       end
		    val delimr = ref "    "
		    val ir = ref 0
		in
		    put "\nInductive "; put or_n;
		    (if n=0 then () else (put param_prolog;
					  pvars (var_delim, "H", n);
					  put ":Prop";
					  put param_epilog));
			 put " : Prop :=\n";
			 iterate
			   (put (!delimr); delimr := "  | ";
			    put or_n; put "_intro_"; inc ir; print f (pack (!ir));
			    put " : H"; print f (pack (!ir));
			    put " -> "; pfvars (or_n, "H", n); put "\n"
			    )
			 |while !ir<n
			 end;
			 put ".\n";
			 or_n
		end
    in
	portype
    end;

fun coq_print_inversion_P_f (ver, fd as |[put, ...]|,
			     portype (* typically coq_print_or_type (ver, fd, or_prefix) *),
			     fun_prefix, state_prefix,
			     rem_name, xname, term_type,
			     AUTO (auto, univ), CAN (autonamer, _)) =
    let val |[intros_tac, inversion_tac, apply_tac, trivial_tac, tauto_tac,
	      dot_tac, semi_tac, ...]|
	    = coq_keywords ver
	val pblocks = coq_print_blocks (ver, fd, state_prefix)
	val pPfvars = coq_print_P_f_vars (ver, fd, fun_prefix, state_prefix)
	memofun pinvPf (P, f, k) =
		if P inset univ
		    then let val rem = gensym rem_name
			 in
			     put "\nRemark "; put rem; put " : ";
			     coq_print_foralls (ver, fd) (xname, term_type, k);
			     pPfvars (P, f, xname, k);
			     put " -> True.\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put trivial_tac; put dot_tac;
			     put "\nQed.\n";
			     rem
			 end
		else let val blkls = if P inset auto
					 then let val fmap = ?auto P
					      in
						  if f inset fmap
						      then #1 (?fmap f)
						  else {}
					      end
				     else {}
			 val n = card blkls
			 val or_n = portype n
			 val rem = gensym rem_name
			 val ir = ref 0
			 val lispian = (case ver of
					    "7" => true
					  | _ => false)
		     in
			 put "\nRemark "; put rem; put " : ";
			 coq_print_foralls (ver, fd) (xname, term_type, k);
			 pPfvars (P, f, xname, k);
			 put " -> ";
			 if n=0
			     then put or_n
			 else (if lispian then put "(" else ();
			       put or_n;
			       put "\n";
			       iterate
				 (case [blk | blk in list blkl
						such that not (empty blk)] of
				      nil => put "    True"
				    | [{_}] => (put "    ";
						if lispian then ()
						    else put "(";
						pblocks ("", xname, blkl);
						if lispian then ()
						    else put ")"
						)
				    | _ => (put "    (";
					    pblocks (" /\\ ", xname, blkl);
					    put ")\n"))
			       | blkl in set blkls
			       end;
			       if lispian then put ")" else ());
			     put ".\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put inversion_tac; put "H"; put dot_tac;
			     put "\n";
			     iterate
			       (put "  "; put intros_tac; put dot_tac; put " ";
				put apply_tac; put or_n; put "_intro_";
				inc ir; print fd (pack (!ir));
				put semi_tac; put tauto_tac; put dot_tac;
				put "\n")
			     | blkl in set blkls
			     end;
			     put "Qed.\n";
			     rem
		     end
    in
	pinvPf
    end;

fun coq_print_ex_type (ver, f as |[put, ...]|, ex_prefix, xname) =
    let val |[param_prolog, param_delim, param_epilog,
	      forall_prolog, forall_midlog, ...]|
	= coq_keywords ver
	val pvars = coq_print_vars f
	memofun pextype (n : int) =
		let val ex_n = let val g as |[convert, ...]| = outstring ex_prefix
			       in
				   print g (pack n);
				   convert ()
			       end
		    val ir = ref 0
		in
		    put "\nInductive "; put ex_n;
		    put " "; put param_prolog;
		    put "A: Set"; put param_delim; put "P : ";
		    iterate
		      (inc ir; put " A -> ")
		    |while !ir<n
		    end;
		    put "Prop"; put param_epilog;
		    put " : Prop :=\n    "; put ex_n; put "_intro : ";
		    ir := 0;
		    iterate
		      (put forall_prolog;
		       put xname; inc ir; print f (pack (!ir));
		       put ":A"; put forall_midlog)
		    |while !ir<n
		    end;
		    ir := 0;
		    if n=0
			then put "P"
		    else (put "(P";
			  iterate
			    (put " "; put xname; inc ir; print f (pack (!ir)))
			  |while !ir<n
			  end;
			  put ")");
			put " -> ("; put ex_n; put " A P).\n";
			ex_n
		end
    in
	pextype
    end;

(*
fun coq_print_inversion_P (ver, fd as |[put, ...]|, portype, pextype,
			   fun_prefix, state_prefix, rem_name, xname, term_type,
			   AUTO (auto, univ), CAN (autonamer, _)) =
    let val |[fun_paren_prolog, var_delim, fun_midlog, fun_paren_epilog,
	      intros_tac, trivial_tac, inversion_tac,
	      apply_tac, eapply_tac, refl_tac, dot_tac, ...]|
	= coq_keywords ver
	val pblocks = coq_print_blocks (ver, fd, state_prefix)
	val pforall = coq_print_forall (ver, fd)
	val pPx = coq_print_Px (ver, fd, state_prefix)
	val pvars = coq_print_vars fd
	val pfvars = coq_print_f_vars (fd, fun_prefix)
	memofun pinvP P =
		if P inset univ
		    then let val rem = gensym rem_name
			 in
			     put "\nRemark "; put rem; put " : ";
			     pforall (xname, term_type);
			     pPx (P, xname);
			     put " -> True.\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put trivial_tac; put dot_tac;
			     put "\nQed.\n";
			     rem
			 end
		else let val fmap = if P inset auto
					then ?auto P
				    else {}
			 val n = card fmap
			 val or_n = portype n
			 val ex_ns = {f => pextype k
				     | f => (_, k, _) in map fmap}
			 val rem = gensym rem_name
			 val ir = ref 0
			 val lispian = (case ver of
					    "7" => true
					  | _ => false)
		     in
			 put "\nRemark "; put rem; put " : ";
			 pforall (xname, term_type);
			 pPx (P, xname);
			 put " -> ";
			 if n=0
			     then put or_n
			 else (if lispian then put "(" else ();
			       put or_n; put "\n";
			       iterate
				 (put "  ("; put (?ex_ns f); put " "; put term_type;
				  if k=0
				      then (put " "; put xname; put "="; put f)
				  else (put " "; put fun_paren_prolog;
					pvars (var_delim, xname, k); put ":";
					put term_type; put fun_midlog; put " ";
					put xname; put "=";
					pfvars (f, xname, k);
					put fun_paren_epilog
					);
				      put ")\n"
				      )
			       | f => (blkls, k, _) in map fmap
			       end;
			       if lispian then put "  )" else put "  ");
			     put ".\nProof.\n  ";
			     put intros_tac; put dot_tac; put " ";
			     put inversion_tac; put " H"; put dot_tac;
			     put "\n";
			     iterate
			       (inc ir;
				iterate
				  (put "  "; put apply_tac;
				   put or_n; put "_intro_";
				   print fd (pack (!ir));
				   put dot_tac; put " ";
				   put eapply_tac;
				   put "("; put (?ex_ns f); put "_intro ";
				   put term_type; put ")";
				   put dot_tac; put " ";
				   put refl_tac; put dot_tac; put "\n")
				| blkl in set blkls
				end)
			     | f => (blkls, k, _) in map fmap
			     end;
			     put "Defined.\n";
			     rem
		     end
    in
	pinvP
    end;
*)

exception CoqPrintSuperclause;
exception McSubsumedDone;
exception CutHistory;

fun superclause_vars (c, orandl) =
    gclause_vars c U union {union {tvars a
				  | a in list andl}
			   | andl in list orandl};

fun coq_print_superclause (ver, f as |[put, ...]|, fun_prefix, state_prefix, varname, varsort, term_type) =
    let val pvars = coq_print_gvars (ver, f, varname, varsort, term_type)
	val pneg = coq_print_gclause_neg (ver, f, fun_prefix, state_prefix, varname, term_type)
	val ppos = coq_print_gclause_pos (ver, f, fun_prefix, state_prefix, varname, term_type)
	val patom = coq_print_atom (ver, f, fun_prefix, state_prefix, varname, term_type)
	val delimr = ref ""
	fun pandl nil = put "True"
	  | pandl [a] = patom a
	  | pandl (a::l) = (patom a; put " /\\ "; pandl l)
	fun pandl0 (andl as [_, _, ...]) =
	    (put "("; pandl andl; put ")")
	  | pandl0 andl = pandl andl
	fun psc (vars, gc, orandl) =
	    (pvars vars; pneg gc;
	     iterate
	       (pandl0 andl; put " \\/ ")
	     | andl in list orandl
	     end;
	     ppos gc)
    in
	psc
    end;

fun justif_superclause (MC_DISTR_POS (c, orandl, ...)) = (c, orandl)
  | justif_superclause (MC_SUBSUMED_SUPER (c, orandl, ...)) = (c, orandl)
  | justif_superclause (MC_CUT_HISTORY (_, j)) = justif_superclause j
  | justif_superclause j = (justif_gclause j, nil)
	    ;

fun epsc_name (neg, pos) =
    let val f as |[put, convert, ...]| = outstring "epsilon"
    in
	iterate
	  (put "_m"; put P)
	| P in set neg
	end;
	iterate
	  (put "_p"; put P)
	| P in set pos
	end;
	convert ()
    end;

exception HeadSelect;
exception FindP;
exception FindFromNeg;
exception FindPredFromNeg;
exception PJustif;

fun find_from_neg (a, nil) = raise FindFromNeg
  | find_from_neg (a, b::l) =
    if a=b then 0 else 1+find_from_neg (a, l)

fun find_pred_from_neg (P, {}) = raise FindPredFromNeg
  | find_pred_from_neg (P, {Q} U rest) =
    if P=Q then 0 else 1+find_pred_from_neg (P, rest);
    
fun coq_print_justif (AUTO (auto, univ),
		      ver,
		      fd as |[put, ...]|,
		      fun_prefix, state_prefix,
		      rem_name, varname, xname, varsort, term_type,
		      fsig,
		      portype,
		      pinvPf, (* typically coq_print_inversion_P_f (fd, portype, fun_prefix, state_prefix, rem_name,
			      varname, term_type, AUTO (auto, univ), CAN (autonamer, univnamer)) *)
		      (*
		       pinvP, (* typically coq_print_inversion_P (fd, portype, pextype, fun_prefix, state_prefix, rem_name,
			      xname, term_type, CAN (autonamer, univnamer)) *)
		       *)
		      CAN (autonamer, univnamer)) =
    let val |[left_tac, right_tac, forall_prolog, forall_midlog,
	      intro_tac, clear_tac, intros_tac, tauto_tac,
	      apply_tac, assum_tac, cut_tac, cut_end, exact_tac, assert_tac,
	      elim_tac, case_tac, fix_tac, induction_tac,
	      inversion_tac, destruct_tac,
	      intuition_tac, auto_tac,
	      rec_def, plain_def, param_prolog, param_epilog,
	      case_prolog, case_delim, case_of, case_midlog, case_epilog,
	      split_tac, simpl_tac, try_tac, trivial_tac,
	      rewrite_tac, discr_tac, decomp_sum_tac,
	      dot_tac, semi_tac, ...]|
	= coq_keywords ver
	val lispian = (case ver of
			   "7" => true
			 | _ => false)
	val pgclause = coq_print_gclause (ver, fd, fun_prefix, state_prefix, varname, varsort, term_type)
	val ppos = coq_print_gclause_pos (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val plits = coq_print_gclause_lits (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val psc = coq_print_superclause (ver, fd, fun_prefix, state_prefix, varname, varsort, term_type)
	val cpname = coq_pred_name (ver, state_prefix, term_type)
	val cfname = coq_fun_name fun_prefix
	val pterm = coq_print_term (fd, fun_prefix, varname)
	val patom = coq_print_atom (ver, fd, fun_prefix, state_prefix, varname, term_type)
	val pvars = coq_print_vars fd
	val fl = fsort fsig
	fun hsel (0, [a]) = ()
	  | hsel (0, [a, ...]) = (put " "; put left_tac; put dot_tac)
	  | hsel (_, nil) = raise HeadSelect
	  | hsel (i, a::l) = (put " "; put right_tac; put dot_tac;
			      hsel (i-1, l))
	fun head_select (i, GCLAUSE (_, pos)) =
	    hsel (i, pos)
	val popen = if lispian then fn () => put "(" else fn () => ()
	val pclose = if lispian then fn () => put ")" else fn () => ()
	fun print_epsc (neg, pos) =
	    (put forall_prolog; put xname; put ":"; put term_type;
	     put forall_midlog;
	     iterate
	       (popen ();
		put (cpname P); put " "; put xname;
		pclose ();
		put " -> ")
	     | P in set neg
	     end;
	     case pos of
		 {} => put "False"
	       | _ => let val delimr = ref ""
		      in
			  iterate
			    (put (!delimr);
			     delimr := " \\/ ";
			     popen (); put (cpname P);
			     put " "; put xname; pclose ())
			  | P in set pos
			  end
		      end)
	fun print_epsc_orn (neg, pos, or_n) =
	    (put forall_prolog; put xname; put ":"; put term_type;
	     put forall_midlog;
	     iterate
	       (popen ();
		put (cpname P); put " "; put xname;
		pclose ();
		put " -> ")
	     | P in set neg
	     end;
	     if empty pos
		 then put or_n
	     else (popen ();
		   put or_n;
		   iterate
		     (put " (";
		      put (cpname P); put " "; put xname;
		      put ")")
		   | P in set pos
		   end;
		   pclose ()))
	fun print_epsc_t ((neg, pos), t) =
	    (iterate
	       (popen (); put (cpname P);
		put " "; pterm t; pclose (); put " -> ")
	     | P in set neg
	     end;
	       case pos of
		   {} => put "False"
		 | _ => let val delimr = ref ""
			in
			    iterate
			      (put (!delimr);
			       delimr := " \\/ ";
			       popen (); put (cpname P);
			       put " "; pterm t; pclose ())
			    | P in set pos
			    end
			end)
	fun phistory {} = ()
	  | phistory ({epsc => _} U rest) =
	    (put "("; print_epsc epsc; put ")\n    -> "; phistory rest)
	fun clear_history h =
	    iterate
	      (put " "; put intro_tac; put "H"; put dot_tac; put " ";
	       put clear_tac; put "H"; put dot_tac)
	    | _ in set h
	    end
	fun names_history h =
	     iterate
	       (put " "; put Hname)
	     | epsc => Hname in map h
	     end
	fun intro_history {} = ()
	  | intro_history h =
	    (put " "; put intros_tac;
	     names_history h;
	     put dot_tac)
	fun intro_from_history (epsc, h) =
	    iterate
	      if epsc=epsc'
		  then (put " "; put intro_tac; put "Hrec"; put dot_tac)
	      else (put " "; put intro_tac; put "H"; put dot_tac; put " ";
		    put clear_tac; put "H"; put dot_tac)
	    | epsc' in set h
	    end
	fun intro_impls impls =
	    if impls=""
		    then ()
		else (put " "; put intros_tac; put impls; put dot_tac;
		      put "\n")
	val sort_vars = sort (op strless);
	fun varnames vars = [varname x | x in list varsort vars]
	    (* sort_vars {varname x | x in set vars} *)
	fun pvarnames {} = ()
	  | pvarnames vars =
	    iterate
	      (put " "; put x)
	    | x in list varnames vars
	    end
	fun intro_vars {} = ()
	  | intro_vars vars =
	    (put " "; put intros_tac; pvarnames vars; put dot_tac)
	fun pvarnames_renamed ({}, sigma) = ()
	  | pvarnames_renamed (vars, sigma) =
	    let val renaming = {varname x => varname y
			       | x => y in map sigma}
	    in
		iterate
		  (put " "; put (if x inset renaming
				     then ?renaming x
				 else x))
		| x in list varnames vars
		end
	    end
	fun intro_vars_renamed ({}, sigma) = ()
	  | intro_vars_renamed (vars, sigma) =
	    (put " "; put intros_tac; pvarnames_renamed (vars, sigma);
	     put dot_tac)
	fun imply_names (H, GCLAUSE (neg, _)) =
	    let val f as |[put, convert, ...]| = outstring ""
		val ir = ref 0
	    in
		iterate
		  (put " "; put H; inc ir; print f (pack (!ir)))
		| _ in list neg
		end;
		convert ()
	    end
	fun intros_until_i (n, Hname) =
	    let val ir = ref 0
	    in
		(if n=0
		    then ()
		else (put " "; put intros_tac;
		      iterate
			(inc ir; put " "; put Hname; print fd (pack (!ir)))
		      |while !ir<n
		      end;
		      put dot_tac));
		    put " "; put intro_tac; put Hname; put dot_tac
	    end
	fun intros_from_neg (a, Hname, c as GCLAUSE (neg, _)) =
	    let val n = find_from_neg (a, neg)
	    in
		intros_until_i (n, Hname)
	    end
	fun intros_from_pred_neg (P, Hname, Qs) =
	    let val n = find_pred_from_neg (P, Qs)
	    in
		intros_until_i (n, Hname)
	    end
	memofun p_hint_state q =
		(put "Hint Constructors ";
		 put (cpname q);
		 put " : h1mc_states_hint.\n")
	fun p_hint_states qs =
	    iterate
	      p_hint_state q
	    | q in set qs
	    end
	memofun p_epsilon (P, qs) =
	(* produce a proof of forall X, P(X) -> \/_{q in qs} q(X) *)
		let val or_n = portype (card qs)
		    val rem = epsc_name ({P}, qs) ^ "_o"
		in
		    p_hint_states qs;
		    put "\nRemark "; put rem; put " : ";
		    print_epsc_orn ({P}, qs, or_n);
		    put ". (* Justify inversion for epsilon clause. *)\nProof.\n ";
		    (* We first deal with a Coq misfeature:
		     intuition knows about or_<n> as a disjunction...
		     unless n>=10.  In this case, we prove
		     A1 \/ ... \/ An instead of (or_<n> A1 ... An),
		     and use a cut to conclude. *)
		    if card qs >= 10
			then (put cut_tac; print_epsc ({P}, qs);
			      put cut_end; put dot_tac;
			      put "\n  "; put intros_tac;
			      put " H0 X H"; put dot_tac; put " ";
			      put decomp_sum_tac; put " (H0 X H)"; put dot_tac;
			      let val ir = ref 0
				  val n = card qs
				  val f as |[convert, tell, seek, truncate,
					     ...]| = outstring or_n
				  val pos = (#put f "_intro_"; tell ())
			      in
				  while !ir < n do
				      (put "\n  "; put apply_tac;
				       seek pos; truncate ();
				       inc ir;
				       print f (pack (!ir));
				       put (convert ());
				       put semi_tac;
				       put assum_tac; put dot_tac)
			      end;
			      put "\n  "
			      )
		    else ();
		    put destruct_tac; put xname; put semi_tac;
		    put intro_tac; put "H"; put semi_tac;
		    put inversion_tac; put "H"; put semi_tac;
		    (case qs of
			 {} => put tauto_tac (* unimportant: we'll never
					      reach this tactic anyway. *)
		       | {_} => (* Coq v8's 'intuition' does not understand
				 1-ary disjunctions... so make a special case.
				 *)
			 (put apply_tac;
			  put or_n; put "_intro_1";
			  put semi_tac; put auto_tac;
			  put "with h1mc_states_hint")
		       | _ =>
			 (put intuition_tac; put auto_tac;
			  put "with h1mc_states_hint"));
		    put dot_tac; put "\nQed.\n";
		    rem
		end

	memofun p_simple_model (SM (qmap, ftables)) =
		let val dtype = gensym "model_"
		    val und = gensym "und_"
		    val v = gensym "val_"
		    val eval = gensym "seval_"
		    val rem = eval ^ "_model"
		    memofun valname (i:int) =
			    let val f as |[put, convert, ...]| = outstring v
			    in
				put "_";
				print f (pack i);
				convert ()
			    end
		    memofun varname (i:int) =
			    let val f as |[put, convert, ...]| = outstring xname
			    in
				print f (pack i);
				convert ()
			    end

		    fun p_simple_model_fun (f, ftable) =
			(put plain_def; put rem; put "_"; put (cfname f);
			 case ftable of
			     {nil => v} =>
			     (put " : "; put dtype; put " := ";
			      put (valname v); put ".\n")
			   | _ =>
			     let val n = len (choose ftable)
				 val sf as |[convert, tell, seek, truncate,
					     ...]| = outstring "v"
				 val pos = tell ()
				 val ir = ref 0
			     in
				 put " "; put param_prolog;
				 while !ir < n do
				     (inc ir;
				      seek pos; truncate ();
				      print sf (pack (!ir));
				      put (convert ());
				      put " ");
				 put " : "; put dtype;
				 put param_epilog;
				 put " : "; put dtype; put " :=\n  ";
				 
			     end)
			 
		    val vals = sort (op <) (rng qmap)
		    val rec_p = (* recursive evaluation function iff
				 some entry in ftables has at least one
				 argument. *)
			exists true
			| f => {[_, ...] => _, ...} in map ftables
			end
			val delimr = ref "    "
			val ir = ref 0
		in
		    (* Define datatype of values, dtype. *)
		    put "\nInductive ";
		    put dtype;
		    put " : Set := ";
		    put und; put ":"; put dtype;
		    iterate
		      (put " | "; put (valname i); put ":"; put dtype)
		    | i in list vals
		    end;
		    put ".\n\n";
		    (* Now define the 'eval' function, mapping
		     all ground terms to their values in the model. *)
		    put (if rec_p then rec_def else plain_def);
		    put eval; put " "; put param_prolog;
		    put "t : "; put term_type;
		    put param_epilog;
		    (case ver of
			 "7" => () (* nothing to do here *)
		       | _ => if rec_p (* Coq v8 is pesky when distinguishing
					recursive from non-recursive functions. *)
				  then put " {struct t}"
			      else ());
		    put " : "; put dtype; put " :=\n  ";
		    put case_prolog; put "t "; put case_of; put "\n";
		    iterate
		      (put (!delimr); delimr := "\n  | ";
		       if k=0
			   then put (cfname f)
		       else (ir := 0;
			     put "("; put (cfname f);
			     while !ir<k do
				 (inc ir; put " "; put (varname (!ir)));
		             put ")");
		       put case_midlog;

		       (case ftable of
			    {nil => v} =>
			    put (valname v)
			  | _ =>
			    let val delim2 = ref ""
			    in
				put "\n    ";
				put case_prolog;
				ir := 0;
				while !ir<k do
				    (put (!delim2);
				     inc ir;
				     delim2 := case_delim;
				     put "("; put eval;
				     put " "; put (varname (!ir));
				     put ")");
				put case_of;
				delim2 := "\n      ";
				iterate
				  (iterate
				     (put (!delim2); delim2 := case_delim;
				      put (valname i))
				   | i in list l
				   end;
				   delim2 := "\n    | ";
				   put case_midlog;
				   put (valname v)
				     )
				| l => v in map ftable
				end;
				ir := 0;
				while !ir<k do
				    (put (!delim2); delim2 := case_delim;
				     inc ir; put "_");
				put case_midlog;
				put und;
				put "\n    ";
				put case_epilog
			    end
			    )
		       )
		    | f => ftable in map ftables
		    val k = (case ftable of
				 {} => 0 (* should not happen *)
			       | {l => _, ...} => len l)
		    end;
		    if empty (ftables <-| fsig)
			then ()
		    else (put (!delimr); put "_ ";
			  put case_midlog; put und; put "\n");
		    put "  "; put case_epilog; put ".\n\nRemark ";
		(* And now prove all lemmas of the
		 form: forall t:term, auto__q(t) -> eval(t)=i,
		 whenever q => i is in qmap. *)
		    put rem; put " : ";
		    put forall_prolog; put xname; put ":"; put term_type;
		    put forall_midlog;
		    delimr := "";
		    iterate
		      (put (!delimr); delimr := " /\\\n  ";
		       put "(("; put (cpname q); put " "; put xname;
		       put ") -> ";
		       put "("; put eval; put " "; put xname; put ")=";
		       put (valname i); put ")")
		    | q => i in map qmap
		    end;
		    put ". (* Verify model. *)\nProof.\n  ";
		    put induction_tac; put xname; put dot_tac;
		    iterate
		      if ?fsig f=0 (* take a shortcut. *)
			  then (put "\n  ("; put intuition_tac;
				put trivial_tac; put ")";
				put semi_tac; put inversion_tac;
				put "H." (* We predict that the
					  hypothesis that will be introduced
					  by 'inversion' will be named H. *)
				)
		      else let val qmapr = ref qmap
			       (* Try to predict the name that
				Coq will give to variables introduced by
				'inversion'. Apparently, if xname="X",
				these variables will be X1, ..., Xk
				if k>=2, and X if k=1.
				*)
			       val vname = if ?fsig f=1
					       then fn _ => xname
					   else varname
			   in
			       while not (empty (!qmapr)) do
				   (put "\n  ";
				    (case !qmapr of
					 {_ => _, _ => _, ...} =>
					 (* Write 'split' unless only one
					  case remains. *)
					 (put split_tac; put dot_tac; put " ")
				       | _ => ());
					case !qmapr of
					    {q => i} U rest =>
					    (* Now prove q(x) -> eval x=i *)
					    (qmapr := rest;
					     put intro_tac; put "H";
					     put dot_tac; put " ";
					     put inversion_tac; put "H";
					     put dot_tac;
					     (* This generates as many
					      subgoals as there are transitions
					      q(f(X1,...,Xk)) :- B
					      in auto. *)
					     let val fmap = if q inset auto
								then ?auto q
							    else {}
						 val blkls = if f inset fmap
								 then #1 (?fmap f)
							     else {}
					     in
						 iterate
						   (iterate
						      (put "\n    ";
						       put cut_tac;
						       put "(";
						       put eval; put " ";
						       inc ir;
						       put (vname (!ir));
						       put ")=";
						       put (valname (?qmap qx));
						       put cut_end;
						       put dot_tac; put " 2:";
						       put tauto_tac;
						       put dot_tac
						       )
						    | {qx, ...} in list blkl
						    end;
						      put "\n      ";
						      put simpl_tac;
						      put dot_tac;
						      iterate
							(put " ";
							 put intro_tac;
							 put "HH";
							 put dot_tac;
							 put " ";
							 put try_tac;
							 put rewrite_tac;
							 put "HH";
							 put dot_tac;
							 put " ";
							 put clear_tac;
							 put "HH";
							 put dot_tac)
						      | _ in list blkl
						      end;
						      put " ";
						      put trivial_tac;
						      put dot_tac
						      )
						 | blkl in set blkls
						    val ir = ref 0
						 end
					     end
					     )
					  | _ => ())
			   end
		    | f in list fl
		    end;
		    put "\nQed.\n";
		    (rem, eval, valname)
		end

	fun put_qed {} = put "Qed.\n"
	  | put_qed _ = put "Defined.\n"

	val done_clauses = ref {}
	fun find_done_clauses hj =
	    if hj inset !done_clauses
		then SOME (?(!done_clauses) hj)
	    else NONE
	fun add_done_clauses (hj,res) =
	    done_clauses := !done_clauses ++ {hj => res}
	fun pjustif hj =
	    (case find_done_clauses hj of
		 SOME rem => rem
	       | NONE => let val rem = pjustif_1 hj
			 in
			     add_done_clauses (hj,rem);
			     rem
			 end)
	and pjustif_1 (h : epsilon_gclause -m> string,
		       MC_TAUTO (c, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Tautology. *)\nProof.";
		clear_history h; put " "; put tauto_tac;
		put dot_tac; put " "; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_CUT_HISTORY (h', j)) =
	    let val domh = dom h
	    in
		if domh=h'
		    then pjustif (h, j)
		else let val newh = h' <| h
			     val remj = pjustif (newh,j)
			     val rem = gensym rem_name
			     val c = justif_gclause j
			 in
			     put "\nRemark "; put rem; put " : ";
			     phistory h; pgclause c;
			     put ". (* Cut history. *)\nProof. ";
			     if h' subset h
				 then ()
			     else put " (* HISTORY BUG. *)";
			     intro_history h; put " ";
			     put exact_tac; put "(";
			     put remj; names_history newh;
			     put ")"; put dot_tac; put "\n"; put_qed h;
			     rem
			 end
	    end
	  | pjustif_1 (h, MC_NORMALIZE (c, sigma, j)) =
	    let val remj = pjustif (h,j)
		val rem = gensym rem_name
		val vars = gclause_vars c
		val c' = justif_gclause j
		val vars' = gclause_vars c'
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Prove equivalent, normalized clause. *)\nProof.\n ";
		intro_history h; put " ";
		intro_vars_renamed (vars, sigma); put "\n  ";
		put cut_tac; plits c'; put cut_end;
		put dot_tac; put " "; put tauto_tac;
		put dot_tac; put " "; put exact_tac;
		put "("; put remj; names_history h;
		pvarnames vars'; put ")";
		put dot_tac; put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_SUBSUMED_UNIV (c, P, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by universal clause. *)\nProof. ";
		put intros_tac; put dot_tac;
		head_select (i, c);
		put " "; put apply_tac; put (univnamer P);
		put dot_tac; put " "; put_qed h;
		rem
	    end
(*
	  | pjustif_1 (h, MC_SUBSUMED_AUTO (c, P, f, k, sigma, blkl, i)) =
	    let val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by automaton clause. *)\nProof. ";
		put intros_tac; put dot_tac;
		head_select (i, c);
		put " "; put apply_tac;
		put (autonamer (P, f, blkl));
		put semi_tac; put " "; put assum_tac; put dot_tac;
		put " "; put_qed h;
		rem
	    end
*)
	  | pjustif_1 (h, MC_SUBSUMED_HISTORY (c, epsc, t)) =
	    let val rem = gensym rem_name
		val vars = gclause_vars c
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Use induction hypothesis. *)\nProof.\n  ";
		intro_from_history (epsc, h); intro_vars vars;
		put "\n  "; put cut_tac; print_epsc_t (epsc, t); put cut_end;
		put dot_tac; put " "; put tauto_tac; put dot_tac; put " ";
		put exact_tac; put "(Hrec "; pterm t; put ")";
		put dot_tac; put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_SUBSUMED_EPSC (c, t, j)) =
	    let val remj = pjustif (h,j)
		val rem = gensym rem_name
		val vars = gclause_vars c
		val GCLAUSE (neg, pos) = justif_gclause j (* an epsilon clause *)
		val epsc = ({P | P $ _ in list neg}, {Q | Q $ _ in list pos})
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumed by epsilon clause. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		put " "; put intros_tac; put dot_tac;
		put "\n  "; put assert_tac; put "(HH:=(";
		put remj; names_history h; put " "; pterm t;
		put "))";
		put dot_tac; put " ";
		put tauto_tac; put dot_tac; put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_ELIM_UNIV_NEG (c, P, i, j)) =
	    let val remj = pjustif (h, j)
		val vars = gclause_vars c
		val cj = justif_gclause j
		val vars' = gclause_vars cj
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Eliminate negative atom by universal clause. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		put " "; put intros_tac; put dot_tac; put " ";
		put apply_tac;
		if empty h andalso empty vars'
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames vars'; put ")");
		    put semi_tac; put " ";
		    put assum_tac; put dot_tac;
		    put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_ELIM_NEG (c, a, k, sigma, jl)) =
	    let val reml = [pjustif (h, j)
			   | j in list jl]
		val vars = gclause_vars c
		val P $ [f $ l] = a
		val invPf = pinvPf (P, f, k)
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Eliminate negative atom. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		intros_from_neg (a, "H", c); (* H : a, where a = P(f(t1,...,tk)) *)
		put " "; put intros_tac; put dot_tac; (* added JGL feb 27, 2008. *)
		put "\n  "; put elim_tac; put "("; put invPf;
		iterate
		  (put " "; pterm t)
		| t in list l
		end;
		put " H)"; put semi_tac; put " "; put intros_tac;
		put dot_tac; put "\n";
		iterate
		  (put "  "; put apply_tac;
		   let val vars' = gclause_vars (justif_gclause j)
		   in
		       if empty h andalso empty vars'
			   then put remj
		       else (put "("; put remj; names_history h;
			     pvarnames vars';
			     put ")");
			   put semi_tac; put " "; put tauto_tac;
			   put dot_tac; put "\n"
		   end)
		|| remj in list reml and j in list jl
		end;
		put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_ELIM_EPSILON_NEG (c, a, qjl)) =
	    let val reml = [pjustif (h, j)
			   | (_, j) in list qjl]
		val vars = gclause_vars c
		val qs = {q | (q, _) in list qjl}
		val P $ [t] = a
		val rem_epsilon = p_epsilon (P, qs)
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Invert negative atom through epsilon clauses. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		intros_from_neg (a, "H", c); (* H : a *)
		put " "; put intros_tac; put dot_tac;
		put "\n  ";
		put elim_tac; put "("; put rem_epsilon;
		put " "; pterm t; put " H)";
		if empty qs
		    then (put dot_tac; put "\n")
		else (put semi_tac; put intros_tac; put dot_tac; put "\n";
		      iterate
			(put "  ";
			 put apply_tac;
			 let val vars' =
				 gclause_vars (justif_gclause j)
			 in
			     if empty h andalso empty vars'
				 then put remj
			     else (put "("; put remj;
				   names_history h;
				   pvarnames vars';
				   put ")");
				 put semi_tac; put " ";
				 put tauto_tac;
				 put dot_tac; put "\n"
			 end)
		      || remj in list reml and (q, j) in list qjl
		      end);
		 put_qed h;
		 rem
	    end
	  | pjustif_1 (h, MC_DEDUCE_POS (c, a, i, blkls, j)) =
	    let val remj = pjustif (h, j)
		val vars = gclause_vars c
		val P $ [f $ l] = a
		val rem = gensym rem_name
		val firstr = ref true
		val impls = imply_names ("A", c)
		val sc = justif_superclause j
		val scvars = superclause_vars sc
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Deduce positive atom. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		intro_impls impls;
		if empty blkls
		    then let val cj = justif_gclause j
			 (* although j is usually a justification
			  for a superclause, since blkls is empty,
			  j will in fact be the justification of
			  a gclause. *)
			 in
			     put "  "; put cut_tac; ppos cj; put cut_end;
			     put dot_tac; put " ";
			     put tauto_tac; put dot_tac; put "\n";
			     if empty h andalso empty vars andalso impls=""
				 then put remj
			     else (put "  "; put exact_tac;
				   put "("; put remj; names_history h;
				   pvarnames scvars;
				   put impls; put ")";
				   put dot_tac; put "\n")
			 end
		else
		    (iterate
		       (if !firstr
			    then (firstr := false;
				  put "  "; put case_tac;
				  if empty h andalso empty vars
				      andalso impls=""
				      then put remj
				  else (put "("; put remj; names_history h;
					pvarnames scvars;
					put impls; put ")"))
			else (put "  "; put intro_tac; put "H";
			      put semi_tac; put " ";
			      put case_tac; put "H";
			      put semi_tac; put " ";
			      put clear_tac; put "H");
			    put dot_tac; (* was not added if !firstr, empty h andalso empty vars; corrected Jan 24, 2008 JGL. *)
			    (if empty h andalso impls=""
				 then ()
			     else (put " "; put clear_tac; names_history h;
				   put impls; put dot_tac));
			    put " ";
			    put intros_tac; put dot_tac;
			    head_select (i, c);
			    put " "; put apply_tac;
			    put (autonamer (P, f, blkl));
			    put semi_tac; put " "; put tauto_tac;
			    put dot_tac; put "\n")
		     | blkl in set blkls
		     end;
		       (if empty h andalso impls=""
			    then ()
			else (put " "; put clear_tac; names_history h;
			      put impls; put dot_tac));
		       put " "; put tauto_tac;
		       put dot_tac; put "\n");
		       put_qed h;
		       rem
	    end
	  | pjustif_1 (h, MC_DISTR_POS (c, orandl, jl)) =
	    let val reml = [pjustif (h, j)
			   | j in list jl]
		val vars = superclause_vars (c, orandl)
		val impls = imply_names ("A", c)
		val rem  = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; psc (vars, c, orandl);
		put ". (* Distribute disjunctions over conjunctions. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		intro_impls impls;
		iterate
		  let val cj = justif_gclause j
		  in
		      put "  "; put cut_tac; ppos cj; put cut_end;
		      put dot_tac; put " 2:";
		      put apply_tac;
		      if empty h andalso empty vars
			  then put remj
		      else (put "("; put remj; names_history h;
			    pvarnames (gclause_vars cj);
			    put ")"; put semi_tac; put " "; put assum_tac);
			  put dot_tac; put "\n"
		  end
		|| remj in list reml and j in list jl
		end;
		put "  "; put tauto_tac; put dot_tac;
		put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_SUBSUMED_SUPER (c, orandl, j)) =
	    let val remj = pjustif (h, j)
		val vars = superclause_vars (c, orandl)
		val impls = imply_names ("A", c)
		val sc = justif_superclause j
		val scvars = superclause_vars sc
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; psc (vars, c, orandl);
		put ". (* Prove a smaller disjunction. *)\nProof.\n ";
		intro_history h; intro_vars vars; intro_impls impls;
		put "  "; put case_tac;
		if empty h andalso empty scvars andalso impls=""
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames scvars;
		      put impls; put ")");
		    put semi_tac; put " "; put tauto_tac;
		    put dot_tac; put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_SUBSUMED (c, j)) =
	    let val remj = pjustif (h, j)
		val rem = gensym rem_name
		val vars = gclause_vars c
		val jc = justif_gclause j
		val vars' = gclause_vars jc
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Subsumption by simpler clause. *)\nProof.\n ";
		intro_history h; intro_vars vars;
		put "\n  "; put cut_tac; plits jc; put cut_end;
		put dot_tac; put " "; put tauto_tac;
		put dot_tac; put " "; put exact_tac;
		if empty h andalso empty vars'
		    then put remj
		else (put "("; put remj; names_history h;
		      pvarnames vars'; put ")");
		    put dot_tac; put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_SPLIT (c, j)) =
	    let val remj = pjustif (h, j)
		val cj = justif_gclause j
		val vars = gclause_vars c
		val varsj = gclause_vars cj
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Split. *)\nProof.\n ";
		intro_history h; intro_vars vars; put "\n";
		put "  "; put cut_tac; plits cj; put cut_end; put dot_tac;
		if empty h
		    then ()
		else (put " "; put clear_tac; names_history h; put dot_tac);
		    put " "; put tauto_tac; put dot_tac; put "\n";
		    put "  "; put exact_tac;
		    if empty h andalso empty vars
			then put remj
		    else (put "("; put remj; names_history h;
			  pvarnames varsj;
			  put ")");
			put dot_tac; put "\n"; put_qed h;
			rem
	    end
          | pjustif_1 (h, MC_EXPLICIT_UNIV (x, qs, info)) =
	    let val rem = gensym rem_name
	    in
		p_hint_states qs;
		put "\nRemark "; put rem; put " : ";
		phistory h;
		put forall_prolog;
		put (varname x); put ":"; put term_type;
		put forall_midlog;
		print_epsc_t (({}, qs), V x);
		put ". (* Check universal disjunction. *)\nProof.\n ";
		intro_history h;
		put induction_tac; put (varname x);
		put semi_tac; put " ";
		put intuition_tac; put auto_tac;
		put "with h1mc_states_hint";
		put dot_tac;
		put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, j as MC_VS (x, q, q', sm as SM (qmap, ...))) =
	    let val rem = gensym rem_name
		val (remm, evalfun, valname) = p_simple_model sm
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h;
		pgclause (justif_gclause j);
		put ". (* Check disjointness. *)\nProof.\n ";
		intro_history h; put " "; put intro_tac; put (varname x);
		put dot_tac; put "\n  ";
		put assert_tac; put "(H:=("; put remm; put " "; put (varname x);
		put "))"; put dot_tac; put " ";
		put intros_tac; put dot_tac;
		iterate
		  (put "\n  "; put cut_tac; put "("; put evalfun;
		   put " "; put (varname x); put ")=";
		   put (valname (?qmap P));
		   put cut_end;
		   put dot_tac; put " 2:"; put tauto_tac;
		   put dot_tac)
		| P in list [q,q']
		end;
		put "\n  ";
		put intro_tac; put "HH"; put dot_tac; put " ";
		put rewrite_tac; put "HH"; put dot_tac; put " ";
		put discr_tac; put dot_tac;
		put "\n"; put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_CUT (c as GCLAUSE (_, pos), j, jal)) =
	    let val remj = pjustif (h, j)
		val c0 = justif_gclause j
		val remjl = [pjustif (h, ji)
			    | (ji, ai) in list jal]
		val or_n = portype (len remjl)
		val vars = gclause_vars c
		val rem = gensym rem_name
	    in
		put "\nHint Constructors ";
		put or_n; put " : "; put or_n; put "_hint.\n";
		put "\nRemark "; put rem; put " : ";
		phistory h; pgclause c;
		put ". (* Cut. *)\nProof.\n ";
		intro_history h; intro_vars vars; put "\n";
		put "  "; put cut_tac; popen ();
		put or_n;
		iterate
		  (put " ("; patom ai; put ")")
		| (_, ai) in list jal
		end;
		pclose (); put cut_end; put dot_tac;
		(* First subgoal is (or_n q1(X) ... qn(X)) -> c,
		 second subgoal is (or_n q1(X) ... qn(X)). *)
		put " "; put intro_tac; put "H"; put dot_tac; put " ";
		put elim_tac; put "H"; put dot_tac; put "\n";
		(* Now we have n subgoals qi(X) -> c, i=1..n. *)
		iterate
		  (put "  "; put assert_tac; put "(HH:=(";
		   put remi; names_history h; pvarnames (gclause_vars ci);
		   put "))"; put dot_tac; put " ";
		   put tauto_tac; put dot_tac; put "\n"
		   )
		|| (ji, ai) in list jal
		and remi in list remjl
		val ci = justif_gclause ji
		end;
		(* And we must now prove (or_n (q1(X) ... qn(X))). *)
		put "  "; put assert_tac; put "(HH:=(";
		put remj; names_history h; pvarnames (gclause_vars c0);
		put "))"; put dot_tac; put " ";
		(* We should call tauto, but apparently Coq v8 does
		 not understand or_n in goal position. *)
		put intuition_tac; put auto_tac;
		put "with "; put or_n; put "_hint"; put dot_tac; put "\n";
		put_qed h;
		rem
	    end
	  | pjustif_1 (h, MC_INDUCT (x, epsc as (neg, pos), optP, jl)) =
	    let val Hname = epsc_name epsc
		val h' = h ++ {epsc => Hname}
		val subj = {f => (pjustif (h', j), k, j)
			   | (f, k, j) in list jl}
		val inversions = case optP of
				     SOME P =>
				     {f => pinvPf (P, f, k)
				     | f => k in map subj <-| fsig}
				   | NONE => {}
		(*
		val reml = [pjustif (h', j)
			   | (_, _, j) in list jl]
		 *)
		val rem = gensym rem_name
	    in
		put "\nRemark "; put rem; put " : ";
		phistory h;
		put forall_prolog;
		put (varname x); put ":"; put term_type;
		put forall_midlog;
		print_epsc_t (epsc, V x);
		put ". (* Induct. *)\nProof.\n "; intro_history h;
		put " "; put fix_tac; put Hname; put " 1";
		(* print fd (pack (card h+1));*) (* print fd (pack (i+1)); *)
		put dot_tac; put "\n  ";
		put intro_tac; put xname; put dot_tac; put " ";
		put case_tac; put xname; put dot_tac;
		iterate
		  if f inset subj
		      then let val (remj, k, j) = ?subj f
			   in
			       put "\n  ";
			       if k<>0
				   then (put intros_tac; put " ";
					 pvars (" ", xname, k);
					 put semi_tac; put " ")
			       else ();
			       put exact_tac;
			       put "("; put remj; names_history h'; put " ";
			       pvars (" ", xname, k); put ")";
			       put dot_tac
			   end
		  else (case optP of
			    SOME P => let val invj = ?inversions f
					  val k = ?fsig f
				      in
					  put "\n  ";
					  if k<>0
					      then (put intros_tac; put " ";
						    pvars (" ", xname, k);
						    put dot_tac)
					  else ();
					  intros_from_pred_neg (P, "H", neg);
					  put " ";
					  put elim_tac; put "("; put invj;
					  put " "; pvars (" ", xname, k);
					  put " H)"; put dot_tac
				      end
			  | NONE => put "\n  (* Sorry, missing proof: \
			    \this is a bug. *) fail.")
		(*
		      (case optP of
			    SOME P =>
			    let val i = let fun findP (i, {Q} U rest) =
						if P=Q
						    then i
						else findP (i+1, rest)
					      | findP _ = raise FindP
					in
					    findP (1, neg)
					end
			    in
				put "\n  ";
				put inversion_tac;
				print fd (pack i);
				put dot_tac
			    end
			  | NONE => put "\n  (* Sorry, missing proof: this is a bug. *) fail.")
		      *)
		| f in list fl
		end;
		put "\n"; put_qed h;
		(*
		put semi_tac; put " ";
		put first_tac;
		let val delimr = ref "["
		in
		    iterate
		      (put (!delimr); delimr := "\n  | ";
		       if k<>0
			   then (put " "; put intros_tac; put " ";
				 pvars (" ", xname, k);
				 put semi_tac; put " ")
		       else ();
			   put exact_tac;
			   put "("; put remj; names_history h'; put " ";
			   pvars (" ", xname, k); put ")")
		    || remj in list reml and (_, k, j) in list jl
		    end;
		    (case optP of
			 SOME P =>
			 let val i = let fun findP (i, {Q} U rest) =
					     if P=Q
						 then i
					     else findP (i+1, rest)
					   | findP _ = raise FindP
				     in
					 findP (1, neg)
				     end
			 in
			     put (!delimr);
			     put " ";
			     put inversion_tac;
			     print fd (pack i)
			 end
		       | NONE => ());
		    put "]";
		    (*
		     put intros_tac;
		     put " until 1";
		     put semi_tac; put " ";
		     put inversion_tac; put "H]";
		     *)
		    put dot_tac; put "\n"; put_qed h;
		end;
		*)
		rem
	    end
    in
	pjustif
    end;

(*
fun std_coq_memos fd =
    let val std_portype = coq_print_or_type (fd, "or_")
	val std_pextype = coq_print_ex_type (fd, "ex_", "x")
	val std_autonamer = CAN (coq_auto_clause_name "trans_", coq_univ_clause_name "univ_")
    in
	(std_portype, std_pextype, std_autonamer)
    end;

fun std_coq_print_justif (A, fd, fun_prefix, state_prefix, rem_name, varname, xname, varsort, term_type) =
    let val (portype, pextype, autonamer) = std_coq_memos fd
	val pinvPf = coq_print_inversion_P_f (fd, portype, fun_prefix, state_prefix, rem_name, xname, term_type,
					      A, autonamer)
 (*
	val pinvP = coq_print_inversion_P (fd, portype, pextype, fun_prefix, state_prefix, rem_name, xname, term_type,
					   A, autonamer)
 *)
	val pjustif = coq_print_justif (A, fd, fun_prefix, state_prefix, rem_name, varname, xname, varsort, term_type,
					portype, pinvPf,
					(* pinvP, *)
					autonamer)
    in
	fn j => pjustif ({}, j)
    end;
*)
