74ecaeff2980151909ed0b55bdfd4ef5e1e99254
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_weak   : forall  h,  [ h ] /⋯⋯/ [   ]
142     (* natural deduction: you may duplicate conclusions *)
143     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)
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)
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)
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
168     (* any Rule by itself counts as a proof *)
169     | nd_rule    : forall {h c} (r:Rule h c), h /⋯⋯/ c
171     where  "H /⋯⋯/ C" := (ND H C).
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.
179   (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
180   Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
181   | nd_structural_id0     :                                                                            Structural nd_id0
182   | nd_structural_id1     : forall h,                                                                  Structural (nd_id1 h)
183   | nd_structural_weak    : forall h,                                                                  Structural (nd_weak h)
184   | nd_structural_copy    : forall h,                                                                  Structural (nd_copy h)
185   | nd_structural_prod    : forall (pf1:h1/⋯⋯/c1)(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
186   | nd_structural_comp    : forall (pf1:h1/⋯⋯/x) (pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
187   | nd_structural_cancell : forall {a},                                                                Structural (@nd_cancell a)
188   | nd_structural_cancelr : forall {a},                                                                Structural (@nd_cancelr a)
189   | nd_structural_llecnac : forall {a},                                                                Structural (@nd_llecnac a)
190   | nd_structural_rlecnac : forall {a},                                                                Structural (@nd_rlecnac a)
191   | nd_structural_assoc   : forall {a b c},                                                            Structural (@nd_assoc a b c)
192   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
193   .
195   (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
196   Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
197     match sl with
198       | T_Leaf None      => nd_id0
199       | T_Leaf (Some x)  => nd_id1 x
200       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
201     end.
203   Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
204     match sl as SL return SL /⋯⋯/ [] with
205       | T_Leaf None      => nd_id0
206       | T_Leaf (Some x)  => nd_weak x
207       | T_Branch a b     => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
208     end.
210   Hint Constructors Structural.
211   Lemma nd_id_structural : forall sl, Structural (nd_id sl).
212     intros.
213     induction sl; simpl; auto.
214     destruct a; auto.
215     Defined.
217   Lemma weak'_structural : forall a, Structural (nd_weak' a).
218     intros.
219     induction a.
220     destruct a; auto.
221     simpl.
222     auto.
223     simpl.
224     auto.
225     Qed.
227   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
228    * structural variations  *)
229   Class ND_Relation :=
230   { ndr_eqv                  : forall {h c  }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _  pf1 pf2)
231   ; ndr_eqv_equivalence      : forall h c, Equivalence (@ndr_eqv h c)
233   (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
234   ; ndr_comp_respects        : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c),      f === f' -> g === g' -> f;;g === f';;g'
235   ; ndr_comp_associativity   : forall (f:a/⋯⋯/b)(g:b/⋯⋯/c)(h:c/⋯⋯/d),                         (f;;g);;h === f;;(g;;h)
236   ; ndr_comp_left_identity   : forall (f:a/⋯⋯/c),                                          nd_id _ ;; f   === f
237   ; ndr_comp_right_identity  : forall (f:a/⋯⋯/c),                                          f ;; nd_id _   === f
239   (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
240   ; ndr_prod_respects        : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d),     f===f' -> g===g' ->    f**g === f'**g'
241   ; ndr_prod_associativity   : forall (f:a/⋯⋯/a')(g:b/⋯⋯/b')(h:c/⋯⋯/c'),       (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
242   ; ndr_prod_left_identity   : forall (f:a/⋯⋯/b),                       (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
243   ; ndr_prod_right_identity  : forall (f:a/⋯⋯/b),                       (f ** nd_id0)  === nd_cancelr ;; f ;; nd_rlecnac
245   (* products and composition must distribute over each other *)
246   ; 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')
248   (* products and duplication must distribute over each other *)
249   ; ndr_prod_preserves_copy  : forall (f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
251   ; ndr_comp_preserves_cancell   : forall (f:a/⋯⋯/b),                     nd_cancell;; f === nd_id _ **  f ;; nd_cancell
252   ; ndr_comp_preserves_cancelr   : forall (f:a/⋯⋯/b),                     nd_cancelr;; f === f ** nd_id _  ;; nd_cancelr
253   ; ndr_comp_preserves_assoc     : forall (f:a/⋯⋯/b)(g:a1/⋯⋯/b1)(h:a2/⋯⋯/b2),
254     nd_assoc;; (f ** (g ** h)) === ((f ** g) ** h) ;; nd_assoc
256   (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
257   ; ndr_structural_indistinguishable : forall (f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
259   (* any two proofs of nothing are "equally good" *)
260   ; ndr_void_proofs_irrelevant : forall (f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
261   }.
263   (*
264    * Natural Deduction proofs which are Structurally Implicit on the
265    * level of judgments.  These proofs have poor compositionality
266    * properties (vertically, they look more like lists than trees) but
267    * are easier to do induction over.
268    *)
269   Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type :=
270   | scnd_weak   : forall c       , SIND c  []
271   | scnd_comp   : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c]
272   | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2)
273   .
274   Hint Constructors SIND.
276   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *)
277   Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
278     : forall h x c,  ND x c -> SIND h x -> SIND h c.
279     intros h x c nd.
280     induction nd; intro k.
281       apply k.
282       apply k.
283       apply scnd_weak.
284       eapply scnd_branch; apply k.
285       inversion k; subst.
286         apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
287       apply IHnd2.
288         apply IHnd1.
289         apply k.
290       inversion k; subst; auto.
291       inversion k; subst; auto.
292       apply scnd_branch; auto.
293       apply scnd_branch; auto.
294       inversion k; subst; inversion X; subst; auto.
295       inversion k; subst; inversion X0; subst; auto.
296       destruct c.
297         destruct o.
298         eapply scnd_comp. apply k. apply r.
299         apply scnd_weak.
300         set (all_rules_one_conclusion _ _ _ r) as bogus.
301           inversion bogus.
302           Defined.
304   (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *)
305   Inductive ClosedSIND : Tree ??Judgment -> Type :=
306   | cnd_weak   : ClosedSIND []
307   | cnd_rule   : forall h c    , ClosedSIND h  -> Rule h c    -> ClosedSIND c
308   | cnd_branch : forall   c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2)
309   .
311   (* we can turn an SIND without hypotheses into a ClosedSIND *)
312   Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c.
313   refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} :=
314     (match pn2 in SIND H C return H=h -> C=c -> _  with
315       | scnd_weak   c                 => let case_weak := tt in _
316       | scnd_comp  ht ct c pn' rule   => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
317       | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
318                                          let q1 := closedFromPnodes _ _ pn' in
319                                          let q2 := closedFromPnodes _ _ pn'' in _
321     end (refl_equal _) (refl_equal _))) h c pn2 cnd).
323   destruct case_weak.
324     intros; subst.
325     apply cnd_weak.
327   destruct case_comp.
328     intros.
329     clear pn2.
330     apply (cnd_rule ct).
331     apply qq.
332     subst.
333     apply cnd0.
334     apply rule.
336   destruct case_branch.
337     intros.
338     apply cnd_branch.
339     apply q1. subst. apply cnd0.
340     apply q2. subst. apply cnd0.
341     Defined.
343   (* undo the above *)
344   Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c :=
345   match cnd in ClosedSIND C return ND [] C with
346   | cnd_weak                   => nd_id0
347   | cnd_rule   h c cndh rhc    => closedNDtoNormalND cndh ;; nd_rule rhc
348   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
349   end.
351   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
352   Section Sequents.
353     Context {S:Type}.   (* type of sequent components *)
354     Context {sequent:S->S->Judgment}.
355     Context {ndr:ND_Relation}.
356     Notation "a |= b" := (sequent a b).
357     Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
359     (* Sequent systems with initial sequents *)
360     Class SequentCalculus :=
361     { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
362     }.
364     (* Sequent systems with a cut rule *)
365     Class CutRule (nd_cutrule_seq:SequentCalculus) :=
366     { nd_cut               :  forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
367     ; nd_cut_left_identity  : forall a b, ((    (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
368     ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a)    );; nd_cut b _ _) === nd_cancelr
369     ; nd_cut_associativity :  forall {a b c d},
370       (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
371     }.
373   End Sequents.
375   (* Sequent systems in which each side of the sequent is a tree of something *)
376   Section SequentsOfTrees.
377     Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}.
378     Context (ndr:ND_Relation).
379     Notation "a |= b" := (sequent a b).
380     Notation "a === b"  := (@ndr_eqv ndr _ _ a b)  : nd_scope.
382     (* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules
383      * mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
384     Class TreeStructuralRules :=
385     { tsr_ant_assoc     : forall x a b c, ND [((a,,b),,c) |= x]     [(a,,(b,,c)) |= x]
386     ; tsr_ant_cossa     : forall x a b c, ND [(a,,(b,,c)) |= x]     [((a,,b),,c) |= x]
387     ; tsr_ant_cancell   : forall x a    , ND [  [],,a     |= x]     [        a   |= x]
388     ; tsr_ant_cancelr   : forall x a    , ND [a,,[]       |= x]     [        a   |= x]
389     ; tsr_ant_llecnac   : forall x a    , ND [      a     |= x]     [    [],,a   |= x]
390     ; tsr_ant_rlecnac   : forall x a    , ND [      a     |= x]     [    a,,[]   |= x]
391     }.
393     Notation "[# a #]"  := (nd_rule a)               : nd_scope.
395     (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *)
396     Context `{se_cut : @CutRule _ sequent ndr sc}.
397     Class SequentExpansion :=
398     { se_expand_left     : forall tau {Gamma Sigma}, ND [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
399     ; se_expand_right    : forall tau {Gamma Sigma}, ND [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
401     (* left and right expansion must commute with cut *)
402     ; se_reflexive_left  : ∀ a c,     nd_seq_reflexive a;; se_expand_left  c === nd_seq_reflexive (c,, a)
403     ; se_reflexive_right : ∀ a c,     nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c)
404     ; se_cut_left        : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c)
405     ; se_cut_right       : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c)
406     }.
407   End SequentsOfTrees.
409   Close Scope nd_scope.
410   Open Scope pf_scope.
412 End Natural_Deduction.
414 Coercion nd_cut : CutRule >-> Funclass.
416 Implicit Arguments ND [ Judgment ].
417 Hint Constructors Structural.
418 Hint Extern 1 => apply nd_id_structural.
419 Hint Extern 1 => apply ndr_structural_indistinguishable.
421 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
422  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
423 Notation "H /⋯⋯/ C" := (@ND _ _ H C)             : pf_scope.
424 Notation "a ;; b"   := (nd_comp a b)             : nd_scope.
425 Notation "a ** b"   := (nd_prod a b)             : nd_scope.
426 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
427 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
429 (* enable setoid rewriting *)
430 Open Scope nd_scope.
431 Open Scope pf_scope.
433 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
434   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
435   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
436   transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
437     as parametric_relation_ndr_eqv.
438   Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
439   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
440     as parametric_morphism_nd_comp.
441     intros; apply ndr_comp_respects; auto.
442     Defined.
443   Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
444   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
445     as parametric_morphism_nd_prod.
446     intros; apply ndr_prod_respects; auto.
447     Defined.
449 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
450 Definition nd_replicate
451   : forall
452     {Judgment}{Rule}{Ob}
453     (h:Ob->Judgment)
454     (c:Ob->Judgment)
455     (j:Tree ??Ob),
456     (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
457     @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
458   intros.
459   induction j; simpl.
460     destruct a; simpl.
461     apply X.
462     apply nd_id0.
463     apply nd_prod; auto.
464     Defined.
466 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
467 Definition nd_map
468   : forall
469     {Judgment}{Rule0}{Rule1}
470     (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
471     {h}{c}
472     (pf:@ND Judgment Rule0 h c)
473     ,
474     @ND Judgment Rule1 h c.
475     intros Judgment Rule0 Rule1 r.
477     refine ((fix nd_map h c pf {struct pf} :=
478      ((match pf
479          in @ND _ _ H C
480           return
481           @ND Judgment Rule1 H C
482         with
483         | nd_id0                     => let case_nd_id0     := tt in _
484         | nd_id1     h               => let case_nd_id1     := tt in _
485         | nd_weak    h               => let case_nd_weak    := tt in _
486         | nd_copy    h               => let case_nd_copy    := tt in _
487         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
488         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
489         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
490         | nd_cancell _               => let case_nd_cancell := tt in _
491         | nd_cancelr _               => let case_nd_cancelr := tt in _
492         | nd_llecnac _               => let case_nd_llecnac := tt in _
493         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
494         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
495         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
496       end))) ); simpl in *.
498     destruct case_nd_id0.      apply nd_id0.
499     destruct case_nd_id1.      apply nd_id1.
500     destruct case_nd_weak.     apply nd_weak.
501     destruct case_nd_copy.     apply nd_copy.
502     destruct case_nd_prod.     apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
503     destruct case_nd_comp.     apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
504     destruct case_nd_cancell.  apply nd_cancell.
505     destruct case_nd_cancelr.  apply nd_cancelr.
506     destruct case_nd_llecnac.  apply nd_llecnac.
507     destruct case_nd_rlecnac.  apply nd_rlecnac.
508     destruct case_nd_assoc.    apply nd_assoc.
509     destruct case_nd_cossa.    apply nd_cossa.
510     apply r. apply rule.
511     Defined.
513 (* "map" over natural deduction proofs, where the result proof has different judgments *)
514 Definition nd_map'
515   : forall
516     {Judgment0}{Rule0}{Judgment1}{Rule1}
517     (f:Judgment0->Judgment1)
518     (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
519     {h}{c}
520     (pf:@ND Judgment0 Rule0 h c)
521     ,
522     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
523     intros Judgment0 Rule0 Judgment1 Rule1 f r.
525     refine ((fix nd_map' h c pf {struct pf} :=
526      ((match pf
527          in @ND _ _ H C
528           return
529           @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
530         with
531         | nd_id0                     => let case_nd_id0     := tt in _
532         | nd_id1     h               => let case_nd_id1     := tt in _
533         | nd_weak    h               => let case_nd_weak    := tt in _
534         | nd_copy    h               => let case_nd_copy    := tt in _
535         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
536         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
537         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
538         | nd_cancell _               => let case_nd_cancell := tt in _
539         | nd_cancelr _               => let case_nd_cancelr := tt in _
540         | nd_llecnac _               => let case_nd_llecnac := tt in _
541         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
542         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
543         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
544       end))) ); simpl in *.
546     destruct case_nd_id0.      apply nd_id0.
547     destruct case_nd_id1.      apply nd_id1.
548     destruct case_nd_weak.     apply nd_weak.
549     destruct case_nd_copy.     apply nd_copy.
550     destruct case_nd_prod.     apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
551     destruct case_nd_comp.     apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
552     destruct case_nd_cancell.  apply nd_cancell.
553     destruct case_nd_cancelr.  apply nd_cancelr.
554     destruct case_nd_llecnac.  apply nd_llecnac.
555     destruct case_nd_rlecnac.  apply nd_rlecnac.
556     destruct case_nd_assoc.    apply nd_assoc.
557     destruct case_nd_cossa.    apply nd_cossa.
558     apply r. apply rule.
559     Defined.
561 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
562 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
563   | nd_property_structural      : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
564   | nd_property_prod            : forall h0 c0 pf0 h1 c1 pf1,
565     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
566   | nd_property_comp            : forall h0 c0 pf0  c1 pf1,
567     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
568   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
569   Hint Constructors nd_property.
571 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
572 Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
573 | cnd_property_weak            : @cnd_property _ _ P _ cnd_weak
574 | cnd_property_rule            : forall h c r cnd',
575   P h c r ->
576   @cnd_property _ _ P h cnd' ->
577   @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
578 | cnd_property_branch          :
579   forall c1 c2 cnd1 cnd2,
580   @cnd_property _ _ P c1 cnd1 ->
581   @cnd_property _ _ P c2 cnd2 ->
582   @cnd_property _ _ P _  (cnd_branch _ _ cnd1 cnd2).
584 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
585 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
586 | scnd_property_weak            : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
587 | scnd_property_comp            : forall h x c r cnd',
588   P x [c] r ->
589   @scnd_property _ _ P h x cnd' ->
590   @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
591 | scnd_property_branch          :
592   forall x c1 c2 cnd1 cnd2,
593   @scnd_property _ _ P x c1 cnd1 ->
594   @scnd_property _ _ P x c2 cnd2 ->
595   @scnd_property _ _ P x _  (scnd_branch _ _ _ cnd1 cnd2).
597 (* renders a proof as LaTeX code *)
598 Section ToLatex.
600   Context {Judgment : Type}.
601   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
602   Context {JudgmentToLatexMath : ToLatexMath Judgment}.
603   Context {RuleToLatexMath     : forall h c, ToLatexMath (Rule h c)}.
605   Open Scope string_scope.
607   Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
609   Definition eolL : LatexMath := rawLatexMath eol.
611   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
612   Section SIND_toLatex.
614     (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
615     Context (hideRule : forall h c (r:Rule h c), bool).
617     Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
618       match pns with
619         | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
620         | scnd_weak     c                => rawLatexMath ""
621         | scnd_comp ht ct c pns rule     => if hideRule _ _ rule
622                                             then SIND_toLatexMath pns
623                                             else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
624                                               SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
625                                               toLatexMath c +++ rawLatexMath "}" +++ eolL
626       end.
627   End SIND_toLatex.
629   (* this is a work-in-progress; please use SIND_toLatexMath for now *)
630   Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
631     match nd with
632       | nd_id0                      => rawLatexMath indent +++
633                                        rawLatexMath "% nd_id0 " +++ eolL
634       | nd_id1  h'                  => rawLatexMath indent +++
635                                        rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
636       | nd_weak h'                  => rawLatexMath indent +++
637                                        rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
638       | nd_copy h'                  => rawLatexMath indent +++
639                                        rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
640                                                          rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
641       | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
642                                        rawLatexMath "% prod " +++ eolL +++
643                                        rawLatexMath indent +++
644                                        rawLatexMath "\begin{array}{c c}" +++ eolL +++
645                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
646                                        rawLatexMath indent +++
647                                        rawLatexMath " & " +++ eolL +++
648                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
649                                        rawLatexMath indent +++
650                                        rawLatexMath "\end{array}"
651       | nd_comp h  m     c  pf1 pf2 => rawLatexMath indent +++
652                                        rawLatexMath "% comp " +++ eolL +++
653                                        rawLatexMath indent +++
654                                        rawLatexMath "\begin{array}{c}" +++ eolL +++
655                                        (nd_toLatexMath pf1 ("  "+++indent)) +++
656                                        rawLatexMath indent +++
657                                        rawLatexMath " \\ " +++ eolL +++
658                                        (nd_toLatexMath pf2 ("  "+++indent)) +++
659                                        rawLatexMath indent +++
660                                        rawLatexMath "\end{array}"
661       | nd_cancell a                => rawLatexMath indent +++
662                                        rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
663       | nd_cancelr a                => rawLatexMath indent +++
664                                        rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
665       | nd_llecnac a                => rawLatexMath indent +++
666                                        rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
667       | nd_rlecnac a                => rawLatexMath indent +++
668                                        rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
669       | nd_assoc   a b c            => rawLatexMath ""
670       | nd_cossa   a b c            => rawLatexMath ""
671       | nd_rule    h c r            => toLatexMath r
672     end.
674 End ToLatex.
676 Close Scope pf_scope.
677 Close Scope nd_scope.