add ndr_void_proofs_irrelevant

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

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index f8baff0..cd225da 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.
@@ -209,6 +212,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
   }.
 
   (* 
@@ -299,6 +305,14 @@ Section Natural_Deduction.
     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.