let RCut take a left environment as well

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index d822dd6..c42842a 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -831,9 +831,9 @@ 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 _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _

-      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
-      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
-      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
+      | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
+      | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _

       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RVoid    _ _       l           => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RVoid    _ _       l           => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _

@@ -1022,41 +1022,46 @@ Section HaskFlattener.
         rewrite <- IHΣ₁₂1.
         rewrite <- IHΣ₁₂2.
         reflexivity.
         rewrite <- IHΣ₁₂1.
         rewrite <- IHΣ₁₂2.
         reflexivity.

-      simpl.
-      repeat drop_simplify.
-      simpl.
-      repeat take_simplify.
+      simpl; repeat drop_simplify.
+      simpl; repeat take_simplify.

       simpl.
       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
       rewrite take_lemma'.
       rewrite mapOptionTree_compose.
       rewrite mapOptionTree_compose.
       rewrite mapOptionTree_compose.
       simpl.
       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
       rewrite take_lemma'.
       rewrite mapOptionTree_compose.
       rewrite mapOptionTree_compose.
       rewrite mapOptionTree_compose.

+      rewrite mapOptionTree_compose.

       rewrite unlev_relev.
       rewrite <- mapOptionTree_compose.
       rewrite <- mapOptionTree_compose.
       rewrite unlev_relev.
       rewrite <- mapOptionTree_compose.
       rewrite <- mapOptionTree_compose.

+      rewrite <- mapOptionTree_compose.

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

+      eapply ALeft.

       eapply ARight.
       unfold x1.
       rewrite drop_to_nothing.
       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
       admit. (* OK *)
       eapply ARight.
       unfold x1.
       rewrite drop_to_nothing.
       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
       admit. (* OK *)

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

       set (mapOptionTree flatten_type Σ₁₂) as a.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
       set (mapOptionTree flatten_type Σ₁₂) as a.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.

+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.

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

-      eapply ga_first.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+      eapply secondify.
+      apply ga_first.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].

       simpl.
       apply precompose.
 
       simpl.
       apply precompose.
 

diff --git a/src/HaskProof.v b/src/HaskProof.v
index b01f5c2..8c6acf4 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -71,7 +71,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
 | RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
 | RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
 

-| RCut           : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,  Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l]
+| RCut           : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]

 | RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
 | RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
 
 | RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
 | RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
 

@@ -97,6 +97,17 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
 .
 
                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
 .
 

+Definition RCut'  : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
+  ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
+  intros.
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+  apply nd_prod.
+  apply nd_id.
+  apply nd_rule.
+  apply RArrange.
+  apply AuCanL.
+  Defined.

 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 (* TODO: change this to (if RBrak/REsc -> False) *)
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 (* TODO: change this to (if RBrak/REsc -> False) *)

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index b787d3e..323c1d6 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -190,7 +190,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"

-    | RCut          _ _ _ _ _ _ _     => "Cut"
+    | RCut          _ _ _ _ _ _ _ _   => "Cut"

     | RLeft         _ _ _ _ _ _       => "Left"
     | RRight        _ _ _ _ _ _       => "Right"
     | RWhere        _ _ _ _ _ _ _ _   => "Where"
     | RLeft         _ _ _ _ _ _       => "Left"
     | RRight        _ _ _ _ _ _       => "Right"
     | RWhere        _ _ _ _ _ _ _ _   => "Where"

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 2ea0c4a..8cbebce 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -764,7 +764,7 @@ 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 _
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _

-      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RCut    Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _

       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _

@@ -914,9 +914,18 @@ Section HaskProofToStrong.
     apply X0'.
 
   destruct case_RCut.
     apply X0'.
 
   destruct case_RCut.

+    apply rassoc.
+    apply swapr.
+    apply rassoc'.
+

     inversion X_.
     subst.
     clear X_.
     inversion X_.
     subst.
     clear X_.

+
+    apply rassoc' in X0.
+    apply swapr in X0.
+    apply rassoc in X0.
+

     induction Σ₃.
     destruct a.
     subst.
     induction Σ₃.
     destruct a.
     subst.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 9d8dd4d..b1d65e6 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -232,9 +232,9 @@ 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 _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _

-      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
-      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
-      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
+      | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
+      | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _

       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RVoid    _ _           l       => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RVoid    _ _           l       => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _

@@ -429,24 +429,38 @@ Section HaskSkolemizer.
         set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
         set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
         set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
         set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.

-        destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+        destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].

         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
         rewrite <- e.
         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
         rewrite <- e.

+        clear e.
+        destruct s.

         eapply nd_comp.
         eapply nd_comp.

-        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+          eapply nd_prod.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply ALeft.
+          eapply arrangeCancelEmptyTree with (q:=x).
+          apply e.
+          apply ACanR.
+          apply nd_id.

         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 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 RCut ].
         apply nd_prod.
         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
         apply nd_prod.

-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
-        apply nd_rule.
-        apply SFlat.
-        apply RArrange.
-        apply ALeft.
-        destruct s.
-        eapply arrangeCancelEmptyTree with (q:=x).
-        rewrite e0.
-        admit.   (* FIXME, but not serious *)

         apply nd_id.
         apply nd_id.

+        eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AId.

 
       destruct case_RLeft.
         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
 
       destruct case_RLeft.
         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 113955f..35373a7 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -961,7 +961,7 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       destruct q.
       simpl in *.
       apply n.
       destruct q.
       simpl in *.
       apply n.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+    eapply nd_comp; [ idtac | eapply RCut' ].

       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply IHX1.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply IHX1.

@@ -1019,7 +1019,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+    eapply nd_comp; [ idtac | eapply RCut' ].

       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply q.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply q.