From 6a7c6977507488245ba4b8cabcf323920c25baef Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 30 May 2011 18:30:46 -0700 Subject: [PATCH 1/1] let RCut take a left environment as well --- src/HaskFlattener.v | 25 +++++++++++++++---------- src/HaskProof.v | 13 ++++++++++++- src/HaskProofToLatex.v | 2 +- src/HaskProofToStrong.v | 11 ++++++++++- src/HaskSkolemizer.v | 42 ++++++++++++++++++++++++++++-------------- src/HaskStrongToProof.v | 4 ++-- 6 files changed, 68 insertions(+), 29 deletions(-) diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index d822dd6..c42842a 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -831,9 +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 _ + | 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 _ @@ -1022,41 +1022,46 @@ Section HaskFlattener. 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. diff --git a/src/HaskProof.v b/src/HaskProof.v index b01f5c2..8c6acf4 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -71,7 +71,7 @@ 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] +| RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l] | RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l] | RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l] @@ -97,6 +97,17 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := [Γ > Δ > (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) *) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index b787d3e..323c1d6 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -190,7 +190,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" - | RCut _ _ _ _ _ _ _ => "Cut" + | RCut _ _ _ _ _ _ _ _ => "Cut" | RLeft _ _ _ _ _ _ => "Left" | RRight _ _ _ _ _ _ => "Right" | RWhere _ _ _ _ _ _ _ _ => "Where" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 2ea0c4a..8cbebce 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -764,7 +764,7 @@ 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 _ + | 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 _ @@ -914,9 +914,18 @@ Section HaskProofToStrong. 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. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 9d8dd4d..b1d65e6 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -232,9 +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 _ + | 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 _ @@ -429,24 +429,38 @@ Section HaskSkolemizer. 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 ]. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 113955f..35373a7 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -961,7 +961,7 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : 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. @@ -1019,7 +1019,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : 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. -- 1.7.10.4