X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;h=caa4dcfe8e434e804311ae61408c0ba8ffe57ed9;hp=719e7142ea22fdc3a0f16849498a7b16335e5b51;hb=423b0bd3972c5bcbbd757cb715e13b5b9104a9a6;hpb=9e7ea73d3a6f4bbfba279164a806490cf95efec4 diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 719e714..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. @@ -464,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. *) @@ -509,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)) @@ -534,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 *) @@ -620,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 _ @@ -635,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. @@ -668,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 _ @@ -683,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. @@ -761,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 +++