From 539d675a181f178e24c15b2a6ad3c990492eed79 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 23:10:41 -0700 Subject: [PATCH] require all branches of LetRec be at the same level in HaskProof --- src/Extraction.v | 1 - src/HaskProof.v | 2 +- src/HaskProofToLatex.v | 2 +- src/HaskProofToStrong.v | 230 ++++++++++++++------------ src/HaskStrong.v | 19 ++- src/HaskStrongToProof.v | 422 ++++++++++++++++++++++++----------------------- src/HaskStrongToWeak.v | 2 +- src/HaskStrongTypes.v | 26 ++- src/HaskWeakToStrong.v | 22 ++- 9 files changed, 395 insertions(+), 331 deletions(-) diff --git a/src/Extraction.v b/src/Extraction.v index 43d404f..d1c84e4 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -230,7 +230,6 @@ Section core2proof. (* Definition TInt : HaskType nil ★. assert (tyConKind' intPrimTyCon = ★). - admit. rewrite <- H. unfold HaskType; intros. apply TCon. diff --git a/src/HaskProof.v b/src/HaskProof.v index e0cef35..046e28e 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -109,7 +109,7 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l, Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] -| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ] +| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)), Rule diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 56cd747..1471e51 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -184,7 +184,7 @@ Section ToLatex. | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" | RBindingGroup _ _ _ _ _ _ => "RBindingGroup" - | RLetRec _ _ _ _ _ => "LetRec" + | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" | REsc _ _ _ _ _ _ => "Esc" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 65c638e..6f75235 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -47,8 +47,8 @@ Section HaskProofToStrong. apply X0. Defined. - Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) l1 l2 q, - update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) l1 q. + Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q, + update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q. intros. induction l1. reflexivity. @@ -58,14 +58,6 @@ Section HaskProofToStrong. reflexivity. Qed. - Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t). - intros. - induction t. - destruct a; auto. - simpl; rewrite H; auto. - simpl; rewrite IHt1; rewrite IHt2; auto. - Qed. - Lemma quark {T} (l1:list T) l2 vf : (In vf (app l1 l2)) <-> (In vf l1) \/ (In vf l2). @@ -134,29 +126,44 @@ Section HaskProofToStrong. Qed. Lemma fresh_lemma' Γ - : forall types vars Σ ξ, Σ = mapOptionTree ξ vars -> + : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars -> FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ - /\ mapOptionTree (update_ξ ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }. + | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ + /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. induction types. intros; destruct a. refine (bind vf = fresh (leaves vars) ; return _). apply FreshMon. destruct vf as [ vf vf_pf ]. - exists [(vf,l)]. + exists [(vf,h)]. split; auto. simpl. - set (helper VV _ vars vf ξ l vf_pf) as q. + set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q. rewrite q. symmetry; auto. simpl. destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto. + split; auto. + apply distinct_cons. + intro. + inversion H0. + apply distinct_nil. refine (return _). exists []; auto. - intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _). + split. + simpl. + symmetry; auto. + split. + simpl. + reflexivity. + simpl. + apply distinct_nil. + intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _). apply FreshMon. - destruct x2 as [vt2 [pf21 pf22]]. - refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _). + destruct x2 as [vt2 [pf21 [pf22 pfdist]]]. + refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev + (leaves vt2)) _ _; return _). apply FreshMon. simpl. rewrite pf21. @@ -166,7 +173,7 @@ Section HaskProofToStrong. destruct x1 as [vt1 [pf11 pf12]]. exists (vt1,,vt2); split; auto. - set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q. set (mapOptionTree_extensional _ _ q) as q'. rewrite q'. clear q' q. @@ -174,7 +181,7 @@ Section HaskProofToStrong. reflexivity. simpl. - set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q. set (mapOptionTree_extensional _ _ q) as q'. rewrite q'. rewrite q'. @@ -182,23 +189,27 @@ Section HaskProofToStrong. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose in *. - rewrite pf12. + split. + destruct pf12. + rewrite H. inversion pf11. rewrite <- mapOptionTree_compose. reflexivity. + + admit. Defined. - Lemma fresh_lemma Γ ξ vars Σ Σ' + Lemma fresh_lemma Γ ξ vars Σ Σ' lev : Σ = mapOptionTree ξ vars -> FreshM { vars' : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ ((vars',Σ')::nil)) vars = Σ - /\ mapOptionTree (update_ξ ξ ((vars',Σ')::nil)) [vars'] = [Σ'] }. + | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ + /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. intros. - set (fresh_lemma' Γ [Σ'] vars Σ ξ H) as q. + set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q. refine (q >>>= fun q' => return _). apply FreshMon. clear q. - destruct q' as [varstypes [pf1 pf2]]. + destruct q' as [varstypes [pf1 [pf2 pfdist]]]. destruct varstypes; try destruct o; try destruct p; simpl in *. destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]. inversion pf2; subst. @@ -209,19 +220,6 @@ Section HaskProofToStrong. inversion pf2. Defined. - Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), - FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. - intros. - set (fresh_lemma' Γ Σ [] [] ξ0 (refl_equal _)) as q. - refine (q >>>= fun q' => return _). - apply FreshMon. - clear q. - destruct q' as [varstypes [pf1 pf2]]. - exists (mapOptionTree (@fst _ _) varstypes). - exists (update_ξ ξ0 (leaves varstypes)). - symmetry; auto. - Defined. - Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★), ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j. @@ -388,94 +386,93 @@ Section HaskProofToStrong. apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto. Defined. - Definition letrec_helper Γ Δ l varstypes ξ' : + Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : ITree (LeveledHaskType Γ ★) (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t) (mapOptionTree (ξ' ○ (@fst _ _)) varstypes) - -> ELetRecBindings Γ Δ ξ' l - (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) varstypes). + -> ELetRecBindings Γ Δ ξ' l varstypes. intros. induction varstypes. destruct a; simpl in *. destruct p. - destruct l0 as [τ l']. simpl. apply ileaf in X. simpl in X. - destruct (eqd_dec (unlev (ξ' v)) τ). - rewrite <- e. apply ELR_leaf. + rename h into τ. + destruct (eqd_dec (unlev (ξ' v)) τ). + rewrite <- e. destruct (ξ' v). simpl. destruct (eqd_dec h0 l). rewrite <- e0. apply X. - apply (Prelude_error "level mismatch; should never happen"). - apply (Prelude_error "letrec type mismatch; should never happen"). + apply (Prelude_error "level mismatch; should never happen"). + apply (Prelude_error "letrec type mismatch; should never happen"). apply ELR_nil. - - simpl; apply ELR_branch. - apply IHvarstypes1. - simpl in X. - inversion X; auto. - apply IHvarstypes2. - simpl in X. - inversion X; auto. - + apply ELR_branch. + apply IHvarstypes1; inversion X; auto. + apply IHvarstypes2; inversion X; auto. Defined. - Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t. - induction t; auto. - simpl. - rewrite IHt; auto. - Qed. - Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) : forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars, - judg2exprType (pcb_judg pcb) -> - (pcb_freevars pcb) = mapOptionTree ξ Σ -> - FreshM - {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars & + judg2exprType (pcb_judg pcb) -> + (pcb_freevars pcb) = mapOptionTree ξ Σ -> + FreshM + {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars & Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}. + intros. simpl in X. destruct pcb. simpl in *. set (sac_types pcb_scb _ avars) as boundvars. - refine (fresh_lemma' _ (unleaves (map (fun x => x@@(weakL' lev)) (vec2list boundvars))) Σ - (mapOptionTree weakLT' pcb_freevars) - (weakLT' ○ ξ) _ + refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _ >>>= fun ξvars => _). apply FreshMon. rewrite H. rewrite <- mapOptionTree_compose. reflexivity. - destruct ξvars as [ exprvars [pf1 pf2 ]]. + destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]]. set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'. + + assert (distinct (vec2list exprvars')) as pfdistinct'. + unfold exprvars'. + rewrite vec2list_list2vec. + apply pfdistinct. + assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'. rewrite <- mapOptionTree_compose in pf2. simpl in pf2. rewrite mapleaves. rewrite <- map_preserves_length. - rewrite map_preserves_length with (f:=update_ξ (weakLT' ○ ξ) (leaves exprvars) ○ (@fst _ _)). + rewrite map_preserves_length with (f:= + (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ) + (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ) + (@weakL' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev) + (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))). rewrite <- mapleaves. - rewrite pf2. + rewrite pf2. + rewrite <- mapleaves'. rewrite leaves_unleaves. rewrite vec2list_map_list2vec. rewrite vec2list_len. reflexivity. - rewrite <- H' in exprvars'. - clear H'. - set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars') as scb. - set (scbwv_ξ scb ξ lev) as ξ'. - refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon. + clear pfdistinct'. + rewrite <- H' in exprvars'. + clear H'. + assert (distinct (vec2list exprvars')) as pfdistinct'. + admit. + + set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') as scb. + set (scbwv_ξ scb ξ lev) as ξ'. + refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon. simpl. unfold ξ'. unfold scbwv_ξ. simpl. - rewrite <- vec2list_map_list2vec. - rewrite <- pf1. admit. apply ileaf in X'. @@ -529,7 +526,7 @@ Section HaskProofToStrong. | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ - | RLetRec Γ Δ lri x y => let case_RLetRec := tt in _ + | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _ end); intro X_; try apply ileaf in X_; simpl in X_. destruct case_RURule. @@ -579,10 +576,10 @@ Section HaskProofToStrong. destruct case_RLam. apply ILeaf. simpl in *; intros. - refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)). + refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ ((⟨vnew, tx @@ x ⟩) :: nil)) as ξ' in *. + set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *. refine (X_ ξ' (vars,,[vnew]) _ >>>= _). apply FreshMon. simpl. @@ -644,10 +641,10 @@ Section HaskProofToStrong. apply ILeaf. simpl in *; intros. destruct vars; try destruct o; inversion H. - refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)). + refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *. + set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. @@ -706,34 +703,24 @@ Section HaskProofToStrong. destruct case_RLetRec. apply ILeaf; simpl; intros. - refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon. - destruct ξvars as [ varstypes [ pf1 pf2 ]]. - refine (X_ ((update_ξ ξ (leaves varstypes))) + refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. + destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. + refine (X_ ((update_ξ ξ t (leaves varstypes))) (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. rewrite pf1. auto. apply ILeaf. - destruct x as [τ l]. inversion X; subst; clear X. - (* getting rid of this will require strengthening RLetRec *) - assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH. - admit. - - apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes)); - rewrite mapleaves; rewrite <- map_compose; simpl; - [ idtac - | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ]. - - clear X0. - rewrite <- mapOptionTree_compose in X1. - set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *. - rewrite <- mapleaves. - rewrite HHH. - - apply (letrec_helper _ _ _ _ _ X1). + apply (@ELetRec _ _ _ _ _ _ _ varstypes). + apply (@letrec_helper Γ Δ t varstypes). + rewrite <- pf2 in X1. + rewrite mapOptionTree_compose. + apply X1. + apply ileaf in X0. + apply X0. destruct case_RCase. apply ILeaf; simpl; intros. @@ -743,12 +730,11 @@ Section HaskProofToStrong. apply ileaf in X0. simpl in X0. set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *. - refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _). + refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev H ; _). apply FreshMon. destruct vars; try destruct o; inversion H; clear H. rename vars1 into varsalts. rename vars2 into varsΣ. - refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto. apply FreshMon. @@ -776,6 +762,38 @@ Section HaskProofToStrong. end)); clear closed2expr'; intros; subst. 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_ξ ξ 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 Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 1e1ce43..151e8d2 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -21,11 +21,11 @@ Section HaskStrong. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} := - { scbwv_sac : @StrongAltCon tc - ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac) - ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes) - ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list - (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes)) + { scbwv_sac : @StrongAltCon tc + ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac) + ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) + ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes) + ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon. @@ -38,8 +38,8 @@ Section HaskStrong. | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) - | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) - | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) + | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, @@ -61,7 +61,8 @@ Section HaskStrong. (weakLT' (tbranches@@l)) } -> Expr Γ Δ ξ (tbranches @@ l) - | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in + | ELetRec : ∀ Γ Δ ξ l τ vars, + let ξ' := update_ξ ξ l (leaves vars) in ELetRecBindings Γ Δ ξ' l vars -> Expr Γ Δ ξ' (τ@@l) -> Expr Γ Δ ξ (τ@@l) @@ -69,7 +70,7 @@ Section HaskStrong. (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *) with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type := | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l [] - | ELR_leaf : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))] + | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)] | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) . diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 143be0b..d17dd38 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -56,13 +56,11 @@ Definition copyAndPivotContext {Γ}{Δ} a b c τ : Context {VV:Type}{eqd_vv:EqDecidable VV}. (* maintenance of Xi *) - Definition dropVar (lv:list VV)(v:VV) : ??VV := - if fold_left - (fun a b:bool => if a then true else if b then true else false) - (map (fun lvv => if eqd_dec lvv v then true else false) lv) - false - then None - else Some v. + Fixpoint dropVar (lv:list VV)(v:VV) : ??VV := + match lv with + | nil => Some v + | v'::lv' => if eqd_dec v v' then None else dropVar lv' v + end. (* later: use mapOptionTreeAndFlatten *) Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV := mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end). @@ -104,7 +102,7 @@ end with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e + | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. @@ -121,27 +119,28 @@ Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} |}. Defined. -Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) := + +Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [ξ v] + | ELR_leaf Γ Δ ξ lev v t e => [t] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2) end. - +(* Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [v] + | ELR_leaf Γ Δ ξ lev v _ _ e => [v] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) end. -Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):= +Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):= match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)] + | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) end. - +*) Lemma stripping_nothing_is_inert {Γ:TypeEnv} @@ -154,12 +153,14 @@ Lemma stripping_nothing_is_inert fold stripOutVars. simpl. fold (stripOutVars nil). - rewrite IHtree1. - rewrite IHtree2. + rewrite <- IHtree1 at 2. + rewrite <- IHtree2 at 2. reflexivity. Qed. - +Ltac eqd_dec_refl X := + destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2]; + [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]. Definition arrangeContext (Γ:TypeEnv)(Δ:CoercionEnv Γ) @@ -179,17 +180,18 @@ Definition arrangeContext [Γ >> Δ > mapOptionTree ξ ctx |- τ] [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]). - induction ctx; simpl in *. + induction ctx. - refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *. + refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end). (* nonempty leaf *) destruct case_Some. unfold stripOutVars in *; simpl. unfold dropVar. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - destruct (eqd_dec v v'); simpl in *. + destruct (eqd_dec v' v); subst. + (* where the leaf is v *) apply inr. subst. @@ -287,12 +289,51 @@ Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : refine (ext_left _ _ _ (nd_rule (RWeak _ _))). Defined. +Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t). + unfold stripOutVars. + rewrite <- mapTree_compose. + induction t; try destruct a0. + simpl. + induction x. + reflexivity. + admit. + subst. + reflexivity. + simpl in *. + rewrite <- IHt1. + rewrite <- IHt2. + reflexivity. + Qed. + +Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t. + induction x. + simpl. + admit. + rewrite strip_lemma. + rewrite IHx. + rewrite <- strip_lemma. + admit. + Qed. + +Lemma distinct_app1 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1. + admit. + Qed. + +Lemma distinct_app2 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l2. + admit. + Qed. + +Lemma strip_distinct x y : distinct (app (leaves y) x) -> stripOutVars x y = y. + admit. + Qed. + Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, + distinct (leaves v) -> ND (@URule Γ Δ) [Γ >> Δ>(mapOptionTree ξ ctx) |- z] [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z]. - induction v. + induction v; intros. destruct a. unfold mapOptionTree in *. simpl in *. @@ -321,37 +362,24 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, simpl in IHv2'. fold (mapOptionTree ξ) in IHv2'. fold X in IHv2'. - set (nd_comp (IHv1 _ _) IHv2') as qq. + set (nd_comp (IHv1 _ _ (distinct_app1 _ _ _ H)) (IHv2' (distinct_app2 _ _ _ H))) as qq. eapply nd_comp. apply qq. clear qq IHv2' IHv2 IHv1. - - assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)). - admit. - rewrite H. - clear H. - - (* FIXME: this only works because the variables are all distinct, but I need to prove that *) - assert ((stripOutVars (leaves v2) v1) = v1). - admit. - rewrite H. - clear H. + rewrite strip_twice_lemma. + rewrite (strip_distinct (leaves v2) v1). apply nd_rule. apply RCossa. + auto. Defined. -Definition update_ξ'' {Γ} ξ tree lev := -(update_ξ ξ - (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) - (leaves tree))). - -Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev : - mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree) +Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : + mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). induction tree; simpl in *; try reflexivity; auto. - unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ lev ((v,t)::nil))) in *. destruct a; simpl; try reflexivity. unfold update_ξ. simpl. @@ -363,6 +391,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t assert (q=eqd_dec v v0). reflexivity. destruct q. +(* reflexivity. rewrite <- H. reflexivity. @@ -376,135 +405,77 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t rewrite <- IHtree1. rewrite <- IHtree2. reflexivity. +*) +admit. +admit. +admit. Qed. - Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) tree tree2 : - mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) + mapOptionTree (update_ξ ξ lev (leaves tree)) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2). -admit. - Qed. - -Lemma updating_stripped_tree_is_inert'' - {Γ} - (ξ:VV -> LeveledHaskType Γ ★) - v tree lev : - mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree) - = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree). -admit. + admit. Qed. -(* -Lemma updating_stripped_tree_is_inert''' - {Γ} - (ξ:VV -> LeveledHaskType Γ) -{T} - (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree -: - mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree) - = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree). -admit. +Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x, + mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l) + (stripOutVars (vec2list (scbwv_exprvars x)) t) + = + mapOptionTree (weakLT' ○ ξ) + (stripOutVars (vec2list (scbwv_exprvars x)) t). + intros. + unfold scbwv_ξ. + unfold scbwv_varstypes. + admit. Qed. -*) (* IDEA: use multi-conclusion proofs instead *) Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) - | lrsp_leaf : forall v e, - (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) -> - LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e) + | lrsp_leaf : forall v t e , + (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) -> + LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e) | lrsp_cons : forall t1 t2 b1 b2, LetRecSubproofs Γ Δ ξ lev t1 b1 -> LetRecSubproofs Γ Δ ξ lev t2 b2 -> LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2). -Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), - eLetRecTypes branches = - mapOptionTree (update_ξ'' ξ tree lev) - (mapOptionTree (@fst _ _) tree). - intros. - induction branches. - reflexivity. - simpl. - unfold update_ξ. - unfold mapOptionTree; simpl. -admit. -admit. - Qed. -Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts', -mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) -= -(* -((mapOptionTreeAndFlatten -(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) - (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)). -*) -((mapOptionTreeAndFlatten pcb_freevars - (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). -admit. -Qed. -Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l). - admit. - Qed. -Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t. -admit. -Qed. - -Lemma letRecSubproofsToND Γ Δ ξ lev tree branches - : LetRecSubproofs Γ Δ ξ lev tree branches -> - ND Rule [] - [ Γ > Δ > - mapOptionTree ξ (eLetRecContext branches) - |- - eLetRecTypes branches - ]. - intro X. - induction X; intros; simpl in *. +Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : + LetRecSubproofs Γ Δ ξ lev tree branches -> + ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches) + |- eLetRecTypes branches @@@ lev ]. + intro X; induction X; intros; simpl in *. apply nd_rule. apply REmptyGroup. set (ξ v) as q in *. destruct q. simpl in *. - assert (h0=lev). - admit. - rewrite H. apply n. eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. Defined. - -Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev, - mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z. -admit. - Qed. - - - Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body, - ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] -> - LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches -> + ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> + LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches -> ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) - simpl. intro branches. intro body. intro pf. intro lrsp. - set ((update_ξ ξ - (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) - (leaves tree)))) as ξ' in *. + set ((update_ξ ξ lev (leaves tree))) as ξ' in *. set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. set (mapOptionTree (@fst _ _) tree) as pctx. set (mapOptionTree ξ' pctx) as passback. - set (fun a b => @RLetRec Γ Δ a b passback) as z. + set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z. eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. @@ -515,68 +486,99 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : unfold ξ' in *. set (@updating_stripped_tree_is_inert') as zz. - unfold update_ξ'' in *. rewrite zz in q'. clear zz. clear ξ'. - simpl in q'. - + Opaque stripOutVars. + simpl. + rewrite <- mapOptionTree_compose in q'. + cut ((mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree) = (mapOptionTree (@snd _ _) tree @@@ lev)). + intro H'. + rewrite <- H'. eapply nd_comp; [ idtac | apply q' ]. + clear H'. clear q'. - unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)). - simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. - rewrite cheat1 in q. - set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. - unfold update_ξ'' in *. - rewrite <- zz in q. + cut ((eLetRecTypes branches @@@ lev) = mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree). + intro H''. + rewrite <- H''. apply q. + admit. + admit. + admit. Defined. +Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)), + distinct (map (@fst _ _) varstypes) -> + map (update_ξ ξ lev varstypes) (map (@fst _ _) varstypes) = + map (fun t => t@@ lev) (map (@snd _ _) varstypes). + intros. + induction varstypes. + reflexivity. + destruct a. + inversion H. + subst. + admit. + Qed. -Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x, - mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l) - (stripOutVars (vec2list (scbwv_exprvars x)) t) - = - mapOptionTree (weakLT' ○ ξ) - (stripOutVars (vec2list (scbwv_exprvars x)) t). +Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1. admit. Qed. +Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2. + admit. + Defined. -Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches -(x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes) -(e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ)) - (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) , -mapOptionTree (weakLT' ○ ξ) - (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),, -unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l -= -mapOptionTree (weakLT' ○ ξ) - (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),, - mapOptionTree - (update_ξ (weakLT' ○ ξ) - (vec2list - (vec_map - (fun - x0 : VV * - HaskType - (app (vec2list (sac_ekinds x)) Γ) - ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩) - (vec_zip (scbwv_exprvars x) - (sac_types x Γ atypes))))) - (unleaves (vec2list (scbwv_exprvars x))) -. -admit. -Qed. +Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2. + admit. + Defined. +Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} : + forall scb:StrongCaseBranchWithVVs _ _ tc atypes, + forall l ξ, vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb) = + vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes). + intros. + unfold scbwv_ξ. + unfold scbwv_varstypes. + set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) as q. + rewrite vec2list_map_list2vec in q. + rewrite fst_zip in q. + rewrite vec2list_map_list2vec in q. + rewrite vec2list_map_list2vec in q. + rewrite snd_zip in q. + rewrite vec2list_map_list2vec in q. + apply vec2list_injective. + apply q. + apply scbwv_exprvars_distinct. + Qed. +Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts', + mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) + = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). + intros. + simpl. + Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end. + hack. + induction alts'. + simpl. + destruct a. + unfold mkProofCaseBranch. + simpl. + reflexivity. + reflexivity. + simpl. + rewrite IHalts'1. + rewrite IHalts'2. + reflexivity. + rewrite H. + reflexivity. + Qed. Definition expr2proof : @@ -595,14 +597,14 @@ Definition expr2proof : | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree branches ebody => - let ξ' := update_ξ'' ξ tree lev in + let ξ' := update_ξ ξ lev (leaves tree) in let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) -((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) + ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' := match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ - | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e) + | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e) | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) end ) _ _ _ _ tree branches) @@ -624,13 +626,17 @@ Definition expr2proof : (weakLT' (tbranches@@l)) }) : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) := match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with - | T_Leaf None => let case_nil := tt in _ - | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x)) + | T_Leaf None => let case_nil := tt in _ | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2) + | T_Leaf (Some x) => + match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with + existT scbx ex => + (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex) + end end) alts') in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) end -); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. + ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. destruct case_EGlobal. apply nd_rule. @@ -659,12 +665,12 @@ Definition expr2proof : destruct case_ELam; intros. unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. - set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'. + set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx. apply UND_to_ND in pfx. unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx. unfold ξ' in pfx. - fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx. + fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx. rewrite updating_stripped_tree_is_inert in pfx. unfold update_ξ in pfx. destruct (eqd_dec v v). @@ -685,7 +691,7 @@ Definition expr2proof : clear pf_body. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'. + set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. @@ -739,28 +745,33 @@ Definition expr2proof : apply e'. destruct case_leaf. - unfold pcb_judg. + clear o x alts alts' e. + eapply nd_comp; [ apply e' | idtac ]. + clear e'. + set (existT + (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes => + Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))) scbx ex) as stuff. + set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]). + simpl in n. + apply n. + clear n. + + rewrite mapleaves'. simpl. - repeat rewrite <- mapOptionTree_compose in *. - set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ - (unleaves (vec2list (scbwv_exprvars (projT1 x)))) - (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*) - _ _ - ))) as q. - rewrite cheat4 in q. - rewrite cheat3. - unfold weakCK'' in q. - simpl in q. - rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q. - Ltac cheater Q := - match goal with - [ Q:?Y |- ?Z ] => - assert (Y=Z) end. - cheater q. - admit. - rewrite <- H. - clear H. - apply q. + rewrite <- mapOptionTree_compose. + rewrite <- updating_stripped_tree_is_inert''' with (l:=l). + replace (vec2list (scbwv_exprvars scbx)) with (leaves (unleaves (vec2list (scbwv_exprvars scbx)))). + rewrite <- mapleaves'. + rewrite vec2list_map_list2vec. + unfold sac_Γ. + rewrite <- (scbwv_coherent scbx l ξ). + rewrite <- vec2list_map_list2vec. + rewrite mapleaves'. + apply arrangeContextAndWeaken''. + rewrite leaves_unleaves. + apply (scbwv_exprvars_distinct scbx). + apply leaves_unleaves. destruct case_nil. apply nd_id0. @@ -772,18 +783,19 @@ Definition expr2proof : apply b2'. destruct case_ECase. - rewrite cheat2. + rewrite case_lemma. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ]. eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod. rewrite <- mapOptionTree_compose. apply dcsp. apply e'. - destruct case_ELetRec; simpl in *; intros. - set (@letRecSubproofsToND') as q. - simpl in q. - apply q. - clear q. + destruct case_ELetRec; intros. + unfold ξ'0 in *. + clear ξ'0. + unfold ξ'1 in *. + clear ξ'1. + apply letRecSubproofsToND'. apply e'. apply subproofs. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index cbe6715..dacdcae 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -194,7 +194,7 @@ Section HaskStrongToWeak. match elrb as E in ELetRecBindings G D X L V return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with | ELR_nil _ _ _ _ => fun ite => return [] - | ELR_leaf _ _ ξ' cv v e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite + | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite ; bind e' = exprToWeakExpr χ e ite ; bind v' = match χ v with Error s => failM s | OK y => return y end ; return [(v',e')] diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index e721de9..f8493b4 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -385,13 +385,35 @@ Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18). Fixpoint update_ξ `{EQD_VV:EqDecidable VV}{Γ} (ξ:VV -> LeveledHaskType Γ ★) - (vt:list (VV * LeveledHaskType Γ ★)) + (lev:HaskLevel Γ) + (vt:list (VV * HaskType Γ ★)) : VV -> LeveledHaskType Γ ★ := match vt with | nil => ξ - | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v' end. +Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, + not (In v (map (@fst _ _) varstypes)) -> + (update_ξ ξ lev varstypes) v = ξ v. + intros. + induction varstypes. + reflexivity. + simpl. + destruct a. + destruct (eqd_dec v0 v). + subst. + simpl in H. + assert False. + apply H. + auto. + inversion H0. + apply IHvarstypes. + unfold not; intros. + apply H. + simpl. + auto. + Defined. (***************************************************************************************************) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index c4e1873..f2ceddf 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -546,7 +546,7 @@ Definition weakExprToStrongExpr : forall | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => weakTypeOfWeakExpr ebody >>= fun tbody => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => - let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in + let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in let ig' := update_ig ig ((ev:CoreVar)::nil) in weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' => castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') @@ -570,7 +570,7 @@ Definition weakExprToStrongExpr : forall | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil)) (update_ig ig ((v:CoreVar)::nil)) τ lev ebody >>= fun ebody' => OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') @@ -631,7 +631,7 @@ Definition weakExprToStrongExpr : forall (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => - let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in + let ξ' := update_ξ ξ lev _ in let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in let binds := (fix binds (t:Tree ??(WeakExprVar * WeakExpr)) @@ -664,7 +664,8 @@ Definition weakExprToStrongExpr : forall mkStrongAltConPlusJunk' tc ac >>= fun sac => list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' => - let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in + (let case_pf := tt in _) >>= fun pf => + let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) (scbwv_ξ scb ξ lev) @@ -679,7 +680,7 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' => castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree) - end)). + end)); try clear binds. destruct case_some. apply (addErrorMessage "case_some"). @@ -693,8 +694,19 @@ Definition weakExprToStrongExpr : forall destruct e''; try apply (Error error_message). apply OK. apply ELR_leaf. + unfold ξ'. + simpl. + induction (leaves (varsTypes rb φ)). + simpl; auto. + destruct (ξ c). + simpl. apply e1. + destruct case_pf. + set (distinct_decidable (vec2list exprvars')) as dec. + destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ]. + apply OK; auto. + destruct case_case. exists scb. apply ebranch'. -- 1.7.10.4