remove ClosedSIND (use "SIND []" instead)

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index ee475da..177bd6d 100644 (file)
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -231,7 +231,7 @@ Section HaskProofStratified.
       Alternating c'.
 
   Require Import Coq.Logic.Eqdep.
       Alternating c'.
 
   Require Import Coq.Logic.Eqdep.

-
+(*

   Lemma magic a b c d ec e :
     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
   Lemma magic a b c d ec e :
     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].

@@ -318,7 +318,7 @@ Section HaskProofStratified.
       destruct c; try destruct o; inversion H.
       destruct j.
       Admitted.
       destruct c; try destruct o; inversion H.
       destruct j.
       Admitted.

-
+*)

   (* any proof in organized form can be "dis-organized" *)
   (*
   Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
   (* any proof in organized form can be "dis-organized" *)
   (*
   Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 06f97a1..52f2154 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -758,15 +758,12 @@ Section HaskProofToStrong.
       apply H2.
     Defined.
 
       apply H2.
     Defined.
 

-  Definition closed2expr : forall c (pn:@ClosedSIND _ Rule c), ITree _ judg2exprType c.
-    refine ((
-      fix closed2expr' j (pn:@ClosedSIND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
-      match pn in @ClosedSIND _ _ J return ITree _ judg2exprType J with
-      | cnd_weak             => let case_nil    := tt in INone _ _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
-      end)); clear closed2expr'; intros; subst.
-        Defined.
+  Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+    match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+    | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
+    | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+    | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+    end.

 
   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 
   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.

@@ -804,7 +801,7 @@ Section HaskProofToStrong.
     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
     intro pf.
     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
     intro pf.

-    set (closedFromSIND _ _ (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+    set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.

     apply closed2expr in cnd.
     apply ileaf in cnd.
     simpl in *.
     apply closed2expr in cnd.
     apply ileaf in cnd.
     simpl in *.

@@ -819,6 +816,7 @@ Section HaskProofToStrong.
     refine (return OK _).
     exists ξ.
     apply (ileaf it).
     refine (return OK _).
     exists ξ.
     apply (ileaf it).

+    apply INone.

     Defined.
 
 End HaskProofToStrong.
     Defined.
 
 End HaskProofToStrong.

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 4ecc166..719e714 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -325,53 +325,6 @@ Section Natural_Deduction.
           inversion bogus.
           Defined.
 
           inversion bogus.
           Defined.
 

-  (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *)
-  Inductive ClosedSIND : Tree ??Judgment -> Type :=
-  | cnd_weak   : ClosedSIND []
-  | cnd_rule   : forall h c    , ClosedSIND h  -> Rule h c    -> ClosedSIND c
-  | cnd_branch : forall   c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2)
-  .
-
-  (* we can turn an SIND without hypotheses into a ClosedSIND *)
-  Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c.
-  refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} := 
-    (match pn2 in SIND H C return H=h -> C=c -> _  with
-      | scnd_weak   c                 => let case_weak := 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 
-                                         let q2 := closedFromPnodes _ _ pn'' in _
-
-    end (refl_equal _) (refl_equal _))) h c pn2 cnd).
-
-  destruct case_weak.
-    intros; subst.
-    apply cnd_weak.
-
-  destruct case_comp.
-    intros.
-    clear pn2.
-    apply (cnd_rule ct).
-    apply qq.
-    subst.
-    apply cnd0.
-    apply rule.
-
-  destruct case_branch.
-    intros.
-    apply cnd_branch.
-    apply q1. subst. apply cnd0.
-    apply q2. subst. apply cnd0.
-    Defined.
-
-  (* undo the above *)
-  Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c :=
-  match cnd in ClosedSIND 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.
-

   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
   Section SequentND.
     Context {S:Type}.                   (* type of sequent components *)
   (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
   Section SequentND.
     Context {S:Type}.                   (* type of sequent components *)

@@ -751,19 +704,6 @@ Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall
   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
   Hint Constructors nd_property.
 
   | nd_property_rule            : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
   Hint Constructors nd_property.
 

-(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
-Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
-| cnd_property_weak            : @cnd_property _ _ P _ cnd_weak
-| cnd_property_rule            : forall h c r cnd',
-  P h c r ->
-  @cnd_property _ _ P h cnd' ->
-  @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
-| cnd_property_branch          :
-  forall c1 c2 cnd1 cnd2,
-  @cnd_property _ _ P c1 cnd1 ->
-  @cnd_property _ _ P c2 cnd2 ->
-  @cnd_property _ _ P _  (cnd_branch _ _ cnd1 cnd2).
-

 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
 | scnd_property_weak            : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
 (* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
 Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
 | scnd_property_weak            : forall c, @scnd_property _ _ P _ _ (scnd_weak c)