add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer
authorAdam Megacz <megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:55:29 +0000 (20:55 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Thu, 26 May 2011 03:55:29 +0000 (20:55 -0700)
examples/Demo.hs
src/ExtractionMain.v
src/HaskFlattener.v
src/HaskProof.v
src/HaskProofToLatex.v
src/HaskProofToStrong.v
src/HaskSkolemizer.v
src/HaskStrongToProof.v

index 4e7f599..afedde6 100644 (file)
@@ -1,13 +1,23 @@
 {-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-}
 module Demo (demo) where
 
-demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]>
+--demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]>
 
 -- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]>
 
---demo const mult =
--- <[ let twelve = ~~(const (12::Int))
---    in  ~~mult (~~mult twelve twelve) (~~mult twelve twelve) ]>
+demo const mult =
+ <[ let     twelve = ~~(const (12::Int))
+    in let  four    = ~~(const (4::Int))
+         in  ~~mult four twelve  ]>
+
+{-
+demo const mult =
+ <[ let     twelve = ~~(const (12::Int))
+    in let  twelvea = twelve
+            four    = ~~(const (4::Int))
+            twelveb = twelve
+         in  ~~mult (~~mult twelvea four) (~~mult twelveb twelveb) ]>
+-}
 
 {-
 demo const mult = demo' 3
index 5be5280..6364a5a 100644 (file)
@@ -235,14 +235,14 @@ Section core2proof.
   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
-       [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
+       [ Γ > Δ > [a @@ lev],,Σ |-       [ s @@ lev ] ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
+    apply nd_id.
     apply nd_rule.
     apply RVar.
-    apply nd_id.
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
@@ -251,13 +251,13 @@ Section core2proof.
     intro pf.
     eapply nd_comp.
     apply pf.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
     apply curry.
     Defined.
 
   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
-    ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
+    ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                  [ s @@ lev ] ].
     intro pf.
     eapply nd_comp.
     eapply pf.
@@ -267,7 +267,8 @@ Section core2proof.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
-    eapply RCanL.
+    eapply RCanR.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
     apply curry.
     Defined.
 
index a5f4261..308e669 100644 (file)
@@ -371,8 +371,8 @@ Section HaskFlattener.
     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 RCanL ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -380,141 +380,117 @@ Section HaskFlattener.
       apply X.
       eapply nd_rule.
       eapply RArrange.
-      apply RuCanL.
-      Defined.
-
-  Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
-     ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
-     intros.
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
-     eapply nd_comp; [ idtac
-       | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
-     eapply nd_comp; [ apply nd_llecnac | idtac ].
-     apply nd_prod.
-     apply X.
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
-     apply ga_comp.
-     Defined.
+      apply RuCanR.
+    Defined.
 
   Definition precompose Γ Δ ec : forall a x y z lev,
     ND Rule
       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
     intros.
-    eapply nd_comp.
-    apply nd_rlecnac.
-    eapply nd_comp.
-    eapply nd_prod.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
     apply nd_id.
-    eapply ga_comp.
-
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
-
-    apply nd_rule.
-    apply RLet.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    apply ga_comp.
     Defined.
 
-  Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
-     ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
-     intros.
-     eapply nd_comp.
-     apply X.
-     apply precompose.
-     Defined.
+  Definition precompose' Γ Δ ec : forall a b x y z lev,
+    ND Rule
+      [ Γ > Δ > 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 ].
+    apply precompose.
+    Defined.
 
-  Definition postcompose : ∀ Γ Δ ec lev a b c,
-     ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
-     intros.
-     eapply nd_comp.
-     apply postcompose'.
-     apply X.
-     apply nd_rule.
-     apply RArrange.
-     apply RCanL.
-     Defined.
+  Definition postcompose_ Γ Δ ec : forall a x y z lev,
+    ND Rule
+      [ Γ > Δ > a                           |- [@ga_mk _ ec x y @@ lev] ]
+      [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
+    apply nd_id.
+    apply ga_comp.
+    Defined.
 
-  Definition firstify : ∀ Γ Δ ec lev a b c Σ,
-    ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
-    ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
+  Definition postcompose  Γ Δ ec : forall x y z lev,
+    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; apply RLet ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod.
+    eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply X.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
-    apply ga_first.
     Defined.
 
-  Definition secondify : ∀ Γ Δ ec lev a b c Σ,
-     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
+  Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
+    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 RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
-    apply X.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
-    apply ga_second.
+    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+    apply ga_first.
     Defined.
 
-  Lemma ga_unkappa     : ∀ Γ Δ ec l z a b Σ,
-    ND Rule
-    [Γ > Δ > Σ                         |- [@ga_mk Γ ec a b @@ l] ] 
-    [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
+  Definition firstify : ∀ Γ Δ ec lev a b c Σ,
+    ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
+    ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
     intros.
-    set (ga_comp Γ Δ ec l z a b) as q.
-
-    set (@RLet Γ Δ) as q'.
-    set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
     eapply nd_comp.
-    Focus 2.
-    eapply nd_rule.
-    eapply RArrange.
-    apply RExch.
-
-    eapply nd_comp.
-    Focus 2.
-    eapply nd_rule.
-    apply q''.
+    apply X.
+    apply first_nd.
+    Defined.
 
-    idtac.
-    clear q'' q'.
-    eapply nd_comp.
-    apply nd_rlecnac.
+  Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
+     ND Rule
+     [ Γ > Δ > Σ                    |- [@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; apply RLet ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
-    apply q.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+    apply ga_second.
     Defined.
 
-  Lemma ga_unkappa'     : ∀ Γ Δ ec l a b Σ x,
-    ND Rule
-    [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ] 
-    [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b @@ l] ].
+  Definition secondify : ∀ Γ Δ ec lev a b c Σ,
+     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod.
-    apply ga_first.
-
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
-    apply nd_prod.
-    apply postcompose.
-    apply ga_uncancell.
-    apply precompose.
+    eapply nd_comp.
+    apply X.
+    apply second_nd.
     Defined.
 
-  Lemma ga_kappa'     : ∀ Γ Δ ec l a b Σ x,
-    ND Rule
-    [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
-    [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ].
-    apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
-    Defined.
+   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
+     ND Rule
+     [Γ > Δ > Σ                          |- [@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 RLet ].
+     eapply nd_comp; [ apply nd_llecnac | idtac ].
+     apply nd_prod.
+     apply ga_first.
+
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+     eapply nd_comp; [ apply nd_llecnac | idtac ].
+     apply nd_prod.
+     apply postcompose.
+     apply ga_uncancell.
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+     apply precompose.
+     Defined.
 
   (* useful for cutting down on the pretty-printed noise
   
@@ -559,17 +535,17 @@ Section HaskFlattener.
           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; apply
-             (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
+             (@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 RuCanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
-          eapply nd_comp; [ idtac | eapply nd_rule;  apply 
-            (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
+          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;  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 ].
           apply ga_comp.
           Defined.
 
@@ -630,7 +606,7 @@ Section HaskFlattener.
         apply RuCanR.
         apply RAssoc.
         apply RCossa.
-        apply RExch.
+        apply RExch.    (* TO DO: check for all-leaf trees here *)
         apply RWeak.
         apply RCont.
         apply RLeft; auto.
@@ -648,29 +624,32 @@ Section HaskFlattener.
     intro pfa.
     intro pfb.
     apply secondify with (c:=a)  in pfb.
-    eapply nd_comp.
-    Focus 2.
+    apply firstify  with (c:=[])  in pfa.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
     eapply nd_comp; [ eapply nd_llecnac | idtac ].
-    eapply nd_prod.
-    apply pfb.
-    clear pfb.
-    apply postcompose'.
-    eapply nd_comp.
+    apply nd_prod.
     apply pfa.
     clear pfa.
-    apply boost.
+
+    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 ].
-    apply precompose'.
+    eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply ga_uncancelr.
-    apply nd_id.
+
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply precompose ].
+    apply pfb.
     Defined.
 
   Definition arrange_brak : forall Γ Δ ec succ t,
    ND Rule
-     [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
-      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@ nil]]
+     [Γ > Δ > 
+      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
+      mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]]
      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]].
+
     intros.
     unfold drop_lev.
     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
@@ -682,6 +661,7 @@ Section HaskFlattener.
     apply y.
     idtac.
     clear y q.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
     simpl.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
@@ -778,8 +758,9 @@ Section HaskFlattener.
   Definition arrange_esc : forall Γ Δ ec succ t,
    ND Rule
      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]]
-     [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
-      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@  nil]].
+     [Γ > Δ > 
+      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
+      mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t @@  nil]].
     intros.
     set (@arrange _ succ (levelMatch (ec::nil))) as q.
     set (@drop_lev Γ (ec::nil) succ) as q'.
@@ -803,7 +784,7 @@ Section HaskFlattener.
     simpl.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     clear q''.
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
@@ -812,15 +793,15 @@ Section HaskFlattener.
     eapply RComp; [ idtac | apply RCanR ].
     apply RLeft.
     apply (@arrange_empty_tree _ _ _ _ e).
-    
+   
     eapply nd_comp.
       eapply nd_rule.
       eapply (@RVar Γ Δ t nil).
     apply nd_rule.
       apply RArrange.
       eapply RComp.
-      apply RuCanL.
-      apply RRight.
+      apply RuCanR.
+      apply RLeft.
       apply RWeak.
 (*
     eapply decide_tree_empty.
@@ -873,52 +854,45 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
-  Lemma tree_of_nothing : forall Γ ec t a,
-    Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
+  Lemma tree_of_nothing : forall Γ ec t,
+    Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
     intros.
-    induction t; try destruct o; try destruct a0.
+    induction t; try destruct o; try destruct a.
     simpl.
     drop_simplify.
     simpl.
-    apply RCanR.
+    apply RId.
     simpl.
-    apply RCanR.
+    apply RId.
+    eapply RComp; [ idtac | apply RCanL ].
+    eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
+    idtac.
     drop_simplify.
-    simpl.
-    eapply RComp.
-    eapply RComp.
-    eapply RAssoc.
-    eapply RRight.
+    apply RRight.
     apply IHt1.
-    apply IHt2.
     Defined.
 
-  Lemma tree_of_nothing' : forall Γ ec t a,
-    Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
+  Lemma tree_of_nothing' : forall Γ ec t,
+    Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
     intros.
-    induction t; try destruct o; try destruct a0.
+    induction t; try destruct o; try destruct a.
     simpl.
     drop_simplify.
     simpl.
-    apply RuCanR.
+    apply RId.
     simpl.
-    apply RuCanR.
+    apply RId.
+    eapply RComp; [ apply RuCanL | idtac ].
+    eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
+    idtac.
     drop_simplify.
-    simpl.
-    eapply RComp.
-    Focus 2.
-    eapply RComp.
-    Focus 2.
-    eapply RCossa.
-    Focus 2.
-    eapply RRight.
-    apply IHt1.
+    apply RLeft.
     apply IHt2.
     Defined.
 
@@ -989,6 +963,7 @@ Section HaskFlattener.
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
+      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
       | RVoid    _ _                   => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
@@ -1130,22 +1105,51 @@ Section HaskFlattener.
       repeat take_simplify.
       simpl.
 
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
+
       eapply nd_comp.
       eapply nd_prod; [ idtac | apply nd_id ].
       eapply boost.
-      apply ga_second.
+      apply (ga_first _ _ _ _ _ _ Σ₂').
 
-      eapply nd_comp.
-      eapply nd_prod.
+      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 *)].
+      apply precompose.
+
+    destruct case_RWhere.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
+      repeat take_simplify.
+      repeat drop_simplify.
+      simpl.
+
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
+
       eapply nd_comp.
-      eapply nd_rule.
-      eapply RArrange.
-      apply RCanR.
-      eapply precompose.
+      eapply nd_prod; [ eapply nd_id | idtac ].
+      eapply (first_nd _ _ _ _ _ _ Σ₃').
+      eapply nd_comp.
+      eapply nd_prod; [ eapply nd_id | idtac ].
+      eapply (second_nd _ _ _ _ _ _ Σ₁').
 
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
+      apply nd_prod; [ idtac | apply nd_id ].
+      eapply nd_comp; [ idtac | eapply precompose' ].
       apply nd_rule.
-      apply RLet.
+      apply RArrange.
+      apply RLeft.
+      apply RCanL.
 
     destruct case_RVoid.
       simpl.
@@ -1242,11 +1246,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.
-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
-      refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
+      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 ].
+      refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
+      eapply nd_comp; [ idtac | eapply arrange_brak ].
       unfold succ_host.
       unfold succ_guest.
-      apply arrange_brak.
+      eapply nd_rule.
+        eapply RArrange.
+        apply RExch.
       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 
     destruct case_SEsc.
@@ -1260,7 +1268,8 @@ Section HaskFlattener.
       take_simplify.
       drop_simplify.
       simpl.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
+      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 ].
       simpl.
       rewrite take_lemma'.
       rewrite unlev_relev.
@@ -1276,13 +1285,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.
 
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+      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 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 RCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
         simpl.
         apply ga_join.
           apply IHx1.
@@ -1307,7 +1318,7 @@ Section HaskFlattener.
         apply IHx2.
 
       (* environment has non-empty leaves *)
-      apply ga_kappa'.
+      apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
 
       (* nesting too deep *)
       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
index d9c6a7e..a8b311e 100644 (file)
@@ -82,9 +82,11 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 
-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
+(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 
-| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
+| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   @@l]]
+| RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂   @@l]]
 
 | RVoid    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
 
