rename constructors of Arrange to start with A instead of R

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index d500e79..df7896b 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -237,7 +237,7 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
        [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
        [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

     eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.

@@ -252,7 +252,7 @@ Section core2proof.
     intro pf.
     eapply nd_comp.
     apply pf.
     intro pf.
     eapply nd_comp.
     apply pf.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].

     apply curry.
     Defined.
 
     apply curry.
     Defined.
 

@@ -268,8 +268,8 @@ Section core2proof.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.

-    eapply RCanR.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply ACanR.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

     apply curry.
     Defined.
 
     apply curry.
     Defined.
 

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 51fd784..1bb35c6 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -287,7 +287,7 @@ Section HaskFlattener.
     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
     intros.
     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
     intros.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].

     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.

@@ -296,7 +296,7 @@ Section HaskFlattener.
       apply X.
       eapply nd_rule.
       eapply RArrange.
       apply X.
       eapply nd_rule.
       eapply RArrange.

-      apply RuCanR.
+      apply AuCanR.

     Defined.
 
   Definition precompose Γ Δ ec : forall a x y z lev,
     Defined.
 
   Definition precompose Γ Δ ec : forall a x y z lev,

@@ -308,7 +308,7 @@ Section HaskFlattener.
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

     apply ga_comp.
     Defined.
 
     apply ga_comp.
     Defined.
 

@@ -317,8 +317,8 @@ Section HaskFlattener.
       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
     intros.
       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
     intros.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ].
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].

     apply precompose.
     Defined.
 
     apply precompose.
     Defined.
 

@@ -338,7 +338,7 @@ Section HaskFlattener.
     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
     intros.
     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
     intros.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].

     eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply X.
     Defined.
     eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply X.
     Defined.

@@ -347,12 +347,12 @@ Section HaskFlattener.
     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
     intros.
     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
     intros.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].

     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].

     apply ga_first.
     Defined.
 
     apply ga_first.
     Defined.
 

@@ -370,12 +370,12 @@ Section HaskFlattener.
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
     intros.
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
     intros.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].

     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].

     apply ga_second.
     Defined.
 
     apply ga_second.
     Defined.
 

@@ -393,7 +393,7 @@ Section HaskFlattener.
      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ] 
      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
      intros.
      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ] 
      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
      intros.

-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.
      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.

@@ -404,7 +404,7 @@ Section HaskFlattener.
      apply nd_prod.
      apply postcompose.
      apply ga_uncancell.
      apply nd_prod.
      apply postcompose.
      apply ga_uncancell.

-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

      apply precompose.
      Defined.
 
      apply precompose.
      Defined.
 

@@ -430,38 +430,38 @@ Section HaskFlattener.
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
           with
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
           with

-          | RId  a               => let case_RId := tt    in ga_id _ _ _ _ _
-          | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
-          | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
-          | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
-          | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
-          | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
-          | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
-          | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
-          | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _ 
-          | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _ 
-          | RLeft  a b c r'      => let case_RLeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
-          | RRight a b c r'      => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
-          | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
+          | AId  a               => let case_AId := tt    in ga_id _ _ _ _ _
+          | ACanL  a             => let case_ACanL := tt  in ga_uncancell _ _ _ _ _
+          | ACanR  a             => let case_ACanR := tt  in ga_uncancelr _ _ _ _ _
+          | AuCanL a             => let case_AuCanL := tt in ga_cancell _ _ _ _ _
+          | AuCanR a             => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
+          | AAssoc a b c         => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
+          | AuAssoc a b c         => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
+          | AExch  a b           => let case_AExch := tt  in ga_swap  _ _ _ _ _ _
+          | AWeak  a             => let case_AWeak := tt  in ga_drop _ _ _ _ _ 
+          | ACont  a             => let case_ACont := tt  in ga_copy  _ _ _ _ _ 
+          | ALeft  a b c r'      => let case_ALeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+          | ARight a b c r'      => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
+          | AComp  c b a r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)

         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 
         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 

-        destruct case_RComp.
+        destruct case_AComp.

           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.

-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].

           eapply nd_comp; [ idtac | eapply nd_rule; apply
              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           apply nd_prod.
           apply r2'.
           eapply nd_comp; [ idtac | eapply nd_rule; apply
              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           apply nd_prod.
           apply r2'.

-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].

           eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           eapply nd_prod.
           apply r1'.
           eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           eapply nd_prod.
           apply r1'.

-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

           apply ga_comp.
           Defined.
 
           apply ga_comp.
           Defined.
 

@@ -485,19 +485,19 @@ Section HaskFlattener.
         match r as R in Arrange A B return
           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
         match r as R in Arrange A B return
           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with

-          | RId  a               => let case_RId := tt  in RId _
-          | RCanL  a             => let case_RCanL := tt  in RCanL _
-          | RCanR  a             => let case_RCanR := tt  in RCanR _
-          | RuCanL a             => let case_RuCanL := tt in RuCanL _
-          | RuCanR a             => let case_RuCanR := tt in RuCanR _
-          | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
-          | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
-          | RExch  a b           => let case_RExch := tt  in RExch _ _
-          | RWeak  a             => let case_RWeak := tt  in RWeak _
-          | RCont  a             => let case_RCont := tt  in RCont _
-          | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (flatten _ _ r')
-          | RRight a b c r'      => let case_RRight := tt in RRight _ (flatten _ _ r')
-          | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (flatten _ _ r1) (flatten _ _ r2)
+          | AId  a               => let case_AId := tt  in AId _
+          | ACanL  a             => let case_ACanL := tt  in ACanL _
+          | ACanR  a             => let case_ACanR := tt  in ACanR _
+          | AuCanL a             => let case_AuCanL := tt in AuCanL _
+          | AuCanR a             => let case_AuCanR := tt in AuCanR _
+          | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
+          | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
+          | AExch  a b           => let case_AExch := tt  in AExch _ _
+          | AWeak  a             => let case_AWeak := tt  in AWeak _
+          | ACont  a             => let case_ACont := tt  in ACont _
+          | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (flatten _ _ r')
+          | ARight a b c r'      => let case_ARight := tt in ARight _ (flatten _ _ r')
+          | AComp  a b c r1 r2   => let case_AComp := tt  in AComp    (flatten _ _ r1) (flatten _ _ r2)

         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
         Defined.
 
         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
         Defined.
 

@@ -511,19 +511,19 @@ Section HaskFlattener.
       apply nd_rule.
       apply RArrange.
       induction r; simpl.
       apply nd_rule.
       apply RArrange.
       induction r; simpl.

-        apply RId.
-        apply RCanL.
-        apply RCanR.
-        apply RuCanL.
-        apply RuCanR.
-        apply RAssoc.
-        apply RCossa.
-        apply RExch.    (* TO DO: check for all-leaf trees here *)
-        apply RWeak.
-        apply RCont.
-        apply RLeft; auto.
-        apply RRight; auto.
-        eapply RComp; [ apply IHr1 | apply IHr2 ].
+        apply AId.
+        apply ACanL.
+        apply ACanR.
+        apply AuCanL.
+        apply AuCanR.
+        apply AAssoc.
+        apply AuAssoc.
+        apply AExch.    (* TO DO: check for all-leaf trees here *)
+        apply AWeak.
+        apply ACont.
+        apply ALeft; auto.
+        apply ARight; auto.
+        eapply AComp; [ apply IHr1 | apply IHr2 ].

 
       apply flatten_arrangement.
         apply r.
 
       apply flatten_arrangement.
         apply r.

@@ -546,11 +546,11 @@ Section HaskFlattener.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].

     eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply ga_uncancelr.
 
     eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply ga_uncancelr.
 

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

     eapply nd_comp; [ idtac | eapply precompose ].
     apply pfb.
     Defined.
     eapply nd_comp; [ idtac | eapply precompose ].
     apply pfb.
     Defined.

