X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;h=caa4dcfe8e434e804311ae61408c0ba8ffe57ed9;hp=56d74cda5ecb82dba4d32a8f12e3bf24d701edab;hb=4ec2860679a25b16cba9df2de6ea971064200756;hpb=2d963cf6994fa510fe67d5bf3852ffcc8090496c diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 56d74cd..caa4dcf 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -142,6 +142,9 @@ Section Natural_Deduction. (* natural deduction: you may duplicate conclusions *) | nd_copy : forall h, h /⋯⋯/ (h,,h) + (* natural deduction: you may re-order conclusions *) + | nd_exch : forall x y, (x,,y) /⋯⋯/ (y,,x) + (* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *) | nd_prod : forall {h1 h2 c1 c2} (pf1: h1 /⋯⋯/ c1 ) @@ -229,18 +232,7 @@ Section Natural_Deduction. Hint Constructors Structural. Hint Constructors BuiltFrom. Hint Constructors NDPredicateClosure. - - Hint Extern 1 => apply nd_structural_id0. - Hint Extern 1 => apply nd_structural_id1. - Hint Extern 1 => apply nd_structural_cancell. - Hint Extern 1 => apply nd_structural_cancelr. - Hint Extern 1 => apply nd_structural_llecnac. - Hint Extern 1 => apply nd_structural_rlecnac. - Hint Extern 1 => apply nd_structural_assoc. - Hint Extern 1 => apply nd_structural_cossa. - Hint Extern 1 => apply ndpc_p. - Hint Extern 1 => apply ndpc_prod. - Hint Extern 1 => apply ndpc_comp. + Hint Unfold StructuralND. Lemma nd_id_structural : forall sl, StructuralND (nd_id sl). intros. @@ -306,6 +298,7 @@ Section Natural_Deduction. apply k. apply scnd_weak. eapply scnd_branch; apply k. + inversion k; subst; auto. inversion k; subst. apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)). apply IHnd2. @@ -325,53 +318,6 @@ Section Natural_Deduction. inversion bogus. Defined. - (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *) - Inductive ClosedSIND : Tree ??Judgment -> Type := - | cnd_weak : ClosedSIND [] - | cnd_rule : forall h c , ClosedSIND h -> Rule h c -> ClosedSIND c - | cnd_branch : forall c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2) - . - - (* we can turn an SIND without hypotheses into a ClosedSIND *) - Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c. - refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} := - (match pn2 in SIND H C return H=h -> C=c -> _ with - | scnd_weak c => let case_weak := tt 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 - let q2 := closedFromPnodes _ _ pn'' in _ - - end (refl_equal _) (refl_equal _))) h c pn2 cnd). - - destruct case_weak. - intros; subst. - apply cnd_weak. - - destruct case_comp. - intros. - clear pn2. - apply (cnd_rule ct). - apply qq. - subst. - apply cnd0. - apply rule. - - destruct case_branch. - intros. - apply cnd_branch. - apply q1. subst. apply cnd0. - apply q2. subst. apply cnd0. - Defined. - - (* undo the above *) - Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c := - match cnd in ClosedSIND C return ND [] C with - | cnd_weak => nd_id0 - | cnd_rule h c cndh rhc => closedNDtoNormalND cndh ;; nd_rule rhc - | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2) - end. - (* Natural Deduction systems whose judgments happen to be pairs of the same type *) Section SequentND. Context {S:Type}. (* type of sequent components *) @@ -511,42 +457,6 @@ Coercion sndr_ndr : SequentND_Relation >-> ND_Relation. Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation. Implicit Arguments ND [ Judgment ]. -Hint Constructors Structural. -Hint Extern 1 => apply nd_id_structural. -Hint Extern 1 => apply ndr_builtfrom_structural. -Hint Extern 1 => apply nd_structural_id0. -Hint Extern 1 => apply nd_structural_id1. -Hint Extern 1 => apply nd_structural_cancell. -Hint Extern 1 => apply nd_structural_cancelr. -Hint Extern 1 => apply nd_structural_llecnac. -Hint Extern 1 => apply nd_structural_rlecnac. -Hint Extern 1 => apply nd_structural_assoc. -Hint Extern 1 => apply nd_structural_cossa. -Hint Extern 1 => apply ndpc_p. -Hint Extern 1 => apply ndpc_prod. -Hint Extern 1 => apply ndpc_comp. -Hint Extern 1 => apply builtfrom_refl. -Hint Extern 1 => apply builtfrom_prod1. -Hint Extern 1 => apply builtfrom_prod2. -Hint Extern 1 => apply builtfrom_comp1. -Hint Extern 1 => apply builtfrom_comp2. -Hint Extern 1 => apply builtfrom_P. - -Hint Extern 1 => apply snd_inert_initial. -Hint Extern 1 => apply snd_inert_cut. -Hint Extern 1 => apply snd_inert_structural. - -Hint Extern 1 => apply cnd_inert_initial. -Hint Extern 1 => apply cnd_inert_cut. -Hint Extern 1 => apply cnd_inert_structural. -Hint Extern 1 => apply cnd_inert_cnd_ant_assoc. -Hint Extern 1 => apply cnd_inert_cnd_ant_cossa. -Hint Extern 1 => apply cnd_inert_cnd_ant_cancell. -Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr. -Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac. -Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac. -Hint Extern 1 => apply cnd_inert_se_expand_left. -Hint Extern 1 => apply cnd_inert_se_expand_right. (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds * of proofs. When only one kind of proof is in use, it's quite helpful though. *) @@ -556,10 +466,39 @@ Notation "a ** b" := (nd_prod a b) : nd_scope. Notation "[# a #]" := (nd_rule a) : nd_scope. Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope. +Hint Constructors Structural. +Hint Constructors ND_Relation. +Hint Constructors BuiltFrom. +Hint Constructors NDPredicateClosure. +Hint Constructors ContextND_Inert. +Hint Constructors SequentND_Inert. +Hint Unfold StructuralND. + (* enable setoid rewriting *) Open Scope nd_scope. Open Scope pf_scope. +Hint Extern 2 (StructuralND (nd_id _)) => apply nd_id_structural. +Hint Extern 2 (NDPredicateClosure _ ( _ ;; _ ) ) => apply ndpc_comp. +Hint Extern 2 (NDPredicateClosure _ ( _ ** _ ) ) => apply ndpc_prod. +Hint Extern 2 (NDPredicateClosure (@Structural _ _) (nd_id _)) => apply nd_id_structural. +Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp1. +Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp2. +Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod1. +Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod2. + +(* Hint Constructors has failed me! *) +Hint Extern 2 (@Structural _ _ _ _ (@nd_id0 _ _)) => apply nd_structural_id0. +Hint Extern 2 (@Structural _ _ _ _ (@nd_id1 _ _ _)) => apply nd_structural_id1. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cancell _ _ _)) => apply nd_structural_cancell. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cancelr _ _ _)) => apply nd_structural_cancelr. +Hint Extern 2 (@Structural _ _ _ _ (@nd_llecnac _ _ _)) => apply nd_structural_llecnac. +Hint Extern 2 (@Structural _ _ _ _ (@nd_rlecnac _ _ _)) => apply nd_structural_rlecnac. +Hint Extern 2 (@Structural _ _ _ _ (@nd_assoc _ _ _ _ _)) => apply nd_structural_assoc. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cossa _ _ _ _ _)) => apply nd_structural_cossa. + +Hint Extern 4 (NDPredicateClosure _ _) => apply ndpc_p. + Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c) reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c)) symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c)) @@ -581,7 +520,8 @@ Section ND_Relation_Facts. (* useful *) Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f. - intros; apply (ndr_builtfrom_structural f); auto. + intros; apply (ndr_builtfrom_structural f). auto. + auto. Defined. (* useful *) @@ -589,6 +529,44 @@ Section ND_Relation_Facts. intros; apply (ndr_builtfrom_structural f); auto. Defined. + Ltac nd_prod_preserves_comp_ltac P EQV := + match goal with + [ |- context [ (?A ** ?B) ;; (?C ** ?D) ] ] => + set (@ndr_prod_preserves_comp _ _ EQV _ _ A _ _ B _ C _ D) as P + end. + + Lemma nd_swap A B C D (f:ND _ A B) (g:ND _ C D) : + (f ** nd_id C) ;; (nd_id B ** g) === + (nd_id A ** g) ;; (f ** nd_id D). + setoid_rewrite <- ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + Qed. + + (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *) + Ltac nd_swap_ltac P EQV := + match goal with + [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => + set (@nd_swap _ _ EQV _ _ _ _ F G) as P + end. + + Lemma nd_prod_split_left A B C D (f:ND _ A B) (g:ND _ B C) : + nd_id D ** (f ;; g) === + (nd_id D ** f) ;; (nd_id D ** g). + setoid_rewrite <- ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + reflexivity. + Qed. + + Lemma nd_prod_split_right A B C D (f:ND _ A B) (g:ND _ B C) : + (f ;; g) ** nd_id D === + (f ** nd_id D) ;; (g ** nd_id D). + setoid_rewrite <- ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + reflexivity. + Qed. + End ND_Relation_Facts. (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *) @@ -629,6 +607,7 @@ Definition nd_map | nd_id1 h => let case_nd_id1 := tt in _ | nd_weak1 h => let case_nd_weak := tt in _ | nd_copy h => let case_nd_copy := tt in _ + | nd_exch x y => let case_nd_exch := tt in _ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ | nd_rule _ _ rule => let case_nd_rule := tt in _ @@ -644,6 +623,7 @@ Definition nd_map destruct case_nd_id1. apply nd_id1. destruct case_nd_weak. apply nd_weak. destruct case_nd_copy. apply nd_copy. + destruct case_nd_exch. apply nd_exch. destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)). destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)). destruct case_nd_cancell. apply nd_cancell. @@ -677,6 +657,7 @@ Definition nd_map' | nd_id1 h => let case_nd_id1 := tt in _ | nd_weak1 h => let case_nd_weak := tt in _ | nd_copy h => let case_nd_copy := tt in _ + | nd_exch x y => let case_nd_exch := tt in _ | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _ | nd_comp _ _ _ top bot => let case_nd_comp := tt in _ | nd_rule _ _ rule => let case_nd_rule := tt in _ @@ -692,6 +673,7 @@ Definition nd_map' destruct case_nd_id1. apply nd_id1. destruct case_nd_weak. apply nd_weak. destruct case_nd_copy. apply nd_copy. + destruct case_nd_exch. apply nd_exch. destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)). destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)). destruct case_nd_cancell. apply nd_cancell. @@ -713,19 +695,6 @@ 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 (for ClosedSIND) *) -Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND 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). - (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *) Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop := | scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c) @@ -783,6 +752,9 @@ Section ToLatex. | nd_copy h' => rawLatexMath indent +++ rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL + | nd_exch x y => rawLatexMath indent +++ + rawLatexMath "\inferrule*[Left=exch]{"+++judgments2latex h+++ + rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++ rawLatexMath "% prod " +++ eolL +++ rawLatexMath indent +++