X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;fp=src%2FNaturalDeduction.v;h=f8baff0a4051152da2b85477f06a80bbb9ac65b0;hp=047ab87746125c9747876a87ef004e0774f2b6b2;hb=ee7da23597402df671f18320edff6604f5f6de7c;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 047ab87..f8baff0 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -218,7 +218,6 @@ Section Natural_Deduction.
    * emit as LaTeX code.
    *)
   Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
-  | scnd_axiom  : forall c       , SCND [] [c]
   | 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]
@@ -226,14 +225,6 @@ Section Natural_Deduction.
   .
   Hint Constructors SCND.
 
-  Definition mkSCNDAxioms (h:Tree ??Judgment) : SCND [] h.
-    induction h.
-      destruct a.
-      apply scnd_leaf.  apply scnd_axiom.
-      apply scnd_weak.
-      apply scnd_branch; auto.
-      Defined.
-
   (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *)
   Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
     : forall h x c,  ND x c -> SCND h x -> SCND h c.
@@ -265,18 +256,16 @@ Section Natural_Deduction.
   (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *)
   Inductive ClosedND : Tree ??Judgment -> Type :=
   | cnd_weak   : ClosedND []
-  | cnd_rule   : forall h c    , ClosedND h -> Rule h  c -> ClosedND c
+  | cnd_rule   : forall h c    , ClosedND h  -> Rule h c    -> ClosedND c
   | cnd_branch : forall   c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2)
   .
 
-  (*
   (* we can turn an SCND without hypotheses into a ClosedND *)
   Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
   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_axiom c                  => let case_axiom := 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 
@@ -284,10 +273,6 @@ Section Natural_Deduction.
 
     end (refl_equal _) (refl_equal _))) h c pn2 cnd).
 
-  destruct case_axiom.
-    intros; subst.
-    (* FIXME *)
-
   destruct case_comp.
     intros.
     clear pn2.
@@ -313,7 +298,6 @@ Section Natural_Deduction.
     apply q1. subst. apply cnd0.
     apply q2. subst. apply cnd0.
     Defined.
-    *)
 
   Close Scope nd_scope.
   Open Scope pf_scope.