From: Adam Megacz Date: Tue, 29 Mar 2011 08:05:18 +0000 (-0700) Subject: swap the order of the hypotheses of RLet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=75a5863eb9fb6cdfa1f07e538f6f948ffec80331;hp=148579e5c8f6b60209a442222b932cf59f163cca swap the order of the hypotheses of RLet --- diff --git a/src/HaskProof.v b/src/HaskProof.v index 4cc4605..8802223 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -80,7 +80,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] -| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] +| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] | REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] | RAbsT : ∀ Γ Δ Σ κ σ l, diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 0218ddd..2b63c4a 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -25,12 +25,6 @@ Section HaskProofToStrong. Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★. - Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type := - match j with - mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) - end. - Definition judg2exprType (j:Judg) : Type := match j with (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> @@ -228,16 +222,21 @@ Section HaskProofToStrong. inversion pf2. Defined. + Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type := + forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ). + Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), - ujudg2exprType ξ (Γ >> Δ > h |- t) -> - ujudg2exprType ξ (Γ >> Δ > j |- t) + ujudg2exprType Γ ξ Δ h t -> + ujudg2exprType Γ ξ Δ j t . intros Γ Δ. refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : - ujudg2exprType ξ (Γ >> Δ > h |- t) -> - ujudg2exprType ξ (Γ >> Δ > j |- t) := - match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) -> - ujudg2exprType ξ (Γ >> Δ > C |- t) with + ujudg2exprType Γ ξ Δ h t -> + ujudg2exprType Γ ξ Δ j t := + match r as R in Arrange H C return + ujudg2exprType Γ ξ Δ H t -> + ujudg2exprType Γ ξ Δ C t + with | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r) | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r) | RCanL a => let case_RCanL := tt in _ @@ -253,31 +252,31 @@ Section HaskProofToStrong. end); clear urule2expr; intros. destruct case_RCanL. - simpl; intros. + simpl; unfold ujudg2exprType; intros. simpl in X. apply (X ([],,vars)). simpl; rewrite <- H; auto. destruct case_RCanR. - simpl; intros. + simpl; unfold ujudg2exprType; intros. simpl in X. apply (X (vars,,[])). simpl; rewrite <- H; auto. destruct case_RuCanL. - simpl; intros. + simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars2); auto. destruct case_RuCanR. - simpl; intros. + simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars1); auto. destruct case_RAssoc. - simpl; intros. + simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. destruct vars1; try destruct o; inversion H. @@ -285,7 +284,7 @@ Section HaskProofToStrong. subst; auto. destruct case_RCossa. - simpl; intros. + simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. destruct vars2; try destruct o; inversion H. @@ -293,20 +292,20 @@ Section HaskProofToStrong. subst; auto. destruct case_RExch. - simpl; intros. + simpl; unfold ujudg2exprType ; intros. simpl in X. destruct vars; try destruct o; inversion H. apply (X (vars2,,vars1)). inversion H; subst; auto. destruct case_RWeak. - simpl; intros. + simpl; unfold ujudg2exprType; intros. simpl in X. apply (X []). auto. destruct case_RCont. - simpl; intros. + simpl; unfold ujudg2exprType ; intros. simpl in X. apply (X (vars,,vars)). simpl. @@ -314,12 +313,13 @@ Section HaskProofToStrong. auto. destruct case_RLeft. - intro vars; intro H. + intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars2 H2). clear r0 e H2. simpl in X. simpl. + unfold ujudg2exprType. intros. apply X with (vars:=vars1,,vars). rewrite H0. @@ -328,12 +328,13 @@ Section HaskProofToStrong. reflexivity. destruct case_RRight. - intro vars; intro H. + intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars1 H1). clear r0 e H2. simpl in X. simpl. + unfold ujudg2exprType. intros. apply X with (vars:=vars,,vars2). rewrite H0. @@ -534,6 +535,7 @@ Section HaskProofToStrong. simpl in q'. apply q' with (vars:=vars). clear q' q. + unfold ujudg2exprType. intros. apply X_ with (vars:=vars0). auto. @@ -645,10 +647,11 @@ Section HaskProofToStrong. apply ileaf in X. apply ileaf in X0. simpl in *. - refine (X0 ξ vars2 _ >>>= fun X0' => _). + refine (X ξ vars2 _ >>>= fun X0' => _). apply FreshMon. auto. - refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _). + + refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _). apply FreshMon. rewrite H1. simpl. @@ -656,6 +659,7 @@ Section HaskProofToStrong. rewrite pf1. rewrite H1. reflexivity. + refine (return _). apply ILeaf. apply ileaf in X0'. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index b0c5b11..c29963e 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -826,10 +826,11 @@ Definition expr2proof : destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; [ idtac | apply pf_let]. - clear pf_let. - eapply nd_comp; [ apply pf_body | idtac ]. - clear pf_body. + apply nd_prod. + apply pf_let. + clear pf_let. + eapply nd_comp; [ apply pf_body | idtac ]. + clear pf_body. fold (@mapOptionTree VV). fold (mapOptionTree ξ). set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.