+(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
+Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
+| cnd_property_weak : @cnd_property _ _ P _ cnd_weak
+| cnd_property_rule : forall h c r cnd',
+ P h c r ->
+ @cnd_property _ _ P h cnd' ->
+ @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
+| cnd_property_branch :
+ forall c1 c2 cnd1 cnd2,
+ @cnd_property _ _ P c1 cnd1 ->
+ @cnd_property _ _ P c2 cnd2 ->
+ @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2).
+
+(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
+Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
+| scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
+| scnd_property_comp : forall h x c r cnd',
+ P x [c] r ->
+ @scnd_property _ _ P h x cnd' ->
+ @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
+| scnd_property_branch :
+ forall x c1 c2 cnd1 cnd2,
+ @scnd_property _ _ P x c1 cnd1 ->
+ @scnd_property _ _ P x c2 cnd2 ->
+ @scnd_property _ _ P x _ (scnd_branch _ _ _ cnd1 cnd2).
+
+(* renders a proof as LaTeX code *)
+Section ToLatex.
+
+ Context {Judgment : Type}.
+ Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
+ Context {JudgmentToLatexMath : ToLatexMath Judgment}.
+ Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}.
+
+ Open Scope string_scope.
+
+ Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
+
+ Definition eolL : LatexMath := rawLatexMath eol.
+
+ (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
+ Section SIND_toLatex.
+
+ (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
+ Context (hideRule : forall h c (r:Rule h c), bool).
+
+ Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
+ match pns with
+ | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
+ | scnd_weak c => rawLatexMath ""
+ | scnd_comp ht ct c pns rule => if hideRule _ _ rule
+ then SIND_toLatexMath pns
+ else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
+ SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
+ toLatexMath c +++ rawLatexMath "}" +++ eolL
+ end.
+ End SIND_toLatex.
+
+ (* this is a work-in-progress; please use SIND_toLatexMath for now *)
+ Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
+ match nd with
+ | nd_id0 => rawLatexMath indent +++
+ rawLatexMath "% nd_id0 " +++ eolL
+ | nd_id1 h' => rawLatexMath indent +++
+ rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
+ | nd_weak1 h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
+ | nd_copy h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
+ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
+ | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% prod " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " & " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% comp " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " \\ " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_cancell a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
+ | nd_cancelr a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
+ | nd_llecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
+ | nd_rlecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
+ | nd_assoc a b c => rawLatexMath ""
+ | nd_cossa a b c => rawLatexMath ""
+ | nd_rule h c r => toLatexMath r
+ end.
+
+End ToLatex.
+