1 (*********************************************************************************************************************************)
2 (* NaturalDeduction:                                                                                                             *)
3 (*                                                                                                                               *)
4 (*   Structurally explicit natural deduction proofs.                                                                             *)
5 (*                                                                                                                               *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Coq.Strings.Ascii.
12 Require Import Coq.Strings.String.
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  *
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  *)
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  *)
112 Section Natural_Deduction.
114   (* any Coq Type may be used as the set of judgments *)
115   Context {Judgment : Type}.
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}.
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 :=
133     (* natural deduction: you may infer nothing from nothing *)
134     | nd_id0    :             [   ] /⋯⋯/ [   ]
136     (* natural deduction: you may infer anything from itself -- "identity proof" *)
137     | nd_id1    : forall  h,  [ h ] /⋯⋯/ [ h ]
139     (* natural deduction: you may discard conclusions *)
140     | nd_weak1  : forall  h,  [ h ] /⋯⋯/ [   ]
142     (* natural deduction: you may duplicate conclusions *)
143     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)
145     (* natural deduction: you may re-order conclusions *)
146     | nd_exch   : forall  x y, (x,,y) /⋯⋯/ (y,,x)
148     (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
149     | nd_prod : forall {h1 h2 c1 c2}
150        (pf1: h1       /⋯⋯/ c1      )
151        (pf2:       h2 /⋯⋯/       c2),
152        (     h1 ,, h2 /⋯⋯/ c1 ,, c2)
154     (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
155     | nd_comp :
156       forall {h x c}
157       (pf1: h /⋯⋯/ x)
158       (pf2: x /⋯⋯/ c),
159        (     h /⋯⋯/ c)
161     (* Structural rules on lists of judgments - note that this is completely separate from the structural
162      * rules for *contexts* within a sequent.  The rules below manipulate lists of *judgments* rather than
163      * lists of *propositions*. *)
164     | nd_cancell : forall {a},       [] ,, a /⋯⋯/ a
165     | nd_cancelr : forall {a},       a ,, [] /⋯⋯/ a
166     | nd_llecnac : forall {a},             a /⋯⋯/ [] ,, a
167     | nd_rlecnac : forall {a},             a /⋯⋯/ a ,, []
168     | nd_assoc   : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c)
169     | nd_cossa   : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c
171     (* any Rule by itself counts as a proof *)
172     | nd_rule    : forall {h c} (r:Rule h c), h /⋯⋯/ c
174     where  "H /⋯⋯/ C" := (ND H C).
176     Notation "H /⋯⋯/ C" := (ND H C) : pf_scope.
177     Notation "a ;; b"   := (nd_comp a b) : nd_scope.
178     Notation "a ** b"   := (nd_prod a b) : nd_scope.
179     Open Scope nd_scope.
180     Open Scope pf_scope.
182   (* a predicate on proofs *)
183   Definition NDPredicate := forall h c, h /⋯⋯/ c -> Prop.
185   (* the structural inference rules are those which do not change, add, remove, or re-order the judgments *)
186   Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
187   | nd_structural_id0     :                                                                            Structural nd_id0
188   | nd_structural_id1     : forall h,                                                                  Structural (nd_id1 h)
189   | nd_structural_cancell : forall {a},                                                                Structural (@nd_cancell a)
190   | nd_structural_cancelr : forall {a},                                                                Structural (@nd_cancelr a)
191   | nd_structural_llecnac : forall {a},                                                                Structural (@nd_llecnac a)
192   | nd_structural_rlecnac : forall {a},                                                                Structural (@nd_rlecnac a)
193   | nd_structural_assoc   : forall {a b c},                                                            Structural (@nd_assoc a b c)
194   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
195   .
197   (* the closure of an NDPredicate under nd_comp and nd_prod *)
198   Inductive NDPredicateClosure (P:NDPredicate) : forall {h c}, h /⋯⋯/ c -> Prop :=
199   | ndpc_p       : forall h c f, P h c f                                                   -> NDPredicateClosure P f
200   | ndpc_prod    : forall (pf1:h1/⋯⋯/c1)(pf2:h2/⋯⋯/c2),
201     NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1**pf2)
202   | ndpc_comp    : forall (pf1:h1/⋯⋯/x) (pf2: x/⋯⋯/c2),
203     NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1;;pf2).
205   (* proofs built up from structural rules via comp and prod *)
206   Definition StructuralND {h}{c} f := @NDPredicateClosure (@Structural) h c f.
208   (* The Predicate (BuiltFrom f P h) asserts that "h" was built from a single occurrence of "f" and proofs which satisfy P *)
209   Inductive BuiltFrom {h'}{c'}(f:h'/⋯⋯/c')(P:NDPredicate) : forall {h c}, h/⋯⋯/c -> Prop :=
210   | builtfrom_refl  : BuiltFrom f P f
211   | builtfrom_P     : forall h c g, @P h c g -> BuiltFrom f P g
212   | builtfrom_prod1 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f1 ** f2)
213   | builtfrom_prod2 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f2 ** f1)
214   | builtfrom_comp1 : forall h x c       f1 f2, P h  x  f1 -> @BuiltFrom _ _ f P x  c  f2 -> BuiltFrom f P (f1 ;; f2)
215   | builtfrom_comp2 : forall h x c       f1 f2, P x  c  f1 -> @BuiltFrom _ _ f P h  x  f2 -> BuiltFrom f P (f2 ;; f1).
217   (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
218   Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
219     match sl with
220       | T_Leaf None      => nd_id0
221       | T_Leaf (Some x)  => nd_id1 x
222       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
223     end.
225   Fixpoint nd_weak (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
226     match sl as SL return SL /⋯⋯/ [] with
227       | T_Leaf None      => nd_id0
228       | T_Leaf (Some x)  => nd_weak1 x
229       | T_Branch a b     => nd_prod (nd_weak a) (nd_weak b) ;; nd_cancelr
230     end.
232   Hint Constructors Structural.
233   Hint Constructors BuiltFrom.
234   Hint Constructors NDPredicateClosure.
235   Hint Unfold StructuralND.
237   Lemma nd_id_structural : forall sl, StructuralND (nd_id sl).
238     intros.
239     induction sl; simpl; auto.
240     destruct a; auto.
241     Defined.
243   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
244    * structural variations  *)
245   Class ND_Relation :=
246   { ndr_eqv                  : forall {h c  }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _  pf1 pf2)
247   ; ndr_eqv_equivalence      : forall h c, Equivalence (@ndr_eqv h c)
249   (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
250   ; ndr_comp_respects        : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c),      f === f' -> g === g' -> f;;g === f';;g'
251   ; ndr_comp_associativity   : forall (f:a/⋯⋯/b)(g:b/⋯⋯/c)(h:c/⋯⋯/d),                         (f;;g);;h === f;;(g;;h)
253   (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
254   ; ndr_prod_respects        : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d),     f===f' -> g===g' ->    f**g === f'**g'
255   ; ndr_prod_associativity   : forall (f:a/⋯⋯/a')(g:b/⋯⋯/b')(h:c/⋯⋯/c'),       (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
257   (* products and composition must distribute over each other *)
258   ; 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')
260   (* Given a proof f, any two proofs built from it using only structural rules are indistinguishable.  Keep in mind that
261    * nd_weak and nd_copy aren't considered structural, so the hypotheses and conclusions of such proofs will be an identical
262    * list, differing only in the "parenthesization" and addition or removal of empty leaves. *)
263   ; ndr_builtfrom_structural : forall (f:a/⋯⋯/b){a' b'}(g1 g2:a'/⋯⋯/b'),
264     BuiltFrom f (@StructuralND) g1 ->
265     BuiltFrom f (@StructuralND) g2 ->
266     g1 === g2
268   (* proofs of nothing are not distinguished from each other *)
269   ; ndr_void_proofs_irrelevant : forall (f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
271   (* products and duplication must distribute over each other *)
272   ; ndr_prod_preserves_copy  : forall (f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
274   (* duplicating a hypothesis and discarding it is irrelevant *)
275   ; ndr_copy_then_weak_left   : forall a,                            nd_copy a;; (nd_weak _ ** nd_id _) ;; nd_cancell === nd_id _
276   ; ndr_copy_then_weak_right  : forall a,                            nd_copy a;; (nd_id _ ** nd_weak _) ;; nd_cancelr === nd_id _
277   }.
279   (*
280    * Natural Deduction proofs which are Structurally Implicit on the
281    * level of judgments.  These proofs have poor compositionality
282    * properties (vertically, they look more like lists than trees) but
283    * are easier to do induction over.
284    *)
285   Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type :=
286   | scnd_weak   : forall c       , SIND c  []
287   | scnd_comp   : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c]
288   | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2)
289   .
290   Hint Constructors SIND.
292   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *)
293   Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
294     : forall h x c,  ND x c -> SIND h x -> SIND h c.
295     intros h x c nd.
296     induction nd; intro k.
297       apply k.
298       apply k.
299       apply scnd_weak.
300       eapply scnd_branch; apply k.
301       inversion k; subst; auto.
302       inversion k; subst.
303         apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
304       apply IHnd2.
305         apply IHnd1.
306         apply k.
307       inversion k; subst; auto.
308       inversion k; subst; auto.
309       apply scnd_branch; auto.
310       apply scnd_branch; auto.
311       inversion k; subst; inversion X; subst; auto.
312       inversion k; subst; inversion X0; subst; auto.
313       destruct c.
314         destruct o.
315         eapply scnd_comp. apply k. apply r.
316         apply scnd_weak.
317         set (all_rules_one_conclusion _ _ _ r) as bogus.
318           inversion bogus.
319           Defined.
321   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
322   Section SequentND.
323     Context {S:Type}.                   (* type of sequent components *)
324     Context {sequent:S->S->Judgment}.   (* pairing operation which forms a sequent from its halves *)
325     Notation "a |= b" := (sequent a b).
327     (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *)
328     Class SequentND :=
329     { snd_initial : forall a,                           [ ] /⋯⋯/ [ a |= a ]
330     ; snd_cut     : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
331     }.
333     Context (sequentND:SequentND).
334     Context (ndr:ND_Relation).
336     (*
337      * A predicate singling out structural rules, initial sequents,
338      * and cut rules.
339      *
340      * Proofs using only structural rules cannot add or remove
341      * judgments - their hypothesis and conclusion judgment-trees will
342      * differ only in "parenthesization" and the presence/absence of
343      * empty leaves.  This means that a proof involving only
344      * structural rules, cut, and initial sequents can ADD new
345      * non-empty judgment-leaves only via snd_initial, and can only
346      * REMOVE non-empty judgment-leaves only via snd_cut.  Since the
347      * initial sequent is a left and right identity for cut, and cut
348      * is associative, any two proofs (with the same hypotheses and
349      * conclusions) using only structural rules, cut, and initial
350      * sequents are logically indistinguishable - their differences
351      * are logically insignificant.
352      *
353      * Note that it is important that nd_weak and nd_copy aren't
354      * considered to be "structural".
355      *)
356     Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
357     | snd_inert_initial   : forall a,                     SequentND_Inert _ _ (snd_initial a)
358     | snd_inert_cut       : forall a b c,                 SequentND_Inert _ _ (snd_cut a b c)
359     | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
360     .
362     (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
363      * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
364     Class SequentND_Relation :=
365     { sndr_ndr   := ndr
366     ; sndr_inert : forall a b (f g:a/⋯⋯/b),
367       NDPredicateClosure SequentND_Inert f ->
368       NDPredicateClosure SequentND_Inert g ->
369       ndr_eqv f g }.
371   End SequentND.
373   (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
374   Section ContextND.
375     Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
376     Context {snd:SequentND(sequent:=sequent)}.
377     Notation "a |= b" := (sequent a b).
379     (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
380     Class ContextND :=
381     { cnd_ant_assoc     : forall x a b c, ND [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x   ]
382     ; cnd_ant_cossa     : forall x a b c, ND [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x   ]
383     ; cnd_ant_cancell   : forall x a    , ND [  [],,a     |= x]     [        a   |= x   ]
384     ; cnd_ant_cancelr   : forall x a    , ND [a,,[]       |= x]     [        a   |= x   ]
385     ; cnd_ant_llecnac   : forall x a    , ND [      a     |= x]     [    [],,a   |= x   ]
386     ; cnd_ant_rlecnac   : forall x a    , ND [      a     |= x]     [    a,,[]   |= x   ]
387     ; cnd_expand_left   : forall a b c  , ND [          a |= b]     [ c,,a       |= c,,b]
388     ; cnd_expand_right  : forall a b c  , ND [          a |= b]     [ a,,c       |= b,,c]
389     ; cnd_snd           := snd
390     }.
392     Context (ContextND).
394     (*
395      * A predicate singling out initial sequents, cuts, context expansion,
396      * and structural rules.
397      *
398      * Any two proofs (with the same hypotheses and conclusions) whose
399      * non-structural rules do nothing other than expand contexts,
400      * re-arrange contexts, or introduce additional initial-sequent
401      * conclusions are indistinguishable.  One important consequence
402      * is that asking for a small initial sequent and then expanding
403      * it using cnd_expand_{right,left} is no different from simply
404      * asking for the larger initial sequent in the first place.
405      *
406      *)
407     Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop :=
408     | cnd_inert_initial           : forall a,                     ContextND_Inert _ _ (snd_initial a)
409     | cnd_inert_cut               : forall a b c,                 ContextND_Inert _ _ (snd_cut a b c)
410     | cnd_inert_structural        : forall a b f, Structural f -> ContextND_Inert a b f
411     | cnd_inert_cnd_ant_assoc     : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc   x a b c)
412     | cnd_inert_cnd_ant_cossa     : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa   x a b c)
413     | cnd_inert_cnd_ant_cancell   : forall x a    , ContextND_Inert _ _ (cnd_ant_cancell x a)
414     | cnd_inert_cnd_ant_cancelr   : forall x a    , ContextND_Inert _ _ (cnd_ant_cancelr x a)
415     | cnd_inert_cnd_ant_llecnac   : forall x a    , ContextND_Inert _ _ (cnd_ant_llecnac x a)
416     | cnd_inert_cnd_ant_rlecnac   : forall x a    , ContextND_Inert _ _ (cnd_ant_rlecnac x a)
417     | cnd_inert_se_expand_left    : forall t g s  , ContextND_Inert _ _ (@cnd_expand_left  _ t g s)
418     | cnd_inert_se_expand_right   : forall t g s  , ContextND_Inert _ _ (@cnd_expand_right _ t g s).
420     Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} :=
421     { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b),
422                            NDPredicateClosure ContextND_Inert f ->
423                            NDPredicateClosure ContextND_Inert g ->
424                            ndr_eqv f g
425     ; cndr_sndr  := sndr
426     }.
428     (* a proof is Analytic if it does not use cut *)
429     (*
430     Definition Analytic_Rule : NDPredicate :=
431       fun h c f => forall c, not (snd_cut _ _ c = f).
432     Definition AnalyticND := NDPredicateClosure Analytic_Rule.
434     (* a proof system has cut elimination if, for every proof, there is an analytic proof with the same conclusion *)
435     Class CutElimination :=
436     { ce_eliminate : forall h c, h/⋯⋯/c -> h/⋯⋯/c
437     ; ce_analytic  : forall h c f, AnalyticND (ce_eliminate h c f)
438     }.
440     (* cut elimination is strong if the analytic proof is furthermore equivalent to the original proof *)
441     Class StrongCutElimination :=
442     { sce_ce       <: CutElimination
443     ; ce_strong     : forall h c f, f === ce_eliminate h c f
444     }.
445     *)
447   End ContextND.
449   Close Scope nd_scope.
450   Open Scope pf_scope.
452 End Natural_Deduction.
454 Coercion snd_cut   : SequentND >-> Funclass.
455 Coercion cnd_snd   : ContextND >-> SequentND.
456 Coercion sndr_ndr  : SequentND_Relation >-> ND_Relation.
457 Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation.
459 Implicit Arguments ND [ Judgment ].
461 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
462  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
463 Notation "H /⋯⋯/ C" := (@ND _ _ H C)             : pf_scope.
464 Notation "a ;; b"   := (nd_comp a b)             : nd_scope.
465 Notation "a ** b"   := (nd_prod a b)             : nd_scope.
466 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
467 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
469 Hint Constructors Structural.
470 Hint Constructors ND_Relation.
471 Hint Constructors BuiltFrom.
472 Hint Constructors NDPredicateClosure.
473 Hint Constructors ContextND_Inert.
474 Hint Constructors SequentND_Inert.
475 Hint Unfold StructuralND.
477 (* enable setoid rewriting *)
478 Open Scope nd_scope.
479 Open Scope pf_scope.
481 Hint Extern 2 (StructuralND (nd_id _)) => apply nd_id_structural.
482 Hint Extern 2 (NDPredicateClosure _ ( _ ;; _ ) ) => apply ndpc_comp.
483 Hint Extern 2 (NDPredicateClosure _ ( _ ** _ ) ) => apply ndpc_prod.
484 Hint Extern 2 (NDPredicateClosure (@Structural _ _) (nd_id _)) => apply nd_id_structural.
485 Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp1.
486 Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp2.
487 Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod1.
488 Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod2.
490 (* Hint Constructors has failed me! *)
491 Hint Extern 2 (@Structural _ _ _ _ (@nd_id0 _ _))         => apply nd_structural_id0.
492 Hint Extern 2 (@Structural _ _ _ _ (@nd_id1 _ _ _))       => apply nd_structural_id1.
493 Hint Extern 2 (@Structural _ _ _ _ (@nd_cancell _ _ _))   => apply nd_structural_cancell.
494 Hint Extern 2 (@Structural _ _ _ _ (@nd_cancelr _ _ _))   => apply nd_structural_cancelr.
495 Hint Extern 2 (@Structural _ _ _ _ (@nd_llecnac _ _ _))   => apply nd_structural_llecnac.
496 Hint Extern 2 (@Structural _ _ _ _ (@nd_rlecnac _ _ _))   => apply nd_structural_rlecnac.
497 Hint Extern 2 (@Structural _ _ _ _ (@nd_assoc _ _ _ _ _)) => apply nd_structural_assoc.
498 Hint Extern 2 (@Structural _ _ _ _ (@nd_cossa _ _ _ _ _)) => apply nd_structural_cossa.
500 Hint Extern 4 (NDPredicateClosure _ _) => apply ndpc_p.
502 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
503   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
504   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
505   transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
506     as parametric_relation_ndr_eqv.
507   Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
508   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
509     as parametric_morphism_nd_comp.
510     intros; apply ndr_comp_respects; auto.
511     Defined.
512   Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
513   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
514     as parametric_morphism_nd_prod.
515     intros; apply ndr_prod_respects; auto.
516     Defined.
518 Section ND_Relation_Facts.
519   Context `{ND_Relation}.
521   (* useful *)
522   Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f.
523     intros; apply (ndr_builtfrom_structural f). auto.
524     auto.
525     Defined.
527   (* useful *)
528   Lemma ndr_comp_left_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (nd_id h ;; f) f.
529     intros; apply (ndr_builtfrom_structural f); auto.
530     Defined.
532   Ltac nd_prod_preserves_comp_ltac P EQV :=
533     match goal with
534       [ |- context [ (?A ** ?B) ;; (?C ** ?D) ] ] =>
535         set (@ndr_prod_preserves_comp _ _ EQV _ _ A _ _ B _ C _ D) as P
536     end.
538   Lemma nd_swap A B C D (f:ND _ A B) (g:ND _ C D) :
539     (f ** nd_id C) ;; (nd_id B ** g) ===
540     (nd_id A ** g) ;; (f ** nd_id D).
541     setoid_rewrite <- ndr_prod_preserves_comp.
542     setoid_rewrite ndr_comp_left_identity.
543     setoid_rewrite ndr_comp_right_identity.
544     reflexivity.
545     Qed.
547   (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
548   Ltac nd_swap_ltac P EQV :=
549     match goal with
550       [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
551         set (@nd_swap _ _ EQV _ _ _ _ F G) as P
552     end.
554   Lemma nd_prod_split_left A B C D (f:ND _ A B) (g:ND _ B C) :
555     nd_id D ** (f ;; g) ===
556     (nd_id D ** f) ;; (nd_id D ** g).
557     setoid_rewrite <- ndr_prod_preserves_comp.
558     setoid_rewrite ndr_comp_left_identity.
559     reflexivity.
560     Qed.
562   Lemma nd_prod_split_right A B C D (f:ND _ A B) (g:ND _ B C) :
563     (f ;; g) ** nd_id D ===
564     (f ** nd_id D) ;; (g ** nd_id D).
565     setoid_rewrite <- ndr_prod_preserves_comp.
566     setoid_rewrite ndr_comp_left_identity.
567     reflexivity.
568     Qed.
570 End ND_Relation_Facts.
572 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
573 Definition nd_replicate
574   : forall
575     {Judgment}{Rule}{Ob}
576     (h:Ob->Judgment)
577     (c:Ob->Judgment)
578     (j:Tree ??Ob),
579     (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
580     @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
581   intros.
582   induction j; simpl.
583     destruct a; simpl.
584     apply X.
585     apply nd_id0.
586     apply nd_prod; auto.
587     Defined.
589 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
590 Definition nd_map
591   : forall
592     {Judgment}{Rule0}{Rule1}
593     (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
594     {h}{c}
595     (pf:@ND Judgment Rule0 h c)
596     ,
597     @ND Judgment Rule1 h c.
598     intros Judgment Rule0 Rule1 r.
600     refine ((fix nd_map h c pf {struct pf} :=
601      ((match pf
602          in @ND _ _ H C
603           return
604           @ND Judgment Rule1 H C
605         with
606         | nd_id0                     => let case_nd_id0     := tt in _
607         | nd_id1     h               => let case_nd_id1     := tt in _
608         | nd_weak1   h               => let case_nd_weak    := tt in _
609         | nd_copy    h               => let case_nd_copy    := tt in _
610         | nd_exch    x y             => let case_nd_exch    := tt in _
611         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
612         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
613         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
614         | nd_cancell _               => let case_nd_cancell := tt in _
615         | nd_cancelr _               => let case_nd_cancelr := tt in _
616         | nd_llecnac _               => let case_nd_llecnac := tt in _
617         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
618         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
619         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
620       end))) ); simpl in *.
622     destruct case_nd_id0.      apply nd_id0.
623     destruct case_nd_id1.      apply nd_id1.
624     destruct case_nd_weak.     apply nd_weak.
625     destruct case_nd_copy.     apply nd_copy.
626     destruct case_nd_exch.     apply nd_exch.
627     destruct case_nd_prod.     apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
628     destruct case_nd_comp.     apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
629     destruct case_nd_cancell.  apply nd_cancell.
630     destruct case_nd_cancelr.  apply nd_cancelr.
631     destruct case_nd_llecnac.  apply nd_llecnac.
632     destruct case_nd_rlecnac.  apply nd_rlecnac.
633     destruct case_nd_assoc.    apply nd_assoc.
634     destruct case_nd_cossa.    apply nd_cossa.
635     apply r. apply rule.
636     Defined.
638 (* "map" over natural deduction proofs, where the result proof has different judgments *)
639 Definition nd_map'
640   : forall
641     {Judgment0}{Rule0}{Judgment1}{Rule1}
642     (f:Judgment0->Judgment1)
643     (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
644     {h}{c}
645     (pf:@ND Judgment0 Rule0 h c)
646     ,
647     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
648     intros Judgment0 Rule0 Judgment1 Rule1 f r.
650     refine ((fix nd_map' h c pf {struct pf} :=
651      ((match pf
652          in @ND _ _ H C
653           return
654           @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
655         with
656         | nd_id0                     => let case_nd_id0     := tt in _
657         | nd_id1     h               => let case_nd_id1     := tt in _
658         | nd_weak1   h               => let case_nd_weak    := tt in _
659         | nd_copy    h               => let case_nd_copy    := tt in _
660         | nd_exch    x y             => let case_nd_exch    := 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 *.
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_exch.     apply nd_exch.
677     destruct case_nd_prod.     apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
678     destruct case_nd_comp.     apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
679     destruct case_nd_cancell.  apply nd_cancell.
680     destruct case_nd_cancelr.  apply nd_cancelr.
681     destruct case_nd_llecnac.  apply nd_llecnac.
682     destruct case_nd_rlecnac.  apply nd_rlecnac.
683     destruct case_nd_assoc.    apply nd_assoc.
684     destruct case_nd_cossa.    apply nd_cossa.
685     apply r. apply rule.
686     Defined.
688 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
689 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
690   | nd_property_structural      : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
691   | nd_property_prod            : forall h0 c0 pf0 h1 c1 pf1,
692     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
693   | nd_property_comp            : forall h0 c0 pf0  c1 pf1,
694     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
695   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
696   Hint Constructors nd_property.
698 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
699 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
700 | scnd_property_weak            : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
701 | scnd_property_comp            : forall h x c r cnd',
702   P x [c] r ->
703   @scnd_property _ _ P h x cnd' ->
704   @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
705 | scnd_property_branch          :
706   forall x c1 c2 cnd1 cnd2,
707   @scnd_property _ _ P x c1 cnd1 ->
708   @scnd_property _ _ P x c2 cnd2 ->
709   @scnd_property _ _ P x _  (scnd_branch _ _ _ cnd1 cnd2).
711 (* renders a proof as LaTeX code *)
712 Section ToLatex.
714   Context {Judgment : Type}.
715   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
716   Context {JudgmentToLatexMath : ToLatexMath Judgment}.
717   Context {RuleToLatexMath     : forall h c, ToLatexMath (Rule h c)}.
719   Open Scope string_scope.
721   Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
723   Definition eolL : LatexMath := rawLatexMath eol.
725   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
726   Section SIND_toLatex.
728     (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
729     Context (hideRule : forall h c (r:Rule h c), bool).
731     Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
732       match pns with
733         | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
734         | scnd_weak     c                => rawLatexMath ""
735         | scnd_comp ht ct c pns rule     => if hideRule _ _ rule
736                                             then SIND_toLatexMath pns
737                                             else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
738                                               SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
739                                               toLatexMath c +++ rawLatexMath "}" +++ eolL
740       end.
741   End SIND_toLatex.
743   (* this is a work-in-progress; please use SIND_toLatexMath for now *)
744   Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
745     match nd with
746       | nd_id0                      => rawLatexMath indent +++
747                                        rawLatexMath "% nd_id0 " +++ eolL
748       | nd_id1  h'                  => rawLatexMath indent +++
749                                        rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
750       | nd_weak1 h'                 => rawLatexMath indent +++
751                                        rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
752       | nd_copy h'                  => rawLatexMath indent +++
753                                        rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
754                                                          rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
755       | nd_exch x y                 => rawLatexMath indent +++
756                                        rawLatexMath "\inferrule*[Left=exch]{"+++judgments2latex h+++
757                                                          rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
758       | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
759                                        rawLatexMath "% prod " +++ eolL +++
760                                        rawLatexMath indent +++
761                                        rawLatexMath "\begin{array}{c c}" +++ eolL +++
762                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
763                                        rawLatexMath indent +++
764                                        rawLatexMath " & " +++ eolL +++
765                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
766                                        rawLatexMath indent +++
767                                        rawLatexMath "\end{array}"
768       | nd_comp h  m     c  pf1 pf2 => rawLatexMath indent +++
769                                        rawLatexMath "% comp " +++ eolL +++
770                                        rawLatexMath indent +++
771                                        rawLatexMath "\begin{array}{c}" +++ eolL +++
772                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
773                                        rawLatexMath indent +++
774                                        rawLatexMath " \\ " +++ eolL +++
775                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
776                                        rawLatexMath indent +++
777                                        rawLatexMath "\end{array}"
778       | nd_cancell a                => rawLatexMath indent +++
779                                        rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
780       | nd_cancelr a                => rawLatexMath indent +++
781                                        rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
782       | nd_llecnac a                => rawLatexMath indent +++
783                                        rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
784       | nd_rlecnac a                => rawLatexMath indent +++
785                                        rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
786       | nd_assoc   a b c            => rawLatexMath ""
787       | nd_cossa   a b c            => rawLatexMath ""
788       | nd_rule    h c r            => toLatexMath r
789     end.
791 End ToLatex.
793 Close Scope pf_scope.
794 Close Scope nd_scope.