@@ -573,7 +573,7 @@ Section HaskFlattener.
     apply y.
     idtac.
     clear y q.
     apply y.
     idtac.
     clear y q.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].

     simpl.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
     simpl.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].

@@ -641,7 +641,7 @@ Section HaskFlattener.
     destruct s.
 
     simpl.
     destruct s.
 
     simpl.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].

     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     clear q''.
     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     clear q''.

@@ -649,8 +649,8 @@ Section HaskFlattener.
     apply nd_prod.
     apply nd_rule.
     apply RArrange.
     apply nd_prod.
     apply nd_rule.
     apply RArrange.

-    eapply RComp; [ idtac | apply RCanR ].
-    apply RLeft.
+    eapply AComp; [ idtac | apply ACanR ].
+    apply ALeft.

     apply (@arrangeCancelEmptyTree _ _ _ _ e).
    
     eapply nd_comp.
     apply (@arrangeCancelEmptyTree _ _ _ _ e).
    
     eapply nd_comp.

@@ -658,10 +658,10 @@ Section HaskFlattener.
       eapply (@RVar Γ Δ t nil).
     apply nd_rule.
       apply RArrange.
       eapply (@RVar Γ Δ t nil).
     apply nd_rule.
       apply RArrange.

-      eapply RComp.
-      apply RuCanR.
-      apply RLeft.
-      apply RWeak.
+      eapply AComp.
+      apply AuCanR.
+      apply ALeft.
+      apply AWeak.

 (*
     eapply decide_tree_empty.
 
 (*
     eapply decide_tree_empty.
 

@@ -685,15 +685,15 @@ Section HaskFlattener.
         simpl.
         apply nd_rule.
         apply RArrange.
         simpl.
         apply nd_rule.
         apply RArrange.

-        apply RLeft.
-        apply RWeak.
+        apply ALeft.
+        apply AWeak.

       simpl.
         apply nd_rule.
         unfold take_lev.
         simpl.
         apply RArrange.
       simpl.
         apply nd_rule.
         unfold take_lev.
         simpl.
         apply RArrange.

-        apply RLeft.
-        apply RWeak.
+        apply ALeft.
+        apply AWeak.

       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 *)
       Defined.
       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 *)
       Defined.

@@ -714,17 +714,17 @@ Section HaskFlattener.
     simpl.
     drop_simplify.
     simpl.
     simpl.
     drop_simplify.
     simpl.

-    apply RId.
+    apply AId.

     simpl.
     simpl.

-    apply RId.
-    eapply RComp; [ idtac | apply RCanL ].
-    eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
+    apply AId.
+    eapply AComp; [ idtac | apply ACanL ].
+    eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].

     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
     idtac.
     drop_simplify.
     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
     idtac.
     drop_simplify.

-    apply RRight.
+    apply ARight.

     apply IHt1.
     Defined.
 
     apply IHt1.
     Defined.
 

@@ -735,17 +735,17 @@ Section HaskFlattener.
     simpl.
     drop_simplify.
     simpl.
     simpl.
     drop_simplify.
     simpl.

-    apply RId.
+    apply AId.

     simpl.
     simpl.

-    apply RId.
-    eapply RComp; [ apply RuCanL | idtac ].
-    eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
+    apply AId.
+    eapply AComp; [ apply AuCanL | idtac ].
+    eapply AComp; [ eapply ARight; apply IHt1 | idtac ].

     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
     idtac.
     drop_simplify.
     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
     idtac.
     drop_simplify.

-    apply RLeft.
+    apply ALeft.

     apply IHt2.
     Defined.
 
     apply IHt2.
     Defined.
 

@@ -901,7 +901,7 @@ Section HaskFlattener.
         eapply nd_rule.
         eapply RArrange.
         simpl.
         eapply nd_rule.
         eapply RArrange.
         simpl.

-        apply RCanR.
+        apply ACanR.

       apply boost.
       simpl.
       apply ga_curry.
       apply boost.
       simpl.
       apply ga_curry.

@@ -967,8 +967,8 @@ Section HaskFlattener.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       apply nd_prod.
       apply nd_id.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       apply nd_prod.
       apply nd_id.

-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)].
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].

       apply precompose.
 
     destruct case_RWhere.
       apply precompose.
 
     destruct case_RWhere.

