X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=79e16cde56fb220250ada5a87a2472025b74f55a;hp=753362e6285ba6a286b9f7d98777c8509b609972;hb=b3214686b18b2d6f6905394494da8d1c17587bdb;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 753362e..79e16cd 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -12,7 +12,6 @@ Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskWeakVars. Require Import HaskProof. Section HaskStrongToProof. @@ -57,19 +56,279 @@ 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. + +Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b := + match t with + | T_Leaf None => T_Leaf None + | T_Leaf (Some x) => T_Leaf (f x) + | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r) + 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). + mapOptionTree' (dropVar lv). + +Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2). + intros T l1. + induction l1; intros. + inversion H. + simpl. + inversion H; subst. + left; auto. + right. + apply IHl1. + apply H0. + Qed. + +Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2). + intros T l1. + induction l1; intros. + apply H. + rewrite <- app_comm_cons. + simpl. + right. + apply IHl1. + auto. + Qed. + +Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2. + intro T. + intro l1. + induction l1; intros. + split; auto. + apply distinct_nil. + simpl in H. + inversion H. + subst. + set (IHl1 _ H3) as H3'. + destruct H3'. + split; auto. + apply distinct_cons; auto. + intro. + apply H2. + apply In_both; auto. + Qed. + +Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B), + mapOptionTree' g (mapOptionTree' f t) + = + mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t. + intros; induction t. + destruct a; auto. + simpl. + destruct (f t); reflexivity. + simpl. + rewrite <- IHt1. + rewrite <- IHt2. + reflexivity. + Qed. + +Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t). + unfold stripOutVars. + rewrite mapOptionTree'_compose. + simpl. + induction t. + destruct a0. + simpl. + induction x. + reflexivity. + simpl. + destruct (eqd_dec v a0). + destruct (eqd_dec v a); reflexivity. + apply IHx. + reflexivity. + simpl. + 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. + 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. + Qed. + +Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. + intros. + induction y. + destruct a0; try reflexivity. + simpl in *. + unfold stripOutVars. + simpl. + destruct (eqd_dec v a). + subst. + assert False. + apply H. + left; auto. + inversion H0. + auto. + rewrite <- IHy1 at 2. + rewrite <- IHy2 at 2. + reflexivity. + unfold not; intro. + apply H. + eapply In_both' in H0. + apply H0. + unfold not; intro. + apply H. + eapply In_both in H0. + apply H0. + Qed. + +Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v. + intros. + induction x. + reflexivity. + simpl. + destruct (eqd_dec v a). + subst. + assert False. apply H. + simpl; auto. + inversion H0. + apply IHx. + unfold not. + intro. + apply H. + simpl; auto. + Qed. + +Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c). + induction a; intros. + simpl. + simpl in H. + apply In_both'. + auto. + rewrite <- ass_app. + rewrite <- app_comm_cons. + simpl. + rewrite ass_app. + rewrite <- app_comm_cons in H. + inversion H. + left; auto. + right. + apply IHa. + apply H0. + Qed. + +Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c). + induction a; intros. + simpl in *. + apply distinct_app in H; auto. + destruct H; auto. + rewrite <- app_comm_cons. + apply distinct_cons. + rewrite <- ass_app in H. + rewrite <- app_comm_cons in H. + inversion H. + subst. + intro q. + apply H2. + rewrite ass_app. + apply in3. + auto. + apply IHa. + rewrite <- ass_app. + rewrite <- ass_app in H. + rewrite <- app_comm_cons in H. + inversion H. + subst. + auto. + Qed. + +Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y. + induction x; intros. + simpl in H. + unfold stripOutVars. + simpl. + induction y; try destruct a; auto. + simpl. + rewrite IHy1. + rewrite IHy2. + reflexivity. + simpl in H. + apply distinct_app in H; destruct H; auto. + apply distinct_app in H; destruct H; auto. + rewrite <- app_comm_cons in H. + inversion H; subst. + set (IHx H3) as qq. + rewrite strip_lemma. + rewrite IHx. + apply strip_distinct. + unfold not; intros. + apply H2. + apply In_both'. + auto. + 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. + simpl. + unfold stripOutVars in *. + rewrite <- IHtree2_1. + rewrite <- IHtree2_2. + reflexivity. + 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. + Qed. + + + + Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := match exp as E in Expr Γ Δ ξ τ with + | EGlobal Γ Δ ξ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) @@ -89,59 +348,63 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) } + (weakLT' (tbranches@@l)) } } ): Tree ??VV := match alts with | T_Leaf None => [] - | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h)) + | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h))) | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2) end) alts),,(expr2antecedent e') 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. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} - (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) +(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) }) - : ProofCaseBranch tc Γ Δ l tbranches atypes. + (weakLT' (tbranches@@l)) } }) + : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. + destruct alt. + exists x. exact - {| pcb_scb := projT1 alt - ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt))) + {| pcb_freevars := mapOptionTree ξ + (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) + (expr2antecedent (projT2 s))) |}. 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,13 +417,11 @@ 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. - - Definition arrangeContext (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -179,17 +440,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 +549,26 @@ Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : refine (ext_left _ _ _ (nd_rule (RWeak _ _))). Defined. +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). + set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. + rewrite p. + simpl. + reflexivity. + Qed. + +Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). + 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,170 +597,71 @@ 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 (distinct_app _ _ _ H) as H'. + destruct H' as [H1 H2]. + set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) 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' v1 (leaves v2)). apply nd_rule. apply RCossa. + apply cheat. + 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) - = 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 *. - destruct a; simpl; try reflexivity. - unfold update_ξ. - simpl. - unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - unfold update_ξ. - unfold dropVar. - simpl. - set (eqd_dec v v0) as q. - assert (q=eqd_dec v v0). - reflexivity. - destruct q. - reflexivity. - rewrite <- H. - reflexivity. - auto. - unfold mapOptionTree. - unfold mapOptionTree in IHtree1. - unfold mapOptionTree in IHtree2. - simpl in *. - simpl in IHtree1. - fold (stripOutVars (v::nil)). - rewrite <- IHtree1. - rewrite <- IHtree2. - reflexivity. - Qed. - - - -Lemma updating_stripped_tree_is_inert' - {Γ} lev - (ξ:VV -> LeveledHaskType Γ ★) - tree tree2 : - mapOptionTree (update_ξ'' ξ tree lev) (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. - 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. - 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 cheat9 : 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 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) + |- (mapOptionTree (@snd _ _) tree) @@@ lev ]. + intro X; induction X; intros; simpl in *. apply nd_rule. apply REmptyGroup. - unfold mapOptionTree. - simpl. -admit. -(* apply n.*) + set (ξ v) as q in *. + destruct q. + simpl in *. + 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 -> + 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]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) - simpl. intro branches. intro body. + intro disti. intro pf. intro lrsp. - set ((update_ξ ξ - (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) - (leaves tree)))) as ξ' in *. + + rewrite mapleaves in disti. + set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma. + rewrite <- mapOptionTree_compose in ξlemma. + + 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. @@ -494,57 +671,91 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply UND_to_ND in q'. unfold ξ' in *. - set (@updating_stripped_tree_is_inert') as zz. - unfold update_ξ'' in *. + set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz. + rewrite <- mapleaves in zz. rewrite zz in q'. clear zz. clear ξ'. - simpl in q'. - + Opaque stripOutVars. + simpl. + rewrite <- mapOptionTree_compose in q'. + rewrite <- ξlemma. eapply nd_comp; [ idtac | apply q' ]. 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 cheat9 in q. - set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. - unfold update_ξ'' in *. - rewrite <- zz in q. + rewrite ξlemma. apply q. - Defined. + clear q'. -(* -Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx), - unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars). -admit. + rewrite <- mapleaves in disti. + apply disti. + Defined. + +Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : + forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, + forall l ξ, + vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) = + vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)). + intros. + unfold scbwv_ξ. + unfold scbwv_varstypes. + set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes)))) + ) as q. + rewrite <- mapleaves' in q. + rewrite <- mapleaves' in q. + rewrite <- mapleaves' in q. + rewrite <- mapleaves' in q. + set (fun z => unleaves_injective _ _ _ (q z)) 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 leaves_unleaves in q'. + rewrite vec2list_map_list2vec in q'. + rewrite vec2list_map_list2vec in q'. + apply q'. + rewrite fst_zip. + apply scbwv_exprvars_distinct. Qed. -*) -Lemma cheat0 : 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. -Defined. -Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l). - admit. - Defined. -Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t. -admit. -Defined. +Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e + (alts':Tree + ??{sac : StrongAltCon & + {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac & + Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}), + + (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) + (mapOptionTree mkProofCaseBranch alts')) + ,, + mapOptionTree ξ (expr2antecedent e) = + mapOptionTree ξ + (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')). + intros. + simpl. + Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end. + hack. + induction alts'. + destruct a; simpl. + destruct s; simpl. + unfold mkProofCaseBranch. + reflexivity. + reflexivity. + simpl. + rewrite IHalts'1. + rewrite IHalts'2. + reflexivity. + rewrite H. + reflexivity. + Qed. Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), @@ -553,54 +764,62 @@ Definition expr2proof : refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := match exp as E in Expr Γ Δ ξ τ with + | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _ | EVar Γ Δ ξ ev => let case_EVar := tt in _ | ELit Γ Δ ξ lit lev => let case_ELit := tt in _ | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in - let e1' := expr2proof _ _ _ _ e1 in - let e2' := expr2proof _ _ _ _ e2 in _ - | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in - let e' := expr2proof _ _ _ _ e in _ + (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2) + | 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 - let pf_let := (expr2proof _ _ _ _ ev) in - let pf_body := (expr2proof _ _ _ _ ebody) in _ + (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree branches ebody => - let e' := expr2proof _ _ _ _ ebody in - let ξ' := update_ξ'' ξ tree lev in - let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) + let ξ' := update_ξ ξ lev (leaves tree) in + let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) + ((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_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) + | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ + | 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) in - let case_ELetRec := tt in _ - | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _ - | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _ - | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _ - | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ + ) _ _ _ _ tree branches) + | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) | ECase Γ Δ ξ l tc tbranches atypes e alts' => let dcsp := ((fix mkdcsp (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (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_Branch b1 b2 => let case_branch := tt in _ + (weakLT' (tbranches@@l)) } }) + : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := + match alts as ALTS return ND Rule [] + (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with + | 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 (projT2 (mkProofCaseBranch X))] with + existT sac (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 ξ' τ' Γ' Δ'. + ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. + + destruct case_EGlobal. + apply nd_rule. + simpl. + destruct t as [t lev]. + apply (RGlobal _ _ _ _ wev). destruct case_EVar. apply nd_rule. @@ -617,16 +836,18 @@ Definition expr2proof : eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. + apply e1'. + apply e2'. 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). @@ -647,7 +868,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. @@ -674,6 +895,7 @@ Definition expr2proof : auto. destruct case_ENote. + destruct t. eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. apply e'. auto. @@ -683,121 +905,86 @@ Definition expr2proof : apply e'. auto. + destruct case_ECoLam; simpl in *; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. + apply e'. + destruct case_ECoApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. - destruct case_leaf. - unfold pcb_judg. - 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 cheat2 in q. -rewrite cheat1. -unfold weakCK'' in q. -simpl in q. -admit. -(* -replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ) - (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) - (expr2antecedent (projT2 x)))) -with (mapOptionTree (scbwv_ξ (projT1 x) ξ l) - (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) - (expr2antecedent (projT2 x)))). -rewrite <- cheat1 in q. -rewrite vec2list_map_list2vec in q. -unfold mapOptionTree. -fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★) - (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)). -admit. -*) -admit. + destruct case_ETyLam; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. + unfold mapOptionTree in e'. + rewrite mapOptionTree_compose in e'. + unfold mapOptionTree. + apply e'. -(* -assert ( + destruct case_leaf. + clear o x alts alts' e. + eapply nd_comp; [ apply e' | idtac ]. + clear e'. + 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. -unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x)))) -= -unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l). -admit. -Set Printing Implicit. -idtac. -rewrite <- H. - - assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))). - apply update_ξ_and_reapply. - rewrite H. - simpl in q. - unfold mapOptionTree in q; simpl in q. - set (@updating_stripped_tree_is_inert''') as u. - unfold mapOptionTree in u. - rewrite u in q. - clear u H. - unfold weakenX' in *. - admit. - unfold mapOptionTree in *. - replace - (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0)) - with - (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0). + rewrite mapleaves'. + simpl. + rewrite <- mapOptionTree_compose. + unfold scbwv_ξ. + rewrite <- mapleaves'. + rewrite vec2list_map_list2vec. + unfold sac_Γ. + rewrite <- (scbwv_coherent scbx l ξ). + rewrite <- vec2list_map_list2vec. + rewrite mapleaves'. + set (@arrangeContextAndWeaken'') as q. + unfold scbwv_ξ. + set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. + unfold scbwv_varstypes in z. + rewrite vec2list_map_list2vec in z. + rewrite fst_zip in z. + rewrite <- z. + clear z. + replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with + (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q. - apply cheat. -*) + rewrite leaves_unleaves. + apply (scbwv_exprvars_distinct scbx). + rewrite leaves_unleaves. + reflexivity. + + destruct case_nil. + apply nd_id0. destruct case_branch. simpl; eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. - apply (mkdcsp b1). - apply (mkdcsp b2). + apply b1'. + apply b2'. destruct case_ECase. - rewrite cheat0. + set (@RCase Γ Δ l tc) as q. + 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'. + admit. apply e'. apply subproofs. - (* - destruct case_ECoLam; simpl in *; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. - apply e'. - - destruct case_ETyLam; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. - unfold mapOptionTree in e'. - rewrite mapOptionTree_compose in e'. - unfold mapOptionTree. - apply e'. - *) - Admitted. + Defined. End HaskStrongToProof. -(* - -(* Figure 7, production "decl"; actually not used in this formalization *) -Inductive Decl :=. -| DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl -| DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl -| DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl. - -(* Figure 1, production "pgm" *) -Inductive Pgm Γ Δ := - mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ. -*) -