@@ -99,7 +101,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 
-| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
@@ -159,6 +161,7 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
+    destruct X0; destruct s; inversion e.
     Qed.
 
 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
index 61b358f..61a0bdb 100644 (file)
@@ -189,12 +189,13 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
-    | RJoin _ _ _ _ _ _       => "RJoin"
+    | RWhere        _ _ _ _ _ _ _ _   => "Where"
+    | RJoin         _ _ _ _ _ _       => "RJoin"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"
-    | RVoid   _ _               => "RVoid"
+    | RVoid         _ _               => "RVoid"
 end.
 
 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
index b6e8efe..6ba094e 100644 (file)
@@ -524,8 +524,9 @@ Section HaskProofToStrong.
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
-      | RJoin Γ p lri m x q   => let case_RJoin := tt in _
-      | RVoid _ _               => let case_RVoid := tt   in _
+      | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
+      | RJoin   Γ p lri m x q         => let case_RJoin := tt in _
+      | RVoid   _ _                   => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
@@ -636,42 +637,84 @@ Section HaskProofToStrong.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.
-    apply (EApp _ _ _ _ _ _ q2' q1').
+    apply (EApp _ _ _ _ _ _ q1' q2').
 
   destruct case_RLet.
     apply ILeaf.
     simpl in *; intros.
     destruct vars; try destruct o; inversion H.