@@ -997,8 +997,8 @@ Section HaskFlattener.
       eapply nd_comp; [ idtac | eapply precompose' ].
       apply nd_rule.
       apply RArrange.
       eapply nd_comp; [ idtac | eapply precompose' ].
       apply nd_rule.
       apply RArrange.

-      apply RLeft.
-      apply RCanL.
+      apply ALeft.
+      apply ACanL.

 
     destruct case_RVoid.
       simpl.
 
     destruct case_RVoid.
       simpl.

@@ -1100,15 +1100,15 @@ Section HaskFlattener.
       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
       unfold empty_tree.
       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
       unfold empty_tree.

-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ].
-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].

       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
       eapply nd_comp; [ idtac | eapply arrange_brak ].
       unfold succ_host.
       unfold succ_guest.
       eapply nd_rule.
         eapply RArrange.
       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
       eapply nd_comp; [ idtac | eapply arrange_brak ].
       unfold succ_host.
       unfold succ_guest.
       eapply nd_rule.
         eapply RArrange.

-        apply RExch.
+        apply AExch.

       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 
     destruct case_SEsc.
       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 
     destruct case_SEsc.

@@ -1122,8 +1122,8 @@ Section HaskFlattener.
       take_simplify.
       drop_simplify.
       simpl.
       take_simplify.
       drop_simplify.
       simpl.

-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].

       simpl.
       rewrite take_lemma'.
       rewrite unlev_relev.
       simpl.
       rewrite take_lemma'.
       rewrite unlev_relev.

@@ -1139,15 +1139,15 @@ Section HaskFlattener.
       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
 
       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
 

-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].

       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; [ idtac | eapply boost ].
       induction x.
         apply ga_id.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; [ idtac | eapply boost ].
       induction x.
         apply ga_id.

-        eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].

         simpl.
         apply ga_join.
           apply IHx1.
         simpl.
         apply ga_join.
           apply IHx1.

diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v
index 8aba304..30a0ae8 100644 (file)
--- a/src/HaskProgrammingLanguage.v
+++ b/src/HaskProgrammingLanguage.v
@@ -73,10 +73,10 @@ Section HaskProgrammingLanguage.
       apply nd_id.
       eapply nd_rule.
       set (@org_fc) as ofc.
       apply nd_id.
       eapply nd_rule.
       set (@org_fc) as ofc.

-      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
-      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
+      set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule.
+      apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])).

       auto.
       auto.

-      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
+      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ].

       apply nd_rule.
       destruct l.
       destruct l0.
       apply nd_rule.
       destruct l.
       destruct l0.

@@ -148,23 +148,23 @@ Section HaskProgrammingLanguage.
   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
     (*
     intros; apply nd_rule. simpl.
   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
     (*
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))).

       auto.
 
     intros; apply nd_rule. simpl.
       auto.
 
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.

 
     intros; apply nd_rule. simpl.
 
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.

 
     intros; apply nd_rule. simpl.
 
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.

 
     intros; apply nd_rule. simpl.
 
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.

 
     intros; apply nd_rule. simpl.
 
     intros; apply nd_rule. simpl.

-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.

       *)
       admit.
       admit.
       *)
       admit.
       admit.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index c887b8a..9787c62 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -67,7 +67,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l,   Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂       @l ]
 
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l,   Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂       @l ]
 

-(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)

 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l])  [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l])  [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 9d88e79..99af119 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -160,19 +160,19 @@ Instance ToLatexMathJudgment : ToLatexMath Judg :=
 
 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
   match r with
 
 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
   match r with

-    | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
-    | RRight  _ _ _ r => nd_uruleToRawLatexMath r
-    | RId     _     => "Id"
-    | RCanL   _     => "CanL"
-    | RCanR   _     => "CanR"
-    | RuCanL  _     => "uCanL"
-    | RuCanR  _     => "uCanR"
-    | RAssoc  _ _ _ => "Assoc"
-    | RCossa  _ _ _ => "Cossa"
-    | RExch   _ _   => "Exch"
-    | RWeak   _     => "Weak"
-    | RCont   _     => "Cont"
-    | RComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)
+    | ALeft   _ _ _ r => nd_uruleToRawLatexMath r
+    | ARight  _ _ _ r => nd_uruleToRawLatexMath r
+    | AId     _     => "Id"
+    | ACanL   _     => "CanL"
+    | ACanR   _     => "CanR"
+    | AuCanL  _     => "uCanL"
+    | AuCanR  _     => "uCanR"
+    | AAssoc  _ _ _ => "Assoc"
+    | AuAssoc  _ _ _ => "Cossa"
+    | AExch   _ _   => "Exch"
+    | AWeak   _     => "Weak"
+    | ACont   _     => "Cont"
+    | AComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)

   end.
 
 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
   end.
 
 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=

@@ -201,19 +201,19 @@ end.
 
 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
   match r with
 
 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
   match r with

-    | RLeft   _ _ _ r             => nd_hideURule r
-    | RRight  _ _ _ r             => nd_hideURule r
-    | RCanL   _                   => true
-    | RCanR   _                   => true
-    | RuCanL  _                   => true
-    | RuCanR  _                   => true
-    | RAssoc  _ _ _               => true
-    | RCossa  _ _ _               => true
-    | RExch      (T_Leaf None) b  => true
-    | RExch   a  (T_Leaf None)    => true
-    | RWeak      (T_Leaf None)    => true
-    | RCont      (T_Leaf None)    => true
-    | RComp   _ _ _ _ _           => false   (* FIXME: do better *)
+    | ALeft   _ _ _ r             => nd_hideURule r
+    | ARight  _ _ _ r             => nd_hideURule r
+    | ACanL   _                   => true
+    | ACanR   _                   => true
+    | AuCanL  _                   => true
+    | AuCanR  _                   => true
+    | AAssoc  _ _ _               => true
+    | AuAssoc  _ _ _               => true
+    | AExch      (T_Leaf None) b  => true
+    | AExch   a  (T_Leaf None)    => true
+    | AWeak      (T_Leaf None)    => true
+    | ACont      (T_Leaf None)    => true
+    | AComp   _ _ _ _ _           => false   (* FIXME: do better *)

     | _                           => false
   end.
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
     | _                           => false
   end.
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index e70322e..299a83b 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -238,49 +238,49 @@ Section HaskProofToStrong.
     ujudg2exprType Γ ξ Δ H t l ->
     ujudg2exprType Γ ξ Δ C t l
  with
     ujudg2exprType Γ ξ Δ H t l ->
     ujudg2exprType Γ ξ Δ C t l
  with

