admit.
Qed.
- Definition flatten_proof :
+ Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
+ drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
+ intros.
+ induction Σ.
+ destruct a; simpl.
+ drop_simplify.
+ auto.
+ drop_simplify.
+ auto.
+ simpl.
+ rewrite <- IHΣ1.
+ rewrite <- IHΣ2.
+ reflexivity.
+ Qed.
+
+ Definition flatten_skolemized_proof :
forall {h}{c},
ND SRule h c ->
ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
| 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 _
| RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
- | RJoin Γ p lri m x q l => let case_RJoin := tt in _
| RVoid _ _ l => let case_RVoid := tt in _
| RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
| REsc Γ Δ t ec succ lev => let case_REsc := tt in _
apply flatten_coercion; auto.
apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
- destruct case_RJoin.
- simpl.
- destruct l;
- [ apply nd_rule; apply RJoin | idtac ];
- apply (Prelude_error "RJoin at depth >0").
-
destruct case_RApp.
simpl.
apply ALeft.
apply ACanL.
+ destruct case_RCut.
+ simpl.
+ destruct l as [|ec lev]; simpl.
+ apply nd_rule.
+ replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
+ apply RCut.
+ induction Σ₁₂; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ₁₂1.
+ rewrite <- IHΣ₁₂2.
+ reflexivity.
+ 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 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 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.
+
+ destruct case_RLeft.
+ simpl.
+ destruct l as [|ec lev].
+ simpl.
+ replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
+ apply nd_rule.
+ apply RLeft.
+ induction Σ; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ1.
+ rewrite <- IHΣ2.
+ reflexivity.
+ repeat drop_simplify.
+ rewrite drop_to_nothing.
+ simpl.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ARight.
+ apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
+ admit (* FIXME *).
+ idtac.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
+ apply boost.
+ take_simplify.
+ simpl.
+ replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ apply ga_second.
+ rewrite take_lemma'.
+ reflexivity.
+
+ destruct case_RRight.
+ simpl.
+ destruct l as [|ec lev].
+ simpl.
+ replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
+ apply nd_rule.
+ apply RRight.
+ induction Σ; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ1.
+ rewrite <- IHΣ2.
+ reflexivity.
+ repeat drop_simplify.
+ rewrite drop_to_nothing.
+ simpl.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ALeft.
+ apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
+ admit (* FIXME *).
+ idtac.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
+ apply boost.
+ take_simplify.
+ simpl.
+ replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ apply ga_first.
+ rewrite take_lemma'.
+ reflexivity.
+
destruct case_RVoid.
simpl.
apply nd_rule.
apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
Defined.
+ Definition flatten_proof :
+ forall {h}{c},
+ ND Rule h c ->
+ ND Rule h c.
+ apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
+ Defined.
+
Definition skolemize_and_flatten_proof :
forall {h}{c},
ND Rule h c ->
intros.
rewrite mapOptionTree_compose.
rewrite mapOptionTree_compose.
- apply flatten_proof.
+ apply flatten_skolemized_proof.
apply skolemize_proof.
apply X.
Defined.
projects / coq-hetmet.git / blobdiff