update submodule pointer

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

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 2bc361f..06b6efe 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -1,5 +1,8 @@
 (*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq                                                                         *)
+(* NaturalDeduction:                                                                                                             *)
+(*                                                                                                                               *)
+(*   Structurally explicit natural deduction proofs.                                                                             *)
+(*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.
@@ -179,6 +182,13 @@ Section Natural_Deduction.
       | T_Branch a b     => nd_prod (nd_id a) (nd_id b)
     end.
 
+  Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
+    match sl as SL return SL /⋯⋯/ [] with
+      | T_Leaf None      => nd_id0
+      | T_Leaf (Some x)  => nd_weak x
+      | T_Branch a b     => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
+    end.
+
   Hint Constructors Structural.
   Lemma nd_id_structural : forall sl, Structural (nd_id sl).
     intros.
@@ -186,6 +196,16 @@ Section Natural_Deduction.
     destruct a; auto.
     Defined.
 
+  Lemma weak'_structural : forall a, Structural (nd_weak' a).
+    intros.
+    induction a.
+    destruct a; auto.
+    simpl.
+    auto.
+    simpl.
+    auto.
+    Qed.
+
   (* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
    * structural variations  *)
   Class ND_Relation :=
@@ -207,8 +227,14 @@ Section Natural_Deduction.
   (* products and composition must distribute over each other *)
   ; ndr_prod_preserves_comp  : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
 
+  (* products and duplication must distribute over each other *)
+  ; ndr_prod_preserves_copy  : forall `(f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
+
   (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
   ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
+
+  (* any two proofs of nothing are "equally good" *)
+  ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
   }.
 
   (* 
@@ -307,11 +333,56 @@ 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_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
+    }.
+
+  End Sequents.
+
+  Section SequentsOfTrees.
+    Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}(sc:SequentCalculus sequent).
+    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]
+    }.
+
+    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]
+    }.
+  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.