-    refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
+
+    refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
     apply FreshMon.
+
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
+    set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
     simpl in *.
-    refine (X ξ  vars2 _ >>>= fun X0' => _).
+
+    refine (X ξ vars1 _ >>>= fun X0' => _).
     apply FreshMon.
+    simpl.
     auto.
 
-    refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+    refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
     apply FreshMon.
-    rewrite H1.
     simpl.
     rewrite pf2.
     rewrite pf1.
-    rewrite H1.
     reflexivity.
+    apply FreshMon.
 
-    refine (return _).
     apply ILeaf.
-    apply ileaf in X0'.
     apply ileaf in X1'.
+    apply ileaf in X0'.
     simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₂).
+    apply ELet with (ev:=vnew)(tv:=σ₁).
     apply X0'.
     apply X1'.
 
+  destruct case_RWhere.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars;  try destruct o; inversion H.
+    destruct vars2; try destruct o; inversion H2.
+    clear H2.
+
+    assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
+    refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
+    apply FreshMon.
+
+    destruct pf as [ vnew [ pf1 pf2 ]].
+    set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+    inversion X_.
+    apply ileaf in X.
+    apply ileaf in X0.
+    simpl in *.
+
+    refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
+    apply FreshMon.
+    simpl.
+    inversion pf1.
+    rewrite H3.
+    rewrite H4.
+    rewrite pf2.
+    reflexivity.
+
+    refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
+    apply FreshMon.
+    reflexivity.
+    apply FreshMon.
+
+    apply ILeaf.
+    apply ileaf in X0'.
+    apply ileaf in X1'.
+    simpl in *.
+    apply ELet with (ev:=vnew)(tv:=σ₁).
+    apply X1'.
+    apply X0'.
+
   destruct case_RVoid.
     apply ILeaf; simpl; intros.
     refine (return _).
@@ -720,11 +763,11 @@ Section HaskProofToStrong.
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
     auto.
     apply (@letrec_helper Γ Δ t varstypes).
-    rewrite <- pf2 in X1.
+    rewrite <- pf2 in X0.
     rewrite mapOptionTree_compose.
-    apply X1.
-    apply ileaf in X0.
     apply X0.
+    apply ileaf in X1.
+    apply X1.
 
   destruct case_RCase.
     apply ILeaf; simpl; intros.
index bfbdf0e..b037bb0 100644 (file)
@@ -130,10 +130,10 @@ Section HaskSkolemizer.
   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 
   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
-    Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev)
+    Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
       (take_arg_types_as_tree (tx ---> te) @@@ lev).
     intros.
