From: Adam Megacz Date: Sun, 29 May 2011 22:48:51 +0000 (-0700) Subject: add RCut, RLeft, RRight rules X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=c90b598203ef23bf8d44d6b5b4a5a4b5901039cf add RCut, RLeft, RRight rules --- diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 1bb35c6..c5587c1 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -784,6 +784,21 @@ Section HaskFlattener. admit. Qed. + 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_proof : forall {h}{c}, ND SRule h c -> @@ -816,6 +831,9 @@ Section HaskFlattener. | 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 _ @@ -1000,6 +1018,125 @@ Section HaskFlattener. 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 unlev_relev. + 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 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 ]. + 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. + 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 ]. + 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. diff --git a/src/HaskProof.v b/src/HaskProof.v index 9787c62..46009f8 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -73,6 +73,10 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l] | RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ 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] + | RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ] | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l] @@ -147,6 +151,9 @@ Lemma no_rules_with_multiple_conclusions : forall c h, destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. Qed. Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 99af119..dedc152 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -190,6 +190,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" + | RCut _ _ _ _ _ _ _ => "Cut" + | RLeft _ _ _ _ _ _ => "Left" + | RRight _ _ _ _ _ _ => "Right" | RWhere _ _ _ _ _ _ _ _ => "Where" | RJoin _ _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 299a83b..b16d4a8 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -509,6 +509,242 @@ Section HaskProofToStrong. Defined. + Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), + FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. + intros Γ Σ. + induction Σ; intro ξ. + destruct a. + destruct l as [τ l]. + set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q. + refine (q >>>= fun q' => return _). + apply FreshMon. + clear q. + destruct q' as [varstypes [pf1 [pf2 distpf]]]. + exists (mapOptionTree (@fst _ _) varstypes). + exists (update_xi ξ l (leaves varstypes)). + symmetry; auto. + refine (return _). + exists []. + exists ξ; auto. + refine (bind f1 = IHΣ1 ξ ; _). + apply FreshMon. + destruct f1 as [vars1 [ξ1 pf1]]. + refine (bind f2 = IHΣ2 ξ1 ; _). + apply FreshMon. + destruct f2 as [vars2 [ξ2 pf22]]. + refine (return _). + exists (vars1,,vars2). + exists ξ2. + simpl. + rewrite pf22. + rewrite pf1. + admit. (* freshness assumption *) + Defined. + + Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p : + forall (X_ : ITree Judg judg2exprType + ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])), + ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p]. + intros. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + + refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). + apply FreshMon. + + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + inversion X_. + apply ileaf in X. + apply ileaf in X0. + simpl in *. + + refine (X ξ vars1 _ >>>= fun X0' => _). + apply FreshMon. + simpl. + auto. + + refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). + apply FreshMon. + simpl. + rewrite pf2. + rewrite pf1. + reflexivity. + apply FreshMon. + + apply ILeaf. + apply ileaf in X1'. + apply ileaf in X0'. + simpl in *. + apply ELet with (ev:=vnew)(tv:=σ₁). + apply X0'. + apply X1'. + Defined. + + Definition vartree Γ Δ Σ lev ξ : + forall vars, Σ @@@ lev = mapOptionTree ξ vars -> + ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ. + induction Σ; intros. + destruct a. + intros; simpl in *. + apply ILeaf. + destruct vars; try destruct o; inversion H. + set (EVar Γ Δ ξ v) as q. + rewrite <- H1 in q. + apply q. + intros. + apply INone. + intros. + destruct vars; try destruct o; inversion H. + apply IBranch. + eapply IHΣ1. + apply H1. + eapply IHΣ2. + apply H2. + Defined. + + + Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + apply X0. + Defined. + + Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + auto. + Defined. + + Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + eapply X with (vars:=[],,vars). + rewrite H; reflexivity. + Defined. + + Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + eapply X with (vars:=vars2). + auto. + Defined. + + Definition rassoc Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars2; try destruct o; inversion H2. + apply X with (vars:=(vars1,,vars2_1),,vars2_2). + subst; reflexivity. + Defined. + + Definition rassoc' Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=vars1_1,,(vars1_2,,vars2)). + subst; reflexivity. + Defined. + + Definition swapr Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=(vars1_2,,vars1_1),,vars2). + subst; reflexivity. + Defined. + + Definition rdup Γ Δ Σ₁ a c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *) + subst; reflexivity. + Defined. + + (* holy cow this is ugly *) + Definition rcut Γ Δ Σ₃ lev Σ₁₂ : + forall Σ₁ Σ₂, + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev]. + + induction Σ₁₂. + intros. + destruct a. + + eapply rlet. + apply IBranch. + apply X. + apply X0. + + simpl in X0. + apply rdrop'' in X0. + apply rdrop'''. + apply X0. + + intros. + simpl in X0. + apply rassoc in X0. + set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q. + set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'. + apply rassoc' in q. + apply swapr in q. + apply rassoc in q. + set (q' q) as q''. + apply rassoc' in q''. + apply rdup in q''. + apply q''. + Defined. Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j. @@ -528,6 +764,9 @@ Section HaskProofToStrong. | 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 _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ | RJoin Γ p lri m x q l => let case_RJoin := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ @@ -645,40 +884,8 @@ Section HaskProofToStrong. apply (EApp _ _ _ _ _ _ q1' q2'). destruct case_RLet. - apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - - refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). - apply FreshMon. - - destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - - refine (X ξ vars1 _ >>>= fun X0' => _). - apply FreshMon. - simpl. - auto. - - refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). - apply FreshMon. - simpl. - rewrite pf2. - rewrite pf1. - reflexivity. - apply FreshMon. - - apply ILeaf. - apply ileaf in X1'. - apply ileaf in X0'. - simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X0'. - apply X1'. + eapply rlet. + apply X_. destruct case_RWhere. apply ILeaf. @@ -720,6 +927,57 @@ Section HaskProofToStrong. apply X1'. apply X0'. + destruct case_RCut. + inversion X_. + subst. + clear X_. + induction Σ₃. + destruct a. + subst. + eapply rcut. + apply X. + apply X0. + + apply ILeaf. + simpl. + intros. + refine (return _). + apply INone. + set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1. + set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2. + apply ileaf in q1. + apply ileaf in q2. + simpl in *. + apply ILeaf. + simpl. + intros. + refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _). + apply FreshMon. + apply FreshMon. + apply IBranch; auto. + + destruct case_RLeft. + apply ILeaf. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H2 >>>= fun X' => return _). + apply FreshMon. + apply IBranch. + eapply vartree. + apply H1. + apply X'. + + destruct case_RRight. + apply ILeaf. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H1 >>>= fun X' => return _). + apply FreshMon. + apply IBranch. + apply X'. + eapply vartree. + apply H2. + destruct case_RVoid. apply ILeaf; simpl; intros. refine (return _). @@ -825,38 +1083,6 @@ Section HaskProofToStrong. | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q) end. - Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), - FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. - intros Γ Σ. - induction Σ; intro ξ. - destruct a. - destruct l as [τ l]. - set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q. - refine (q >>>= fun q' => return _). - apply FreshMon. - clear q. - destruct q' as [varstypes [pf1 [pf2 distpf]]]. - exists (mapOptionTree (@fst _ _) varstypes). - exists (update_xi ξ l (leaves varstypes)). - symmetry; auto. - refine (return _). - exists []. - exists ξ; auto. - refine (bind f1 = IHΣ1 ξ ; _). - apply FreshMon. - destruct f1 as [vars1 [ξ1 pf1]]. - refine (bind f2 = IHΣ2 ξ1 ; _). - apply FreshMon. - destruct f2 as [vars2 [ξ2 pf22]]. - refine (return _). - exists (vars1,,vars2). - exists ξ2. - simpl. - rewrite pf22. - rewrite pf1. - admit. - Defined. - Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★) {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}). diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 259d24e..6b6c756 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -232,6 +232,9 @@ Section HaskSkolemizer. | 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 _ @@ -429,6 +432,73 @@ Section HaskSkolemizer. apply ALeft. eapply AuAssoc. + destruct case_RCut. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''. + 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 (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + rewrite <- e. + eapply nd_comp. + eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; 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. + + destruct case_RLeft. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + apply nd_rule. + eapply SFlat. + eapply RLeft. + + destruct case_RRight. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ]. + 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 AExch ]. (* yuck *) + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + eapply nd_rule. + eapply SFlat. + apply RRight. + destruct case_RVoid. simpl. destruct l.