-          | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RId     a       => let case_RId    := tt in _
-          | RCanL   a       => let case_RCanL  := tt in _
-          | RCanR   a       => let case_RCanR  := tt in _
-          | RuCanL  a       => let case_RuCanL := tt in _
-          | RuCanR  a       => let case_RuCanR := tt in _
-          | RAssoc  a b c   => let case_RAssoc := tt in _
-          | RCossa  a b c   => let case_RCossa := tt in _
-          | RExch   a b     => let case_RExch  := tt in _
-          | RWeak   a       => let case_RWeak  := tt in _
-          | RCont   a       => let case_RCont  := tt in _
-          | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
+          | ALeft   h c ctx r => let case_ALeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | ARight  h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | AId     a       => let case_AId    := tt in _
+          | ACanL   a       => let case_ACanL  := tt in _
+          | ACanR   a       => let case_ACanR  := tt in _
+          | AuCanL  a       => let case_AuCanL := tt in _
+          | AuCanR  a       => let case_AuCanR := tt in _
+          | AAssoc  a b c   => let case_AAssoc := tt in _
+          | AuAssoc  a b c   => let case_AuAssoc := tt in _
+          | AExch   a b     => let case_AExch  := tt in _
+          | AWeak   a       => let case_AWeak  := tt in _
+          | ACont   a       => let case_ACont  := tt in _
+          | AComp   a b c f g => let case_AComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)

           end); clear urule2expr; intros.
 
           end); clear urule2expr; intros.
 

-      destruct case_RId.
+      destruct case_AId.

         apply X.
 
         apply X.
 

-      destruct case_RCanL.
+      destruct case_ACanL.

         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X ([],,vars)).
         simpl; rewrite <- H; auto.
 
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X ([],,vars)).
         simpl; rewrite <- H; auto.
 

-      destruct case_RCanR.
+      destruct case_ACanR.

         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X (vars,,[])).
         simpl; rewrite <- H; auto.
 
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X (vars,,[])).
         simpl; rewrite <- H; auto.
 

-      destruct case_RuCanL.
+      destruct case_AuCanL.

         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars2); auto.
 
         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars2); auto.
 

-      destruct case_RuCanR.
+      destruct case_AuCanR.

         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars1); auto.
 
         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars1); auto.
 

-      destruct case_RAssoc.
+      destruct case_AAssoc.

         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.

@@ -288,7 +288,7 @@ Section HaskProofToStrong.
         apply (X (vars1_1,,(vars1_2,,vars2))).
         subst; auto.
 
         apply (X (vars1_1,,(vars1_2,,vars2))).
         subst; auto.
 

-      destruct case_RCossa.
+      destruct case_AuAssoc.

         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.

@@ -296,20 +296,20 @@ Section HaskProofToStrong.
         apply (X ((vars1,,vars2_1),,vars2_2)).
         subst; auto.
 
         apply (X ((vars1,,vars2_1),,vars2_2)).
         subst; auto.
 

-      destruct case_RExch.
+      destruct case_AExch.

         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
         apply (X (vars2,,vars1)).
         inversion H; subst; auto.
         
         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
         apply (X (vars2,,vars1)).
         inversion H; subst; auto.
         

-      destruct case_RWeak.
+      destruct case_AWeak.

         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X []).
         auto.
         
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X []).
         auto.
         

-      destruct case_RCont.
+      destruct case_ACont.

         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         apply (X (vars,,vars)).
         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         apply (X (vars,,vars)).

@@ -317,7 +317,7 @@ Section HaskProofToStrong.
         rewrite <- H.
         auto.
 
         rewrite <- H.
         auto.
 

-      destruct case_RLeft.
+      destruct case_ALeft.

         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars2 H2).
         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars2 H2).

@@ -332,7 +332,7 @@ Section HaskProofToStrong.
           simpl.
           reflexivity.
 
           simpl.
           reflexivity.
 

-      destruct case_RRight.
+      destruct case_ARight.

         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars1 H1).
         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars1 H1).

@@ -347,7 +347,7 @@ Section HaskProofToStrong.
           simpl.
           reflexivity.
 
           simpl.
           reflexivity.
 

-      destruct case_RComp.
+      destruct case_AComp.

         apply e2.
         apply e1.
         apply X.
         apply e2.
         apply e1.
         apply X.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 76e1bdb..259d24e 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -125,14 +125,14 @@ Section HaskSkolemizer.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.

-      apply RId.
+      apply AId.

     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).

-      apply RCanR.
+      apply ACanR.

         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").

@@ -146,14 +146,14 @@ Section HaskSkolemizer.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.

-      apply RId.
+      apply AId.

     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).

-      apply RuCanR.
+      apply AuCanR.

         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").

@@ -251,7 +251,7 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RArrange.
         apply nd_rule.
         apply SFlat.
         apply RArrange.

-        apply RRight.
+        apply ARight.

         apply d.
 
       destruct case_RBrak.
         apply d.
 
       destruct case_RBrak.

@@ -288,7 +288,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].

         apply nd_rule.
         apply SFlat.
         apply RLit.
         apply nd_rule.
         apply SFlat.
         apply RLit.

@@ -303,7 +303,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].

         apply nd_rule.
         apply SFlat.
         apply RVar.
         apply nd_rule.
         apply SFlat.
         apply RVar.

@@ -318,7 +318,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
         rewrite H.
         rewrite H0.
         simpl.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].

         apply nd_rule.
         apply SFlat.
         apply RGlobal.
         apply nd_rule.
         apply SFlat.
         apply RGlobal.

@@ -334,9 +334,9 @@ Section HaskSkolemizer.
         apply nd_rule.
           apply SFlat.
           apply RArrange.
         apply nd_rule.
           apply SFlat.
           apply RArrange.

-          eapply RComp.
-          eapply RCossa.
-          eapply RLeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.

           apply take_arrange.
 
       destruct case_RCast.
           apply take_arrange.
 
       destruct case_RCast.

