+ (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
+ Section SequentND.
+ Context {S:Type}. (* type of sequent components *)
+ Context {sequent:S->S->Judgment}. (* pairing operation which forms a sequent from its halves *)
+ Notation "a |= b" := (sequent a b).
+
+ (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *)
+ Class SequentND :=
+ { snd_initial : forall a, [ ] /⋯⋯/ [ a |= a ]
+ ; snd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
+ }.
+
+ Context (sequentND:SequentND).
+ Context (ndr:ND_Relation).
+
+ (*
+ * A predicate singling out structural rules, initial sequents,
+ * and cut rules.
+ *
+ * Proofs using only structural rules cannot add or remove
+ * judgments - their hypothesis and conclusion judgment-trees will
+ * differ only in "parenthesization" and the presence/absence of
+ * empty leaves. This means that a proof involving only
+ * structural rules, cut, and initial sequents can ADD new
+ * non-empty judgment-leaves only via snd_initial, and can only
+ * REMOVE non-empty judgment-leaves only via snd_cut. Since the
+ * initial sequent is a left and right identity for cut, and cut
+ * is associative, any two proofs (with the same hypotheses and
+ * conclusions) using only structural rules, cut, and initial
+ * sequents are logically indistinguishable - their differences
+ * are logically insignificant.
+ *
+ * Note that it is important that nd_weak and nd_copy aren't
+ * considered to be "structural".
+ *)
+ Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | snd_inert_initial : forall a, SequentND_Inert _ _ (snd_initial a)
+ | snd_inert_cut : forall a b c, SequentND_Inert _ _ (snd_cut a b c)
+ | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
+ .
+
+ (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
+ * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
+ Class SequentND_Relation :=
+ { sndr_ndr := ndr
+ ; sndr_inert : forall a b (f g:a/⋯⋯/b),
+ NDPredicateClosure SequentND_Inert f ->
+ NDPredicateClosure SequentND_Inert g ->
+ ndr_eqv f g }.
+
+ End SequentND.
+
+ (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
+ Section ContextND.
+ Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
+ Context {snd:SequentND(sequent:=sequent)}.
+ Notation "a |= b" := (sequent a b).
+
+ (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
+ Class ContextND :=
+ { cnd_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x ]
+ ; cnd_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x ]
+ ; cnd_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x ]
+ ; cnd_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x ]
+ ; cnd_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x ]
+ ; cnd_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x ]
+ ; cnd_expand_left : forall a b c , ND [ a |= b] [ c,,a |= c,,b]
+ ; cnd_expand_right : forall a b c , ND [ a |= b] [ a,,c |= b,,c]
+ ; cnd_snd := snd
+ }.
+
+ Context `(ContextND).
+
+ (*
+ * A predicate singling out initial sequents, cuts, context expansion,
+ * and structural rules.
+ *
+ * Any two proofs (with the same hypotheses and conclusions) whose
+ * non-structural rules do nothing other than expand contexts,
+ * re-arrange contexts, or introduce additional initial-sequent
+ * conclusions are indistinguishable. One important consequence
+ * is that asking for a small initial sequent and then expanding
+ * it using cnd_expand_{right,left} is no different from simply
+ * asking for the larger initial sequent in the first place.
+ *
+ *)
+ Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | cnd_inert_initial : forall a, ContextND_Inert _ _ (snd_initial a)
+ | cnd_inert_cut : forall a b c, ContextND_Inert _ _ (snd_cut a b c)
+ | cnd_inert_structural : forall a b f, Structural f -> ContextND_Inert a b f
+ | cnd_inert_cnd_ant_assoc : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc x a b c)
+ | cnd_inert_cnd_ant_cossa : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa x a b c)
+ | cnd_inert_cnd_ant_cancell : forall x a , ContextND_Inert _ _ (cnd_ant_cancell x a)
+ | cnd_inert_cnd_ant_cancelr : forall x a , ContextND_Inert _ _ (cnd_ant_cancelr x a)
+ | cnd_inert_cnd_ant_llecnac : forall x a , ContextND_Inert _ _ (cnd_ant_llecnac x a)
+ | cnd_inert_cnd_ant_rlecnac : forall x a , ContextND_Inert _ _ (cnd_ant_rlecnac x a)
+ | cnd_inert_se_expand_left : forall t g s , ContextND_Inert _ _ (@cnd_expand_left _ t g s)
+ | cnd_inert_se_expand_right : forall t g s , ContextND_Inert _ _ (@cnd_expand_right _ t g s).
+
+ Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} :=
+ { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b),
+ NDPredicateClosure ContextND_Inert f ->
+ NDPredicateClosure ContextND_Inert g ->
+ ndr_eqv f g
+ ; cndr_sndr := sndr
+ }.
+
+ (* a proof is Analytic if it does not use cut *)
+ (*
+ Definition Analytic_Rule : NDPredicate :=
+ fun h c f => forall c, not (snd_cut _ _ c = f).
+ Definition AnalyticND := NDPredicateClosure Analytic_Rule.
+
+ (* a proof system has cut elimination if, for every proof, there is an analytic proof with the same conclusion *)
+ Class CutElimination :=
+ { ce_eliminate : forall h c, h/⋯⋯/c -> h/⋯⋯/c
+ ; ce_analytic : forall h c f, AnalyticND (ce_eliminate h c f)
+ }.
+
+ (* cut elimination is strong if the analytic proof is furthermore equivalent to the original proof *)
+ Class StrongCutElimination :=
+ { sce_ce <: CutElimination
+ ; ce_strong : forall h c f, f === ce_eliminate h c f
+ }.