047ab87746125c9747876a87ef004e0774f2b6b2
1 (*********************************************************************************************************************************)
2 (* NaturalDeduction: structurally explicit proofs in Coq                                                                         *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.Ascii.
9 Require Import Coq.Strings.String.
11 (*
12  * IMPORTANT!!!
13  *
14  * Unlike most formalizations, this library offers TWO different ways
15  * to represent a natural deduction proof.  To demonstrate this,
16  * consider the signature of the propositional calculus:
17  *
18  *   Variable  PropositionalVariable : Type.
19  *
20  *   Inductive Formula : Prop :=
21  *   | formula_var : PropositionalVariable -> Formula   (* every propositional variable is a formula *)
22  *   | formula_and :   Formula ->  Formula -> Formula   (* the conjunction of any two formulae is a formula *)
23  *   | formula_or  :   Formula ->  Formula -> Formula   (* the disjunction of any two formulae is a formula *)
24  *
25  * And couple this with the theory of conjunction and disjunction:
26  * φ\/ψ is true if either φ is true or ψ is true, and φ/\ψ is true
27  * if both φ and ψ are true.
28  *
29  * 1) Structurally implicit proofs
30  *
31  *    This is what you would call the "usual" representation –- it's
32  *    what most people learn when they first start programming in Coq:
33  *
34  *    Inductive IsTrue : Formula -> Prop :=
35  *    | IsTrue_or1 : forall f1 f2, IsTrue f1 ->              IsTrue (formula_or  f1 f2)
36  *    | IsTrue_or2 : forall f1 f2,              IsTrue f2 -> IsTrue (formula_or  f1 f2)
37  *    | IsTrue_and : forall f1 f2, IsTrue f2 -> IsTrue f2 -> IsTrue (formula_and f1 f2)
38  *
39  *    Here each judgment (such as "φ is true") is represented by a Coq
40  *    type; furthermore:
41  *
42  *       1. A proof of a judgment is any inhabitant of that Coq type.
43  *
44  *       2. A proof of a judgment "J2" from hypothesis judgment "J1"
45  *          is any Coq function from the Coq type for J1 to the Coq
46  *          type for J2; Composition of (hypothetical) proofs is
47  *          represented by composition of Coq functions.
48  *
49  *       3. A pair of judgments is represented by their product (Coq
50  *          type [prod]) in Coq; a pair of proofs is represented by
51  *          their pair (Coq function [pair]) in Coq.
52  *
53  *       4. Duplication of hypotheses is represented by the Coq
54  *          function (fun x => (x,x)).  Dereliction of hypotheses is
55  *          represented by the coq function (fun (x,y) => x) or (fun
56  *          (x,y) => y).  Exchange of the order of hypotheses is
57  *          represented by the Coq function (fun (x,y) => (y,x)).
58  *
59  *    The above can be done using lists instead of tuples.
60  *
61  *    The advantage of this approach is that it requires a minimum
62  *    amount of syntax, and takes maximum advantage of Coq's
63  *    automation facilities.
64  *
66  *    properties *generically* across different signatures and
67  *    theories.  Each signature has its own type of judgments, and
68  *    each theory has its own type of proofs.  In the present
69  *    development we will want to prove –– in this generic manner --
70  *    that various classes of natural deduction calculi form various
71  *    kinds of categories.  So we will need this ability to reason
72  *    about proofs independently of the type used to represent
73  *    judgments and (more importantly) of the set of basic inference
74  *    rules.
75  *
76  * 2) Structurally explicit proofs
77  *
78  *    Structurally explicit proofs are formalized in this file
79  *    (NaturalDeduction.v) and are designed specifically in order to
80  *    circumvent the problem in the previous paragraph.
81  *
82  *)
84 (*
85  * REGARDING LISTS versus TREES:
86  *
87  * You'll notice that this formalization uses (Tree (option A)) in a
88  * lot of places where you might find (list A) more natural.  If this
89  * bothers you, see the end of the file for the technical reasons why.
90  * In short, it lets us avoid having to mess about with JMEq or EqDep,
91  * which are not as well-supported by the Coq core as the theory of
92  * CiC proper.
93  *)
95 Section Natural_Deduction.
97   (* any Coq Type may be used as the set of judgments *)
98   Context {Judgment : Type}.
100   (* any Coq Type –- indexed by the hypothesis and conclusion judgments -- may be used as the set of basic inference rules *)
101   Context {Rule     : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
103   (*
104    *  This type represents a valid Natural Deduction proof from a list
105    *  (tree) of hypotheses; the notation H/⋯⋯/C is meant to look like
106    *  a proof tree with the middle missing if you tilt your head to
107    *  the left (yeah, I know it's a stretch).  Note also that this
108    *  type is capable of representing proofs with multiple
109    *  conclusions, whereas a Rule may have only one conclusion.
110    *)
111   Inductive ND :
112     forall hypotheses:Tree ??Judgment,
113       forall conclusions:Tree ??Judgment,
114         Type :=
116     (* natural deduction: you may infer anything from itself -- "identity proof" *)
117     | nd_id0    :             [   ] /⋯⋯/ [   ]
118     | nd_id1    : forall  h,  [ h ] /⋯⋯/ [ h ]
120     (* natural deduction: you may discard conclusions *)
121     | nd_weak   : forall  h,  [ h ] /⋯⋯/ [   ]
123     (* natural deduction: you may duplicate conclusions *)
124     | nd_copy   : forall  h,    h   /⋯⋯/ (h,,h)
126     (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
127     | nd_prod : forall {h1 h2 c1 c2}
128        (pf1: h1       /⋯⋯/ c1      )
129        (pf2:       h2 /⋯⋯/       c2),
130        (     h1 ,, h2 /⋯⋯/ c1 ,, c2)
132     (* natural deduction: given a proof of every hypothesis, you may discharge them -- "proof composition" *)
133     | nd_comp :
134       forall {h x c}
135       `(pf1: h /⋯⋯/ x)
136       `(pf2: x /⋯⋯/ c),
137        (     h /⋯⋯/ c)
139     (* structural rules on lists of judgments *)
140     | nd_cancell : forall {a},       [] ,, a /⋯⋯/ a
141     | nd_cancelr : forall {a},       a ,, [] /⋯⋯/ a
142     | nd_llecnac : forall {a},             a /⋯⋯/ [] ,, a
143     | nd_rlecnac : forall {a},             a /⋯⋯/ a ,, []
144     | nd_assoc   : forall {a b c}, (a,,b),,c /⋯⋯/ a,,(b,,c)
145     | nd_cossa   : forall {a b c}, a,,(b,,c) /⋯⋯/ (a,,b),,c
147     (* any Rule by itself counts as a proof *)
148     | nd_rule    : forall {h c} (r:Rule h c), h /⋯⋯/ c
150     where  "H /⋯⋯/ C" := (ND H C).
152     Notation "H /⋯⋯/ C" := (ND H C) : pf_scope.
153     Notation "a ;; b"   := (nd_comp a b) : nd_scope.
154     Notation "a ** b"   := (nd_prod a b) : nd_scope.
155     Open Scope nd_scope.
156     Open Scope pf_scope.
158   (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
159   Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
160   | nd_structural_id0     :                                                                            Structural nd_id0
161   | nd_structural_id1     : forall h,                                                                  Structural (nd_id1 h)
162   | nd_structural_weak    : forall h,                                                                  Structural (nd_weak h)
163   | nd_structural_copy    : forall h,                                                                  Structural (nd_copy h)
164   | nd_structural_prod    : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
165   | nd_structural_comp    : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
166   | nd_structural_cancell : forall {a},                                                                Structural (@nd_cancell a)
167   | nd_structural_cancelr : forall {a},                                                                Structural (@nd_cancelr a)
168   | nd_structural_llecnac : forall {a},                                                                Structural (@nd_llecnac a)
169   | nd_structural_rlecnac : forall {a},                                                                Structural (@nd_rlecnac a)
170   | nd_structural_assoc   : forall {a b c},                                                            Structural (@nd_assoc a b c)
171   | nd_structural_cossa   : forall {a b c},                                                            Structural (@nd_cossa a b c)
172   .
174   (* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
175   Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
176     match sl with
177       | T_Leaf None      => nd_id0
178       | T_Leaf (Some x)  => nd_id1 x
179       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
180     end.
182   Hint Constructors Structural.
183   Lemma nd_id_structural : forall sl, Structural (nd_id sl).
184     intros.
185     induction sl; simpl; auto.
186     destruct a; auto.
187     Defined.
189   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
190    * structural variations  *)
191   Class ND_Relation :=
192   { ndr_eqv                  : forall {h c  }, h /⋯⋯/ c -> h /⋯⋯/ c -> Prop where "pf1 === pf2" := (@ndr_eqv _ _  pf1 pf2)
193   ; ndr_eqv_equivalence      : forall h c, Equivalence (@ndr_eqv h c)
195   (* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
196   ; ndr_comp_respects        : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c),      f === f' -> g === g' -> f;;g === f';;g'
197   ; ndr_comp_associativity   : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d),                         (f;;g);;h === f;;(g;;h)
198   ; ndr_comp_left_identity   : forall `(f:a/⋯⋯/c),                                          nd_id _ ;; f   === f
199   ; ndr_comp_right_identity  : forall `(f:a/⋯⋯/c),                                          f ;; nd_id _   === f
201   (* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
202   ; ndr_prod_respects        : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d),     f===f' -> g===g' ->    f**g === f'**g'
203   ; ndr_prod_associativity   : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'),       (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
204   ; ndr_prod_left_identity   : forall `(f:a/⋯⋯/b),                       (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
205   ; ndr_prod_right_identity  : forall `(f:a/⋯⋯/b),                       (f ** nd_id0)  === nd_cancelr ;; f ;; nd_rlecnac
207   (* products and composition must distribute over each other *)
208   ; 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')
210   (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
211   ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
212   }.
214   (*
215    * Single-conclusion proofs; this is an alternate representation
216    * where each inference has only a single conclusion.  These have
217    * worse compositionality properties than ND's, but are easier to
218    * emit as LaTeX code.
219    *)
220   Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
221   | scnd_axiom  : forall c       , SCND [] [c]
222   | scnd_comp   : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
223   | scnd_weak   : forall c       , SCND c  []
224   | scnd_leaf   : forall ht c    , SCND ht [c]  -> SCND ht [c]
225   | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
226   .
227   Hint Constructors SCND.
229   Definition mkSCNDAxioms (h:Tree ??Judgment) : SCND [] h.
230     induction h.
231       destruct a.
232       apply scnd_leaf.  apply scnd_axiom.
233       apply scnd_weak.
234       apply scnd_branch; auto.
235       Defined.
237   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *)
238   Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
239     : forall h x c,  ND x c -> SCND h x -> SCND h c.
240     intros h x c nd.
241     induction nd; intro k.
242       apply k.
243       apply k.
244       apply scnd_weak.
245       eapply scnd_branch; apply k.
246       inversion k; subst.
247         apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
248       apply IHnd2.
249         apply IHnd1.
250         apply k.
251       inversion k; subst; auto.
252       inversion k; subst; auto.
253       apply scnd_branch; auto.
254       apply scnd_branch; auto.
255       inversion k; subst; inversion X; subst; auto.
256       inversion k; subst; inversion X0; subst; auto.
257       destruct c.
258         destruct o.
259         apply scnd_leaf. eapply scnd_comp. apply k. apply r.
260         apply scnd_weak.
261         set (all_rules_one_conclusion _ _ _ r) as bogus.
262           inversion bogus.
263           Defined.
265   (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *)
266   Inductive ClosedND : Tree ??Judgment -> Type :=
267   | cnd_weak   : ClosedND []
268   | cnd_rule   : forall h c    , ClosedND h -> Rule h  c -> ClosedND c
269   | cnd_branch : forall   c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2)
270   .
272   (*
273   (* we can turn an SCND without hypotheses into a ClosedND *)
274   Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
275   refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
276     (match pn2 in SCND H C return H=h -> C=c -> _  with
277       | scnd_weak   c                 => let case_weak := tt in _
278       | scnd_leaf   ht z pn'          => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _
279       | scnd_axiom c                  => let case_axiom := tt in _
280       | scnd_comp  ht ct c pn' rule   => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
281       | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
282                                         let q1 := closedFromPnodes _ _ pn' in
283                                         let q2 := closedFromPnodes _ _ pn'' in _
285     end (refl_equal _) (refl_equal _))) h c pn2 cnd).
287   destruct case_axiom.
288     intros; subst.
289     (* FIXME *)
291   destruct case_comp.
292     intros.
293     clear pn2.
294     apply (cnd_rule ct).
295     apply qq.
296     subst.
297     apply cnd0.
298     apply rule.
300   destruct case_weak.
301     intros; subst.
302     apply cnd_weak.
304   destruct case_leaf.
305     intros.
306     apply qq.
307     subst.
308     apply cnd0.
310   destruct case_branch.
311     intros.
312     apply cnd_branch.
313     apply q1. subst. apply cnd0.
314     apply q2. subst. apply cnd0.
315     Defined.
316     *)
318   Close Scope nd_scope.
319   Open Scope pf_scope.
321 End Natural_Deduction.
323 Implicit Arguments ND [ Judgment ].
324 Hint Constructors Structural.
325 Hint Extern 1 => apply nd_id_structural.
326 Hint Extern 1 => apply ndr_structural_indistinguishable.
328 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
329  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
330 Notation "H /⋯⋯/ C" := (@ND _ _ H C)             : pf_scope.
331 Notation "a ;; b"   := (nd_comp a b)             : nd_scope.
332 Notation "a ** b"   := (nd_prod a b)             : nd_scope.
333 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
334 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
336 (* enable setoid rewriting *)
337 Open Scope nd_scope.
338 Open Scope pf_scope.
340 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
341   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
342   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
343   transitivity proved by (@Equivalence_Transitive _ _ (ndr_eqv_equivalence h c))
344     as parametric_relation_ndr_eqv.
345   Add Parametric Morphism {jt rt ndr h x c} : (@nd_comp jt rt h x c)
346   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
347     as parametric_morphism_nd_comp.
348     intros; apply ndr_comp_respects; auto.
349     Defined.
350   Add Parametric Morphism {jt rt ndr a b c d} : (@nd_prod jt rt a b c d)
351   with signature ((ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)) ==> (ndr_eqv(ND_Relation:=ndr)))
352     as parametric_morphism_nd_prod.
353     intros; apply ndr_prod_respects; auto.
354     Defined.
356 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
357 Definition nd_replicate
358   : forall
359     {Judgment}{Rule}{Ob}
360     (h:Ob->Judgment)
361     (c:Ob->Judgment)
362     (j:Tree ??Ob),
363     (forall (o:Ob), @ND Judgment Rule [h o] [c o]) ->
364     @ND Judgment Rule (mapOptionTree h j) (mapOptionTree c j).
365   intros.
366   induction j; simpl.
367     destruct a; simpl.
368     apply X.
369     apply nd_id0.
370     apply nd_prod; auto.
371     Defined.
373 (* "map" over natural deduction proofs, where the result proof has the same judgments (but different rules) *)
374 Definition nd_map
375   : forall
376     {Judgment}{Rule0}{Rule1}
377     (r:forall h c, Rule0 h c -> @ND Judgment Rule1 h c)
378     {h}{c}
379     (pf:@ND Judgment Rule0 h c)
380     ,
381     @ND Judgment Rule1 h c.
382     intros Judgment Rule0 Rule1 r.
384     refine ((fix nd_map h c pf {struct pf} :=
385      ((match pf
386          in @ND _ _ H C
387           return
388           @ND Judgment Rule1 H C
389         with
390         | nd_id0                     => let case_nd_id0     := tt in _
391         | nd_id1     h               => let case_nd_id1     := tt in _
392         | nd_weak    h               => let case_nd_weak    := tt in _
393         | nd_copy    h               => let case_nd_copy    := tt in _
394         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
395         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
396         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
397         | nd_cancell _               => let case_nd_cancell := tt in _
398         | nd_cancelr _               => let case_nd_cancelr := tt in _
399         | nd_llecnac _               => let case_nd_llecnac := tt in _
400         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
401         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
402         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
403       end))) ); simpl in *.
405     destruct case_nd_id0.      apply nd_id0.
406     destruct case_nd_id1.      apply nd_id1.
407     destruct case_nd_weak.     apply nd_weak.
408     destruct case_nd_copy.     apply nd_copy.
409     destruct case_nd_prod.     apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
410     destruct case_nd_comp.     apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
411     destruct case_nd_cancell.  apply nd_cancell.
412     destruct case_nd_cancelr.  apply nd_cancelr.
413     destruct case_nd_llecnac.  apply nd_llecnac.
414     destruct case_nd_rlecnac.  apply nd_rlecnac.
415     destruct case_nd_assoc.    apply nd_assoc.
416     destruct case_nd_cossa.    apply nd_cossa.
417     apply r. apply rule.
418     Defined.
420 (* "map" over natural deduction proofs, where the result proof has different judgments *)
421 Definition nd_map'
422   : forall
423     {Judgment0}{Rule0}{Judgment1}{Rule1}
424     (f:Judgment0->Judgment1)
425     (r:forall h c, Rule0 h c -> @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c))
426     {h}{c}
427     (pf:@ND Judgment0 Rule0 h c)
428     ,
429     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
430     intros Judgment0 Rule0 Judgment1 Rule1 f r.
432     refine ((fix nd_map' h c pf {struct pf} :=
433      ((match pf
434          in @ND _ _ H C
435           return
436           @ND Judgment1 Rule1 (mapOptionTree f H) (mapOptionTree f C)
437         with
438         | nd_id0                     => let case_nd_id0     := tt in _
439         | nd_id1     h               => let case_nd_id1     := tt in _
440         | nd_weak    h               => let case_nd_weak    := tt in _
441         | nd_copy    h               => let case_nd_copy    := tt in _
442         | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
443         | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
444         | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
445         | nd_cancell _               => let case_nd_cancell := tt in _
446         | nd_cancelr _               => let case_nd_cancelr := tt in _
447         | nd_llecnac _               => let case_nd_llecnac := tt in _
448         | nd_rlecnac _               => let case_nd_rlecnac := tt in _
449         | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
450         | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
451       end))) ); simpl in *.
453     destruct case_nd_id0.      apply nd_id0.
454     destruct case_nd_id1.      apply nd_id1.
455     destruct case_nd_weak.     apply nd_weak.
456     destruct case_nd_copy.     apply nd_copy.
457     destruct case_nd_prod.     apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
458     destruct case_nd_comp.     apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
459     destruct case_nd_cancell.  apply nd_cancell.
460     destruct case_nd_cancelr.  apply nd_cancelr.
461     destruct case_nd_llecnac.  apply nd_llecnac.
462     destruct case_nd_rlecnac.  apply nd_rlecnac.
463     destruct case_nd_assoc.    apply nd_assoc.
464     destruct case_nd_cossa.    apply nd_cossa.
465     apply r. apply rule.
466     Defined.
468 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate *)
469 Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h}{c}, @ND Judgment Rule h c -> Prop :=
470   | nd_property_structural      : forall h c pf, Structural pf -> @nd_property _ _ P h c pf
471   | nd_property_prod            : forall h0 c0 pf0 h1 c1 pf1,
472     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P h1 c1 pf1 -> @nd_property _ _ P _ _ (nd_prod pf0 pf1)
473   | nd_property_comp            : forall h0 c0 pf0  c1 pf1,
474     @nd_property _ _ P h0 c0 pf0 -> @nd_property _ _ P c0 c1 pf1 -> @nd_property _ _ P _ _ (nd_comp pf0 pf1)
475   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
476   Hint Constructors nd_property.
478 Close Scope pf_scope.
479 Close Scope nd_scope.