src/NaturalDeduction.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeduction:                                                                                                             *)
   3 (*                                                                                                                               *)
   4 (*   Structurally explicit natural deduction proofs.                                                                             *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Coq.Strings.Ascii.
  12 Require Import Coq.Strings.String.
  13
  14 (*
  15  * IMPORTANT!!!
  16  *
  17  * Unlike most formalizations, this library offers TWO different ways
  18  * to represent a natural deduction proof.  To demonstrate this,
  19  * consider the signature of the propositional calculus:
  20  *
  21  *   Variable  PropositionalVariable : Type.
  22  *
  23  *   Inductive Formula : Prop :=
  24  *   | formula_var : PropositionalVariable -> Formula   (* every propositional variable is a formula *)
  25  *   | formula_and :   Formula ->  Formula -> Formula   (* the conjunction of any two formulae is a formula *)
  26  *   | formula_or  :   Formula ->  Formula -> Formula   (* the disjunction of any two formulae is a formula *)
  27  *
  28  * And couple this with the theory of conjunction and disjunction:
  29  * φ\/ψ is true if either φ is true or ψ is true, and φ/\ψ is true
  30  * if both φ and ψ are true.
  31  *
  32  * 1) Structurally implicit proofs
  33  *
  34  *    This is what you would call the "usual" representation –- it's
  35  *    what most people learn when they first start programming in Coq:
  36  *
  37  *    Inductive IsTrue : Formula -> Prop :=
  38  *    | IsTrue_or1 : forall f1 f2, IsTrue f1 ->              IsTrue (formula_or  f1 f2)
  39  *    | IsTrue_or2 : forall f1 f2,              IsTrue f2 -> IsTrue (formula_or  f1 f2)
  40  *    | IsTrue_and : forall f1 f2, IsTrue f2 -> IsTrue f2 -> IsTrue (formula_and f1 f2)
  41  *
  42  *    Here each judgment (such as "φ is true") is represented by a Coq
  43  *    type; furthermore:
  44  *
  45  *       1. A proof of a judgment is any inhabitant of that Coq type.
  46  *
  47  *       2. A proof of a judgment "J2" from hypothesis judgment "J1"
  48  *          is any Coq function from the Coq type for J1 to the Coq
  49  *          type for J2; Composition of (hypothetical) proofs is
  50  *          represented by composition of Coq functions.
  51  *
  52  *       3. A pair of judgments is represented by their product (Coq
  53  *          type [prod]) in Coq; a pair of proofs is represented by
  54  *          their pair (Coq function [pair]) in Coq.
  55  *
  56  *       4. Duplication of hypotheses is represented by the Coq
  57  *          function (fun x => (x,x)).  Dereliction of hypotheses is
  58  *          represented by the coq function (fun (x,y) => x) or (fun
  59  *          (x,y) => y).  Exchange of the order of hypotheses is
  60  *          represented by the Coq function (fun (x,y) => (y,x)).
  61  *
  62  *    The above can be done using lists instead of tuples.
  63  *
  64  *    The advantage of this approach is that it requires a minimum
  65  *    amount of syntax, and takes maximum advantage of Coq's
  66  *    automation facilities.
  67  *
  68  *    The disadvantage is that one cannot reason about proof-theoretic
  69  *    properties *generically* across different signatures and
  70  *    theories.  Each signature has its own type of judgments, and
  71  *    each theory has its own type of proofs.  In the present
  72  *    development we will want to prove –– in this generic manner --
  73  *    that various classes of natural deduction calculi form various
  74  *    kinds of categories.  So we will need this ability to reason
  75  *    about proofs independently of the type used to represent
  76  *    judgments and (more importantly) of the set of basic inference
  77  *    rules.
  78  *
  79  * 2) Structurally explicit proofs
  80  *
  81  *    Structurally explicit proofs are formalized in this file
  82  *    (NaturalDeduction.v) and are designed specifically in order to
  83  *    circumvent the problem in the previous paragraph.
  84  *
  85  *)
  86
  87 (*
  88  * REGARDING LISTS versus TREES:
  89  *
  90  * You'll notice that this formalization uses (Tree (option A)) in a
  91  * lot of places where you might find (list A) more natural.  If this
  92  * bothers you, see the end of the file for the technical reasons why.
  93  * In short, it lets us avoid having to mess about with JMEq or EqDep,
  94  * which are not as well-supported by the Coq core as the theory of
  95  * CiC proper.
  96  *)
  97
  98 Section Natural_Deduction.
  99
 100   (* any Coq Type may be used as the set of judgments *)
 101   Context {Judgment : Type}.
 102
 103   (* any Coq Type –- indexed by the hypothesis and conclusion judgments -- may be used as the set of basic inference rules *)
 104   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
 105
 106   (*
 107    *  This type represents a valid Natural Deduction proof from a list
 108    *  (tree) of hypotheses; the notation H/⋯⋯/C is meant to look like
 109    *  a proof tree with the middle missing if you tilt your head to
 110    *  the left (yeah, I know it's a stretch).  Note also that this
 111    *  type is capable of representing proofs with multiple
 112    *  conclusions, whereas a Rule may have only one conclusion.
 113    *)
 114   Inductive ND :
 115     forall hypotheses:Tree ??Judgment,
 116       forall conclusions:Tree ??Judgment,
 117         Type :=
 118
 119     (* natural deduction: you may infer anything from itself -- "identity proof" *)
 120     | nd_id0    :             [   ] /⋯⋯/ [   ]
 121     | nd_id1    : forall  h,  [ h ] /⋯⋯/ [ h ]
 122
 123     (* natural deduction: you may discard conclusions *)
 124     | nd_weak   : forall  h,  [ h ] /⋯⋯/ [   ]
 125
 126     (* natural deduction: you may duplicate conclusions *)
 127     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)
 128
 129     (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
 130     | nd_prod : forall {h1 h2 c1 c2}
 131        (pf1: h1       /⋯⋯/ c1      )
 132        (pf2:       h2 /⋯⋯/       c2),
 133        (     h1 ,, h2 /⋯⋯/ c1 ,, c2)
 134
 135     (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
 136     | nd_comp :
 137       forall {h x c}
 138       `(pf1: h /⋯⋯/ x)
 139       `(pf2: x /⋯⋯/ c),
 140        (     h /⋯⋯/ c)
 141
 142     (* structural rules on lists of judgments *)
 143     | nd_cancell : forall {a},       [] ,, a /⋯⋯/ a
 144     | nd_cancelr : forall {a},       a ,, [] /⋯⋯/ a
 145     | nd_llecnac : forall {a},             a /⋯⋯/ [] ,, a
 146     | nd_rlecnac : forall {a},             a /⋯⋯/ a ,, []
 147     | nd_assoc   : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c)
 148     | nd_cossa   : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c
 149
 150     (* any Rule by itself counts as a proof *)
 151     | nd_rule    : forall {h c} (r:Rule h c), h /⋯⋯/ c
 152
 153     where  "H /⋯⋯/ C" := (ND H C).
 154
 155     Notation "H /⋯⋯/ C" := (ND H C) : pf_scope.
 156     Notation "a ;; b"   := (nd_comp a b) : nd_scope.
 157     Notation "a ** b"   := (nd_prod a b) : nd_scope.
 158     Open Scope nd_scope.
 159     Open Scope pf_scope.
 160
 161   (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
 162   Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
 163   | nd_structural_id0     :                                                                            Structural nd_id0
 164   | nd_structural_id1     : forall h,                                                                  Structural (nd_id1 h)
 165   | nd_structural_weak    : forall h,                                                                  Structural (nd_weak h)
 166   | nd_structural_copy    : forall h,                                                                  Structural (nd_copy h)
 167   | nd_structural_prod    : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
 168   | nd_structural_comp    : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
 169   | nd_structural_cancell : forall {a},                                                                Structural (@nd_cancell a)
 170   | nd_structural_cancelr : forall {a},                                                                Structural (@nd_cancelr a)
 171   | nd_structural_llecnac : forall {a},                                                                Structural (@nd_llecnac a)
 172   | nd_structural_rlecnac : forall {a},                                                                Structural (@nd_rlecnac a)
 173   | nd_structural_assoc   : forall {a b c},                                                            Structural (@nd_assoc a b c)
 174   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
 175   .
 176
 177   (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
 178   Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
 179     match sl with
 180       | T_Leaf None      => nd_id0
 181       | T_Leaf (Some x)  => nd_id1 x
 182       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
 183     end.
 184
 185   Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
 186     match sl as SL return SL /⋯⋯/ [] with
 187       | T_Leaf None      => nd_id0
 188       | T_Leaf (Some x)  => nd_weak x
 189       | T_Branch a b     => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
 190     end.
 191
 192   Hint Constructors Structural.
 193   Lemma nd_id_structural : forall sl, Structural (nd_id sl).
 194     intros.
 195     induction sl; simpl; auto.
 196     destruct a; auto.
 197     Defined.
 198
 199   Lemma weak'_structural : forall a, Structural (nd_weak' a).
 200     intros.
 201     induction a.
 202     destruct a; auto.
 203     simpl.
 204     auto.
 205     simpl.
 206     auto.
 207     Qed.
 208
 209   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
 210    * structural variations  *)
 211   Class ND_Relation :=
 212   { ndr_eqv                  : forall {h c  }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _  pf1 pf2)
 213   ; ndr_eqv_equivalence      : forall h c, Equivalence (@ndr_eqv h c)
 214
 215   (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
 216   ; ndr_comp_respects        : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c),      f === f' -> g === g' -> f;;g === f';;g'
 217   ; ndr_comp_associativity   : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d),                         (f;;g);;h === f;;(g;;h)
 218   ; ndr_comp_left_identity   : forall `(f:a/⋯⋯/c),                                          nd_id _ ;; f   === f
 219   ; ndr_comp_right_identity  : forall `(f:a/⋯⋯/c),                                          f ;; nd_id _   === f
 220
 221   (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
 222   ; ndr_prod_respects        : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d),     f===f' -> g===g' ->    f**g === f'**g'
 223   ; ndr_prod_associativity   : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'),       (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
 224   ; ndr_prod_left_identity   : forall `(f:a/⋯⋯/b),                       (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
 225   ; ndr_prod_right_identity  : forall `(f:a/⋯⋯/b),                       (f ** nd_id0)  === nd_cancelr ;; f ;; nd_rlecnac
 226
 227   (* products and composition must distribute over each other *)
 228   ; ndr_prod_preserves_comp  : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
 229
 230   (* products and duplication must distribute over each other *)
 231   ; ndr_prod_preserves_copy  : forall `(f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
 232
 233   (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
 234   ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
 235
 236   (* any two proofs of nothing are "equally good" *)
 237   ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
 238   }.
 239
 240   (*
 241    * Single-conclusion proofs; this is an alternate representation
 242    * where each inference has only a single conclusion.  These have
 243    * worse compositionality properties than ND's, but are easier to
 244    * emit as LaTeX code.
 245    *)
 246   Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
 247   | scnd_comp   : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
 248   | scnd_weak   : forall c       , SCND c  []
 249   | scnd_leaf   : forall ht c    , SCND ht [c]  -> SCND ht [c]
 250   | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
 251   .
 252   Hint Constructors SCND.
 253
 254   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *)
 255   Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
 256     : forall h x c,  ND x c -> SCND h x -> SCND h c.
 257     intros h x c nd.
 258     induction nd; intro k.
 259       apply k.
 260       apply k.
 261       apply scnd_weak.
 262       eapply scnd_branch; apply k.
 263       inversion k; subst.
 264         apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
 265       apply IHnd2.
 266         apply IHnd1.
 267         apply k.
 268       inversion k; subst; auto.
 269       inversion k; subst; auto.
 270       apply scnd_branch; auto.
 271       apply scnd_branch; auto.
 272       inversion k; subst; inversion X; subst; auto.
 273       inversion k; subst; inversion X0; subst; auto.
 274       destruct c.
 275         destruct o.
 276         apply scnd_leaf. eapply scnd_comp. apply k. apply r.
 277         apply scnd_weak.
 278         set (all_rules_one_conclusion _ _ _ r) as bogus.
 279           inversion bogus.
 280           Defined.
 281
 282   (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *)
 283   Inductive ClosedND : Tree ??Judgment -> Type :=
 284   | cnd_weak   : ClosedND []
 285   | cnd_rule   : forall h c    , ClosedND h  -> Rule h c    -> ClosedND c
 286   | cnd_branch : forall   c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2)
 287   .
 288
 289   (* we can turn an SCND without hypotheses into a ClosedND *)
 290   Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
 291   refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
 292     (match pn2 in SCND H C return H=h -> C=c -> _  with
 293       | scnd_weak   c                 => let case_weak := tt in _
 294       | scnd_leaf   ht z pn'          => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _
 295       | scnd_comp  ht ct c pn' rule   => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
 296       | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
 297                                         let q1 := closedFromPnodes _ _ pn' in
 298                                         let q2 := closedFromPnodes _ _ pn'' in _
 299
 300     end (refl_equal _) (refl_equal _))) h c pn2 cnd).
 301
 302   destruct case_comp.
 303     intros.
 304     clear pn2.
 305     apply (cnd_rule ct).
 306     apply qq.
 307     subst.
 308     apply cnd0.
 309     apply rule.
 310
 311   destruct case_weak.
 312     intros; subst.
 313     apply cnd_weak.
 314
 315   destruct case_leaf.
 316     intros.
 317     apply qq.
 318     subst.
 319     apply cnd0.
 320
 321   destruct case_branch.
 322     intros.
 323     apply cnd_branch.
 324     apply q1. subst. apply cnd0.
 325     apply q2. subst. apply cnd0.
 326     Defined.
 327
 328   (* undo the above *)
 329   Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
 330   match cnd in ClosedND C return ND [] C with
 331   | cnd_weak                   => nd_id0
 332   | cnd_rule   h c cndh rhc    => closedNDtoNormalND cndh ;; nd_rule rhc
 333   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
 334   end.
 335
 336   Section Sequents.
 337     Context {S:Type}.   (* type of sequent components *)
 338     Context {sequent:S->S->Judgment}.
 339     Context {ndr:ND_Relation}.
 340     Notation "a |= b" := (sequent a b).
 341     Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
 342
 343     Class SequentCalculus :=
 344     { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
 345     }.
 346
 347     Class CutRule (nd_cutrule_seq:SequentCalculus) :=
 348     { nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
 349     ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
 350     ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
 351     ; nd_cut_associativity :  forall {a b c d},
 352       (nd_id1 (a|=b) ** nd_cut b c d) ;; (nd_cut a b d) === nd_cossa ;; (nd_cut a b c ** nd_id1 (c|=d)) ;; nd_cut a c d
 353     }.
 354
 355   End Sequents.
 356 (*Implicit Arguments SequentCalculus [ S ]*)
 357 (*Implicit Arguments CutRule [ S ]*)
 358   Section SequentsOfTrees.
 359     Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}.
 360     Context (ndr:ND_Relation).
 361     Notation "a |= b" := (sequent a b).
 362     Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
 363
 364     Class TreeStructuralRules :=
 365     { tsr_ant_assoc     : forall {x a b c}, ND [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x]
 366     ; tsr_ant_cossa     : forall {x a b c}, ND [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x]
 367     ; tsr_ant_cancell   : forall {x a    }, ND [  [],,a     |= x]     [        a   |= x]
 368     ; tsr_ant_cancelr   : forall {x a    }, ND [a,,[]       |= x]     [        a   |= x]
 369     ; tsr_ant_llecnac   : forall {x a    }, ND [      a     |= x]     [    [],,a   |= x]
 370     ; tsr_ant_rlecnac   : forall {x a    }, ND [      a     |= x]     [    a,,[]   |= x]
 371     }.
 372
 373     Notation "[# a #]"  := (nd_rule a)               : nd_scope.
 374
 375     Context `{se_cut : @CutRule _ sequent ndr sc}.
 376     Class SequentExpansion :=
 377     { se_expand_left     : forall tau {Gamma Sigma}, ND [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
 378     ; se_expand_right    : forall tau {Gamma Sigma}, ND [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
 379
 380     (* left and right expansion must commute with cut *)
 381     ; se_reflexive_left  : ∀ a c,     nd_seq_reflexive a;; se_expand_left  c === nd_seq_reflexive (c,, a)
 382     ; se_reflexive_right : ∀ a c,     nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c)
 383     ; se_cut_left        : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c)
 384     ; se_cut_right       : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c)
 385     }.
 386   End SequentsOfTrees.
 387
 388   Close Scope nd_scope.
 389   Open Scope pf_scope.
 390
 391 End Natural_Deduction.
 392
 393 Coercion nd_cut : CutRule >-> Funclass.
 394
 395 Implicit Arguments ND [ Judgment ].
 396 Hint Constructors Structural.
 397 Hint Extern 1 => apply nd_id_structural.
 398 Hint Extern 1 => apply ndr_structural_indistinguishable.
 399
 400 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
 401  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
 402 Notation "H /⋯⋯/ C" := (@ND _ _ H C)             : pf_scope.
 403 Notation "a ;; b"   := (nd_comp a b)             : nd_scope.
 404 Notation "a ** b"   := (nd_prod a b)             : nd_scope.
 405 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
 406 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
 407
 408 (* enable setoid rewriting *)
 409 Open Scope nd_scope.
 410 Open Scope pf_scope.
 411
 412 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
 413   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
 414   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
 415   transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
 416     as parametric_relation_ndr_eqv.
 417   Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
 418   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
 419     as parametric_morphism_nd_comp.
 420     intros; apply ndr_comp_respects; auto.
 421     Defined.
 422   Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
 423   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
 424     as parametric_morphism_nd_prod.
 425     intros; apply ndr_prod_respects; auto.
 426     Defined.
 427
 428 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
 429 Definition nd_replicate
 430   : forall
 431     {Judgment}{Rule}{Ob}
 432     (h:Ob->Judgment)
 433     (c:Ob->Judgment)
 434     (j:Tree ??Ob),
 435     (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
 436     @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
 437   intros.
 438   induction j; simpl.
 439     destruct a; simpl.
 440     apply X.
 441     apply nd_id0.
 442     apply nd_prod; auto.
 443     Defined.
 444
 445 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
 446 Definition nd_map
 447   : forall
 448     {Judgment}{Rule0}{Rule1}
 449     (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
 450     {h}{c}
 451     (pf:@ND Judgment Rule0 h c)
 452     ,
 453     @ND Judgment Rule1 h c.
 454     intros Judgment Rule0 Rule1 r.
 455
 456     refine ((fix nd_map h c pf {struct pf} :=
 457      ((match pf
 458          in @ND _ _ H C
 459           return
 460           @ND Judgment Rule1 H C
 461         with
 462         | nd_id0                     => let case_nd_id0     := tt in _
 463         | nd_id1     h               => let case_nd_id1     := tt in _
 464         | nd_weak    h               => let case_nd_weak    := tt in _
 465         | nd_copy    h               => let case_nd_copy    := tt in _
 466         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 467         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 468         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 469         | nd_cancell _               => let case_nd_cancell := tt in _
 470         | nd_cancelr _               => let case_nd_cancelr := tt in _
 471         | nd_llecnac _               => let case_nd_llecnac := tt in _
 472         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 473         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 474         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 475       end))) ); simpl in *.
 476
 477     destruct case_nd_id0.      apply nd_id0.
 478     destruct case_nd_id1.      apply nd_id1.
 479     destruct case_nd_weak.     apply nd_weak.
 480     destruct case_nd_copy.     apply nd_copy.
 481     destruct case_nd_prod.     apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
 482     destruct case_nd_comp.     apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
 483     destruct case_nd_cancell.  apply nd_cancell.
 484     destruct case_nd_cancelr.  apply nd_cancelr.
 485     destruct case_nd_llecnac.  apply nd_llecnac.
 486     destruct case_nd_rlecnac.  apply nd_rlecnac.
 487     destruct case_nd_assoc.    apply nd_assoc.
 488     destruct case_nd_cossa.    apply nd_cossa.
 489     apply r. apply rule.
 490     Defined.
 491
 492 (* "map" over natural deduction proofs, where the result proof has different judgments *)
 493 Definition nd_map'
 494   : forall
 495     {Judgment0}{Rule0}{Judgment1}{Rule1}
 496     (f:Judgment0->Judgment1)
 497     (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
 498     {h}{c}
 499     (pf:@ND Judgment0 Rule0 h c)
 500     ,
 501     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
 502     intros Judgment0 Rule0 Judgment1 Rule1 f r.
 503
 504     refine ((fix nd_map' h c pf {struct pf} :=
 505      ((match pf
 506          in @ND _ _ H C
 507           return
 508           @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
 509         with
 510         | nd_id0                     => let case_nd_id0     := tt in _
 511         | nd_id1     h               => let case_nd_id1     := tt in _
 512         | nd_weak    h               => let case_nd_weak    := tt in _
 513         | nd_copy    h               => let case_nd_copy    := tt in _
 514         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 515         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 516         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 517         | nd_cancell _               => let case_nd_cancell := tt in _
 518         | nd_cancelr _               => let case_nd_cancelr := tt in _
 519         | nd_llecnac _               => let case_nd_llecnac := tt in _
 520         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 521         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 522         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 523       end))) ); simpl in *.
 524
 525     destruct case_nd_id0.      apply nd_id0.
 526     destruct case_nd_id1.      apply nd_id1.
 527     destruct case_nd_weak.     apply nd_weak.
 528     destruct case_nd_copy.     apply nd_copy.
 529     destruct case_nd_prod.     apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
 530     destruct case_nd_comp.     apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
 531     destruct case_nd_cancell.  apply nd_cancell.
 532     destruct case_nd_cancelr.  apply nd_cancelr.
 533     destruct case_nd_llecnac.  apply nd_llecnac.
 534     destruct case_nd_rlecnac.  apply nd_rlecnac.
 535     destruct case_nd_assoc.    apply nd_assoc.
 536     destruct case_nd_cossa.    apply nd_cossa.
 537     apply r. apply rule.
 538     Defined.
 539
 540 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
 541 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
 542   | nd_property_structural      : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
 543   | nd_property_prod            : forall h0 c0 pf0 h1 c1 pf1,
 544     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
 545   | nd_property_comp            : forall h0 c0 pf0  c1 pf1,
 546     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
 547   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
 548   Hint Constructors nd_property.
 549
 550 Close Scope pf_scope.
 551 Close Scope nd_scope.