X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=ab10fd82545bf6add1720110a24f2c5202ca0f36;hp=299a83be3703e2cded3a29e49bbeafc697dca2d4;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5 diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 299a83b..ab10fd8 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -393,9 +393,9 @@ Section HaskProofToStrong. exists x; auto. Defined. - Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x }) - : ITree { x:X & F x } (fun x => J (projT1 x)) t - -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t). + Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y)) + : ITree (X * Y) (fun x => J (fst x)) t + -> ITree X (fun x:X => J x) (mapOptionTree (@fst _ _) t). intro it. induction it; simpl in *. apply INone. @@ -418,12 +418,13 @@ Section HaskProofToStrong. Defined. Definition case_helper tc Γ Δ lev tbranches avars ξ : - forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac}, - prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> + forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)), + prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb))) + {vars' : Tree ??VV & (snd pcb) = mapOptionTree ξ vars'} -> ((fun sac => FreshM { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) - (weakT' tbranches) (weakL' lev) }) (projT1 pcb)). + (weakT' tbranches) (weakL' lev) }) (fst pcb)). intro pcb. intro X. simpl in X. @@ -435,7 +436,7 @@ Section HaskProofToStrong. destruct s as [vars vars_pf]. refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars - (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _). + (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _ ; _). apply FreshMon. rewrite vars_pf. rewrite <- mapOptionTree_compose. @@ -470,14 +471,15 @@ Section HaskProofToStrong. Defined. Definition gather_branch_variables - Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon & - ProofCaseBranch tc Γ Δ lev tbranches avars sac}) + Γ Δ + (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev + (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★))) : forall vars, - mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars - -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts) - -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) - { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' }) + mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars + -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts) + -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q))) + { vars' : _ & (snd q) = mapOptionTree ξ vars' }) alts. induction alts; intro vars; @@ -487,7 +489,7 @@ Section HaskProofToStrong. simpl in *. apply ileaf in source. apply ILeaf. - destruct s as [sac pcb]. + destruct p as [sac pcb]. simpl in *. split. intros. @@ -509,6 +511,242 @@ Section HaskProofToStrong. 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_xi ξ 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. (* freshness assumption *) + Defined. + + Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p : + forall (X_ : ITree Judg judg2exprType + ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])), + ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p]. + intros. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + + refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). + apply FreshMon. + + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + inversion X_. + apply ileaf in X. + apply ileaf in X0. + simpl in *. + + refine (X ξ vars1 _ >>>= fun X0' => _). + apply FreshMon. + simpl. + auto. + + refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). + apply FreshMon. + simpl. + rewrite pf2. + rewrite pf1. + reflexivity. + apply FreshMon. + + apply ILeaf. + apply ileaf in X1'. + apply ileaf in X0'. + simpl in *. + apply ELet with (ev:=vnew)(tv:=σ₁). + apply X0'. + apply X1'. + Defined. + + Definition vartree Γ Δ Σ lev ξ : + forall vars, Σ @@@ lev = mapOptionTree ξ vars -> + ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ. + induction Σ; intros. + destruct a. + intros; simpl in *. + apply ILeaf. + destruct vars; try destruct o; inversion H. + set (EVar Γ Δ ξ v) as q. + rewrite <- H1 in q. + apply q. + intros. + apply INone. + intros. + destruct vars; try destruct o; inversion H. + apply IBranch. + eapply IHΣ1. + apply H1. + eapply IHΣ2. + apply H2. + Defined. + + + Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + apply X0. + Defined. + + Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + auto. + Defined. + + Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + eapply X with (vars:=[],,vars). + rewrite H; reflexivity. + Defined. + + Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + eapply X with (vars:=vars2). + auto. + Defined. + + Definition rassoc Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars2; try destruct o; inversion H2. + apply X with (vars:=(vars1,,vars2_1),,vars2_2). + subst; reflexivity. + Defined. + + Definition rassoc' Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=vars1_1,,(vars1_2,,vars2)). + subst; reflexivity. + Defined. + + Definition swapr Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=(vars1_2,,vars1_1),,vars2). + subst; reflexivity. + Defined. + + Definition rdup Γ Δ Σ₁ a c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *) + subst; reflexivity. + Defined. + + (* holy cow this is ugly *) + Definition rcut Γ Δ Σ₃ lev Σ₁₂ : + forall Σ₁ Σ₂, + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev]. + + induction Σ₁₂. + intros. + destruct a. + + eapply rlet. + apply IBranch. + apply X. + apply X0. + + simpl in X0. + apply rdrop'' in X0. + apply rdrop'''. + apply X0. + + intros. + simpl in X0. + apply rassoc in X0. + set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q. + set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'. + apply rassoc' in q. + apply swapr in q. + apply rassoc in q. + set (q' q) as q''. + apply rassoc' in q''. + apply rdup in q''. + apply q''. + Defined. Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j. @@ -522,14 +760,14 @@ Section HaskProofToStrong. | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ | RLam Γ Δ Σ tx te x => let case_RLam := tt in _ | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ + | RAbsT Γ Δ Σ κ σ a n => let case_RAbsT := tt in _ | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ - | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ @@ -610,19 +848,6 @@ Section HaskProofToStrong. apply ileaf in X. simpl in X. apply X. - destruct case_RJoin. - apply ILeaf; simpl; intros. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - destruct vars; inversion H. - destruct o; inversion H3. - refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _). - apply FreshMon. - apply FreshMon. - apply IBranch; auto. - destruct case_RApp. apply ILeaf. inversion X_. @@ -644,81 +869,65 @@ Section HaskProofToStrong. simpl in *. apply (EApp _ _ _ _ _ _ q1' q2'). - destruct case_RLet. - apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - - refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). - apply FreshMon. + destruct case_RCut. + apply rassoc. + apply swapr. + apply rassoc'. - destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. + subst. + clear X_. - refine (X ξ vars1 _ >>>= fun X0' => _). - apply FreshMon. - simpl. - auto. + apply rassoc' in X0. + apply swapr in X0. + apply rassoc in X0. - refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). - apply FreshMon. - simpl. - rewrite pf2. - rewrite pf1. - reflexivity. - apply FreshMon. + induction Σ₃. + destruct a. + subst. + eapply rcut. + apply X. + apply X0. apply ILeaf. - apply ileaf in X1'. - apply ileaf in X0'. + simpl. + intros. + refine (return _). + apply INone. + set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1. + set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2. + apply ileaf in q1. + apply ileaf in q2. simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X0'. - apply X1'. - - destruct case_RWhere. apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - destruct vars2; try destruct o; inversion H2. - clear H2. - - assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. - refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)). + simpl. + intros. + refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _). apply FreshMon. - - destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - - refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _). apply FreshMon. - simpl. - inversion pf1. - rewrite H3. - rewrite H4. - rewrite pf2. - reflexivity. + apply IBranch; auto. - refine (X0 ξ vars2_1 _ >>>= fun X1' => _). - apply FreshMon. - reflexivity. + destruct case_RLeft. + apply ILeaf. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H2 >>>= fun X' => return _). apply FreshMon. + apply IBranch. + eapply vartree. + apply H1. + apply X'. + destruct case_RRight. apply ILeaf. - apply ileaf in X0'. - apply ileaf in X1'. - simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X1'. - apply X0'. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H1 >>>= fun X' => return _). + apply FreshMon. + apply IBranch. + apply X'. + eapply vartree. + apply H2. destruct case_RVoid. apply ILeaf; simpl; intros. @@ -731,12 +940,12 @@ Section HaskProofToStrong. apply (ileaf X). destruct case_RAbsT. - apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. + apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. rewrite mapOptionTree_compose. rewrite <- H. reflexivity. apply ileaf in X. simpl in *. - apply ETyLam. + apply (ETyLam _ _ _ _ _ _ n). apply X. destruct case_RAppCo. @@ -757,7 +966,7 @@ Section HaskProofToStrong. refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. refine (X_ ((update_xi ξ t (leaves varstypes))) - (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. + ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. rewrite pf1. @@ -825,38 +1034,6 @@ Section HaskProofToStrong. | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q) end. - 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_xi ξ 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 Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★) {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).