X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;fp=src%2FNaturalDeduction.v;h=56d74cda5ecb82dba4d32a8f12e3bf24d701edab;hp=3a06d669c6d5184be3488e695b9501ceaef7c2aa;hb=2d963cf6994fa510fe67d5bf3852ffcc8090496c;hpb=77e8c70f4fd7a32db036fee5884a98208d450de2

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 3a06d66..56d74cd 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -479,6 +479,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.