(* 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 )
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.
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.
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. *)
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))
(* 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 *)
| 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 _
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.
| 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 _
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.
| 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 +++
projects / coq-hetmet.git / blobdiff