NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStruc...

[coq-hetmet.git] / src / NaturalDeduction.v

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 3b01c6d..8568e38 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -362,26 +362,26 @@ Section Natural_Deduction.
     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#]
+    ; 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.