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_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}
152 ( h1 ,, h2 /⋯⋯/ c1 ,, c2)
154 (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
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.
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)
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 :=
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)
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
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).
239 induction sl; simpl; auto.
243 (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
244 * structural variations *)
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 ->
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 _
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.
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)
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.
296 induction nd; intro k.
300 eapply scnd_branch; apply k.
301 inversion k; subst; auto.
303 apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
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.
315 eapply scnd_comp. apply k. apply r.
317 set (all_rules_one_conclusion _ _ _ r) as bogus.
321 (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
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 *)
329 { snd_initial : forall a, [ ] /⋯⋯/ [ a |= a ]
330 ; snd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
333 Context (sequentND:SequentND).
334 Context (ndr:ND_Relation).
337 * A predicate singling out structural rules, initial sequents,
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.
353 * Note that it is important that nd_weak and nd_copy aren't
354 * considered to be "structural".
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
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 :=
366 ; sndr_inert : forall a b (f g:a/⋯⋯/b),
367 NDPredicateClosure SequentND_Inert f ->
368 NDPredicateClosure SequentND_Inert g ->
373 (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
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 *)
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]
392 Context `(ContextND).
395 * A predicate singling out initial sequents, cuts, context expansion,
396 * and structural rules.
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.
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 ->
428 (* a proof is Analytic if it does not use cut *)
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)
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
449 Close Scope nd_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 *)
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.
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.
518 Section ND_Relation_Facts.
519 Context `{ND_Relation}.
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.
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.
532 Ltac nd_prod_preserves_comp_ltac P EQV :=
534 [ |- context [ (?A ** ?B) ;; (?C ** ?D) ] ] =>
535 set (@ndr_prod_preserves_comp _ _ EQV _ _ A _ _ B _ C _ D) as P
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.
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 :=
550 [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
551 set (@nd_swap _ _ EQV _ _ _ _ F G) as P
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.
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.
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
579 (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
580 @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
589 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
592 {Judgment}{Rule0}{Rule1}
593 (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
595 (pf:@ND Judgment Rule0 h c)
597 @ND Judgment Rule1 h c.
598 intros Judgment Rule0 Rule1 r.
600 refine ((fix nd_map h c pf {struct pf} :=
604 @ND Judgment Rule1 H C
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.
638 (* "map" over natural deduction proofs, where the result proof has different judgments *)
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))
645 (pf:@ND Judgment0 Rule0 h c)
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} :=
654 @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
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.
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',
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 *)
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 :=
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
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) :=
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
793 Close Scope pf_scope.
794 Close Scope nd_scope.