@@ -370,14 +370,14 @@ Section HaskSkolemizer.
         rewrite H0.
         simpl.
         eapply nd_comp.
         rewrite H0.
         simpl.
         eapply nd_comp.

-        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
+        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].

         eapply nd_rule.
         eapply SFlat.
         eapply RArrange.
         eapply nd_rule.
         eapply SFlat.
         eapply RArrange.

-        eapply RLeft.
+        eapply ALeft.

         eapply take_unarrange.
 
         eapply take_unarrange.
 

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].

         eapply nd_rule; eapply SFlat; apply RWhere.
 
       destruct case_RLet.
         eapply nd_rule; eapply SFlat; apply RWhere.
 
       destruct case_RLet.

@@ -393,17 +393,17 @@ Section HaskSkolemizer.
         rewrite H0.
 
         eapply nd_comp.
         rewrite H0.
 
         eapply nd_comp.

-        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
+        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].

 
         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
 
         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].

         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
         apply nd_prod.
           apply nd_id.
           apply nd_rule.
           eapply SFlat.
           eapply RArrange.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
         apply nd_prod.
           apply nd_id.
           apply nd_rule.
           eapply SFlat.
           eapply RArrange.

-          eapply RCossa.
+          eapply AuAssoc.

 
       destruct case_RWhere.
         simpl.
 
       destruct case_RWhere.
         simpl.

@@ -418,16 +418,16 @@ Section HaskSkolemizer.
         rewrite H0.
 
         eapply nd_comp.
         rewrite H0.
 
         eapply nd_comp.

-        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
+        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].

         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
         apply nd_prod; [ idtac | eapply nd_id ].
         eapply nd_rule; apply SFlat; eapply RArrange.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
         apply nd_prod; [ idtac | eapply nd_id ].
         eapply nd_rule; apply SFlat; eapply RArrange.

-        eapply RComp.
-        eapply RCossa.
-        apply RLeft.
-        eapply RCossa.
+        eapply AComp.
+        eapply AuAssoc.
+        apply ALeft.
+        eapply AuAssoc.

 
       destruct case_RVoid.
         simpl.
 
       destruct case_RVoid.
         simpl.

@@ -435,7 +435,7 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RVoid.
         apply nd_rule.
         apply SFlat.
         apply RVoid.

-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].

         apply nd_rule.
         apply SFlat.
         apply RVoid.
         apply nd_rule.
         apply SFlat.
         apply RVoid.

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8aa4005..1b9f6af 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -621,16 +621,16 @@ Definition factorContextLeft
             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply RuCanR.
+              apply AuCanR.

 
             (* where the leaf is NOT v *)
             apply inl.
 
             (* where the leaf is NOT v *)
             apply inl.

-              apply RuCanL.
+              apply AuCanL.

   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.

