From: Adam Megacz Date: Sat, 28 May 2011 04:39:45 +0000 (-0700) Subject: move more arrange routines into NaturalDeductionContext X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=91f06dc68cf5888360f1819429b10e054f94b243;ds=sidebyside move more arrange routines into NaturalDeductionContext --- diff --git a/src/General.v b/src/General.v index ae27b9f..ee5cb16 100644 --- 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 }. +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 @@ -520,6 +525,12 @@ Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) := 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 => diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index cc9c9aa..51fd784 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -132,29 +132,11 @@ Section HaskFlattener. 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) -(* - | [ |- 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)] ] => @@ -582,7 +564,7 @@ Section HaskFlattener. 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. @@ -632,59 +614,6 @@ Section HaskFlattener. 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] @@ -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. - 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. @@ -722,7 +651,7 @@ Section HaskFlattener. apply RArrange. eapply RComp; [ idtac | apply RCanR ]. apply RLeft. - apply (@arrange_empty_tree _ _ _ _ e). + apply (@arrangeCancelEmptyTree _ _ _ _ e). eapply nd_comp. eapply nd_rule. @@ -769,12 +698,6 @@ Section HaskFlattener. *) 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. diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v index 4e9a802..03fc704 100644 --- a/src/NaturalDeductionContext.v +++ b/src/NaturalDeductionContext.v @@ -51,7 +51,7 @@ Section NaturalDeductionContext. 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. @@ -68,7 +68,23 @@ Section NaturalDeductionContext. 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. @@ -90,7 +106,8 @@ Section NaturalDeductionContext. 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. @@ -112,17 +129,127 @@ Section NaturalDeductionContext. 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. + (* 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.