From d97b00a6ff6e8e2244927d17bda4b9762fc3d716 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 30 May 2011 18:58:37 -0700 Subject: [PATCH] remove RLet and RWhere --- src/HaskFlattener.v | 83 ++++++++--------------------------------------- src/HaskProof.v | 23 +++++++++---- src/HaskProofToLatex.v | 2 -- src/HaskProofToStrong.v | 46 -------------------------- src/HaskSkolemizer.v | 54 ++---------------------------- src/HaskStrongToProof.v | 2 +- 6 files changed, 34 insertions(+), 176 deletions(-) diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index c42842a..1731aad 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -288,7 +288,7 @@ Section HaskFlattener. 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. @@ -304,7 +304,7 @@ Section HaskFlattener. [ Γ > Δ > 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. @@ -327,7 +327,7 @@ Section HaskFlattener. [ Γ > Δ > 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. @@ -348,7 +348,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@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. @@ -371,7 +371,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@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. @@ -394,12 +394,12 @@ Section HaskFlattener. [Γ > Δ > Σ,,[@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. @@ -450,14 +450,14 @@ Section HaskFlattener. 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'. @@ -537,13 +537,13 @@ Section HaskFlattener. 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 ]. @@ -576,7 +576,7 @@ Section HaskFlattener. 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. @@ -643,7 +643,7 @@ Section HaskFlattener. 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. @@ -830,11 +830,9 @@ Section HaskFlattener. | 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 _ | 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 _ @@ -958,59 +956,6 @@ Section HaskFlattener. 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. @@ -1277,7 +1222,7 @@ Section HaskFlattener. 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. diff --git a/src/HaskProof.v b/src/HaskProof.v index 8c6acf4..5e6fac4 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -68,9 +68,6 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := (* order is important here; we want to be able to skolemize without introducing new AExch'es *) | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l] -| 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] @@ -109,6 +106,23 @@ Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, apply AuCanL. Defined. +Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ 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. + eapply nd_rule; eapply RArrange; eapply AuCanL. + Defined. + +Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, + ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]. + intros. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply RCut. + Defined. + (* A rule is considered "flat" if it is neither RBrak nor REsc *) (* TODO: change this to (if RBrak/REsc -> False) *) Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := @@ -123,7 +137,6 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l) | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 ) | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) -| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) | Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l) | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). @@ -159,8 +172,6 @@ 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. 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 323c1d6..716a983 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -189,11 +189,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo" | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" - | RLet _ _ _ _ _ _ _ => "Let" | RCut _ _ _ _ _ _ _ _ => "Cut" | RLeft _ _ _ _ _ _ => "Left" | RRight _ _ _ _ _ _ => "Right" - | RWhere _ _ _ _ _ _ _ _ => "Where" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 8cbebce..0d90d4c 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -763,11 +763,9 @@ Section HaskProofToStrong. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ | 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 _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ @@ -869,50 +867,6 @@ Section HaskProofToStrong. simpl in *. apply (EApp _ _ _ _ _ _ q1' q2'). - destruct case_RLet. - eapply rlet. - apply X_. - - destruct case_RWhere. - apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - destruct vars2; try destruct o; inversion H2. - clear H2. - - assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. - refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (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,,([vnew],,vars2_2)) _ >>>= fun X0' => _). - apply FreshMon. - simpl. - inversion pf1. - rewrite H3. - rewrite H4. - rewrite pf2. - reflexivity. - - refine (X0 ξ vars2_1 _ >>>= fun X1' => _). - apply FreshMon. - reflexivity. - apply FreshMon. - - apply ILeaf. - apply ileaf in X0'. - apply ileaf in X1'. - simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X1'. - apply X0'. - destruct case_RCut. apply rassoc. apply swapr. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index b1d65e6..435b687 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -231,11 +231,9 @@ Section HaskSkolemizer. | 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 _ | 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 _ @@ -372,56 +370,8 @@ Section HaskSkolemizer. eapply take_unarrange. eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. - eapply nd_rule; eapply SFlat; apply RWhere. - - destruct case_RLet. - simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RLet. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - - eapply nd_comp. - eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ]. - - set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ]. - apply nd_prod. - apply nd_id. - apply nd_rule. - eapply SFlat. - eapply RArrange. - eapply AuAssoc. - - destruct case_RWhere. - simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RWhere. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - - eapply nd_comp. - eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. - 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 RWhere ]. - apply nd_prod; [ idtac | eapply nd_id ]. - eapply nd_rule; apply SFlat; eapply RArrange. - eapply AComp. - eapply AuAssoc. - apply ALeft. - eapply AuAssoc. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply SFlat; eapply RCut. destruct case_RCut. simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ]. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 35373a7..1f1229d 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -1189,7 +1189,7 @@ Definition expr2proof : inversion H. destruct case_ELet; intros; simpl in *. - 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 pf_let. -- 1.7.10.4