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)] ] =>
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.
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]
[(@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.
apply RArrange.
eapply RComp; [ idtac | apply RCanR ].
apply RLeft.
- apply (@arrange_empty_tree _ _ _ _ e).
+ apply (@arrangeCancelEmptyTree _ _ _ _ e).
eapply nd_comp.
eapply nd_rule.
*)
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.
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.
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.
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.
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.