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

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 047ab87..5cf67db 100644
--- 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 :=
@@ -209,6 +229,9 @@ Section Natural_Deduction.
 
   (* 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
   }.
 
   (* 
@@ -218,7 +241,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 +248,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 +279,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 +296,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 +321,14 @@ Section Natural_Deduction.
     apply q1. subst. apply cnd0.
     apply q2. subst. apply cnd0.
     Defined.
-    *)
+
+  (* undo the above *)
+  Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
+  match cnd in ClosedND 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.
 
   Close Scope nd_scope.
   Open Scope pf_scope.