From: Adam Megacz Date: Mon, 30 May 2011 23:22:42 +0000 (-0700) Subject: remove RJoin rule X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=171beb27508a340b24ab14837e72451d0b500805;hp=1a562d1799fa63f750837833093cb9d6296d9fc1 remove RJoin rule --- diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index d805de4..d822dd6 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -835,7 +835,6 @@ Section HaskFlattener. | 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 _ @@ -931,12 +930,6 @@ Section HaskFlattener. 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. diff --git a/src/HaskProof.v b/src/HaskProof.v index 46009f8..b01f5c2 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -65,8 +65,6 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l] -| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ] - (* 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] @@ -115,7 +113,6 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | 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_RJoin : ∀ q a b c d e l, Rule_Flat (RJoin q a b c d e 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). @@ -153,7 +150,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. 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 dedc152..b787d3e 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -194,7 +194,6 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RLeft _ _ _ _ _ _ => "Left" | RRight _ _ _ _ _ _ => "Right" | RWhere _ _ _ _ _ _ _ _ => "Where" - | RJoin _ _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" @@ -223,7 +222,8 @@ Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with | RArrange _ _ _ _ _ _ r => nd_hideURule r | RVoid _ _ _ => true - | RJoin _ _ _ _ _ _ _ => true + | RLeft _ _ _ _ _ _ => true + | RRight _ _ _ _ _ _ => true | _ => false end. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index b16d4a8..2ea0c4a 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -768,7 +768,6 @@ Section HaskProofToStrong. | 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 _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ @@ -849,19 +848,6 @@ Section HaskProofToStrong. apply ileaf in X. simpl in X. apply X. - destruct case_RJoin. - apply ILeaf; simpl; intros. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - destruct vars; inversion H. - destruct o; inversion H3. - refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _). - apply FreshMon. - apply FreshMon. - apply IBranch; auto. - destruct case_RApp. apply ILeaf. inversion X_. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 6b6c756..9d8dd4d 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -236,7 +236,6 @@ Section HaskSkolemizer. | 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 _ @@ -351,14 +350,6 @@ Section HaskSkolemizer. apply γ. apply (Prelude_error "found RCast at level >0"). - destruct case_RJoin. - simpl. - destruct l. - apply nd_rule. - apply SFlat. - apply RJoin. - apply (Prelude_error "found RJoin at level >0"). - destruct case_RApp. simpl. destruct lev. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 1b9f6af..113955f 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -961,10 +961,13 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; auto. - Defined. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply IHX1. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply IHX2. + Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), @@ -1015,10 +1018,14 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod; auto. - Defined. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply pf. + Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,