X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofCategory.v;h=4140f7dba9ae80e12d78b7d01c8e4bc7343eaf3b;hp=cf1fb8621856a76ff753a527f29042fd9894df12;hb=6ef9f270b138fc7aab48013d55a8192ff022c0f1;hpb=9adf3f5756893322d0114f89c0908590817eda2b

diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v
index cf1fb86..4140f7d 100644
--- a/src/HaskProofCategory.v
+++ b/src/HaskProofCategory.v
@@ -115,10 +115,10 @@ Section HaskProofCategory.
     Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]]
     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 
-  | PCF_REmptyGroup      :                 Rule_PCF ec [           ] [ pcfjudg []  [] ] (REmptyGroup   Γ Δ  )
+  | PCF_RVoid      :                 Rule_PCF ec [           ] [ pcfjudg []  [] ] (RVoid   Γ Δ  )
 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
-  | PCF_RBindingGroup    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
-    (RBindingGroup Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
+  | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
+    (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
   (* need int/boolean case *)
   Implicit Arguments Rule_PCF [ ].
 
@@ -228,24 +228,24 @@ Section HaskProofCategory.
   Require Import Coq.Logic.Eqdep.
 
   Lemma magic a b c d ec e :
-    ClosedND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
-    ClosedND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
+    ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
+    ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
   admit.
   Defined.
 
-  Definition orgify : forall Γ Δ Σ τ (pf:ClosedND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
+  Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 
     refine (
-      fix  orgify_fc' Γ Δ Σ τ (pf:ClosedND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
+      fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
         let case_main := tt in _
-      with orgify_fc c (pf:ClosedND c) {struct pf} : Alternating c :=
+      with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
       (match c as C return C=c -> Alternating C with
         | T_Leaf None                    => fun _ => alt_nil
         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
       end (refl_equal _))
       with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
-        (pf:ClosedND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
+        (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
         let case_pcf := tt in _
       for orgify_fc').
 
@@ -296,13 +296,13 @@ Section HaskProofCategory.
     Admitted.
 
   Definition pcfify Γ Δ ec : forall Σ τ,
-    ClosedND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
+    ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
       -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
 
     refine ((
-      fix pcfify Σ τ (pn:@ClosedND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
+      fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
       : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
-     (match pn in @ClosedND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
+     (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
       | cnd_weak             => let case_nil    := tt in _
       | cnd_rule h c cnd' r  => let case_rule   := tt in _
       | cnd_branch _ _ c1 c2 => let case_branch := tt in _
@@ -361,14 +361,14 @@ Section HaskProofCategory.
       exists (RVar _ _ _ _).
       apply PCF_RVar.
     apply nd_rule.
-      exists (REmptyGroup _ _ ).
-      apply PCF_REmptyGroup.
+      exists (RVoid _ _ ).
+      apply PCF_RVoid.
     eapply nd_comp.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply (nd_prod IHa1 IHa2).
       apply nd_rule.
-        exists (RBindingGroup _ _ _ _ _ _). 
-        apply PCF_RBindingGroup.
+        exists (RJoin _ _ _ _ _ _). 
+        apply PCF_RJoin.
         Defined.
 
   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
@@ -417,7 +417,7 @@ Section HaskProofCategory.
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
     apply nd_rule.
-    set (@PCF_RBindingGroup Γ Δ lev a b a c) as q'.
+    set (@PCF_RJoin Γ Δ lev a b a c) as q'.
     refine (existT _ _ _).
     apply q'.
     Defined.
@@ -426,7 +426,7 @@ Section HaskProofCategory.
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
     apply nd_rule.
-    set (@PCF_RBindingGroup Γ Δ lev b a c a) as q'.
+    set (@PCF_RJoin Γ Δ lev b a c a) as q'.
     refine (existT _ _ _).
     apply q'.
     Defined.
@@ -484,13 +484,13 @@ Section HaskProofCategory.
       apply org_fc with (r:=RVar _ _ _ _).
       auto.
     apply nd_rule.
-      apply org_fc with (r:=REmptyGroup _ _ ).
+      apply org_fc with (r:=RVoid _ _ ).
       auto.
     eapply nd_comp.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply (nd_prod IHa1 IHa2).
       apply nd_rule.
-        apply org_fc with (r:=RBindingGroup _ _ _ _ _ _). 
+        apply org_fc with (r:=RJoin _ _ _ _ _ _). 
         auto.
         Defined.
 
@@ -534,7 +534,7 @@ Section HaskProofCategory.
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
     apply nd_rule.
-    apply org_fc with (r:=RBindingGroup Γ Δ a b a c).
+    apply org_fc with (r:=RJoin Γ Δ a b a c).
     auto.
     Defined.
 
@@ -542,7 +542,7 @@ Section HaskProofCategory.
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
     apply nd_rule.
-    apply org_fc with (r:=RBindingGroup Γ Δ b a c a).
+    apply org_fc with (r:=RJoin Γ Δ b a c a).
     auto.
     Defined.
 
@@ -632,22 +632,22 @@ Section HaskProofCategory.
 
     induction X; simpl.
 
-    (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
-    apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto.
+    (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
+    apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto.
 
     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
     apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
 
-    (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
+    (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
     eapply nd_comp;
       [ idtac
       | eapply nd_rule
       ; eapply (org_fc  _ _ (RArrange _ _ _ _ _ (RWeak _)))
       ; auto ].
       eapply nd_rule.
-      eapply (org_fc _ _ (REmptyGroup _ _)); auto.
+      eapply (org_fc _ _ (RVoid _ _)); auto.
     
-    (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
+    (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       set (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))
@@ -657,15 +657,15 @@ Section HaskProofCategory.
       apply q.
       apply q.
       apply nd_rule. 
-      eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
       auto.
       auto.
 
-    (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
+    (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
     eapply nd_comp.
       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
       apply nd_rule.
-      eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
+      eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )).
       auto.
 
     (* nd_comp becomes pl_subst (aka nd_cut) *)
@@ -719,8 +719,8 @@ Section HaskProofCategory.
                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
-                | PCF_RBindingGroup    b c d e          => let case_RBindingGroup := tt in _
-                | PCF_REmptyGroup                       => let case_REmptyGroup   := tt in _
+                | PCF_RJoin    b c d e          => let case_RJoin := tt in _
+                | PCF_RVoid                       => let case_RVoid   := tt in _
               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
               end); simpl in *.
@@ -820,11 +820,11 @@ Section HaskProofCategory.
         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
         admit.
 
-      destruct case_REmptyGroup.
+      destruct case_RVoid.
         (* ga_id u *)
         admit.
 
-      destruct case_RBindingGroup.
+      destruct case_RJoin.
         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
         admit.