-    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+    destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
       apply RId.
@@ -152,9 +152,9 @@ Section HaskSkolemizer.
 
   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
-      ([tx @@ lev],, take_arg_types_as_tree te @@@ lev).
+      ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
     intros.
-    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+    destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
       apply RId.
@@ -184,13 +184,13 @@ Section HaskSkolemizer.
   | SFlat  : forall h c, Rule h c -> SRule h c
   | SBrak  : forall Γ Δ t ec Σ l,
     SRule
-    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
+    [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
     [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
 
   | SEsc   : forall Γ Δ t ec Σ l,
     SRule
     [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
-    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
+    [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
     .
 
   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
@@ -245,10 +245,11 @@ Section HaskSkolemizer.
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
+      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
       | RVoid    _ _                   => let case_RVoid := tt   in _
-      | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
-      | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
+      | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
+      | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); clear X h c.
@@ -347,8 +348,8 @@ Section HaskSkolemizer.
           apply SFlat.
           apply RArrange.
           eapply RComp.
-          apply RCossa.
-          apply RLeft.
+          eapply RCossa.
+          eapply RLeft.
           apply take_arrange.
 
       destruct case_RCast.
@@ -383,23 +384,16 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
-        set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
+        eapply nd_comp.
+        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
+        eapply nd_rule.
+        eapply SFlat.
+        eapply RArrange.
+        eapply RLeft.
+        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 RExch ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
-        clear q.
-        apply nd_prod.
-        apply nd_rule.
-        apply SFlat.
-        apply RArrange.
-        apply RCanR.
-        apply nd_rule.
-          apply SFlat.
-          apply RArrange.
-          eapply RComp; [ idtac | eapply RAssoc ].
-          apply RLeft.
-          eapply RComp; [ idtac | apply RExch ].
-          apply take_unarrange.
+        eapply nd_rule; eapply SFlat; apply RWhere.
 
       destruct case_RLet.
         simpl.
@@ -407,29 +401,48 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RLet.
-        set (check_hof σ₂) as hof_tx.
+        set (check_hof σ₁) as hof_tx.
         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
         destruct a.
         rewrite H.
         rewrite H0.
-        set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
+
+        eapply nd_comp.
+        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
+
+        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; eapply RLeft; apply RExch ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
-        clear q.
+        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.
+
+      destruct case_RWhere.
+        simpl.
+        destruct lev.
         apply nd_rule.
         apply SFlat.
-        apply RArrange.
-        apply RCanR.
-        eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
-        apply nd_rule.
-        apply SFlat.
-        apply RArrange.
+        apply RWhere.
+        set (check_hof σ₁) as hof_tx.
+        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
+        destruct a.
+        rewrite H.
+        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_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 RExch.
+        eapply RCossa.
 
       destruct case_RVoid.
         simpl.
index 9c3b041..5f3baa3 100644 (file)
@@ -19,6 +19,9 @@ Section HaskStrongToProof.
 Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
   RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
 
+Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
+  RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
+
 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 ]. 
@@ -522,9 +525,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
   | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
-  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e2),,(expr2antecedent e1)
+  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
-  | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
+  | ELet     Γ Δ ξ tv t  lev v ev ebody           => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody)))
   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
