add n-ary form of nd_weak

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

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 2bc361f..5cf67db 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 :=
@@ -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
   }.
 
   (*