X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;h=acb21d0f61343a8d968960b043355ed203cafbbf;hp=855b66a7614d31985359c0d5eb8ec09f8054aeda;hb=148579e5c8f6b60209a442222b932cf59f163cca;hpb=8cb97991a95d5761a28ca94767b8fe637d1411d9

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 855b66a..acb21d0 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -240,13 +240,12 @@ Section Natural_Deduction.
   (* 
    * 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.
@@ -273,7 +272,7 @@ Section Natural_Deduction.
       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.
@@ -291,7 +290,6 @@ Section Natural_Deduction.
   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 
@@ -299,24 +297,18 @@ Section Natural_Deduction.
 
     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.
@@ -333,11 +325,65 @@ Section Natural_Deduction.
   | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
   end.
 
+  Section Sequents.
+    Context {S:Type}.   (* type of sequent components *)
+    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.
+
+    Class SequentCalculus :=
+    { 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 ]
+    ; 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_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}.
+    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}, 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}, 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.
+
   Close Scope nd_scope.
   Open Scope pf_scope.
 
 End Natural_Deduction.
 
+Coercion nd_cut : CutRule >-> Funclass.
+
 Implicit Arguments ND [ Judgment ].
 Hint Constructors Structural.
 Hint Extern 1 => apply nd_id_structural.
@@ -493,5 +539,30 @@ 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 *)
+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.