move more arrange routines into NaturalDeductionContext

diff --git a/src/General.v b/src/General.v
index ae27b9f..ee5cb16 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -106,6 +106,11 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
   end.
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
   end.
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.

+Lemma mapOptionTree_distributes
+  : forall T R (a b:Tree ??T) (f:T->R),
+    mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
+  reflexivity.
+  Qed.

 
 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
   match tt with
 
 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
   match tt with

@@ -520,6 +525,12 @@ Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
       end
   end.
 
       end
   end.
 

+Definition takeT' {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+  match takeT tf with
+    | None   => []
+    | Some x => x
+  end.
+

 (* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
 Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
   fun t =>
 (* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
 Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
   fun t =>

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index cc9c9aa..51fd784 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -132,29 +132,11 @@ Section HaskFlattener.
     rewrite <- IHx2 at 2.
     reflexivity.
     Qed.
     rewrite <- IHx2 at 2.
     reflexivity.
     Qed.

-(*
-  Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
-    intros.
-    induction x.
-    destruct a; simpl; try reflexivity.
-    apply drop_lev_lemma.
-    simpl.
-    change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
-      with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
-    simpl.
-    rewrite IHx1.
-    rewrite IHx2.
-    reflexivity.
-    Qed.
-*)
+

   Ltac drop_simplify :=
     match goal with
       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
         rewrite (drop_lev_lemma G L X)
   Ltac drop_simplify :=
     match goal with
       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
         rewrite (drop_lev_lemma G L X)

-(*
-      | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
-        rewrite (drop_lev_lemma' G L X)
-*)

       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
         rewrite (drop_lev_lemma_s G L E X)
       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
         rewrite (drop_lev_lemma_s G L E X)
       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>

@@ -582,7 +564,7 @@ Section HaskFlattener.
 
     intros.
     unfold drop_lev.
 
     intros.
     unfold drop_lev.

-    set (@arrange' _ succ (levelMatch (ec::nil))) as q.
+    set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.

     set (arrangeMap _ _ flatten_leveled_type q) as y.
     eapply nd_comp.
     Focus 2.
     set (arrangeMap _ _ flatten_leveled_type q) as y.
     eapply nd_comp.
     Focus 2.

@@ -632,59 +614,6 @@ Section HaskFlattener.
       apply IHsucc2.
     Defined.
 
       apply IHsucc2.
     Defined.
 

-  Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
-    t = mapTree (fun _:A => None) q ->
-    Arrange t [].
-    intros T A q.
-    induction q; intros.
-      simpl in H.
-      rewrite H.
-      apply RId.
-    simpl in *.
-    destruct t; try destruct o; inversion H.
-      set (IHq1 _ H1) as x1.
-      set (IHq2 _ H2) as x2.
-      eapply RComp.
-        eapply RRight.
-        rewrite <- H1.
-        apply x1.
-      eapply RComp.
-        apply RCanL.
-        rewrite <- H2.
-        apply x2.
-      Defined.
-
-(*  Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
-    t = mapTree (fun _:A => None) q ->
-    Arrange [] t.
-  Defined.*)
-
-  Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
-    sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
-    intro T.
-    refine (fix foo t :=
-      match t with
-        | T_Leaf x => _
-        | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
-      end).
-    intros.
-    destruct x.
-    right; apply tt.
-    left.
-      exists (T_Leaf tt).
-      auto.
-    destruct b1'.
-    destruct b2'.
-    destruct s.
-    destruct s0.
-    subst.
-    left.
-    exists (x,,x0).
-    reflexivity.
-    right; auto.
-    right; auto.
-    Defined.
-

   Definition arrange_esc : forall Γ Δ ec succ t,
    ND Rule
      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
   Definition arrange_esc : forall Γ Δ ec succ t,
    ND Rule
      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]

@@ -692,7 +621,7 @@ Section HaskFlattener.
       [(@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.
       [(@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 (@arrangePartition _ succ (levelMatch (ec::nil))) as q.

     set (@drop_lev Γ (ec::nil) succ) as q'.
     assert (@drop_lev Γ (ec::nil) succ=q') as H.
       reflexivity.
     set (@drop_lev Γ (ec::nil) succ) as q'.
     assert (@drop_lev Γ (ec::nil) succ=q') as H.
       reflexivity.

@@ -722,7 +651,7 @@ Section HaskFlattener.
     apply RArrange.
     eapply RComp; [ idtac | apply RCanR ].
     apply RLeft.
     apply RArrange.
     eapply RComp; [ idtac | apply RCanR ].
     apply RLeft.

-    apply (@arrange_empty_tree _ _ _ _ e).
+    apply (@arrangeCancelEmptyTree _ _ _ _ e).

    
     eapply nd_comp.
       eapply nd_rule.
    
     eapply nd_comp.
       eapply nd_rule.

@@ -769,12 +698,6 @@ Section HaskFlattener.
 *)
       Defined.
 
 *)
       Defined.
 

-  Lemma mapOptionTree_distributes
-    : forall T R (a b:Tree ??T) (f:T->R),
-      mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
-    reflexivity.
-    Qed.
-

   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
     intros.
     induction t.
   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
     intros.
     induction t.

diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v
index 4e9a802..03fc704 100644 (file)
--- a/src/NaturalDeductionContext.v
+++ b/src/NaturalDeductionContext.v
@@ -51,7 +51,7 @@ Section NaturalDeductionContext.
     eapply RComp; [ apply IHX1 | apply IHX2 ].
     Defined.
   
     eapply RComp; [ apply IHX1 | apply IHX2 ].
     Defined.
   

-  (* a frequently-used Arrange *)
+  (* 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.
   Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
     Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
     eapply RComp.

@@ -68,7 +68,23 @@ Section NaturalDeductionContext.
     eapply RAssoc.
     Defined.
 
     eapply RAssoc.
     Defined.
 

-  Definition arrange :
+  (* like RExch, 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) :=
+    RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+
+  (* like RExch, 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)) :=
+    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 ]. 
+    eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
+    apply RAssoc.
+    Defined.
+
+  (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
+  Definition arrangePartition :

     forall {T} (Σ:Tree ??T) (f:T -> bool),
       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
     intros.
     forall {T} (Σ:Tree ??T) (f:T -> bool),
       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
     intros.

@@ -90,7 +106,8 @@ Section NaturalDeductionContext.
       apply IHΣ1.
       Defined.
 
       apply IHΣ1.
       Defined.
 

-  Definition arrange' :
+  (* inverse of arrangePartition *)
+  Definition arrangeUnPartition :

     forall {T} (Σ:Tree ??T) (f:T -> bool),
       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
     intros.
     forall {T} (Σ:Tree ??T) (f:T -> bool),
       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
     intros.

@@ -112,17 +129,127 @@ Section NaturalDeductionContext.
       apply IHΣ1.
       Defined.
 
       apply IHΣ1.
       Defined.
 

-  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 ]. 
-    eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
-    apply RAssoc.
+  (* we can decide if a tree consists exclusively of (T_Leaf None)'s *)
+  Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+    sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+    intro T.
+    refine (fix foo t :=
+      match t with
+        | T_Leaf x => _
+        | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+      end).
+    intros.
+    destruct x.
+    right; apply tt.
+    left.
+      exists (T_Leaf tt).
+      auto.
+    destruct b1'.
+    destruct b2'.
+    destruct s.
+    destruct s0.
+    subst.
+    left.
+    exists (x,,x0).
+    reflexivity.
+    right; auto.
+    right; auto.

     Defined.
 
     Defined.
 

+  (* if a tree is empty, we can Arrange it to [] *)
+  Definition arrangeCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+    t = mapTree (fun _:A => None) q ->
+    Arrange t [].
+    intros T A q.
+    induction q; intros.
+      simpl in H.
+      rewrite H.
+      apply RId.
+    simpl in *.
+    destruct t; try destruct o; inversion H.
+      set (IHq1 _ H1) as x1.
+      set (IHq2 _ H2) as x2.
+      eapply RComp.
+        eapply RRight.
+        rewrite <- H1.
+        apply x1.
+      eapply RComp.
+        apply RCanL.
+        rewrite <- H2.
+        apply x2.
+      Defined.
+
+  (* if a tree is empty, we can Arrange it from [] *)
+  Definition arrangeUnCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+    t = mapTree (fun _:A => None) q ->
+    Arrange [] t.
+    intros T A q.
+    induction q; intros.
+      simpl in H.
+      rewrite H.
+      apply RId.
+    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.
+        apply x1.
+      eapply RComp.
+        eapply RLeft.
+        apply x2.
+      rewrite H.
+      apply RId.
+      Defined.
+
+  (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
+  Lemma arrangeDrop {T} pred
+    : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (dropT (mkFlags pred Σ₁)) (dropT (mkFlags pred Σ₂)).
+
+    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)
+      end)); clear arrangeTake; intros.
+
+    destruct case_RCanL.
+      simpl; destruct (pred None); simpl; apply RCanL.
+
+    destruct case_RCanR.
+      simpl; destruct (pred None); simpl; apply RCanR.
+
+    destruct case_RuCanL.
+      simpl; destruct (pred None); simpl; apply RuCanL.
+
+    destruct case_RuCanR.
+      simpl; destruct (pred None); simpl; apply RuCanR.
+
+    destruct case_RWeak.
+      simpl; destruct (pred None); simpl; apply RWeak.
+
+    destruct case_RCont.
+      simpl; destruct (pred None); simpl; apply RCont.
+
+      Defined.
+
+  (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
+  (*
+  Lemma arrangeTake {T} pred
+    : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
+    unfold takeT'.
+    *)
+

 End NaturalDeductionContext.
 End NaturalDeductionContext.