-          apply RuCanR.
+          apply AuCanR.

   
       (* branch *)
       refine (
   
       (* branch *)
       refine (

@@ -650,45 +650,45 @@ Definition factorContextLeft
     destruct case_Neither.
       apply inl.
       simpl.
     destruct case_Neither.
       apply inl.
       simpl.

-      eapply RComp; [idtac | apply RuCanL ].
-        exact (RComp
+      eapply AComp; [idtac | apply AuCanL ].
+        exact (AComp

           (* order will not matter because these are central as morphisms *)
           (* order will not matter because these are central as morphisms *)

-          (RRight _ (RComp lpf (RCanL _)))
-          (RLeft  _ (RComp rpf (RCanL _)))).
+          (ARight _ (AComp lpf (ACanL _)))
+          (ALeft  _ (AComp rpf (ACanL _)))).

 
     destruct case_Right.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
 
     destruct case_Right.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply RComp; [ idtac | eapply pivotContext' ].
-      eapply RComp.
-      eapply RRight.
-      eapply RComp.
+      eapply AComp; [ idtac | eapply pivotContext' ].
+      eapply AComp.
+      eapply ARight.
+      eapply AComp.

       apply lpf.
       apply lpf.

-      apply RCanL.
-      eapply RLeft.
+      apply ACanL.
+      eapply ALeft.

       apply rpf.
 
     destruct case_Left.
       apply inr.
       fold (stripOutVars (v::nil)).
       simpl.
       apply rpf.
 
     destruct case_Left.
       apply inr.
       fold (stripOutVars (v::nil)).
       simpl.

-      eapply RComp.
-      eapply RLeft.
-      eapply RComp.
+      eapply AComp.
+      eapply ALeft.
+      eapply AComp.

       apply rpf.
       simpl.
       apply rpf.
       simpl.

-      eapply RCanL.
-      eapply RComp; [ idtac | eapply RCossa ].
-      eapply RRight.
+      eapply ACanL.
+      eapply AComp; [ idtac | eapply AuAssoc ].
+      eapply ARight.

       apply lpf.
 
     destruct case_Both.
       apply inr.
       simpl.
       apply lpf.
 
     destruct case_Both.
       apply inr.
       simpl.

-      eapply RComp; [ idtac | eapply RRight; eapply RCont ].
-      eapply RComp; [ eapply RRight; eapply lpf | idtac ].
-      eapply RComp; [ eapply RLeft; eapply rpf | idtac ].
+      eapply AComp; [ idtac | eapply ARight; eapply ACont ].
+      eapply AComp; [ eapply ARight; eapply lpf | idtac ].
+      eapply AComp; [ eapply ALeft; eapply rpf | idtac ].

       clear lpf rpf.
       simpl.
       apply arrangeSwapMiddle.
       clear lpf rpf.
       simpl.
       apply arrangeSwapMiddle.

@@ -726,16 +726,16 @@ Definition factorContextRight
             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply RuCanL.
+              apply AuCanL.

 
             (* where the leaf is NOT v *)
             apply inl.
 
             (* where the leaf is NOT v *)
             apply inl.

-              apply RuCanR.
+              apply AuCanR.

   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.

-          apply RuCanR.
+          apply AuCanR.

   
       (* branch *)
       refine (
   
       (* branch *)
       refine (

@@ -754,51 +754,51 @@ Definition factorContextRight
 
     destruct case_Neither.
       apply inl.
 
     destruct case_Neither.
       apply inl.

-      eapply RComp; [idtac | apply RuCanR ].
-        exact (RComp
+      eapply AComp; [idtac | apply AuCanR ].
+        exact (AComp

           (* order will not matter because these are central as morphisms *)
           (* order will not matter because these are central as morphisms *)

-          (RRight _ (RComp lpf (RCanR _)))
-          (RLeft  _ (RComp rpf (RCanR _)))).
+          (ARight _ (AComp lpf (ACanR _)))
+          (ALeft  _ (AComp rpf (ACanR _)))).

 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).
 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).

-      set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.
+      set (ARight (mapOptionTree ξ ctx2)  (AComp lpf ((ACanR _)))) as q.

       simpl in *.
       simpl in *.

-      eapply RComp.
+      eapply AComp.

       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.

-      eapply RComp; [ idtac | apply RAssoc ].
-      apply RLeft.
+      eapply AComp; [ idtac | apply AAssoc ].
+      apply ALeft.

       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply RComp; [ idtac | eapply pivotContext ].
-      set (RComp rpf (RCanR _ )) as rpf'.
-      set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
+      eapply AComp; [ idtac | eapply pivotContext ].
+      set (AComp rpf (ACanR _ )) as rpf'.
+      set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.

       simpl in *.
       simpl in *.

-      eapply RComp; [ idtac | apply qq ].
+      eapply AComp; [ idtac | apply qq ].

       clear qq rpf' rpf.
       clear qq rpf' rpf.

-      apply (RRight (mapOptionTree ξ ctx2)).
+      apply (ARight (mapOptionTree ξ ctx2)).

       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply RComp; [ idtac | eapply copyAndPivotContext ].
+      eapply AComp; [ idtac | eapply copyAndPivotContext ].

         (* order will not matter because these are central as morphisms *)
         (* order will not matter because these are central as morphisms *)

-        exact (RComp (RRight _ lpf) (RLeft _ rpf)).
+        exact (AComp (ARight _ lpf) (ALeft _ rpf)).

 
     Defined.
 
 
     Defined.
 

-(* same as before, but use RWeak if necessary *)
+(* same as before, but use AWeak if necessary *)

 Definition factorContextLeftAndWeaken  
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
 Definition factorContextLeftAndWeaken  
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)

@@ -809,8 +809,8 @@ Definition factorContextLeftAndWeaken
           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
   set (factorContextLeft Γ Δ v ctx ξ) as q.
   destruct q; auto.
           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
   set (factorContextLeft Γ Δ v ctx ξ) as q.
   destruct q; auto.

-  eapply RComp; [ apply a | idtac ].
-  refine (RRight _ (RWeak _)).
+  eapply AComp; [ apply a | idtac ].
+  refine (ARight _ (AWeak _)).

   Defined.
 
 Definition factorContextLeftAndWeaken''
   Defined.
 
 Definition factorContextLeftAndWeaken''

@@ -836,7 +836,7 @@ Definition factorContextLeftAndWeaken''
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.

-    apply RuCanL.
+    apply AuCanL.

     intros.
     unfold mapOptionTree in *.
     simpl in *.
     intros.
     unfold mapOptionTree in *.
     simpl in *.

@@ -855,15 +855,15 @@ Definition factorContextLeftAndWeaken''
       unfold stripOutVars in q.
       rewrite q in IHv1'.
       clear q.
       unfold stripOutVars in q.
       rewrite q in IHv1'.
       clear q.

-    eapply RComp; [ idtac | eapply RAssoc ].
-    eapply RComp; [ idtac | eapply IHv1' ].
+    eapply AComp; [ idtac | eapply AAssoc ].
+    eapply AComp; [ idtac | eapply IHv1' ].

     clear IHv1'.
     apply IHv2; auto.
     auto.
     auto.
     Defined.
 
     clear IHv1'.
     apply IHv2; auto.
     auto.
     auto.
     Defined.
 

-(* same as before, but use RWeak if necessary *)
+(* same as before, but use AWeak if necessary *)

 Definition factorContextRightAndWeaken  
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
 Definition factorContextRightAndWeaken  
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)

@@ -874,8 +874,8 @@ Definition factorContextRightAndWeaken
           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
   set (factorContextRight Γ Δ v ctx ξ) as q.
   destruct q; auto.
           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
   set (factorContextRight Γ Δ v ctx ξ) as q.
   destruct q; auto.

-  eapply RComp; [ apply a | idtac ].
-  refine (RLeft _ (RWeak _)).
+  eapply AComp; [ apply a | idtac ].
+  refine (ALeft _ (AWeak _)).

   Defined.
 
 Definition factorContextRightAndWeaken''
   Defined.
 
 Definition factorContextRightAndWeaken''

@@ -899,7 +899,7 @@ Definition factorContextRightAndWeaken''
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.

-    apply RuCanR.
+    apply AuCanR.

     intros.
     unfold mapOptionTree in *.
     simpl in *.
     intros.
     unfold mapOptionTree in *.
     simpl in *.

@@ -918,14 +918,14 @@ Definition factorContextRightAndWeaken''
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].

-    set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
-    eapply RComp.
+    set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
+    eapply AComp.

       apply qq.
       clear qq IHv2' IHv2 IHv1.
       rewrite strip_swap_lemma.
       rewrite strip_twice_lemma.
       rewrite (notin_strip_inert' v1 (leaves v2)).
       apply qq.
       clear qq IHv2' IHv2 IHv1.
       rewrite strip_swap_lemma.
       rewrite strip_twice_lemma.
       rewrite (notin_strip_inert' v1 (leaves v2)).

-        apply RCossa.
+        apply AuAssoc.

         apply distinct_swap.
         auto.
     Defined.
         apply distinct_swap.
         auto.
     Defined.

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 670d8bd..077f7b5 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -108,4 +108,4 @@ Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
   (* un-letrec-ify multi branch letrecs *)
   | WELetRec mlr e                       => WELetRec mlr (simplifyWeakExpr e )
   end.
   (* un-letrec-ify multi branch letrecs *)
   | WELetRec mlr e                       => WELetRec mlr (simplifyWeakExpr e )
   end.

-*)
\ No newline at end of file
+*)

diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v
index 03fc704..57dfdb8 100644 (file)
--- a/src/NaturalDeductionContext.v
+++ b/src/NaturalDeductionContext.v
@@ -14,19 +14,19 @@ Section NaturalDeductionContext.
 
   (* Figure 3, production $\vdash_E$, Uniform rules *)
   Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
 
   (* Figure 3, production $\vdash_E$, Uniform rules *)
   Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=

-  | RId     : forall a        ,                Arrange           a                  a
-  | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
-  | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
-  | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
-  | RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
-  | RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
-  | RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
-  | RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
-  | RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
-  | RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
-  | RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
-  | RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
-  | RComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
+  | AId     : forall a        ,                Arrange           a                  a
+  | ACanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
+  | ACanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
+  | AuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
+  | AuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
+  | AAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
+  | AuAssoc  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
+  | AExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
+  | AWeak   : forall a        ,                Arrange  (       []   )      (       a   )
+  | ACont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
+  | ALeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
+  | ARight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
+  | AComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c

   .
   
   (* "Arrange" objects are parametric in the type of the leaves of the tree *)
   .
   
   (* "Arrange" objects are parametric in the type of the leaves of the tree *)

@@ -36,51 +36,51 @@ Section NaturalDeductionContext.
       Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
     intros.
     induction X; simpl.
       Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
     intros.
     induction X; simpl.

-    apply RId.
-    apply RCanL.
-    apply RCanR.
-    apply RuCanL.
-    apply RuCanR.
-    apply RAssoc.
-    apply RCossa.
-    apply RExch.
-    apply RWeak.
-    apply RCont.
-    apply RLeft; auto.
-    apply RRight; auto.
-    eapply RComp; [ apply IHX1 | apply IHX2 ].
+    apply AId.
+    apply ACanL.
+    apply ACanR.
+    apply AuCanL.
+    apply AuCanR.
+    apply AAssoc.
+    apply AuAssoc.
+    apply AExch.
+    apply AWeak.
+    apply ACont.
+    apply ALeft; auto.
+    apply ARight; auto.
+    eapply AComp; [ apply IHX1 | apply IHX2 ].

     Defined.
   
   (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *)
   Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
     Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
     Defined.
   
   (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *)
   Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
     Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).

-    eapply RComp.
-    apply RCossa.
-    eapply RComp.
-    eapply RLeft.
-    eapply RComp.
-    eapply RAssoc.
-    eapply RRight.
-    apply RExch.
-    eapply RComp.
-    eapply RLeft.
-    eapply RCossa.
-    eapply RAssoc.
+    eapply AComp.
+    apply AuAssoc.
+    eapply AComp.
+    eapply ALeft.
+    eapply AComp.
+    eapply AAssoc.
+    eapply ARight.
+    apply AExch.
+    eapply AComp.
+    eapply ALeft.
+    eapply AuAssoc.
+    eapply AAssoc.

     Defined.
 
     Defined.
 

-  (* like RExch, but works on nodes which are an Assoc away from being adjacent *)
+  (* like AExch, but works on nodes which are an Assoc away from being adjacent *)

   Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
   Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=

-    RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+    AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _).

 
 

-  (* like RExch, but works on nodes which are an Assoc away from being adjacent *)  
+  (* like AExch, but works on nodes which are an Assoc away from being adjacent *)  

   Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
   Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=

-    RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
+    AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _).

   
   Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
   
   Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).

