ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ idtac | apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
[ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
[ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
intros.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
[ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
[ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
intros.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
[ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ idtac | apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
[ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ idtac | apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
[Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply ga_first.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply postcompose.
set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply
+ eapply nd_comp; [ idtac | apply
(@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply r2'.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ idtac | apply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
eapply nd_prod.
apply r1'.
intro pfb.
apply secondify with (c:=a) in pfb.
apply firstify with (c:=[]) in pfa.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ eapply nd_llecnac | idtac ].
apply nd_prod.
apply pfa.
clear pfa.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
simpl.
eapply nd_comp; [ apply nd_llecnac | idtac ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
apply nd_prod.
Focus 2.
apply nd_id.
simpl.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
- eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ idtac | apply RLet ].
clear q''.
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
reflexivity.
Qed.
- Definition flatten_proof :
+ Definition flatten_skolemized_proof :
forall {h}{c},
ND SRule h c ->
ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
| 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 _
+ | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
+ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
+ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := 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.
Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
*)
- destruct case_RLet.
- simpl.
- destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
- repeat drop_simplify.
- repeat take_simplify.
- simpl.
-
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
-
- eapply nd_comp.
- eapply nd_prod; [ idtac | apply nd_id ].
- eapply boost.
- apply (ga_first _ _ _ _ _ _ Σ₂').
-
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
- apply nd_prod.
- apply nd_id.
- eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
- apply precompose.
-
- destruct case_RWhere.
- simpl.
- destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
- repeat take_simplify.
- repeat drop_simplify.
- simpl.
-
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
-
- eapply nd_comp.
- eapply nd_prod; [ eapply nd_id | idtac ].
- eapply (first_nd _ _ _ _ _ _ Σ₃').
- eapply nd_comp.
- eapply nd_prod; [ eapply nd_id | idtac ].
- eapply (second_nd _ _ _ _ _ _ Σ₁').
-
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
- apply nd_prod; [ idtac | apply nd_id ].
- eapply nd_comp; [ idtac | eapply precompose' ].
- apply nd_rule.
- apply RArrange.
- apply ALeft.
- apply ACanL.
-
destruct case_RCut.
simpl.
destruct l as [|ec lev]; simpl.
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.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ idtac | eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; [ idtac | eapply boost ].
induction x.
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