X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;h=acb21d0f61343a8d968960b043355ed203cafbbf;hp=407948b134bc763b3cad1963a8ce341bc5df117d;hb=148579e5c8f6b60209a442222b932cf59f163cca;hpb=85e4f0fd6b0673c1cc763eeb2585b7dc3d388455 diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 407948b..acb21d0 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -182,6 +182,13 @@ Section Natural_Deduction. | T_Branch a b => nd_prod (nd_id a) (nd_id b) end. + Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] := + match sl as SL return SL /⋯⋯/ [] with + | T_Leaf None => nd_id0 + | T_Leaf (Some x) => nd_weak x + | T_Branch a b => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr + end. + Hint Constructors Structural. Lemma nd_id_structural : forall sl, Structural (nd_id sl). intros. @@ -189,6 +196,16 @@ Section Natural_Deduction. destruct a; auto. Defined. + Lemma weak'_structural : forall a, Structural (nd_weak' a). + intros. + induction a. + destruct a; auto. + simpl. + auto. + simpl. + auto. + Qed. + (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to * structural variations *) Class ND_Relation := @@ -210,20 +227,25 @@ Section Natural_Deduction. (* products and composition must distribute over each other *) ; 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') + (* products and duplication must distribute over each other *) + ; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b + (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *) ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g + + (* any two proofs of nothing are "equally good" *) + ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g }. (* * Single-conclusion proofs; this is an alternate representation * where each inference has only a single conclusion. These have - * worse compositionality properties than ND's, but are easier to - * emit as LaTeX code. + * worse compositionality properties than ND's (they don't form a + * category), but are easier to emit as LaTeX code. *) Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type := - | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c] | scnd_weak : forall c , SCND c [] - | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c] + | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c] | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2) . Hint Constructors SCND. @@ -250,7 +272,7 @@ Section Natural_Deduction. inversion k; subst; inversion X0; subst; auto. destruct c. destruct o. - apply scnd_leaf. eapply scnd_comp. apply k. apply r. + eapply scnd_comp. apply k. apply r. apply scnd_weak. set (all_rules_one_conclusion _ _ _ r) as bogus. inversion bogus. @@ -268,7 +290,6 @@ Section Natural_Deduction. refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} := (match pn2 in SCND H C return H=h -> C=c -> _ with | scnd_weak c => let case_weak := tt in _ - | scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _ | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _ | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in let q1 := closedFromPnodes _ _ pn' in @@ -276,24 +297,18 @@ Section Natural_Deduction. end (refl_equal _) (refl_equal _))) h c pn2 cnd). - destruct case_comp. - intros. - clear pn2. - apply (cnd_rule ct). - apply qq. - subst. - apply cnd0. - apply rule. - destruct case_weak. intros; subst. apply cnd_weak. - destruct case_leaf. + destruct case_comp. intros. + clear pn2. + apply (cnd_rule ct). apply qq. subst. apply cnd0. + apply rule. destruct case_branch. intros. @@ -310,11 +325,65 @@ Section Natural_Deduction. | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2) end. + Section Sequents. + Context {S:Type}. (* type of sequent components *) + Context {sequent:S->S->Judgment}. + Context {ndr:ND_Relation}. + Notation "a |= b" := (sequent a b). + Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + + Class SequentCalculus := + { nd_seq_reflexive : forall a, ND [ ] [ a |= a ] + }. + + Class CutRule (nd_cutrule_seq:SequentCalculus) := + { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] + ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell + ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr + ; nd_cut_associativity : forall {a b c d}, + (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 + }. + + End Sequents. +(*Implicit Arguments SequentCalculus [ S ]*) +(*Implicit Arguments CutRule [ S ]*) + Section SequentsOfTrees. + Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}. + Context (ndr:ND_Relation). + Notation "a |= b" := (sequent a b). + Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + + Class TreeStructuralRules := + { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x] + ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x] + ; tsr_ant_cancell : forall {x a }, ND [ [],,a |= x] [ a |= x] + ; tsr_ant_cancelr : forall {x a }, ND [a,,[] |= x] [ a |= x] + ; tsr_ant_llecnac : forall {x a }, ND [ a |= x] [ [],,a |= x] + ; tsr_ant_rlecnac : forall {x a }, ND [ a |= x] [ a,,[] |= x] + }. + + Notation "[# a #]" := (nd_rule a) : nd_scope. + + Context `{se_cut : @CutRule _ sequent ndr sc}. + Class SequentExpansion := + { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] + ; se_expand_right : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] + + (* left and right expansion must commute with cut *) + ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; se_expand_left c === nd_seq_reflexive (c,, a) + ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c) + ; se_cut_left : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c) + ; se_cut_right : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c) + }. + End SequentsOfTrees. + Close Scope nd_scope. Open Scope pf_scope. End Natural_Deduction. +Coercion nd_cut : CutRule >-> Funclass. + Implicit Arguments ND [ Judgment ]. Hint Constructors Structural. Hint Extern 1 => apply nd_id_structural. @@ -470,5 +539,30 @@ Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall | nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r). Hint Constructors nd_property. +(* witnesses the fact that every Rule in a particular proof satisfies the given predicate *) +Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedND Judgment Rule c -> Prop := +| cnd_property_weak : @cnd_property _ _ P _ cnd_weak +| cnd_property_rule : forall h c r cnd', + P h c r -> + @cnd_property _ _ P h cnd' -> + @cnd_property _ _ P c (cnd_rule _ _ cnd' r) +| cnd_property_branch : + forall c1 c2 cnd1 cnd2, + @cnd_property _ _ P c1 cnd1 -> + @cnd_property _ _ P c2 cnd2 -> + @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2). + +Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SCND Judgment Rule h c -> Prop := +| scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c) +| scnd_property_comp : forall h x c r cnd', + P x [c] r -> + @scnd_property _ _ P h x cnd' -> + @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r) +| scnd_property_branch : + forall x c1 c2 cnd1 cnd2, + @scnd_property _ _ P x c1 cnd1 -> + @scnd_property _ _ P x c2 cnd2 -> + @scnd_property _ _ P x _ (scnd_branch _ _ _ cnd1 cnd2). + Close Scope pf_scope. Close Scope nd_scope.