-    eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
-    eapply RComp; [ idtac | apply RCossa ]. 
-    eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
-    apply RAssoc.
+    eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ].
+    eapply AComp; [ idtac | apply AuAssoc ]. 
+    eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ].
+    apply AAssoc.

     Defined.
 
   (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
     Defined.
 
   (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)

@@ -93,16 +93,16 @@ Section NaturalDeductionContext.
       destruct a.
       simpl.
       destruct (f t); simpl.
       destruct a.
       simpl.
       destruct (f t); simpl.

-      apply RuCanL.
-      apply RuCanR.
+      apply AuCanL.
+      apply AuCanR.

       simpl.
       simpl.

-      apply RuCanL.
+      apply AuCanL.

       simpl in *.
       simpl in *.

-      eapply RComp; [ idtac | apply arrangeSwapMiddle ].
-      eapply RComp.
-      eapply RLeft.
+      eapply AComp; [ idtac | apply arrangeSwapMiddle ].
+      eapply AComp.
+      eapply ALeft.

       apply IHΣ2.
       apply IHΣ2.

-      eapply RRight.
+      eapply ARight.

       apply IHΣ1.
       Defined.
 
       apply IHΣ1.
       Defined.
 

@@ -116,16 +116,16 @@ Section NaturalDeductionContext.
       destruct a.
       simpl.
       destruct (f t); simpl.
       destruct a.
       simpl.
       destruct (f t); simpl.

-      apply RCanL.
-      apply RCanR.
+      apply ACanL.
+      apply ACanR.

       simpl.
       simpl.

-      apply RCanL.
+      apply ACanL.

       simpl in *.
       simpl in *.

-      eapply RComp; [ apply arrangeSwapMiddle | idtac ].
-      eapply RComp.
-      eapply RLeft.
+      eapply AComp; [ apply arrangeSwapMiddle | idtac ].
+      eapply AComp.
+      eapply ALeft.

       apply IHΣ2.
       apply IHΣ2.

-      eapply RRight.
+      eapply ARight.

       apply IHΣ1.
       Defined.
 
       apply IHΣ1.
       Defined.
 

@@ -164,17 +164,17 @@ Section NaturalDeductionContext.
     induction q; intros.
       simpl in H.
       rewrite H.
     induction q; intros.
       simpl in H.
       rewrite H.

-      apply RId.
+      apply AId.

     simpl in *.
     destruct t; try destruct o; inversion H.
       set (IHq1 _ H1) as x1.
       set (IHq2 _ H2) as x2.
     simpl in *.
     destruct t; try destruct o; inversion H.
       set (IHq1 _ H1) as x1.
       set (IHq2 _ H2) as x2.

-      eapply RComp.
-        eapply RRight.
+      eapply AComp.
+        eapply ARight.

         rewrite <- H1.
         apply x1.
         rewrite <- H1.
         apply x1.

-      eapply RComp.
-        apply RCanL.
+      eapply AComp.
+        apply ACanL.

         rewrite <- H2.
         apply x2.
       Defined.
         rewrite <- H2.
         apply x2.
       Defined.

@@ -187,21 +187,21 @@ Section NaturalDeductionContext.
     induction q; intros.
       simpl in H.
       rewrite H.
     induction q; intros.
       simpl in H.
       rewrite H.

-      apply RId.
+      apply AId.

     simpl in *.
     destruct t; try destruct o; inversion H.
       set (IHq1 _ H1) as x1.
       set (IHq2 _ H2) as x2.
     simpl in *.
     destruct t; try destruct o; inversion H.
       set (IHq1 _ H1) as x1.
       set (IHq2 _ H2) as x2.

-      eapply RComp.
-        apply RuCanL.
-      eapply RComp.
-        eapply RRight.
+      eapply AComp.
+        apply AuCanL.
+      eapply AComp.
+        eapply ARight.

         apply x1.
         apply x1.

-      eapply RComp.
-        eapply RLeft.
+      eapply AComp.
+        eapply ALeft.

         apply x2.
       rewrite H.
         apply x2.
       rewrite H.

-      apply RId.
+      apply AId.

       Defined.
 
   (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
       Defined.
 
   (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)

@@ -210,38 +210,38 @@ Section NaturalDeductionContext.
 
     refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
       match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with
 
     refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
       match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with

-        | RId  a               => let case_RId := tt    in RId _
-        | RCanL  a             => let case_RCanL := tt  in _
-        | RCanR  a             => let case_RCanR := tt  in _
-        | RuCanL a             => let case_RuCanL := tt in _
-        | RuCanR a             => let case_RuCanR := tt in _
-        | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
-        | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
-        | RExch  a b           => let case_RExch := tt  in RExch _ _
-        | RWeak  a             => let case_RWeak := tt  in _
-        | RCont  a             => let case_RCont := tt  in _
-        | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (arrangeTake _ _ r')
-        | RRight a b c r'      => let case_RRight := tt in RRight _ (arrangeTake _ _ r')
-        | RComp  a b c r1 r2   => let case_RComp := tt  in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
+        | AId  a               => let case_AId := tt    in AId _
+        | ACanL  a             => let case_ACanL := tt  in _
+        | ACanR  a             => let case_ACanR := tt  in _
+        | AuCanL a             => let case_AuCanL := tt in _
+        | AuCanR a             => let case_AuCanR := tt in _
+        | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
+        | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
+        | AExch  a b           => let case_AExch := tt  in AExch _ _
+        | AWeak  a             => let case_AWeak := tt  in _
+        | ACont  a             => let case_ACont := tt  in _
+        | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (arrangeTake _ _ r')
+        | ARight a b c r'      => let case_ARight := tt in ARight _ (arrangeTake _ _ r')
+        | AComp  a b c r1 r2   => let case_AComp := tt  in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)

       end)); clear arrangeTake; intros.
 
       end)); clear arrangeTake; intros.
 

