1 (*********************************************************************************************************************************)
2 (* HaskStrongToProof: convert HaskStrong to HaskProof *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskStrongTypes.
14 Require Import HaskStrong.
15 Require Import HaskProof.
17 Section HaskStrongToProof.
19 (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
20 * expansion on an entire uniform proof *)
21 Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
22 := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
23 Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
24 := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
26 Definition pivotContext {Γ}{Δ} a b c τ :
28 [ Γ >> Δ > (a,,b),,c |- τ]
29 [ Γ >> Δ > (a,,c),,b |- τ].
30 set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
32 eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ].
33 eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
37 Definition copyAndPivotContext {Γ}{Δ} a b c τ :
39 [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
40 [ Γ >> Δ > (a,,c),,b |- τ].
41 set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
43 eapply nd_comp; [ idtac | apply q ].
45 eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
46 set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
48 eapply nd_comp ; [ idtac | apply q ].
56 Context {VV:Type}{eqd_vv:EqDecidable VV}.
58 (* maintenance of Xi *)
59 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
62 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
65 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
67 | T_Leaf None => T_Leaf None
68 | T_Leaf (Some x) => T_Leaf (f x)
69 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
72 (* later: use mapOptionTreeAndFlatten *)
73 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
74 mapOptionTree' (dropVar lv).
76 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
88 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
92 rewrite <- app_comm_cons.
99 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
102 induction l1; intros.
108 set (IHl1 _ H3) as H3'.
111 apply distinct_cons; auto.
117 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
118 mapOptionTree' g (mapOptionTree' f t)
120 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
124 destruct (f t); reflexivity.
131 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
133 rewrite mapOptionTree'_compose.
141 destruct (eqd_dec v a0).
142 destruct (eqd_dec v a); reflexivity.
151 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
157 rewrite mapOptionTree'_compose.
159 destruct a; try reflexivity.
161 destruct (dropVar y v); reflexivity.
168 rewrite <- strip_lemma.
169 rewrite app_comm_cons.
175 Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
178 destruct a0; try reflexivity.
182 destruct (eqd_dec v a).
189 rewrite <- IHy1 at 2.
190 rewrite <- IHy2 at 2.
194 eapply In_both' in H0.
198 eapply In_both in H0.
202 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
207 destruct (eqd_dec v a).
209 assert False. apply H.
219 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
226 rewrite <- app_comm_cons.
229 rewrite <- app_comm_cons in H.
237 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
240 apply distinct_app in H; auto.
242 rewrite <- app_comm_cons.
244 rewrite <- ass_app in H.
245 rewrite <- app_comm_cons in H.
255 rewrite <- ass_app in H.
256 rewrite <- app_comm_cons in H.
262 Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
267 induction y; try destruct a; auto.
273 apply distinct_app in H; destruct H; auto.
274 apply distinct_app in H; destruct H; auto.
275 rewrite <- app_comm_cons in H.
280 apply strip_distinct.
288 Lemma updating_stripped_tree_is_inert'
290 (ξ:VV -> LeveledHaskType Γ ★)
292 mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
293 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
302 set (eqd_dec v v0) as q.
305 set (dropVar (map (@fst _ _) lv) v) as b in *.
312 unfold stripOutVars in *.
313 rewrite <- IHtree2_1.
314 rewrite <- IHtree2_2.
318 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
319 distinct (map (@fst _ _) (leaves varstypes)) ->
320 mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
321 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
329 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
330 match exp as E in Expr Γ Δ ξ τ with
331 | EGlobal Γ Δ ξ _ _ => []
332 | EVar Γ Δ ξ ev => [ev]
333 | ELit Γ Δ ξ lit lev => []
334 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
335 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
336 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
337 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
338 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
339 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
340 | ENote Γ Δ ξ t n e => expr2antecedent e
341 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
342 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
343 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
344 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
345 | ELetRec Γ Δ ξ l τ vars branches body =>
346 let branch_context := eLetRecContext branches
347 in let all_contexts := (expr2antecedent body),,branch_context
348 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
349 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
350 ((fix varsfromalts (alts:
351 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
353 (sac_Δ scb Γ atypes (weakCK'' Δ))
355 (weakLT' (tbranches@@l)) }
359 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
360 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
361 end) alts),,(expr2antecedent e')
363 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
365 | ELR_nil Γ Δ ξ lev => []
366 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
367 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
370 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
371 (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
373 (sac_Δ scb Γ atypes (weakCK'' Δ))
375 (weakLT' (tbranches@@l)) })
376 : ProofCaseBranch tc Γ Δ l tbranches atypes.
378 {| pcb_scb := projT1 alt
379 ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
384 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
386 | ELR_nil Γ Δ ξ lev => []
387 | ELR_leaf Γ Δ ξ lev v t e => [t]
388 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
391 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
393 | ELR_nil Γ Δ ξ lev => []
394 | ELR_leaf Γ Δ ξ lev v _ _ e => [v]
395 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
398 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
400 | ELR_nil Γ Δ ξ lev => []
401 | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)]
402 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
406 Lemma stripping_nothing_is_inert
408 (ξ:VV -> LeveledHaskType Γ ★)
410 stripOutVars nil tree = tree.
412 simpl; destruct a; reflexivity.
416 fold (stripOutVars nil).
417 rewrite <- IHtree1 at 2.
418 rewrite <- IHtree2 at 2.
422 Definition arrangeContext
423 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
424 v (* variable to be pivoted, if found *)
425 ctx (* initial context *)
426 τ (* type of succedent *)
427 (ξ:VV -> LeveledHaskType Γ ★)
430 (* a proof concluding in a context where that variable does not appear *)
432 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
433 [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ])
435 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
437 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
438 [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
442 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
446 unfold stripOutVars in *; simpl.
448 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
450 destruct (eqd_dec v' v); subst.
452 (* where the leaf is v *)
458 (* where the leaf is NOT v *)
465 apply inl; simpl in *.
474 | inr rpf => let case_Both := tt in _
475 | inl rpf => let case_Left := tt in _
479 | inr rpf => let case_Right := tt in _
480 | inl rpf => let case_Neither := tt in _
482 end); clear IHctx1; clear IHctx2.
484 destruct case_Neither.
486 eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
488 (* order will not matter because these are central as morphisms *)
489 (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
490 (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
495 fold (stripOutVars (v::nil)).
496 set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
502 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
503 eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
504 set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
505 [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq.
512 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
513 fold (stripOutVars (v::nil)).
514 eapply nd_comp; [ idtac | eapply pivotContext ].
515 set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
516 set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
518 eapply nd_comp; [ idtac | apply qq ].
520 set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
527 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
528 fold (stripOutVars (v::nil)).
529 eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
531 (* order will not matter because these are central as morphisms *)
532 (ext_right _ _ _ lpf)
533 (ext_left _ _ _ rpf)).
537 (* same as before, but use RWeak if necessary *)
538 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
540 [Γ >> Δ>mapOptionTree ξ ctx |- τ]
541 [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ].
542 set (arrangeContext Γ Δ v ctx τ ξ) as q.
544 eapply nd_comp; [ apply n | idtac ].
546 refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
549 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
550 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
551 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
552 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
558 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
562 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
563 distinct (leaves v) ->
565 [Γ >> Δ>(mapOptionTree ξ ctx) |- z]
566 [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
570 unfold mapOptionTree in *.
572 fold (mapOptionTree ξ) in *.
574 apply arrangeContextAndWeaken.
576 unfold mapOptionTree; simpl in *.
578 rewrite (@stripping_nothing_is_inert Γ); auto.
582 unfold mapOptionTree in *.
584 fold (mapOptionTree ξ) in *.
585 set (mapOptionTree ξ) as X in *.
587 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
588 unfold stripOutVars in IHv2'.
590 fold (stripOutVars (leaves v2)) in IHv2'.
591 fold (stripOutVars (leaves v1)) in IHv2'.
593 unfold mapOptionTree in IHv2'.
595 fold (mapOptionTree ξ) in IHv2'.
597 set (distinct_app _ _ _ H) as H'.
598 destruct H' as [H1 H2].
599 set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) as qq.
602 clear qq IHv2' IHv2 IHv1.
603 rewrite strip_twice_lemma.
605 rewrite (strip_distinct' v1 (leaves v2)).
612 (* IDEA: use multi-conclusion proofs instead *)
613 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
614 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
615 | lrsp_leaf : forall v t e ,
616 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
617 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
618 | lrsp_cons : forall t1 t2 b1 b2,
619 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
620 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
621 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
623 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
624 LetRecSubproofs Γ Δ ξ lev tree branches ->
625 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
626 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
627 intro X; induction X; intros; simpl in *.
634 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
635 eapply nd_comp; [ apply nd_llecnac | idtac ].
639 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
640 forall branches body,
641 distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
642 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
643 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
644 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
646 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
653 rewrite mapleaves in disti.
654 set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
655 rewrite <- mapOptionTree_compose in ξlemma.
657 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
658 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
659 set (mapOptionTree (@fst _ _) tree) as pctx.
660 set (mapOptionTree ξ' pctx) as passback.
661 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
662 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
665 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
666 unfold passback in *; clear passback.
667 unfold pctx in *; clear pctx.
668 eapply UND_to_ND in q'.
671 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
672 rewrite <- mapleaves in zz.
678 rewrite <- mapOptionTree_compose in q'.
680 eapply nd_comp; [ idtac | apply q' ].
684 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
685 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
686 eapply nd_comp; [ apply nd_llecnac | idtac ].
692 rewrite <- mapleaves in disti.
696 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
697 forall scb:StrongCaseBranchWithVVs _ _ tc atypes,
699 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
700 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes)).
703 unfold scbwv_varstypes.
704 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
705 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes))))
707 rewrite <- mapleaves' in q.
708 rewrite <- mapleaves' in q.
709 rewrite <- mapleaves' in q.
710 rewrite <- mapleaves' in q.
711 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
712 rewrite vec2list_map_list2vec in q'.
713 rewrite fst_zip in q'.
714 rewrite vec2list_map_list2vec in q'.
715 rewrite vec2list_map_list2vec in q'.
716 rewrite snd_zip in q'.
717 rewrite leaves_unleaves in q'.
718 rewrite vec2list_map_list2vec in q'.
719 rewrite vec2list_map_list2vec in q'.
722 apply scbwv_exprvars_distinct.
725 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
726 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
727 = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
730 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
735 unfold mkProofCaseBranch.
748 Definition expr2proof :
749 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
750 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
752 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
753 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
754 match exp as E in Expr Γ Δ ξ τ with
755 | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
756 | EVar Γ Δ ξ ev => let case_EVar := tt in _
757 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
758 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
759 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
760 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
761 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
762 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
763 | ELetRec Γ Δ ξ lev t tree branches ebody =>
764 let ξ' := update_ξ ξ lev (leaves tree) in
765 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
766 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
767 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
768 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
769 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
770 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
771 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
772 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
774 ) _ _ _ _ tree branches)
775 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
776 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
777 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
778 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
779 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
780 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
781 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
782 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
783 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
786 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
788 (sac_Δ scb Γ atypes (weakCK'' Δ))
790 (weakLT' (tbranches@@l)) })
791 : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
792 match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
793 | T_Leaf None => let case_nil := tt in _
794 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
796 match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with
798 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
801 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
803 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
805 destruct case_EGlobal.
808 destruct t as [t lev].
809 apply (RGlobal _ _ _ _ wev).
813 unfold mapOptionTree; simpl.
822 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
823 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
824 eapply nd_comp; [ apply nd_llecnac | idtac ].
829 destruct case_ELam; intros.
830 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
831 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
832 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
833 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
834 apply UND_to_ND in pfx.
835 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
837 fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx.
838 rewrite updating_stripped_tree_is_inert in pfx.
839 unfold update_ξ in pfx.
840 destruct (eqd_dec v v).
841 eapply nd_comp; [ idtac | apply pfx ].
849 destruct case_ELet; intros; simpl in *.
850 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
851 eapply nd_comp; [ apply nd_llecnac | idtac ].
852 apply nd_prod; [ idtac | apply pf_let].
854 eapply nd_comp; [ apply pf_body | idtac ].
856 fold (@mapOptionTree VV).
857 fold (mapOptionTree ξ).
858 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
859 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
860 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
862 rewrite updating_stripped_tree_is_inert in n.
863 unfold update_ξ in n.
864 destruct (eqd_dec lev lev).
867 apply UND_to_ND in n.
869 assert False. apply n0; auto. inversion H.
872 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
875 destruct case_EBrak; intros.
876 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
880 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
886 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
890 destruct case_ETyApp; simpl in *; intros.
891 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
895 destruct case_ECoLam; simpl in *; intros.
896 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
899 destruct case_ECoApp; simpl in *; intros.
900 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
904 destruct case_ETyLam; intros.
905 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
906 unfold mapOptionTree in e'.
907 rewrite mapOptionTree_compose in e'.
908 unfold mapOptionTree.
912 clear o x alts alts' e.
913 eapply nd_comp; [ apply e' | idtac ].
916 (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes =>
917 Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ))
918 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))) scbx ex) as stuff.
919 set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
926 rewrite <- mapOptionTree_compose.
928 rewrite <- mapleaves'.
929 rewrite vec2list_map_list2vec.
931 rewrite <- (scbwv_coherent scbx l ξ).
932 rewrite <- vec2list_map_list2vec.
934 set (@arrangeContextAndWeaken'') as q.
936 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
937 unfold scbwv_varstypes in z.
938 rewrite vec2list_map_list2vec in z.
939 rewrite fst_zip in z.
942 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
943 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
945 rewrite leaves_unleaves.
946 apply (scbwv_exprvars_distinct scbx).
947 rewrite leaves_unleaves.
953 destruct case_branch.
954 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
961 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
962 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
963 rewrite <- mapOptionTree_compose.
967 destruct case_ELetRec; intros.
972 apply letRecSubproofsToND'.
979 End HaskStrongToProof.