From 1cfe65d4e2d3292cc038882d8518dd7a48e2c40a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 26 Apr 2011 18:26:42 -0700 Subject: [PATCH] prove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!) --- src/HaskProofToStrong.v | 1 + src/HaskStrong.v | 5 +- src/HaskStrongToProof.v | 342 ++++++++++++++++++++++++++++++++++++++--------- src/HaskStrongToWeak.v | 2 +- src/HaskWeakToStrong.v | 14 +- 5 files changed, 295 insertions(+), 69 deletions(-) diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 52f2154..3aee219 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -715,6 +715,7 @@ Section HaskProofToStrong. inversion X; subst; clear X. apply (@ELetRec _ _ _ _ _ _ _ varstypes). + auto. apply (@letrec_helper Γ Δ t varstypes). rewrite <- pf2 in X1. rewrite mapOptionTree_compose. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index c5f46dc..478985d 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -61,6 +61,7 @@ Section HaskStrong. Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, + distinct (leaves (mapOptionTree (@fst _ _) vars)) -> let ξ' := update_ξ ξ l (leaves vars) in ELetRecBindings Γ Δ ξ' l vars -> Expr Γ Δ ξ' (τ@@l) -> @@ -91,8 +92,8 @@ Section HaskStrong. | ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2" | ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => "\~_ ->"+++ exprToString e - | ECase Γ Δ ξ l tc tbranches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME" - | ELetRec _ _ _ _ _ vars elrb e => "letrec FIXME in " +++ exprToString e + | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME" + | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e end. Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index c1e54aa..13f4907 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -121,31 +121,83 @@ Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOu reflexivity. Qed. -Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t. -(* - induction x. - simpl. +Lemma strip_nil_lemma t : stripOutVars nil t = t. + induction t; simpl. + unfold stripOutVars. + destruct a; reflexivity. + rewrite <- IHt1 at 2. + rewrite <- IHt2 at 2. + reflexivity. + Qed. + +Lemma strip_swap0_lemma : forall a a0 y t, + stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t. + intros. unfold stripOutVars. - simpl. - rewrite mapOptionTree'_compose. induction t. - destruct a; try reflexivity. - simpl. - destruct (dropVar y v); reflexivity. - simpl. - rewrite IHt1. - rewrite IHt2. - reflexivity. - rewrite strip_lemma. - rewrite IHx. - rewrite <- strip_lemma. - rewrite app_comm_cons. - reflexivity. -*) - admit. + destruct a1; simpl; [ idtac | reflexivity ]. + destruct (eqd_dec v a); subst. + destruct (eqd_dec a a0); subst. + reflexivity. + reflexivity. + destruct (eqd_dec v a0); subst. + reflexivity. + reflexivity. + simpl in *. + rewrite IHt1. + rewrite IHt2. + reflexivity. + Qed. + +Lemma strip_swap1_lemma : forall a y t, + stripOutVars (a :: nil) (stripOutVars y t) = + stripOutVars y (stripOutVars (a :: nil) t). + intros. + induction y. + rewrite strip_nil_lemma. + rewrite strip_nil_lemma. + reflexivity. + rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)). + rewrite <- IHy. + clear IHy. + rewrite <- (strip_lemma a y t). + rewrite <- strip_lemma. + rewrite <- strip_lemma. + apply strip_swap0_lemma. + Qed. + +Lemma strip_swap_lemma : forall x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t). + intros; induction t. + destruct a; simpl. + + induction x. + rewrite strip_nil_lemma. + rewrite strip_nil_lemma. + reflexivity. + rewrite strip_lemma. + rewrite (strip_lemma a x [v]). + rewrite IHx. + clear IHx. + apply strip_swap1_lemma. + reflexivity. + unfold stripOutVars in *. + simpl. + rewrite IHt1. + rewrite IHt2. + reflexivity. Qed. -Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. +Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t. + induction x; simpl. + apply strip_nil_lemma. + rewrite strip_lemma. + rewrite IHx. + clear IHx. + rewrite <- strip_lemma. + reflexivity. + Qed. + +Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. intros. induction y. destruct a0; try reflexivity. @@ -232,7 +284,7 @@ Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app auto. Qed. -Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y. +Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y. induction x; intros. simpl in H. unfold stripOutVars. @@ -250,7 +302,7 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars set (IHx H3) as qq. rewrite strip_lemma. rewrite IHx. - apply strip_distinct. + apply notin_strip_inert. unfold not; intros. apply H2. apply In_both'. @@ -258,46 +310,212 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars auto. Qed. +Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'. + intros. + induction y; auto. + simpl in H. + inversion H. + auto. + apply IHy. + simpl in H. + destruct (eqd_dec v a). + inversion H. + auto. + Qed. + Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) lv tree2 : mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2). + induction tree2. - destruct a. - simpl. - induction lv. - reflexivity. - simpl. - destruct a. - simpl. - set (eqd_dec v v0) as q. - destruct q. - auto. - set (dropVar (map (@fst _ _) lv) v) as b in *. - destruct b. - inversion IHlv. - admit. - auto. - reflexivity. + destruct a; [ idtac | reflexivity ]; simpl. + induction lv; [ reflexivity | idtac ]; simpl. + destruct a; simpl. + set (eqd_dec v v0) as q; destruct q; auto. + set (dropVar (map (@fst _ _) lv) v) as b in *. + assert (dropVar (map (@fst _ _) lv) v=b). reflexivity. + destruct b; [ idtac | reflexivity ]. + apply dropvar_lemma in H. + subst. + inversion IHlv. + rewrite H0. + clear H0 IHlv. + destruct (eqd_dec v0 v1). + subst. + assert False. apply n. intros; auto. inversion H. + reflexivity. + unfold stripOutVars in *. + simpl. + rewrite <- IHtree2_1. + rewrite <- IHtree2_2. + reflexivity. + Qed. + +Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False. + intros; induction a; auto. + simpl in H. + inversion H; subst. + apply H2; auto. + unfold In; simpl. + left; auto. + apply IHa. + clear IHa. + rewrite <- app_comm_cons in H. + inversion H; subst. + inversion H3; subst. + apply distinct_cons; auto. + intros. + apply H2. simpl. - unfold stripOutVars in *. - rewrite <- IHtree2_1. - rewrite <- IHtree2_2. - reflexivity. + right; auto. Qed. -Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)), - distinct (map (@fst _ _) (leaves varstypes)) -> - mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = - mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). - admit. +Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b). + intros. + apply distinct_cons. + induction b; intros; simpl; auto. + rewrite <- app_comm_cons in H. + inversion H; subst. + set (IHb H4) as H4'. + apply H4'. + inversion H0; subst; auto. + apply distinct_bogus in H; inversion H. + induction b; intros; simpl; auto. + apply distinct_nil. + apply distinct_app in H. + destruct H; auto. Qed. +Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b. + induction a; intros; simpl; auto. + rewrite <- app_comm_cons in H. + inversion H. + subst. + left; left; auto. + set (IHa _ _ H0) as H'. + destruct H'. + left; right; auto. + right; auto. + Qed. +Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b). + intros. + induction a; simpl; auto. + simpl in H. + inversion H; auto. + assert (distinct (app a1 b)) as Q. + intros. + apply IHa. + clear IHa. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply distinct_cons; [ idtac | apply Q ]. + intros. + apply in_both in H0. + destruct H0. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply H3. + apply In_both; auto. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply H3. + apply In_both'; auto. + simpl. + right; auto. + Qed. + +Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a). + induction a; intros; simpl; auto. + Qed. + +Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). + intros. + induction b. + rewrite <- app_nil_end in H; auto. + rewrite <- app_comm_cons. + set (distinct_lemma _ _ _ H) as H'. + set (IHb H') as H''. + apply distinct_cons; [ idtac | apply H'' ]. + intros. + apply in_both in H0. + clear H'' H'. + destruct H0. + apply distinct_app in H. + destruct H. + inversion H1; auto. + clear IHb. + rewrite nil_app in H. + rewrite ass_app in H. + apply distinct_app in H. + destruct H; auto. + apply distinct_swap' in H. + inversion H; auto. + Qed. +Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : + forall v1 v2, + distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) -> + mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). + induction varstypes; intros. + destruct a; simpl; [ idtac | reflexivity ]. + destruct p. + simpl. + simpl in H. + induction (leaves v1). + simpl; auto. + destruct (eqd_dec v v); auto. + assert False. apply n. auto. inversion H0. + simpl. + destruct a. + destruct (eqd_dec v0 v); subst; auto. + simpl in H. + rewrite map_app in H. + simpl in H. + rewrite nil_app in H. + apply distinct_swap in H. + rewrite app_ass in H. + apply distinct_app in H. + destruct H. + apply distinct_swap in H0. + simpl in H0. + inversion H0; subst. + assert False. + apply H3. + simpl; left; auto. + inversion H1. + apply IHl. + simpl in H. + inversion H; auto. + set (IHvarstypes1 v1 (varstypes2,,v2)) as i1. + set (IHvarstypes2 (v1,,varstypes1) v2) as i2. + simpl in *. + rewrite <- i1. + rewrite <- i2. + rewrite ass_app. + rewrite ass_app. + rewrite ass_app. + rewrite ass_app. + reflexivity. + clear i1 i2 IHvarstypes1 IHvarstypes2. + repeat rewrite ass_app in *; auto. + clear i1 i2 IHvarstypes1 IHvarstypes2. + repeat rewrite ass_app in *; auto. + Qed. +Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : + distinct (map (@fst _ _) (leaves varstypes)) -> + mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). + set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q. + simpl in q. + rewrite <- app_nil_end in q. + apply q. + Qed. Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := match exp as E in Expr Γ Δ ξ τ with @@ -315,7 +533,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e - | ELetRec Γ Δ ξ l τ vars branches body => + | ELetRec Γ Δ ξ l τ vars _ branches body => let branch_context := eLetRecContext branches in let all_contexts := (expr2antecedent body),,branch_context in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts @@ -499,10 +717,6 @@ Definition arrangeContextAndWeaken refine (RLeft _ (RWeak _)). Defined. -Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). - admit. - Qed. - Definition arrangeContextAndWeaken'' (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -547,11 +761,11 @@ Definition arrangeContextAndWeaken'' eapply RComp. apply qq. clear qq IHv2' IHv2 IHv1. + rewrite strip_swap_lemma. rewrite strip_twice_lemma. - - rewrite (strip_distinct' v1 (leaves v2)). + rewrite (notin_strip_inert' v1 (leaves v2)). apply RCossa. - apply cheat. + apply distinct_swap. auto. Defined. @@ -592,11 +806,10 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : - forall branches body, - distinct (leaves (mapOptionTree (@fst _ _) tree)) -> + forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), 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]]. + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) intro branches. @@ -605,8 +818,11 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : intro pf. intro lrsp. - rewrite mapleaves in disti. - set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma. + assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'. + apply disti. + rewrite mapleaves in disti'. + + set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma. rewrite <- mapOptionTree_compose in ξlemma. set ((update_ξ ξ lev (leaves tree))) as ξ' in *. @@ -620,7 +836,6 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. - rewrite <- mapleaves in disti. set (q' disti) as q''. unfold ξ' in *. @@ -722,7 +937,7 @@ Definition expr2proof : | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e) | 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 => + | ELetRec Γ Δ ξ lev t tree disti branches ebody => let ξ' := update_ξ ξ lev (leaves tree) in let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) @@ -929,7 +1144,6 @@ Definition expr2proof : unfold ξ'1 in *. clear ξ'1. apply letRecSubproofsToND'. - admit. apply e'. apply subproofs. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index e956dd6..79d954c 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -181,7 +181,7 @@ Section HaskStrongToWeak. (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes)) ; return WECase vscrut' escrut' tbranches' tc tys branches' - | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★ + | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★ => bind tleaf = typeToWeakType (snd vt) ite ; bind v' = mkWeakExprVar tleaf ; return ((fst vt),v')) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 1b34865..6d4bf16 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -510,7 +510,14 @@ Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar) | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2 end. -(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *) +Definition checkDistinct : + forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv). + intros. + set (distinct_decidable lv) as q. + destruct q. + exact (OK d). + exact (Error "checkDistinct failed"). + Defined. Definition weakExprToStrongExpr : forall (Γ:TypeEnv) @@ -644,8 +651,9 @@ Definition weakExprToStrongExpr : forall OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2') end) rb in binds >>= fun binds' => + checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' => - OK (ELetRec Γ Δ ξ lev τ _ binds' e') + OK (ELetRec Γ Δ ξ lev τ _ _ binds' e') | WECase vscrut escrut tbranches tc avars alts => weakTypeOfWeakExpr escrut >>= fun tscrut => @@ -700,6 +708,8 @@ Definition weakExprToStrongExpr : forall destruct (ξ c). simpl. apply e1. + rewrite mapleaves. + apply rb_distinct. destruct case_pf. set (distinct_decidable (vec2list exprvars')) as dec. -- 1.7.10.4