remove ClosedSIND (use "SIND []" instead)

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

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 3a06d66..719e714 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -325,53 +325,6 @@ Section Natural_Deduction.
           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 *)
@@ -479,6 +432,25 @@ Section Natural_Deduction.
     ; cndr_sndr  := sndr
     }.
 
+    (* a proof is Analytic if it does not use cut *)
+    (*
+    Definition Analytic_Rule : NDPredicate :=
+      fun h c f => forall c, not (snd_cut _ _ c = f).
+    Definition AnalyticND := NDPredicateClosure Analytic_Rule.
+
+    (* a proof system has cut elimination if, for every proof, there is an analytic proof with the same conclusion *)
+    Class CutElimination :=
+    { ce_eliminate : forall h c, h/⋯⋯/c -> h/⋯⋯/c
+    ; ce_analytic  : forall h c f, AnalyticND (ce_eliminate h c f)
+    }.
+
+    (* cut elimination is strong if the analytic proof is furthermore equivalent to the original proof *)
+    Class StrongCutElimination :=
+    { sce_ce       <: CutElimination
+    ; ce_strong     : forall h c f, f === ce_eliminate h c f
+    }.
+    *)
+
   End ContextND.
 
   Close Scope nd_scope.
@@ -570,6 +542,44 @@ Section ND_Relation_Facts.
     intros; apply (ndr_builtfrom_structural f); auto.
     Defined.
 
+  Ltac nd_prod_preserves_comp_ltac P EQV :=
+    match goal with
+      [ |- context [ (?A ** ?B) ;; (?C ** ?D) ] ] => 
+        set (@ndr_prod_preserves_comp _ _ EQV _ _ A _ _ B _ C _ D) as P
+    end.
+
+  Lemma nd_swap A B C D (f:ND _ A B) (g:ND _ C D) :
+    (f ** nd_id C) ;; (nd_id B ** g) ===
+    (nd_id A ** g) ;; (f ** nd_id D).
+    setoid_rewrite <- ndr_prod_preserves_comp.
+    setoid_rewrite ndr_comp_left_identity.
+    setoid_rewrite ndr_comp_right_identity.
+    reflexivity.
+    Qed.
+
+  (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
+  Ltac nd_swap_ltac P EQV :=
+    match goal with
+      [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => 
+        set (@nd_swap _ _ EQV _ _ _ _ F G) as P
+    end.
+
+  Lemma nd_prod_split_left A B C D (f:ND _ A B) (g:ND _ B C) :
+    nd_id D ** (f ;; g) ===
+    (nd_id D ** f) ;; (nd_id D ** g).
+    setoid_rewrite <- ndr_prod_preserves_comp.
+    setoid_rewrite ndr_comp_left_identity.
+    reflexivity.
+    Qed.
+
+  Lemma nd_prod_split_right A B C D (f:ND _ A B) (g:ND _ B C) :
+    (f ;; g) ** nd_id D ===
+    (f ** nd_id D) ;; (g ** nd_id D).
+    setoid_rewrite <- ndr_prod_preserves_comp.
+    setoid_rewrite ndr_comp_left_identity.
+    reflexivity.
+    Qed.
+
 End ND_Relation_Facts.
 
 (* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
@@ -694,19 +704,6 @@ 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 (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)