-    destruct case_RCanL.
-      simpl; destruct (pred None); simpl; apply RCanL.
+    destruct case_ACanL.
+      simpl; destruct (pred None); simpl; apply ACanL.

 
 

-    destruct case_RCanR.
-      simpl; destruct (pred None); simpl; apply RCanR.
+    destruct case_ACanR.
+      simpl; destruct (pred None); simpl; apply ACanR.

 
 

-    destruct case_RuCanL.
-      simpl; destruct (pred None); simpl; apply RuCanL.
+    destruct case_AuCanL.
+      simpl; destruct (pred None); simpl; apply AuCanL.

 
 

-    destruct case_RuCanR.
-      simpl; destruct (pred None); simpl; apply RuCanR.
+    destruct case_AuCanR.
+      simpl; destruct (pred None); simpl; apply AuCanR.

 
 

-    destruct case_RWeak.
-      simpl; destruct (pred None); simpl; apply RWeak.
+    destruct case_AWeak.
+      simpl; destruct (pred None); simpl; apply AWeak.

 
 

-    destruct case_RCont.
-      simpl; destruct (pred None); simpl; apply RCont.
+    destruct case_ACont.
+      simpl; destruct (pred None); simpl; apply ACont.

 
       Defined.
 
 
       Defined.
 

diff --git a/src/PCF.v b/src/PCF.v
index 5caf2dc..373519b 100644 (file)
--- a/src/PCF.v
+++ b/src/PCF.v
@@ -183,8 +183,8 @@ Section PCF.
       eapply nd_prod.
       apply nd_id.
       apply (PCF_Arrange [h] ([],,[h]) [h0]).
       eapply nd_prod.
       apply nd_id.
       apply (PCF_Arrange [h] ([],,[h]) [h0]).

-      apply RuCanL.
-      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
+      apply AuCanL.
+      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].

       apply nd_rule.
       (*
       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
       apply nd_rule.
       (*
       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.

@@ -241,27 +241,27 @@ Section PCF.
   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 
     intros; apply nd_rule. unfold PCFRule. simpl.
   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
+      exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).

       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
       apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
+      exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).

       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
       apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RCanL _)).
+      exists (RArrange _ _ _ _ _ (ACanL _)).

       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
       apply (PCF_RArrange _ _ lev ([],,a) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RCanR _)).
+      exists (RArrange _ _ _ _ _ (ACanR _)).

       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
       apply (PCF_RArrange _ _ lev (a,,[]) _ _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RuCanL _)).
+      exists (RArrange _ _ _ _ _ (AuCanL _)).

       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.
       apply (PCF_RArrange _ _ lev _ ([],,a) _).
 
     intros; apply nd_rule. unfold PCFRule. simpl.

-      exists (RArrange _ _ _ _ _ (RuCanR _)).
+      exists (RArrange _ _ _ _ _ (AuCanR _)).

       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
       Defined.
 
       apply (PCF_RArrange _ _ lev _ (a,,[]) _).
       Defined.