@@ -535,7 +538,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
   | ELetRec  Γ Δ ξ l τ vars _ branches body       =>
       let branch_context := eLetRecContext branches
-   in let all_contexts := (expr2antecedent body),,branch_context
+   in let all_contexts := branch_context,,(expr2antecedent body)
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
     ((fix varsfromalts (alts:
@@ -598,7 +601,112 @@ Lemma stripping_nothing_is_inert
     reflexivity.
     Qed.
 
-Definition arrangeContext
+Definition factorContextLeft
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★)
+     :
+    (* a proof concluding in a context where that variable does not appear *)
+     sum (Arrange
+          (mapOptionTree ξ                        ctx                        )
+          (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx))                ))
+   
+    (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
+        (Arrange
+          (mapOptionTree ξ                         ctx                       )
+          (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))                )).
+
+  induction ctx.
+  
+    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
+  
+        (* nonempty leaf *)
+        destruct case_Some.
+          unfold stripOutVars in *; simpl.
+          unfold dropVar.
+          unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
+
+          destruct (eqd_dec v' v); subst.
+          
+            (* where the leaf is v *)
+            apply inr.
+              subst.
+              apply RuCanR.
+
+            (* where the leaf is NOT v *)
+            apply inl.
+              apply RuCanL.
+  
+        (* empty leaf *)
+        destruct case_None.
+          apply inl; simpl in *.
+          apply RuCanR.
+  
+      (* branch *)
+      refine (
+        match IHctx1 with
+          | inr lpf =>
+            match IHctx2 with
+              | inr rpf => let case_Both := tt in _
+              | inl rpf => let case_Left := tt in _
+            end
+          | inl lpf =>
+            match IHctx2 with
+              | inr rpf => let case_Right   := tt in _
+              | inl rpf => let case_Neither := tt in _
+            end
+        end); clear IHctx1; clear IHctx2.
+
+    destruct case_Neither.
+      apply inl.
+      simpl.
+      eapply RComp; [idtac | apply RuCanL ].
+        exact (RComp
+          (* order will not matter because these are central as morphisms *)
+          (RRight _ (RComp lpf (RCanL _)))
+          (RLeft  _ (RComp rpf (RCanL _)))).
+
+    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.
+      apply lpf.
+      apply RCanL.
+      eapply RLeft.
+      apply rpf.
+
+    destruct case_Left.
+      apply inr.
+      fold (stripOutVars (v::nil)).
+      simpl.
+      eapply RComp.
+      eapply RLeft.
+      eapply RComp.
+      apply rpf.
+      simpl.
+      eapply RCanL.
+      eapply RComp; [ idtac | eapply RCossa ].
+      eapply RRight.
+      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 ].
+      clear lpf rpf.
+      simpl.
+      apply arrangeSwapMiddle.
+      Defined.
+
+Definition factorContextRight
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
@@ -703,7 +811,72 @@ Definition arrangeContext
     Defined.
 
 (* same as before, but use RWeak if necessary *)
