X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=143be0b5324fd29cfb526e3cf479b3bdcacf1f95;hp=18e7825a94a43b7f5a4a9e7f5b489c94ea59ebf4;hb=ff9fafbf161b4f12688d5986518be874d39ab3ee;hpb=8c26722a1ee110077968a8a166eb7130266b2035 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 18e7825..143be0b 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -14,9 +14,6 @@ Require Import HaskStrongTypes. Require Import HaskStrong. 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 @@ -72,6 +69,7 @@ Context {VV:Type}{eqd_vv:EqDecidable VV}. 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,9 +87,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? let branch_context := eLetRecContext branches in let all_contexts := (expr2antecedent body),,branch_context in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts - | ECase Γ Δ ξ l tc tbranches sac atypes e' alts => + | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) @@ -106,48 +104,41 @@ 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. +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. -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 Γ ★) := 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 Γ ★):= 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. @@ -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. @@ -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 ]. @@ -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 Γ Δ ξ τ), @@ -544,55 +586,57 @@ 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 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 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 _ - | ECase Γ Δ ξ l tc tbranches sac atypes 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_EGlobal. + apply nd_rule. + simpl. + destruct t as [t lev]. + apply (RGlobal _ _ _ _ wev). destruct case_EVar. apply nd_rule. @@ -609,6 +653,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 ξ). @@ -630,7 +676,7 @@ Definition expr2proof : auto. inversion H. - 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]. @@ -666,20 +712,21 @@ Definition expr2proof : auto. destruct case_ENote. + destruct t. eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. 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'. - destruct case_ECoApp; intros. + destruct case_ECoApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. @@ -691,26 +738,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. @@ -718,54 +787,7 @@ 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. -(* - -(* 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 Γ Δ. -*)