X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=3798a36fa341888940a05b0c0c9b888ebfb8bdff;hb=53d4f1ce851b924cab5dc39419179a366001cbca;hp=c0a0bb3531b962482bb4d8728d1ee9fe8ae66f26;hpb=976b9bb93bf6ab296b3ac60dcdb4e87b1c665376;p=coq-hetmet.git diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index c0a0bb3..3798a36 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -12,18 +12,16 @@ Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskStrongTypes. Require Import HaskStrong. +Require Import HaskWeakVars. Require Import HaskProof. -Axiom fail : forall {A}, string -> A. - Extract Inlined Constant fail => "Prelude.error". - Section HaskStrongToProof. (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform * expansion on an entire uniform proof *) -Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) +Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)). -Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) +Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)). Definition pivotContext {Γ}{Δ} a b c τ : @@ -75,27 +73,27 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) - | ELam Γ Δ ξ t1 t2 lev v pf e => stripOutVars (v::nil) (expr2antecedent e) + | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e) | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev)) | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e - | ECast Γ Δ ξ γ t1 t2 lev wfco e => expr2antecedent e + | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e | ENote Γ Δ ξ t n e => expr2antecedent e | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => expr2antecedent e - | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => expr2antecedent e - | ETyApp Γ Δ κ σ τ ξ l pf e => expr2antecedent e + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e + | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e + | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e | 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 - | ECase Γ Δ ξ lev tc avars tbranches e' alts => + | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc avars + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) - (weakLT' (tbranches@@lev)) } + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) } ): Tree ??VV := match alts with | T_Leaf None => [] @@ -106,55 +104,48 @@ end with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => expr2antecedent e + | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. -(* -Definition caseBranchRuleInfoFromEStrongAltCon - `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) : - @StrongAltConRuleInfo n tc Γ lev tbranches. - set (ecase2antecedent _ _ _ _ _ _ _ _ ecb) as Σ. - destruct ecb. - apply Build_StrongAltConRuleInfo with (pcb_scb := alt)(pcb_Σ := mapOptionTree ξ Σ). - Defined. - -Definition judgFromEStrongAltCon - `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) : - Judg. - apply caseBranchRuleInfoFromEStrongAltCon in ecb. - destruct ecb. - eapply pcb_judg. - Defined. - -Implicit Arguments caseBranchRuleInfoFromEStrongAltCon [ [Γ] [Δ] [ξ] [lev] [tc] [avars] [tbranches] ]. -*) -Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. -Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ) := +Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} + (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes + & Expr (sac_Γ scb Γ) + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) }) + : ProofCaseBranch tc Γ Δ l tbranches atypes. + exact + {| pcb_scb := projT1 alt + ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt))) + |}. + Defined. + +Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev] + | ELR_leaf Γ Δ ξ lev v e => [ξ v] | 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 Γ Δ ξ t 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 * LeveledHaskType Γ ★):= match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)] + | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) end. Lemma stripping_nothing_is_inert {Γ:TypeEnv} - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) tree : stripOutVars nil tree = tree. induction tree. @@ -175,7 +166,7 @@ Definition arrangeContext v (* variable to be pivoted, if found *) ctx (* initial context *) τ (* type of succedent *) - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) : (* a proof concluding in a context where that variable does not appear *) @@ -340,7 +331,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, rewrite H. clear H. - (* FIXME TOTAL BOGOSITY *) + (* 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. @@ -352,10 +343,10 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, Definition update_ξ'' {Γ} ξ tree lev := (update_ξ ξ - (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) (leaves tree))). -Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree lev : +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. @@ -391,7 +382,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree Lemma updating_stripped_tree_is_inert' {Γ} lev - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) tree tree2 : mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2). @@ -400,7 +391,7 @@ admit. Lemma updating_stripped_tree_is_inert'' {Γ} - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) v tree lev : mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree) = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree). @@ -424,15 +415,14 @@ admit. 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) + (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) -> + LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ 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 dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), - +Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), eLetRecTypes branches = mapOptionTree (update_ξ'' ξ tree lev) (mapOptionTree (@fst _ _) tree). @@ -445,6 +435,24 @@ Lemma dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tre 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 -> @@ -458,8 +466,12 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches induction X; intros; simpl in *. apply nd_rule. apply REmptyGroup. - unfold mapOptionTree. - simpl. + 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 ]. @@ -467,7 +479,7 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches Defined. -Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ) tree z lev, +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. @@ -487,7 +499,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : intro pf. intro lrsp. set ((update_ξ ξ - (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) (leaves tree)))) as ξ' in *. set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. set (mapOptionTree (@fst _ _) tree) as pctx. @@ -520,22 +532,52 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. - rewrite dork in q. + rewrite cheat1 in q. set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. unfold update_ξ'' in *. rewrite <- zz in q. apply q. Defined. -(* -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. + +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). + admit. Qed. -*) -Lemma cheat : forall {T} (a b:T), a=b. - 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. + + + Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), @@ -547,52 +589,47 @@ Definition expr2proof : | 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 pf 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 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 Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e) - | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) + | 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) 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 wfco 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 wfco1 wfco2 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyApp Γ Δ κ σ τ ξ l pf e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ECase Γ Δ ξ lev tbranches tc avars e alts => -(* + ) _ _ _ _ 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 avars + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) - (weakLT' (tbranches@@lev)) }) - : ND Rule [] (mapOptionTree judgFromEStrongAltCon alts) := - match alts as ALTS return ND Rule [] (mapOptionTree judgFromEStrongAltCon ALTS) with + (sac_Δ scb Γ 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 _ - end) alts) - in *) let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2) + end) alts') + in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) end -); clear exp ξ' τ' Γ' Δ'; simpl in *. +); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. destruct case_EVar. apply nd_rule. @@ -609,6 +646,8 @@ 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 ξ). @@ -629,9 +668,8 @@ Definition expr2proof : apply n. auto. inversion H. - apply pf. - destruct case_ELet; intros. + destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | apply pf_let]. @@ -662,7 +700,7 @@ Definition expr2proof : apply e'. destruct case_ECast. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast with (γ:=γ)]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ]. apply e'. auto. @@ -671,19 +709,17 @@ Definition expr2proof : apply e'. auto. - destruct case_ETyApp; intros. + destruct case_ETyApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ]. apply e'. auto. - destruct case_ECoLam; intros. + destruct case_ECoLam; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. apply e'. - auto. - auto. - destruct case_ECoApp; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) σ₁ σ₂ σ γ l) ]. + destruct case_ECoApp; simpl in *; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. @@ -694,26 +730,48 @@ Definition expr2proof : unfold mapOptionTree. apply e'. + 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 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. + + destruct case_nil. + apply nd_id0. + + destruct case_branch. + simpl; eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply b1'. + apply b2'. + destruct case_ECase. - unfold mapOptionTree; simpl; fold (mapOptionTree ξ). - apply (fail "ECase not implemented"). - (* + rewrite cheat2. 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_elr_leaf; intros. - assert (unlev (ξ0 v) = t0). - apply cheat. - set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q. - rewrite H in q. - apply q. - apply e'0. - destruct case_ELetRec; intros. + destruct case_ELetRec; simpl in *; intros. set (@letRecSubproofsToND') as q. simpl in q. apply q. @@ -721,41 +779,6 @@ Definition expr2proof : apply e'. apply subproofs. - (* - destruct case_leaf. - unfold pcb_judg. - simpl. - clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u. - repeat rewrite <- mapOptionTree_compose in *. - set (nd_comp ecb' - (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q. - idtac. - 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). - apply q. - apply cheat. - - destruct case_branch. - simpl; eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply (mkdcsp b1). - apply (mkdcsp b2). - *) - Defined. End HaskStrongToProof. @@ -772,3 +795,4 @@ Inductive Decl :=. Inductive Pgm Γ Δ := mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ. *) +