-Definition arrangeContextAndWeaken  
+Definition factorContextLeftAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
+  set (factorContextLeft Γ Δ v ctx ξ) as q.
+  destruct q; auto.
+  eapply RComp; [ apply a | idtac ].
+  refine (RRight _ (RWeak _)).
+  Defined.
+
+Definition factorContextLeftAndWeaken''
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
+  distinct (leaves v) ->
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
+
+  induction v; intros.
+    destruct a.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    intros.
+    set (@factorContextLeftAndWeaken) as q.
+    simpl in q.
+    apply q.
+    apply Δ.
+
+  unfold mapOptionTree; simpl in *.
+    intros.
+    rewrite (@stripping_nothing_is_inert Γ); auto.
+    apply RuCanL.
+    intros.
+    unfold mapOptionTree in *.
+    simpl in *.
+    fold (mapOptionTree ξ) in *.
+    set (mapOptionTree ξ) as X in *.
+
+    set (distinct_app _ _ _ H) as H'.
+    destruct H' as [H1 H2].
+
+    set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
+
+    unfold X in *.
+    simpl in *.
+      rewrite <- strip_twice_lemma.
+      set (notin_strip_inert' v2 (leaves v1)) as q.
+      unfold stripOutVars in q.
+      rewrite q in IHv1'.
+      clear q.
+    eapply RComp; [ idtac | eapply RAssoc ].
+    eapply RComp; [ idtac | eapply IHv1' ].
+    clear IHv1'.
+    apply IHv2; auto.
+    auto.
+    auto.
+    Defined.
+
+(* same as before, but use RWeak if necessary *)
+Definition factorContextRightAndWeaken  
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
@@ -711,13 +884,13 @@ Definition arrangeContextAndWeaken
        Arrange
           (mapOptionTree ξ                        ctx                )
           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
-  set (arrangeContext Γ Δ v ctx ξ) as q.
+  set (factorContextRight Γ Δ v ctx ξ) as q.
   destruct q; auto.
   eapply RComp; [ apply a | idtac ].
   refine (RLeft _ (RWeak _)).
   Defined.
 
-Definition arrangeContextAndWeaken''
+Definition factorContextRightAndWeaken''
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
@@ -732,7 +905,7 @@ Definition arrangeContextAndWeaken''
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.
-    apply arrangeContextAndWeaken.
+    apply factorContextRightAndWeaken.
     apply Δ.
 
   unfold mapOptionTree; simpl in *.
@@ -833,7 +1006,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
-  set (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
+  set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   set (q' disti) as q''.
@@ -855,7 +1028,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod; auto.
     rewrite ξlemma.
     apply q.
@@ -1007,7 +1180,7 @@ Definition expr2proof  :
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
-      set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
+      set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
         eapply RArrange in pfx.
         unfold mapOptionTree in pfx; simpl in pfx.
         unfold ξ' in pfx.
@@ -1024,16 +1197,14 @@ Definition expr2proof  :
 
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      eapply nd_comp; [ apply nd_rlecnac | idtac ].
       apply nd_prod.
-        apply pf_let.
-        clear pf_let.
-        eapply nd_comp; [ apply pf_body | idtac ].
-        clear pf_body.
+      apply pf_let.
+      eapply nd_comp; [ apply pf_body | idtac ].
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
-      set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
+      set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.
@@ -1102,7 +1273,7 @@ Definition expr2proof  :
       rewrite <- (scbwv_coherent scbx l ξ).
       rewrite <- vec2list_map_list2vec.
       rewrite mapleaves'.
-      set (@arrangeContextAndWeaken'') as q.
+      set (@factorContextRightAndWeaken'') as q.
       unfold scbwv_ξ.
       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
       unfold scbwv_varstypes in z.
@@ -1110,6 +1281,7 @@ Definition expr2proof  :
       rewrite fst_zip in z.
       rewrite <- z.
       clear z.
+
       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.