X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=e93ddd9978478a03d5ad2a8cc58420d6ed2f06c1;hp=1b9f6af57abb1d37949acab4950ed27e743e06a8;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 1b9f6af..e93ddd9 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -520,7 +520,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e | ENote Γ Δ ξ t l n e => expr2antecedent e - | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e + | ETyLam Γ Δ ξ κ σ l n e => expr2antecedent e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e @@ -549,23 +549,6 @@ match elrb with | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. -Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} -(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_gamma sac Γ) - (sac_delta sac Γ atypes (weakCK'' Δ)) - (scbwv_xi scb ξ l) - (weakT' tbranches) (weakL' l) } }) - : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. - destruct alt. - exists x. - exact - {| pcb_freevars := mapOptionTree ξ - (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) - (expr2antecedent (projT2 s))) - |}. - Defined. - - Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] @@ -961,10 +944,13 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; auto. - Defined. + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply IHX1. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply IHX2. + Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), @@ -994,7 +980,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. + set (@factorContextLeftAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. set (q' disti) as q''. @@ -1015,10 +1001,14 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod; auto. - Defined. + + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply pf. + Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, @@ -1050,6 +1040,21 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : Qed. +Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} +(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) + (weakT' tbranches) (weakL' l) } }) + : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★). + destruct alt. + split. + apply x. + apply (mapOptionTree ξ + (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) + (expr2antecedent (projT2 s)))). + Defined. + Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e (alts':Tree ??{sac : StrongAltCon & @@ -1057,7 +1062,7 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}), - (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) + (mapOptionTreeAndFlatten (fun x => snd x) (mapOptionTree mkProofCaseBranch alts')) ,, mapOptionTree ξ (expr2antecedent e) = @@ -1112,7 +1117,7 @@ Definition expr2proof : | 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) + | ETyLam Γ Δ ξ κ σ l n 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) @@ -1124,13 +1129,15 @@ Definition expr2proof : (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l) } }) - : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := + : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] - (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with + (mapOptionTree (fun x => pcb_judg (snd (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 + match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes + (fst (mkProofCaseBranch X)) + (snd (mkProofCaseBranch X))] with existT sac (existT scbx ex) => (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex) end @@ -1182,7 +1189,7 @@ Definition expr2proof : inversion H. destruct case_ELet; intros; simpl in *. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply pf_let. @@ -1243,10 +1250,10 @@ Definition expr2proof : destruct case_leaf. clear o x alts alts' e. - eapply nd_comp; [ apply e' | idtac ]. + simpl. + apply (fun x => nd_comp e' x). clear e'. - apply nd_rule. - apply RArrange. + unfold pcb_judg. simpl. rewrite mapleaves'. simpl. @@ -1255,26 +1262,40 @@ Definition expr2proof : rewrite <- mapleaves'. rewrite vec2list_map_list2vec. unfold sac_gamma. - rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. - set (@factorContextRightAndWeaken'') as q. - unfold scbwv_xi. 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. + unfold sac_gamma in *. + simpl in *. + Unset Printing Implicit. + idtac. + apply nd_rule. + apply RArrange. + set (scbwv_exprvars_distinct scbx) as q'. + rewrite <- leaves_unleaves in q'. + apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')). + clear q'. - replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with - (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). - apply q. - apply (sac_delta sac Γ atypes (weakCK'' Δ)). - rewrite leaves_unleaves. - apply (scbwv_exprvars_distinct scbx). + set (scbwv_coherent scbx l ξ) as H. rewrite leaves_unleaves. - reflexivity. + unfold scbwv_varstypes. + apply ALeft. + rewrite <- mapleaves'. + rewrite <- mapleaves'. + rewrite mapleaves'. + rewrite vec2list_map_list2vec. + rewrite <- H. + clear H. + rewrite <- mapleaves'. + rewrite vec2list_map_list2vec. + unfold scbwv_xi. + unfold scbwv_varstypes. + apply AId. destruct case_nil. apply nd_id0.