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  * Unlike most formalizations, this library offers two different ways
  16  * to represent a natural deduction proof.  To demonstrate this,
  17  * consider the signature of the propositional calculus:
  18  *
  19  *   Variable  PropositionalVariable : Type.
  20  *
  21  *   Inductive Formula : Prop :=
  22  *   | formula_var : PropositionalVariable -> Formula   (* every propositional variable is a formula *)
  23  *   | formula_and :   Formula ->  Formula -> Formula   (* the conjunction of any two formulae is a formula *)
  24  *   | formula_or  :   Formula ->  Formula -> Formula   (* the disjunction of any two formulae is a formula *)
  25  *
  26  * And couple this with the theory of conjunction and disjunction:
  27  * φ\/ψ is true if either φ is true or ψ is true, and φ/\ψ is true
  28  * if both φ and ψ are true.
  29  *
  30  * 1) Structurally implicit proofs
  31  *
  32  *    This is what you would call the "usual" representation –- it's
  33  *    what most people learn when they first start programming in Coq:
  34  *
  35  *    Inductive IsTrue : Formula -> Prop :=
  36  *    | IsTrue_or1 : forall f1 f2, IsTrue f1 ->              IsTrue (formula_or  f1 f2)
  37  *    | IsTrue_or2 : forall f1 f2,              IsTrue f2 -> IsTrue (formula_or  f1 f2)
  38  *    | IsTrue_and : forall f1 f2, IsTrue f2 -> IsTrue f2 -> IsTrue (formula_and f1 f2)
  39  *
  40  *    Here each judgment (such as "φ is true") is represented by a Coq
  41  *    type; furthermore:
  42  *
  43  *       1. A proof of a judgment is any inhabitant of that Coq type.
  44  *
  45  *       2. A proof of a judgment "J2" from hypothesis judgment "J1"
  46  *          is any Coq function from the Coq type for J1 to the Coq
  47  *          type for J2; Composition of (hypothetical) proofs is
  48  *          represented by composition of Coq functions.
  49  *
  50  *       3. A pair of judgments is represented by their product (Coq
  51  *          type [prod]) in Coq; a pair of proofs is represented by
  52  *          their pair (Coq function [pair]) in Coq.
  53  *
  54  *       4. Duplication of hypotheses is represented by the Coq
  55  *          function (fun x => (x,x)).  Dereliction of hypotheses is
  56  *          represented by the coq function (fun (x,y) => x) or (fun
  57  *          (x,y) => y).  Exchange of the order of hypotheses is
  58  *          represented by the Coq function (fun (x,y) => (y,x)).
  59  *
  60  *    The above can be done using lists instead of tuples.
  61  *
  62  *    The advantage of this approach is that it requires a minimum
  63  *    amount of syntax, and takes maximum advantage of Coq's
  64  *    automation facilities.
  65  *
  66  *    The disadvantage is that one cannot reason about proof-theoretic
  67  *    properties *generically* across different signatures and
  68  *    theories.  Each signature has its own type of judgments, and
  69  *    each theory has its own type of proofs.  In the present
  70  *    development we will want to prove –– in this generic manner --
  71  *    that various classes of natural deduction calculi form various
  72  *    kinds of categories.  So we will need this ability to reason
  73  *    about proofs independently of the type used to represent
  74  *    judgments and (more importantly) of the set of basic inference
  75  *    rules.
  76  *
  77  * 2) Structurally explicit proofs
  78  *
  79  *    Structurally explicit proofs are formalized in this file
  80  *    (NaturalDeduction.v) and are designed specifically in order to
  81  *    circumvent the problem in the previous paragraph.
  82  *
  83  *    These proofs are actually structurally explicit on (potentially)
  84  *    two different levels.  The beginning of this file formalizes
  85  *    natural deduction proofs with explicit structural operations for
  86  *    manipulating lists of judgments – for example, the open
  87  *    hypotheses of an incomplete proof.  The class
  88  *    TreeStructuralRules further down in the file instantiates ND
  89  *    such that Judgments is actually a pair of trees of propositions,
  90  *    and there will be a whole *other* set of rules for manipulating
  91  *    the structure of a tree of propositions *within* a single
  92  *    judgment.
  93  *
  94  *    The flattening functor ends up mapping the first kind of
  95  *    structural operation (moving around judgments) onto the second
  96  *    kind (moving around propositions/types).  That's why everything
  97  *    is so laboriously explicit - there's important information in
  98  *    those structural operations.
  99  *)
 100
 101 (*
 102  * REGARDING LISTS versus TREES:
 103  *
 104  * You'll notice that this formalization uses (Tree (option A)) in a
 105  * lot of places where you might find (list A) more natural.  If this
 106  * bothers you, see the end of the file for the technical reasons why.
 107  * In short, it lets us avoid having to mess about with JMEq or EqDep,
 108  * which are not as well-supported by the Coq core as the theory of
 109  * CiC proper.
 110  *)
 111
 112 Section Natural_Deduction.
 113
 114   (* any Coq Type may be used as the set of judgments *)
 115   Context {Judgment : Type}.
 116
 117   (* any Coq Type –- indexed by the hypothesis and conclusion judgments -- may be used as the set of basic inference rules *)
 118   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
 119
 120   (*
 121    *  This type represents a valid Natural Deduction proof from a list
 122    *  (tree) of hypotheses; the notation H/⋯⋯/C is meant to look like
 123    *  a proof tree with the middle missing if you tilt your head to
 124    *  the left (yeah, I know it's a stretch).  Note also that this
 125    *  type is capable of representing proofs with multiple
 126    *  conclusions, whereas a Rule may have only one conclusion.
 127    *)
 128   Inductive ND :
 129     forall hypotheses:Tree ??Judgment,
 130       forall conclusions:Tree ??Judgment,
 131         Type :=
 132
 133     (* natural deduction: you may infer nothing from nothing *)
 134     | nd_id0    :             [   ] /⋯⋯/ [   ]
 135
 136     (* natural deduction: you may infer anything from itself -- "identity proof" *)
 137     | nd_id1    : forall  h,  [ h ] /⋯⋯/ [ h ]
 138
 139     (* natural deduction: you may discard conclusions *)
 140     | nd_weak1  : forall  h,  [ h ] /⋯⋯/ [   ]
 141
 142     (* natural deduction: you may duplicate conclusions *)
 143     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)
 144
 145     (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
 146     | nd_prod : forall {h1 h2 c1 c2}
 147        (pf1: h1       /⋯⋯/ c1      )
 148        (pf2:       h2 /⋯⋯/       c2),
 149        (     h1 ,, h2 /⋯⋯/ c1 ,, c2)
 150
 151     (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
 152     | nd_comp :
 153       forall {h x c}
 154       `(pf1: h /⋯⋯/ x)
 155       `(pf2: x /⋯⋯/ c),
 156        (     h /⋯⋯/ c)
 157
 158     (* Structural rules on lists of judgments - note that this is completely separate from the structural
 159      * rules for *contexts* within a sequent.  The rules below manipulate lists of *judgments* rather than
 160      * lists of *propositions*. *)
 161     | nd_cancell : forall {a},       [] ,, a /⋯⋯/ a
 162     | nd_cancelr : forall {a},       a ,, [] /⋯⋯/ a
 163     | nd_llecnac : forall {a},             a /⋯⋯/ [] ,, a
 164     | nd_rlecnac : forall {a},             a /⋯⋯/ a ,, []
 165     | nd_assoc   : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c)
 166     | nd_cossa   : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c
 167
 168     (* any Rule by itself counts as a proof *)
 169     | nd_rule    : forall {h c} (r:Rule h c), h /⋯⋯/ c
 170
 171     where  "H /⋯⋯/ C" := (ND H C).
 172
 173     Notation "H /⋯⋯/ C" := (ND H C) : pf_scope.
 174     Notation "a ;; b"   := (nd_comp a b) : nd_scope.
 175     Notation "a ** b"   := (nd_prod a b) : nd_scope.
 176     Open Scope nd_scope.
 177     Open Scope pf_scope.
 178
 179   (* a predicate on proofs *)
 180   Definition NDPredicate := forall h c, h /⋯⋯/ c -> Prop.
 181
 182   (* the structural inference rules are those which do not change, add, remove, or re-order the judgments *)
 183   Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
 184   | nd_structural_id0     :                                                                            Structural nd_id0
 185   | nd_structural_id1     : forall h,                                                                  Structural (nd_id1 h)
 186   | nd_structural_cancell : forall {a},                                                                Structural (@nd_cancell a)
 187   | nd_structural_cancelr : forall {a},                                                                Structural (@nd_cancelr a)
 188   | nd_structural_llecnac : forall {a},                                                                Structural (@nd_llecnac a)
 189   | nd_structural_rlecnac : forall {a},                                                                Structural (@nd_rlecnac a)
 190   | nd_structural_assoc   : forall {a b c},                                                            Structural (@nd_assoc a b c)
 191   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
 192   .
 193
 194   (* the closure of an NDPredicate under nd_comp and nd_prod *)
 195   Inductive NDPredicateClosure (P:NDPredicate) : forall {h c}, h /⋯⋯/ c -> Prop :=
 196   | ndpc_p       : forall h c f, P h c f                                                   -> NDPredicateClosure P f
 197   | ndpc_prod    : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2),
 198     NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1**pf2)
 199   | ndpc_comp    : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2),
 200     NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1;;pf2).
 201
 202   (* proofs built up from structural rules via comp and prod *)
 203   Definition StructuralND {h}{c} f := @NDPredicateClosure (@Structural) h c f.
 204
 205   (* The Predicate (BuiltFrom f P h) asserts that "h" was built from a single occurrence of "f" and proofs which satisfy P *)
 206   Inductive BuiltFrom {h'}{c'}(f:h'/⋯⋯/c')(P:NDPredicate) : forall {h c}, h/⋯⋯/c -> Prop :=
 207   | builtfrom_refl  : BuiltFrom f P f
 208   | builtfrom_P     : forall h c g, @P h c g -> BuiltFrom f P g
 209   | builtfrom_prod1 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f1 ** f2)
 210   | builtfrom_prod2 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f2 ** f1)
 211   | builtfrom_comp1 : forall h x c       f1 f2, P h  x  f1 -> @BuiltFrom _ _ f P x  c  f2 -> BuiltFrom f P (f1 ;; f2)
 212   | builtfrom_comp2 : forall h x c       f1 f2, P x  c  f1 -> @BuiltFrom _ _ f P h  x  f2 -> BuiltFrom f P (f2 ;; f1).
 213
 214   (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
 215   Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
 216     match sl with
 217       | T_Leaf None      => nd_id0
 218       | T_Leaf (Some x)  => nd_id1 x
 219       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
 220     end.
 221
 222   Fixpoint nd_weak (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
 223     match sl as SL return SL /⋯⋯/ [] with
 224       | T_Leaf None      => nd_id0
 225       | T_Leaf (Some x)  => nd_weak1 x
 226       | T_Branch a b     => nd_prod (nd_weak a) (nd_weak b) ;; nd_cancelr
 227     end.
 228
 229   Hint Constructors Structural.
 230   Hint Constructors BuiltFrom.
 231   Hint Constructors NDPredicateClosure.
 232
 233   Hint Extern 1 => apply nd_structural_id0.
 234   Hint Extern 1 => apply nd_structural_id1.
 235   Hint Extern 1 => apply nd_structural_cancell.
 236   Hint Extern 1 => apply nd_structural_cancelr.
 237   Hint Extern 1 => apply nd_structural_llecnac.
 238   Hint Extern 1 => apply nd_structural_rlecnac.
 239   Hint Extern 1 => apply nd_structural_assoc.
 240   Hint Extern 1 => apply nd_structural_cossa.
 241   Hint Extern 1 => apply ndpc_p.
 242   Hint Extern 1 => apply ndpc_prod.
 243   Hint Extern 1 => apply ndpc_comp.
 244
 245   Lemma nd_id_structural : forall sl, StructuralND (nd_id sl).
 246     intros.
 247     induction sl; simpl; auto.
 248     destruct a; auto.
 249     Defined.
 250
 251   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
 252    * structural variations  *)
 253   Class ND_Relation :=
 254   { ndr_eqv                  : forall {h c  }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _  pf1 pf2)
 255   ; ndr_eqv_equivalence      : forall h c, Equivalence (@ndr_eqv h c)
 256
 257   (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
 258   ; ndr_comp_respects        : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c),      f === f' -> g === g' -> f;;g === f';;g'
 259   ; ndr_comp_associativity   : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d),                         (f;;g);;h === f;;(g;;h)
 260
 261   (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
 262   ; ndr_prod_respects        : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d),     f===f' -> g===g' ->    f**g === f'**g'
 263   ; ndr_prod_associativity   : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'),       (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
 264
 265   (* products and composition must distribute over each other *)
 266   ; 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')
 267
 268   (* Given a proof f, any two proofs built from it using only structural rules are indistinguishable.  Keep in mind that
 269    * nd_weak and nd_copy aren't considered structural, so the hypotheses and conclusions of such proofs will be an identical
 270    * list, differing only in the "parenthesization" and addition or removal of empty leaves. *)
 271   ; ndr_builtfrom_structural : forall `(f:a/⋯⋯/b){a' b'}(g1 g2:a'/⋯⋯/b'),
 272     BuiltFrom f (@StructuralND) g1 ->
 273     BuiltFrom f (@StructuralND) g2 ->
 274     g1 === g2
 275
 276   (* proofs of nothing are not distinguished from each other *)
 277   ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
 278
 279   (* products and duplication must distribute over each other *)
 280   ; ndr_prod_preserves_copy  : forall `(f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
 281
 282   (* duplicating a hypothesis and discarding it is irrelevant *)
 283   ; ndr_copy_then_weak_left   : forall a,                            nd_copy a;; (nd_weak _ ** nd_id _) ;; nd_cancell === nd_id _
 284   ; ndr_copy_then_weak_right  : forall a,                            nd_copy a;; (nd_id _ ** nd_weak _) ;; nd_cancelr === nd_id _
 285   }.
 286
 287   (*
 288    * Natural Deduction proofs which are Structurally Implicit on the
 289    * level of judgments.  These proofs have poor compositionality
 290    * properties (vertically, they look more like lists than trees) but
 291    * are easier to do induction over.
 292    *)
 293   Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type :=
 294   | scnd_weak   : forall c       , SIND c  []
 295   | scnd_comp   : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c]
 296   | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2)
 297   .
 298   Hint Constructors SIND.
 299
 300   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *)
 301   Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
 302     : forall h x c,  ND x c -> SIND h x -> SIND h c.
 303     intros h x c nd.
 304     induction nd; intro k.
 305       apply k.
 306       apply k.
 307       apply scnd_weak.
 308       eapply scnd_branch; apply k.
 309       inversion k; subst.
 310         apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
 311       apply IHnd2.
 312         apply IHnd1.
 313         apply k.
 314       inversion k; subst; auto.
 315       inversion k; subst; auto.
 316       apply scnd_branch; auto.
 317       apply scnd_branch; auto.
 318       inversion k; subst; inversion X; subst; auto.
 319       inversion k; subst; inversion X0; subst; auto.
 320       destruct c.
 321         destruct o.
 322         eapply scnd_comp. apply k. apply r.
 323         apply scnd_weak.
 324         set (all_rules_one_conclusion _ _ _ r) as bogus.
 325           inversion bogus.
 326           Defined.
 327
 328   (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *)
 329   Inductive ClosedSIND : Tree ??Judgment -> Type :=
 330   | cnd_weak   : ClosedSIND []
 331   | cnd_rule   : forall h c    , ClosedSIND h  -> Rule h c    -> ClosedSIND c
 332   | cnd_branch : forall   c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2)
 333   .
 334
 335   (* we can turn an SIND without hypotheses into a ClosedSIND *)
 336   Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c.
 337   refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} :=
 338     (match pn2 in SIND H C return H=h -> C=c -> _  with
 339       | scnd_weak   c                 => let case_weak := tt in _
 340       | scnd_comp  ht ct c pn' rule   => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
 341       | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
 342                                          let q1 := closedFromPnodes _ _ pn' in
 343                                          let q2 := closedFromPnodes _ _ pn'' in _
 344
 345     end (refl_equal _) (refl_equal _))) h c pn2 cnd).
 346
 347   destruct case_weak.
 348     intros; subst.
 349     apply cnd_weak.
 350
 351   destruct case_comp.
 352     intros.
 353     clear pn2.
 354     apply (cnd_rule ct).
 355     apply qq.
 356     subst.
 357     apply cnd0.
 358     apply rule.
 359
 360   destruct case_branch.
 361     intros.
 362     apply cnd_branch.
 363     apply q1. subst. apply cnd0.
 364     apply q2. subst. apply cnd0.
 365     Defined.
 366
 367   (* undo the above *)
 368   Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c :=
 369   match cnd in ClosedSIND C return ND [] C with
 370   | cnd_weak                   => nd_id0
 371   | cnd_rule   h c cndh rhc    => closedNDtoNormalND cndh ;; nd_rule rhc
 372   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
 373   end.
 374
 375   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
 376   Section SequentND.
 377     Context {S:Type}.                   (* type of sequent components *)
 378     Context {sequent:S->S->Judgment}.   (* pairing operation which forms a sequent from its halves *)
 379     Notation "a |= b" := (sequent a b).
 380
 381     (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *)
 382     Class SequentND :=
 383     { snd_initial : forall a,                           [ ] /⋯⋯/ [ a |= a ]
 384     ; snd_cut     : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
 385     }.
 386
 387     Context (sequentND:SequentND).
 388     Context (ndr:ND_Relation).
 389
 390     (*
 391      * A predicate singling out structural rules, initial sequents,
 392      * and cut rules.
 393      *
 394      * Proofs using only structural rules cannot add or remove
 395      * judgments - their hypothesis and conclusion judgment-trees will
 396      * differ only in "parenthesization" and the presence/absence of
 397      * empty leaves.  This means that a proof involving only
 398      * structural rules, cut, and initial sequents can ADD new
 399      * non-empty judgment-leaves only via snd_initial, and can only
 400      * REMOVE non-empty judgment-leaves only via snd_cut.  Since the
 401      * initial sequent is a left and right identity for cut, and cut
 402      * is associative, any two proofs (with the same hypotheses and
 403      * conclusions) using only structural rules, cut, and initial
 404      * sequents are logically indistinguishable - their differences
 405      * are logically insignificant.
 406      *
 407      * Note that it is important that nd_weak and nd_copy aren't
 408      * considered to be "structural".
 409      *)
 410     Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
 411     | snd_inert_initial   : forall a,                     SequentND_Inert _ _ (snd_initial a)
 412     | snd_inert_cut       : forall a b c,                 SequentND_Inert _ _ (snd_cut a b c)
 413     | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
 414     .
 415
 416     (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
 417      * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
 418     Class SequentND_Relation :=
 419     { sndr_ndr   := ndr
 420     ; sndr_inert : forall a b (f g:a/⋯⋯/b),
 421       NDPredicateClosure SequentND_Inert f ->
 422       NDPredicateClosure SequentND_Inert g ->
 423       ndr_eqv f g }.
 424
 425   End SequentND.
 426
 427   (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
 428   Section ContextND.
 429     Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
 430     Context {snd:SequentND(sequent:=sequent)}.
 431     Notation "a |= b" := (sequent a b).
 432
 433     (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
 434     Class ContextND :=
 435     { cnd_ant_assoc     : forall x a b c, ND [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x   ]
 436     ; cnd_ant_cossa     : forall x a b c, ND [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x   ]
 437     ; cnd_ant_cancell   : forall x a    , ND [  [],,a     |= x]     [        a   |= x   ]
 438     ; cnd_ant_cancelr   : forall x a    , ND [a,,[]       |= x]     [        a   |= x   ]
 439     ; cnd_ant_llecnac   : forall x a    , ND [      a     |= x]     [    [],,a   |= x   ]
 440     ; cnd_ant_rlecnac   : forall x a    , ND [      a     |= x]     [    a,,[]   |= x   ]
 441     ; cnd_expand_left   : forall a b c  , ND [          a |= b]     [ c,,a       |= c,,b]
 442     ; cnd_expand_right  : forall a b c  , ND [          a |= b]     [ a,,c       |= b,,c]
 443     ; cnd_snd           := snd
 444     }.
 445
 446     Context `(ContextND).
 447
 448     (*
 449      * A predicate singling out initial sequents, cuts, context expansion,
 450      * and structural rules.
 451      *
 452      * Any two proofs (with the same hypotheses and conclusions) whose
 453      * non-structural rules do nothing other than expand contexts,
 454      * re-arrange contexts, or introduce additional initial-sequent
 455      * conclusions are indistinguishable.  One important consequence
 456      * is that asking for a small initial sequent and then expanding
 457      * it using cnd_expand_{right,left} is no different from simply
 458      * asking for the larger initial sequent in the first place.
 459      *
 460      *)
 461     Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop :=
 462     | cnd_inert_initial           : forall a,                     ContextND_Inert _ _ (snd_initial a)
 463     | cnd_inert_cut               : forall a b c,                 ContextND_Inert _ _ (snd_cut a b c)
 464     | cnd_inert_structural        : forall a b f, Structural f -> ContextND_Inert a b f
 465     | cnd_inert_cnd_ant_assoc     : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc   x a b c)
 466     | cnd_inert_cnd_ant_cossa     : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa   x a b c)
 467     | cnd_inert_cnd_ant_cancell   : forall x a    , ContextND_Inert _ _ (cnd_ant_cancell x a)
 468     | cnd_inert_cnd_ant_cancelr   : forall x a    , ContextND_Inert _ _ (cnd_ant_cancelr x a)
 469     | cnd_inert_cnd_ant_llecnac   : forall x a    , ContextND_Inert _ _ (cnd_ant_llecnac x a)
 470     | cnd_inert_cnd_ant_rlecnac   : forall x a    , ContextND_Inert _ _ (cnd_ant_rlecnac x a)
 471     | cnd_inert_se_expand_left    : forall t g s  , ContextND_Inert _ _ (@cnd_expand_left  _ t g s)
 472     | cnd_inert_se_expand_right   : forall t g s  , ContextND_Inert _ _ (@cnd_expand_right _ t g s).
 473
 474     Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} :=
 475     { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b),
 476                            NDPredicateClosure ContextND_Inert f ->
 477                            NDPredicateClosure ContextND_Inert g ->
 478                            ndr_eqv f g
 479     ; cndr_sndr  := sndr
 480     }.
 481
 482   End ContextND.
 483
 484   Close Scope nd_scope.
 485   Open Scope pf_scope.
 486
 487 End Natural_Deduction.
 488
 489 Coercion snd_cut   : SequentND >-> Funclass.
 490 Coercion cnd_snd   : ContextND >-> SequentND.
 491 Coercion sndr_ndr  : SequentND_Relation >-> ND_Relation.
 492 Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation.
 493
 494 Implicit Arguments ND [ Judgment ].
 495 Hint Constructors Structural.
 496 Hint Extern 1 => apply nd_id_structural.
 497 Hint Extern 1 => apply ndr_builtfrom_structural.
 498 Hint Extern 1 => apply nd_structural_id0.
 499 Hint Extern 1 => apply nd_structural_id1.
 500 Hint Extern 1 => apply nd_structural_cancell.
 501 Hint Extern 1 => apply nd_structural_cancelr.
 502 Hint Extern 1 => apply nd_structural_llecnac.
 503 Hint Extern 1 => apply nd_structural_rlecnac.
 504 Hint Extern 1 => apply nd_structural_assoc.
 505 Hint Extern 1 => apply nd_structural_cossa.
 506 Hint Extern 1 => apply ndpc_p.
 507 Hint Extern 1 => apply ndpc_prod.
 508 Hint Extern 1 => apply ndpc_comp.
 509 Hint Extern 1 => apply builtfrom_refl.
 510 Hint Extern 1 => apply builtfrom_prod1.
 511 Hint Extern 1 => apply builtfrom_prod2.
 512 Hint Extern 1 => apply builtfrom_comp1.
 513 Hint Extern 1 => apply builtfrom_comp2.
 514 Hint Extern 1 => apply builtfrom_P.
 515
 516 Hint Extern 1 => apply snd_inert_initial.
 517 Hint Extern 1 => apply snd_inert_cut.
 518 Hint Extern 1 => apply snd_inert_structural.
 519
 520 Hint Extern 1 => apply cnd_inert_initial.
 521 Hint Extern 1 => apply cnd_inert_cut.
 522 Hint Extern 1 => apply cnd_inert_structural.
 523 Hint Extern 1 => apply cnd_inert_cnd_ant_assoc.
 524 Hint Extern 1 => apply cnd_inert_cnd_ant_cossa.
 525 Hint Extern 1 => apply cnd_inert_cnd_ant_cancell.
 526 Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr.
 527 Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac.
 528 Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac.
 529 Hint Extern 1 => apply cnd_inert_se_expand_left.
 530 Hint Extern 1 => apply cnd_inert_se_expand_right.
 531
 532 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
 533  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
 534 Notation "H /⋯⋯/ C" := (@ND _ _ H C)             : pf_scope.
 535 Notation "a ;; b"   := (nd_comp a b)             : nd_scope.
 536 Notation "a ** b"   := (nd_prod a b)             : nd_scope.
 537 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
 538 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
 539
 540 (* enable setoid rewriting *)
 541 Open Scope nd_scope.
 542 Open Scope pf_scope.
 543
 544 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
 545   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
 546   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
 547   transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
 548     as parametric_relation_ndr_eqv.
 549   Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
 550   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
 551     as parametric_morphism_nd_comp.
 552     intros; apply ndr_comp_respects; auto.
 553     Defined.
 554   Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
 555   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
 556     as parametric_morphism_nd_prod.
 557     intros; apply ndr_prod_respects; auto.
 558     Defined.
 559
 560 Section ND_Relation_Facts.
 561   Context `{ND_Relation}.
 562
 563   (* useful *)
 564   Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f.
 565     intros; apply (ndr_builtfrom_structural f); auto.
 566     Defined.
 567
 568   (* useful *)
 569   Lemma ndr_comp_left_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (nd_id h ;; f) f.
 570     intros; apply (ndr_builtfrom_structural f); auto.
 571     Defined.
 572
 573 End ND_Relation_Facts.
 574
 575 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
 576 Definition nd_replicate
 577   : forall
 578     {Judgment}{Rule}{Ob}
 579     (h:Ob->Judgment)
 580     (c:Ob->Judgment)
 581     (j:Tree ??Ob),
 582     (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
 583     @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
 584   intros.
 585   induction j; simpl.
 586     destruct a; simpl.
 587     apply X.
 588     apply nd_id0.
 589     apply nd_prod; auto.
 590     Defined.
 591
 592 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
 593 Definition nd_map
 594   : forall
 595     {Judgment}{Rule0}{Rule1}
 596     (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
 597     {h}{c}
 598     (pf:@ND Judgment Rule0 h c)
 599     ,
 600     @ND Judgment Rule1 h c.
 601     intros Judgment Rule0 Rule1 r.
 602
 603     refine ((fix nd_map h c pf {struct pf} :=
 604      ((match pf
 605          in @ND _ _ H C
 606           return
 607           @ND Judgment Rule1 H C
 608         with
 609         | nd_id0                     => let case_nd_id0     := tt in _
 610         | nd_id1     h               => let case_nd_id1     := tt in _
 611         | nd_weak1   h               => let case_nd_weak    := tt in _
 612         | nd_copy    h               => let case_nd_copy    := tt in _
 613         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 614         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 615         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 616         | nd_cancell _               => let case_nd_cancell := tt in _
 617         | nd_cancelr _               => let case_nd_cancelr := tt in _
 618         | nd_llecnac _               => let case_nd_llecnac := tt in _
 619         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 620         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 621         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 622       end))) ); simpl in *.
 623
 624     destruct case_nd_id0.      apply nd_id0.
 625     destruct case_nd_id1.      apply nd_id1.
 626     destruct case_nd_weak.     apply nd_weak.
 627     destruct case_nd_copy.     apply nd_copy.
 628     destruct case_nd_prod.     apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
 629     destruct case_nd_comp.     apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
 630     destruct case_nd_cancell.  apply nd_cancell.
 631     destruct case_nd_cancelr.  apply nd_cancelr.
 632     destruct case_nd_llecnac.  apply nd_llecnac.
 633     destruct case_nd_rlecnac.  apply nd_rlecnac.
 634     destruct case_nd_assoc.    apply nd_assoc.
 635     destruct case_nd_cossa.    apply nd_cossa.
 636     apply r. apply rule.
 637     Defined.
 638
 639 (* "map" over natural deduction proofs, where the result proof has different judgments *)
 640 Definition nd_map'
 641   : forall
 642     {Judgment0}{Rule0}{Judgment1}{Rule1}
 643     (f:Judgment0->Judgment1)
 644     (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
 645     {h}{c}
 646     (pf:@ND Judgment0 Rule0 h c)
 647     ,
 648     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
 649     intros Judgment0 Rule0 Judgment1 Rule1 f r.
 650
 651     refine ((fix nd_map' h c pf {struct pf} :=
 652      ((match pf
 653          in @ND _ _ H C
 654           return
 655           @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
 656         with
 657         | nd_id0                     => let case_nd_id0     := tt in _
 658         | nd_id1     h               => let case_nd_id1     := tt in _
 659         | nd_weak1   h               => let case_nd_weak    := tt in _
 660         | nd_copy    h               => let case_nd_copy    := tt in _
 661         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 662         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 663         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 664         | nd_cancell _               => let case_nd_cancell := tt in _
 665         | nd_cancelr _               => let case_nd_cancelr := tt in _
 666         | nd_llecnac _               => let case_nd_llecnac := tt in _
 667         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 668         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 669         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 670       end))) ); simpl in *.
 671
 672     destruct case_nd_id0.      apply nd_id0.
 673     destruct case_nd_id1.      apply nd_id1.
 674     destruct case_nd_weak.     apply nd_weak.
 675     destruct case_nd_copy.     apply nd_copy.
 676     destruct case_nd_prod.     apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
 677     destruct case_nd_comp.     apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
 678     destruct case_nd_cancell.  apply nd_cancell.
 679     destruct case_nd_cancelr.  apply nd_cancelr.
 680     destruct case_nd_llecnac.  apply nd_llecnac.
 681     destruct case_nd_rlecnac.  apply nd_rlecnac.
 682     destruct case_nd_assoc.    apply nd_assoc.
 683     destruct case_nd_cossa.    apply nd_cossa.
 684     apply r. apply rule.
 685     Defined.
 686
 687 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
 688 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
 689   | nd_property_structural      : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
 690   | nd_property_prod            : forall h0 c0 pf0 h1 c1 pf1,
 691     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
 692   | nd_property_comp            : forall h0 c0 pf0  c1 pf1,
 693     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
 694   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
 695   Hint Constructors nd_property.
 696
 697 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
 698 Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
 699 | cnd_property_weak            : @cnd_property _ _ P _ cnd_weak
 700 | cnd_property_rule            : forall h c r cnd',
 701   P h c r ->
 702   @cnd_property _ _ P h cnd' ->
 703   @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
 704 | cnd_property_branch          :
 705   forall c1 c2 cnd1 cnd2,
 706   @cnd_property _ _ P c1 cnd1 ->
 707   @cnd_property _ _ P c2 cnd2 ->
 708   @cnd_property _ _ P _  (cnd_branch _ _ cnd1 cnd2).
 709
 710 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
 711 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
 712 | scnd_property_weak            : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
 713 | scnd_property_comp            : forall h x c r cnd',
 714   P x [c] r ->
 715   @scnd_property _ _ P h x cnd' ->
 716   @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
 717 | scnd_property_branch          :
 718   forall x c1 c2 cnd1 cnd2,
 719   @scnd_property _ _ P x c1 cnd1 ->
 720   @scnd_property _ _ P x c2 cnd2 ->
 721   @scnd_property _ _ P x _  (scnd_branch _ _ _ cnd1 cnd2).
 722
 723 (* renders a proof as LaTeX code *)
 724 Section ToLatex.
 725
 726   Context {Judgment : Type}.
 727   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
 728   Context {JudgmentToLatexMath : ToLatexMath Judgment}.
 729   Context {RuleToLatexMath     : forall h c, ToLatexMath (Rule h c)}.
 730
 731   Open Scope string_scope.
 732
 733   Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
 734
 735   Definition eolL : LatexMath := rawLatexMath eol.
 736
 737   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
 738   Section SIND_toLatex.
 739
 740     (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
 741     Context (hideRule : forall h c (r:Rule h c), bool).
 742
 743     Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
 744       match pns with
 745         | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
 746         | scnd_weak     c                => rawLatexMath ""
 747         | scnd_comp ht ct c pns rule     => if hideRule _ _ rule
 748                                             then SIND_toLatexMath pns
 749                                             else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
 750                                               SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
 751                                               toLatexMath c +++ rawLatexMath "}" +++ eolL
 752       end.
 753   End SIND_toLatex.
 754
 755   (* this is a work-in-progress; please use SIND_toLatexMath for now *)
 756   Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
 757     match nd with
 758       | nd_id0                      => rawLatexMath indent +++
 759                                        rawLatexMath "% nd_id0 " +++ eolL
 760       | nd_id1  h'                  => rawLatexMath indent +++
 761                                        rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
 762       | nd_weak1 h'                 => rawLatexMath indent +++
 763                                        rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
 764       | nd_copy h'                  => rawLatexMath indent +++
 765                                        rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
 766                                                          rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
 767       | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
 768                                        rawLatexMath "% prod " +++ eolL +++
 769                                        rawLatexMath indent +++
 770                                        rawLatexMath "\begin{array}{c c}" +++ eolL +++
 771                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
 772                                        rawLatexMath indent +++
 773                                        rawLatexMath " & " +++ eolL +++
 774                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
 775                                        rawLatexMath indent +++
 776                                        rawLatexMath "\end{array}"
 777       | nd_comp h  m     c  pf1 pf2 => rawLatexMath indent +++
 778                                        rawLatexMath "% comp " +++ eolL +++
 779                                        rawLatexMath indent +++
 780                                        rawLatexMath "\begin{array}{c}" +++ eolL +++
 781                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
 782                                        rawLatexMath indent +++
 783                                        rawLatexMath " \\ " +++ eolL +++
 784                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
 785                                        rawLatexMath indent +++
 786                                        rawLatexMath "\end{array}"
 787       | nd_cancell a                => rawLatexMath indent +++
 788                                        rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
 789       | nd_cancelr a                => rawLatexMath indent +++
 790                                        rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
 791       | nd_llecnac a                => rawLatexMath indent +++
 792                                        rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
 793       | nd_rlecnac a                => rawLatexMath indent +++
 794                                        rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
 795       | nd_assoc   a b c            => rawLatexMath ""
 796       | nd_cossa   a b c            => rawLatexMath ""
 797       | nd_rule    h c r            => toLatexMath r
 798     end.
 799
 800 End ToLatex.
 801
 802 Close Scope pf_scope.
 803 Close Scope nd_scope.