1 (*********************************************************************************************************************************)
2 (* NaturalDeduction: *)
4 (* Structurally explicit natural deduction proofs. *)
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.
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:
19 * Variable PropositionalVariable : Type.
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 *)
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.
30 * 1) Structurally implicit proofs
32 * This is what you would call the "usual" representation –- it's
33 * what most people learn when they first start programming in Coq:
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)
40 * Here each judgment (such as "φ is true") is represented by a Coq
43 * 1. A proof of a judgment is any inhabitant of that Coq type.
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.
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.
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)).
60 * The above can be done using lists instead of tuples.
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.
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
77 * 2) Structurally explicit proofs
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.
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
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.
102 * REGARDING LISTS versus TREES:
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
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}.
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.
129 forall hypotheses:Tree ??Judgment,
130 forall conclusions:Tree ??Judgment,
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}
149 ( h1 ,, h2 /⋯⋯/ c1 ,, c2)
151 (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
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.
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)
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 :=
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)
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
210 Hint Constructors Structural.
211 Lemma nd_id_structural : forall sl, Structural (nd_id sl).
213 induction sl; simpl; auto.
217 Lemma weak'_structural : forall a, Structural (nd_weak' a).
227 (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
228 * structural variations *)
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 (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
252 ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
254 (* any two proofs of nothing are "equally good" *)
255 ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
259 * Natural Deduction proofs which are Structurally Implicit on the
260 * level of judgments. These proofs have poor compositionality
261 * properties (vertically, they look more like lists than trees) but
262 * are easier to do induction over.
264 Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type :=
265 | scnd_weak : forall c , SIND c []
266 | scnd_comp : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c]
267 | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2)
269 Hint Constructors SIND.
271 (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *)
272 Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
273 : forall h x c, ND x c -> SIND h x -> SIND h c.
275 induction nd; intro k.
279 eapply scnd_branch; apply k.
281 apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
285 inversion k; subst; auto.
286 inversion k; subst; auto.
287 apply scnd_branch; auto.
288 apply scnd_branch; auto.
289 inversion k; subst; inversion X; subst; auto.
290 inversion k; subst; inversion X0; subst; auto.
293 eapply scnd_comp. apply k. apply r.
295 set (all_rules_one_conclusion _ _ _ r) as bogus.
299 (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *)
300 Inductive ClosedSIND : Tree ??Judgment -> Type :=
301 | cnd_weak : ClosedSIND []
302 | cnd_rule : forall h c , ClosedSIND h -> Rule h c -> ClosedSIND c
303 | cnd_branch : forall c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2)
306 (* we can turn an SIND without hypotheses into a ClosedSIND *)
307 Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c.
308 refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} :=
309 (match pn2 in SIND H C return H=h -> C=c -> _ with
310 | scnd_weak c => let case_weak := tt in _
311 | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
312 | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
313 let q1 := closedFromPnodes _ _ pn' in
314 let q2 := closedFromPnodes _ _ pn'' in _
316 end (refl_equal _) (refl_equal _))) h c pn2 cnd).
331 destruct case_branch.
334 apply q1. subst. apply cnd0.
335 apply q2. subst. apply cnd0.
339 Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c :=
340 match cnd in ClosedSIND C return ND [] C with
342 | cnd_rule h c cndh rhc => closedNDtoNormalND cndh ;; nd_rule rhc
343 | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
346 (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
348 Context {S:Type}. (* type of sequent components *)
349 Context {sequent:S->S->Judgment}.
350 Context {ndr:ND_Relation}.
351 Notation "a |= b" := (sequent a b).
352 Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
354 (* Sequent systems with initial sequents *)
355 Class SequentCalculus :=
356 { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
359 (* Sequent systems with a cut rule *)
360 Class CutRule (nd_cutrule_seq:SequentCalculus) :=
361 { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
362 ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
363 ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr
364 ; nd_cut_associativity : forall {a b c d},
365 (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
370 (* Sequent systems in which each side of the sequent is a tree of something *)
371 Section SequentsOfTrees.
372 Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}.
373 Context (ndr:ND_Relation).
374 Notation "a |= b" := (sequent a b).
375 Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
377 (* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules
378 * mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
379 Class TreeStructuralRules :=
380 { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
381 ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
382 ; tsr_ant_cancell : forall {x a }, ND [ [],,a |= x] [ a |= x]
383 ; tsr_ant_cancelr : forall {x a }, ND [a,,[] |= x] [ a |= x]
384 ; tsr_ant_llecnac : forall {x a }, ND [ a |= x] [ [],,a |= x]
385 ; tsr_ant_rlecnac : forall {x a }, ND [ a |= x] [ a,,[] |= x]
388 Notation "[# a #]" := (nd_rule a) : nd_scope.
390 (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *)
391 Context `{se_cut : @CutRule _ sequent ndr sc}.
392 Class SequentExpansion :=
393 { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
394 ; se_expand_right : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
396 (* left and right expansion must commute with cut *)
397 ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; se_expand_left c === nd_seq_reflexive (c,, a)
398 ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c)
399 ; se_cut_left : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c)
400 ; se_cut_right : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c)
404 Close Scope nd_scope.
407 End Natural_Deduction.
409 Coercion nd_cut : CutRule >-> Funclass.
411 Implicit Arguments ND [ Judgment ].
412 Hint Constructors Structural.
413 Hint Extern 1 => apply nd_id_structural.
414 Hint Extern 1 => apply ndr_structural_indistinguishable.
416 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
417 * of proofs. When only one kind of proof is in use, it's quite helpful though. *)
418 Notation "H /⋯⋯/ C" := (@ND _ _ H C) : pf_scope.
419 Notation "a ;; b" := (nd_comp a b) : nd_scope.
420 Notation "a ** b" := (nd_prod a b) : nd_scope.
421 Notation "[# a #]" := (nd_rule a) : nd_scope.
422 Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope.
424 (* enable setoid rewriting *)
428 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
429 reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c))
430 symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c))
431 transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
432 as parametric_relation_ndr_eqv.
433 Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
434 with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
435 as parametric_morphism_nd_comp.
436 intros; apply ndr_comp_respects; auto.
438 Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
439 with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
440 as parametric_morphism_nd_prod.
441 intros; apply ndr_prod_respects; auto.
444 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
445 Definition nd_replicate
451 (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
452 @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
461 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
464 {Judgment}{Rule0}{Rule1}
465 (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
467 (pf:@ND Judgment Rule0 h c)
469 @ND Judgment Rule1 h c.
470 intros Judgment Rule0 Rule1 r.
472 refine ((fix nd_map h c pf {struct pf} :=
476 @ND Judgment Rule1 H C
478 | nd_id0 => let case_nd_id0 := tt in _
479 | nd_id1 h => let case_nd_id1 := tt in _
480 | nd_weak h => let case_nd_weak := tt in _
481 | nd_copy h => let case_nd_copy := tt in _
482 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
483 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
484 | nd_rule _ _ rule => let case_nd_rule := tt in _
485 | nd_cancell _ => let case_nd_cancell := tt in _
486 | nd_cancelr _ => let case_nd_cancelr := tt in _
487 | nd_llecnac _ => let case_nd_llecnac := tt in _
488 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
489 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
490 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
491 end))) ); simpl in *.
493 destruct case_nd_id0. apply nd_id0.
494 destruct case_nd_id1. apply nd_id1.
495 destruct case_nd_weak. apply nd_weak.
496 destruct case_nd_copy. apply nd_copy.
497 destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
498 destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
499 destruct case_nd_cancell. apply nd_cancell.
500 destruct case_nd_cancelr. apply nd_cancelr.
501 destruct case_nd_llecnac. apply nd_llecnac.
502 destruct case_nd_rlecnac. apply nd_rlecnac.
503 destruct case_nd_assoc. apply nd_assoc.
504 destruct case_nd_cossa. apply nd_cossa.
508 (* "map" over natural deduction proofs, where the result proof has different judgments *)
511 {Judgment0}{Rule0}{Judgment1}{Rule1}
512 (f:Judgment0->Judgment1)
513 (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
515 (pf:@ND Judgment0 Rule0 h c)
517 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
518 intros Judgment0 Rule0 Judgment1 Rule1 f r.
520 refine ((fix nd_map' h c pf {struct pf} :=
524 @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
526 | nd_id0 => let case_nd_id0 := tt in _
527 | nd_id1 h => let case_nd_id1 := tt in _
528 | nd_weak h => let case_nd_weak := tt in _
529 | nd_copy h => let case_nd_copy := tt in _
530 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
531 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
532 | nd_rule _ _ rule => let case_nd_rule := tt in _
533 | nd_cancell _ => let case_nd_cancell := tt in _
534 | nd_cancelr _ => let case_nd_cancelr := tt in _
535 | nd_llecnac _ => let case_nd_llecnac := tt in _
536 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
537 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
538 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
539 end))) ); simpl in *.
541 destruct case_nd_id0. apply nd_id0.
542 destruct case_nd_id1. apply nd_id1.
543 destruct case_nd_weak. apply nd_weak.
544 destruct case_nd_copy. apply nd_copy.
545 destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
546 destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
547 destruct case_nd_cancell. apply nd_cancell.
548 destruct case_nd_cancelr. apply nd_cancelr.
549 destruct case_nd_llecnac. apply nd_llecnac.
550 destruct case_nd_rlecnac. apply nd_rlecnac.
551 destruct case_nd_assoc. apply nd_assoc.
552 destruct case_nd_cossa. apply nd_cossa.
556 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
557 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
558 | nd_property_structural : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
559 | nd_property_prod : forall h0 c0 pf0 h1 c1 pf1,
560 @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
561 | nd_property_comp : forall h0 c0 pf0 c1 pf1,
562 @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
563 | nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
564 Hint Constructors nd_property.
566 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
567 Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
568 | cnd_property_weak : @cnd_property _ _ P _ cnd_weak
569 | cnd_property_rule : forall h c r cnd',
571 @cnd_property _ _ P h cnd' ->
572 @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
573 | cnd_property_branch :
574 forall c1 c2 cnd1 cnd2,
575 @cnd_property _ _ P c1 cnd1 ->
576 @cnd_property _ _ P c2 cnd2 ->
577 @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2).
579 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
580 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
581 | scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
582 | scnd_property_comp : forall h x c r cnd',
584 @scnd_property _ _ P h x cnd' ->
585 @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
586 | scnd_property_branch :
587 forall x c1 c2 cnd1 cnd2,
588 @scnd_property _ _ P x c1 cnd1 ->
589 @scnd_property _ _ P x c2 cnd2 ->
590 @scnd_property _ _ P x _ (scnd_branch _ _ _ cnd1 cnd2).
592 (* renders a proof as LaTeX code *)
595 Context {Judgment : Type}.
596 Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
597 Context {JudgmentToLatexMath : ToLatexMath Judgment}.
598 Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}.
600 Open Scope string_scope.
602 Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
604 Definition eolL : LatexMath := rawLatexMath eol.
606 (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
607 Section SIND_toLatex.
609 (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
610 Context (hideRule : forall h c (r:Rule h c), bool).
612 Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
614 | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
615 | scnd_weak c => rawLatexMath ""
616 | scnd_comp ht ct c pns rule => if hideRule _ _ rule
617 then SIND_toLatexMath pns
618 else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
619 SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
620 toLatexMath c +++ rawLatexMath "}" +++ eolL
624 (* this is a work-in-progress; please use SIND_toLatexMath for now *)
625 Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
627 | nd_id0 => rawLatexMath indent +++
628 rawLatexMath "% nd_id0 " +++ eolL
629 | nd_id1 h' => rawLatexMath indent +++
630 rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
631 | nd_weak h' => rawLatexMath indent +++
632 rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
633 | nd_copy h' => rawLatexMath indent +++
634 rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
635 rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
636 | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
637 rawLatexMath "% prod " +++ eolL +++
638 rawLatexMath indent +++
639 rawLatexMath "\begin{array}{c c}" +++ eolL +++
640 (nd_toLatexMath pf1 (" "+++indent)) +++
641 rawLatexMath indent +++
642 rawLatexMath " & " +++ eolL +++
643 (nd_toLatexMath pf2 (" "+++indent)) +++
644 rawLatexMath indent +++
645 rawLatexMath "\end{array}"
646 | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
647 rawLatexMath "% comp " +++ eolL +++
648 rawLatexMath indent +++
649 rawLatexMath "\begin{array}{c}" +++ eolL +++
650 (nd_toLatexMath pf1 (" "+++indent)) +++
651 rawLatexMath indent +++
652 rawLatexMath " \\ " +++ eolL +++
653 (nd_toLatexMath pf2 (" "+++indent)) +++
654 rawLatexMath indent +++
655 rawLatexMath "\end{array}"
656 | nd_cancell a => rawLatexMath indent +++
657 rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
658 | nd_cancelr a => rawLatexMath indent +++
659 rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
660 | nd_llecnac a => rawLatexMath indent +++
661 rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
662 | nd_rlecnac a => rawLatexMath indent +++
663 rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
664 | nd_assoc a b c => rawLatexMath ""
665 | nd_cossa a b c => rawLatexMath ""
666 | nd_rule h c r => toLatexMath r
671 Close Scope pf_scope.
672 Close Scope nd_scope.