| 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 _
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.
+ 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 ALeft.
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_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 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.
| 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]
[Γ > Δ > (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) *)
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RApp _ _ _ _ _ _ _ => "App"
| RLet _ _ _ _ _ _ _ => "Let"
- | RCut _ _ _ _ _ _ _ => "Cut"
+ | RCut _ _ _ _ _ _ _ _ => "Cut"
| RLeft _ _ _ _ _ _ => "Left"
| RRight _ _ _ _ _ _ => "Right"
| RWhere _ _ _ _ _ _ _ _ => "Where"
| 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 _
apply X0'.
destruct case_RCut.
+ apply rassoc.
+ apply swapr.
+ apply rassoc'.
+
inversion X_.
subst.
clear X_.
+
+ apply rassoc' in X0.
+ apply swapr in X0.
+ apply rassoc in X0.
+
induction Σ₃.
destruct a.
subst.
| 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 _
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.
+ clear e.
+ destruct s.
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 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 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.
+ 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 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.
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.