(*
* 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.
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.
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
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.
Section Sequents.
Context {S:Type}. (* type of sequent components *)
- Context (sequent:S->S->Judgment).
- Context (ndr:ND_Relation).
+ 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.
{ 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 ]
+ 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_cut a b c ** nd_id1 (c|=d)) ;; (nd_cut a c d) === nd_assoc ;; (nd_id1 (a|=b) ** nd_cut b c d) ;; nd_cut a b 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}(sc:SequentCalculus sequent).
+ 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}, Rule [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
- ; tsr_ant_cossa : forall {x a b c}, Rule [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
- ; tsr_ant_cancell : forall {x a }, Rule [ [],,a |= x] [ a |= x]
- ; tsr_ant_cancelr : forall {x a }, Rule [a,,[] |= x] [ a |= x]
- ; tsr_ant_llecnac : forall {x a }, Rule [ a |= x] [ [],,a |= x]
- ; tsr_ant_rlecnac : forall {x a }, Rule [ a |= x] [ a,,[] |= x]
+ { 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}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
- ; se_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
+ { 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.
| 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.
projects / coq-hetmet.git / blobdiff