1 (*********************************************************************************************************************************)
2 (* HaskProofToStrong: convert HaskProof to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import NaturalDeductionContext.
10 Require Import Coq.Strings.String.
11 Require Import Coq.Lists.List.
12 Require Import Coq.Init.Specif.
13 Require Import HaskKinds.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
18 Section HaskProofToStrong.
20 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
22 Definition fresh := FMT_fresh freshM.
23 Definition FreshM := FMT freshM.
24 Definition FreshMon := FMT_Monad freshM.
25 Existing Instance FreshMon.
27 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
29 Definition judg2exprType (j:Judg) : Type :=
31 (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
32 FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
35 Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
40 Definition ileaf `(it:ITree X F [t]) : F t.
45 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
46 update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
56 Lemma quark {T} (l1:list T) l2 vf :
57 (In vf (app l1 l2)) <->
58 (In vf l1) \/ (In vf l2).
85 right; apply H0; auto.
86 right; apply H0; auto.
89 Lemma splitter {T} (l1:list T) l2 vf :
90 (In vf (app l1 l2) → False)
91 -> (In vf l1 → False) /\ (In vf l2 → False).
93 split; intros; apply H; rewrite quark.
99 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
100 (In vf (leaves tl) -> False) ->
101 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
107 set (eqd_dec vf t) as x in *.
123 Lemma fresh_lemma'' Γ
124 : forall types ξ lev,
125 FreshM { varstypes : _
126 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
127 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
132 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
133 FreshM { varstypes : _
134 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
135 /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
136 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
139 refine (bind vf = fresh (leaves vars) ; return _).
141 destruct vf as [ vf vf_pf ].
145 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
149 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
165 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
167 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
168 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
169 (leaves vt2)) _ _; return _).
175 clear IHtypes1 IHtypes2.
176 destruct x1 as [vt1 [pf11 pf12]].
177 exists (vt1,,vt2); split; auto.
179 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
180 set (mapOptionTree_extensional _ _ q) as q'.
187 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
188 set (mapOptionTree_extensional _ _ q) as q'.
192 rewrite <- mapOptionTree_compose.
193 rewrite <- mapOptionTree_compose.
194 rewrite <- mapOptionTree_compose in *.
199 rewrite <- mapOptionTree_compose.
205 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
206 : Σ = mapOptionTree ξ vars ->
208 | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
209 /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
211 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
212 refine (q >>>= fun q' => return _).
215 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
216 destruct varstypes; try destruct o; try destruct p; simpl in *.
217 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
218 inversion pf2; subst.
220 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
226 Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
227 forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
229 Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
230 ujudg2exprType Γ ξ Δ h t l ->
231 ujudg2exprType Γ ξ Δ j t l
234 refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
235 ujudg2exprType Γ ξ Δ h t l ->
236 ujudg2exprType Γ ξ Δ j t l :=
237 match r as R in Arrange H C return
238 ujudg2exprType Γ ξ Δ H t l ->
239 ujudg2exprType Γ ξ Δ C t l
241 | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
242 | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
243 | AId a => let case_AId := tt in _
244 | ACanL a => let case_ACanL := tt in _
245 | ACanR a => let case_ACanR := tt in _
246 | AuCanL a => let case_AuCanL := tt in _
247 | AuCanR a => let case_AuCanR := tt in _
248 | AAssoc a b c => let case_AAssoc := tt in _
249 | AuAssoc a b c => let case_AuAssoc := tt in _
250 | AExch a b => let case_AExch := tt in _
251 | AWeak a => let case_AWeak := tt in _
252 | ACont a => let case_ACont := tt in _
253 | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
254 end); clear urule2expr; intros.
260 simpl; unfold ujudg2exprType; intros.
262 apply (X ([],,vars)).
263 simpl; rewrite <- H; auto.
266 simpl; unfold ujudg2exprType; intros.
268 apply (X (vars,,[])).
269 simpl; rewrite <- H; auto.
271 destruct case_AuCanL.
272 simpl; unfold ujudg2exprType; intros.
273 destruct vars; try destruct o; inversion H.
275 apply (X vars2); auto.
277 destruct case_AuCanR.
278 simpl; unfold ujudg2exprType; intros.
279 destruct vars; try destruct o; inversion H.
281 apply (X vars1); auto.
283 destruct case_AAssoc.
284 simpl; unfold ujudg2exprType; intros.
286 destruct vars; try destruct o; inversion H.
287 destruct vars1; try destruct o; inversion H.
288 apply (X (vars1_1,,(vars1_2,,vars2))).
291 destruct case_AuAssoc.
292 simpl; unfold ujudg2exprType; intros.
294 destruct vars; try destruct o; inversion H.
295 destruct vars2; try destruct o; inversion H.
296 apply (X ((vars1,,vars2_1),,vars2_2)).
300 simpl; unfold ujudg2exprType ; intros.
302 destruct vars; try destruct o; inversion H.
303 apply (X (vars2,,vars1)).
304 inversion H; subst; auto.
307 simpl; unfold ujudg2exprType; intros.
313 simpl; unfold ujudg2exprType ; intros.
315 apply (X (vars,,vars)).
321 intro vars; unfold ujudg2exprType; intro H.
322 destruct vars; try destruct o; inversion H.
323 apply (fun q => e ξ q vars2 H2).
327 unfold ujudg2exprType.
329 apply X with (vars:=vars1,,vars).
335 destruct case_ARight.
336 intro vars; unfold ujudg2exprType; intro H.
337 destruct vars; try destruct o; inversion H.
338 apply (fun q => e ξ q vars1 H1).
342 unfold ujudg2exprType.
344 apply X with (vars:=vars,,vars2).
356 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
358 (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
359 (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
360 -> ELetRecBindings Γ Δ ξ' l varstypes.
363 destruct a; simpl in *.
366 apply ileaf in X. simpl in X.
369 destruct (eqd_dec (unlev (ξ' v)) τ).
373 destruct (eqd_dec h0 l).
378 apply (Prelude_error "level mismatch; should never happen").
379 apply (Prelude_error "letrec type mismatch; should never happen").
383 apply IHvarstypes1; inversion X; auto.
384 apply IHvarstypes2; inversion X; auto.
387 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
388 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
389 | INone => T_Leaf None
390 | ILeaf x y => T_Leaf (Some _)
391 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
396 Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y))
397 : ITree (X * Y) (fun x => J (fst x)) t
398 -> ITree X (fun x:X => J x) (mapOptionTree (@fst _ _) t).
400 induction it; simpl in *.
404 simpl; apply IBranch; auto.
407 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
408 refine (fix rec t := match t with
409 | T_Leaf None => T_Leaf None
410 | T_Leaf (Some x) => T_Leaf (Some _)
411 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
413 destruct x as [x fx].
414 refine (bind fx' = fx ; return _).
420 Definition case_helper tc Γ Δ lev tbranches avars ξ :
421 forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)),
422 prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb)))
423 {vars' : Tree ??VV & (snd pcb) = mapOptionTree ξ vars'} ->
425 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
426 & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
427 (weakT' tbranches) (weakL' lev) }) (fst pcb)).
432 destruct pcb as [sac pcb].
436 destruct s as [vars vars_pf].
438 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
439 (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _ ; _).
442 rewrite <- mapOptionTree_compose.
444 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
445 set (mapOptionTree (@fst _ _) localvars) as localvars'.
447 set (list2vec (leaves localvars')) as localvars''.
448 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
449 rewrite H'' in localvars''.
450 cut (distinct (vec2list localvars'')). intro H'''.
451 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
453 refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
458 rewrite <- mapOptionTree_compose.
473 Definition gather_branch_variables
475 (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev
476 (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★)))
479 mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars
480 -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts)
481 -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q)))
482 { vars' : _ & (snd q) = mapOptionTree ξ vars' })
488 destruct a; [ idtac | apply INone ].
490 apply ileaf in source.
492 destruct p as [sac pcb].
504 destruct vars; try destruct o; simpl in pf; inversion pf.
509 apply (IHalts1 vars1 H0 X); auto.
510 apply (IHalts2 vars2 H1 X0); auto.
514 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
515 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
517 induction Σ; intro ξ.
520 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
521 refine (q >>>= fun q' => return _).
524 destruct q' as [varstypes [pf1 [pf2 distpf]]].
525 exists (mapOptionTree (@fst _ _) varstypes).
526 exists (update_xi ξ l (leaves varstypes)).
531 refine (bind f1 = IHΣ1 ξ ; _).
533 destruct f1 as [vars1 [ξ1 pf1]].
534 refine (bind f2 = IHΣ2 ξ1 ; _).
536 destruct f2 as [vars2 [ξ2 pf22]].
538 exists (vars1,,vars2).
543 admit. (* freshness assumption *)
546 Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
547 forall (X_ : ITree Judg judg2exprType
548 ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])),
549 ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
553 destruct vars; try destruct o; inversion H.
555 refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
558 destruct pf as [ vnew [ pf1 pf2 ]].
559 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
565 refine (X ξ vars1 _ >>>= fun X0' => _).
570 refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
582 apply ELet with (ev:=vnew)(tv:=σ₁).
587 Definition vartree Γ Δ Σ lev ξ :
588 forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
589 ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
594 destruct vars; try destruct o; inversion H.
595 set (EVar Γ Δ ξ v) as q.
601 destruct vars; try destruct o; inversion H.
610 Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev :
611 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
612 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
618 set (X ξ vars H) as q.
620 refine (q >>>= fun q' => return _).
626 Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev :
627 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
628 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
634 set (X ξ vars H) as q.
636 refine (q >>>= fun q' => return _).
642 Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev :
643 ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
644 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
649 eapply X with (vars:=[],,vars).
650 rewrite H; reflexivity.
653 Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev :
654 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
655 ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
660 destruct vars; try destruct o; inversion H.
661 eapply X with (vars:=vars2).
665 Definition rassoc Γ Δ Σ₁ a b c lev :
666 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
667 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
672 destruct vars; try destruct o; inversion H.
673 destruct vars2; try destruct o; inversion H2.
674 apply X with (vars:=(vars1,,vars2_1),,vars2_2).
678 Definition rassoc' Γ Δ Σ₁ a b c lev :
679 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
680 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
685 destruct vars; try destruct o; inversion H.
686 destruct vars1; try destruct o; inversion H1.
687 apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
691 Definition swapr Γ Δ Σ₁ a b c lev :
692 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
693 ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
698 destruct vars; try destruct o; inversion H.
699 destruct vars1; try destruct o; inversion H1.
700 apply X with (vars:=(vars1_2,,vars1_1),,vars2).
704 Definition rdup Γ Δ Σ₁ a c lev :
705 ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
706 ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
711 destruct vars; try destruct o; inversion H.
712 apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *)
716 (* holy cow this is ugly *)
717 Definition rcut Γ Δ Σ₃ lev Σ₁₂ :
719 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
720 ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
721 ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
740 set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q.
741 set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
746 apply rassoc' in q''.
751 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
755 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
756 | RArrange a b c d e l r => let case_RURule := tt in _
757 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
758 | RLit Γ Δ l _ => let case_RLit := tt in _
759 | RVar Γ Δ σ p => let case_RVar := tt in _
760 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
761 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
762 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
763 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
764 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
765 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
766 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
767 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
768 | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
769 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
770 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
771 | RVoid _ _ l => let case_RVoid := tt in _
772 | RBrak Σ a b c n m => let case_RBrak := tt in _
773 | REsc Σ a b c n m => let case_REsc := tt in _
774 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
775 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
776 end); intro X_; try apply ileaf in X_; simpl in X_.
778 destruct case_RURule.
779 apply ILeaf. simpl. intros.
780 set (@urule2expr a b _ _ e l r0 ξ) as q.
781 unfold ujudg2exprType.
782 unfold ujudg2exprType in q.
783 apply q with (vars:=vars).
785 apply X_ with (vars:=vars0).
790 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
795 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
800 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
805 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
809 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
810 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
811 set (@EVar _ _ _ Δ ξ v) as q.
817 destruct case_RGlobal.
818 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
824 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
826 destruct pf as [ vnew [ pf1 pf2 ]].
827 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
828 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
838 apply ELam with (ev:=vnew).
845 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
848 apply ileaf in X. simpl in X.
858 destruct vars. try destruct o; inversion H.
861 set (X1 ξ vars1 H5) as q1.
862 set (X2 ξ vars2 H6) as q2.
863 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
870 apply (EApp _ _ _ _ _ _ q1' q2').
897 set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
898 set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
905 refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
913 destruct vars; try destruct o; inversion H.
914 refine (X_ _ _ H2 >>>= fun X' => return _).
921 destruct case_RRight.
924 destruct vars; try destruct o; inversion H.
925 refine (X_ _ _ H1 >>>= fun X' => return _).
933 apply ILeaf; simpl; intros.
938 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
943 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
944 rewrite mapOptionTree_compose.
947 apply ileaf in X. simpl in *.
951 destruct case_RAppCo.
952 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
958 destruct case_RAbsCo.
959 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
964 destruct case_RLetRec.
965 apply ILeaf; simpl; intros.
966 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
967 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
968 refine (X_ ((update_xi ξ t (leaves varstypes)))
969 ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_. apply FreshMon.
975 inversion X; subst; clear X.
977 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
979 apply (@letrec_helper Γ Δ t varstypes).
980 rewrite mapOptionTree_compose.
981 rewrite mapOptionTree_compose.
983 replace ((mapOptionTree unlev (y @@@ t))) with y.
985 clear pf1 X0 X1 pfdist pf2 vars varstypes.
986 induction y; try destruct a; auto.
995 apply ILeaf; simpl; intros.
1002 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1003 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1004 rename Σ into body_freevars_types.
1005 rename vars into all_freevars.
1006 rename X0 into body_expr.
1007 rename X into alts_exprs.
1009 destruct all_freevars; try destruct o; inversion H.
1010 rename all_freevars2 into body_freevars.
1011 rename all_freevars1 into alts_freevars.
1013 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1014 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1015 apply fix_indexing in alts_exprs'.
1016 simpl in alts_exprs'.
1017 apply unindex_tree in alts_exprs'.
1018 simpl in alts_exprs'.
1019 apply fix2 in alts_exprs'.
1020 apply treeM in alts_exprs'.
1022 refine ( alts_exprs' >>>= fun Y =>
1024 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1030 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1031 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1032 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
1033 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1034 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1037 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1038 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1039 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1041 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1042 apply closed2expr in cnd.
1046 refine (bind ξvars = manyFresh _ Σ ξ0; _).
1048 destruct ξvars as [vars ξpf].
1049 destruct ξpf as [ξ pf].
1050 refine (cnd ξ vars _ >>>= fun it => _).
1053 refine (return OK _).
1061 End HaskProofToStrong.