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