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 (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
397 : ITree { x:X & F x } (fun x => J (projT1 x)) t
398 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) 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:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
422 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
424 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
425 & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
426 (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
431 destruct pcb as [sac pcb].
435 destruct s as [vars vars_pf].
437 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
438 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
441 rewrite <- mapOptionTree_compose.
443 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
444 set (mapOptionTree (@fst _ _) localvars) as localvars'.
446 set (list2vec (leaves localvars')) as localvars''.
447 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
448 rewrite H'' in localvars''.
449 cut (distinct (vec2list localvars'')). intro H'''.
450 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
452 refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
457 rewrite <- mapOptionTree_compose.
472 Definition gather_branch_variables
473 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
474 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
477 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
478 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
479 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
480 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
486 destruct a; [ idtac | apply INone ].
488 apply ileaf in source.
490 destruct s as [sac pcb].
502 destruct vars; try destruct o; simpl in pf; inversion pf.
507 apply (IHalts1 vars1 H0 X); auto.
508 apply (IHalts2 vars2 H1 X0); auto.
512 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
513 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
515 induction Σ; intro ξ.
518 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
519 refine (q >>>= fun q' => return _).
522 destruct q' as [varstypes [pf1 [pf2 distpf]]].
523 exists (mapOptionTree (@fst _ _) varstypes).
524 exists (update_xi ξ l (leaves varstypes)).
529 refine (bind f1 = IHΣ1 ξ ; _).
531 destruct f1 as [vars1 [ξ1 pf1]].
532 refine (bind f2 = IHΣ2 ξ1 ; _).
534 destruct f2 as [vars2 [ξ2 pf22]].
536 exists (vars1,,vars2).
541 admit. (* freshness assumption *)
544 Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
545 forall (X_ : ITree Judg judg2exprType
546 ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])),
547 ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
551 destruct vars; try destruct o; inversion H.
553 refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
556 destruct pf as [ vnew [ pf1 pf2 ]].
557 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
563 refine (X ξ vars1 _ >>>= fun X0' => _).
568 refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
580 apply ELet with (ev:=vnew)(tv:=σ₁).
585 Definition vartree Γ Δ Σ lev ξ :
586 forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
587 ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
592 destruct vars; try destruct o; inversion H.
593 set (EVar Γ Δ ξ v) as q.
599 destruct vars; try destruct o; inversion H.
608 Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev :
609 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
610 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
616 set (X ξ vars H) as q.
618 refine (q >>>= fun q' => return _).
624 Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev :
625 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
626 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
632 set (X ξ vars H) as q.
634 refine (q >>>= fun q' => return _).
640 Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev :
641 ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
642 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
647 eapply X with (vars:=[],,vars).
648 rewrite H; reflexivity.
651 Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev :
652 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
653 ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
658 destruct vars; try destruct o; inversion H.
659 eapply X with (vars:=vars2).
663 Definition rassoc Γ Δ Σ₁ a b c lev :
664 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
665 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
670 destruct vars; try destruct o; inversion H.
671 destruct vars2; try destruct o; inversion H2.
672 apply X with (vars:=(vars1,,vars2_1),,vars2_2).
676 Definition rassoc' Γ Δ Σ₁ a b c lev :
677 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
678 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
683 destruct vars; try destruct o; inversion H.
684 destruct vars1; try destruct o; inversion H1.
685 apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
689 Definition swapr Γ Δ Σ₁ a b c lev :
690 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
691 ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
696 destruct vars; try destruct o; inversion H.
697 destruct vars1; try destruct o; inversion H1.
698 apply X with (vars:=(vars1_2,,vars1_1),,vars2).
702 Definition rdup Γ Δ Σ₁ a c lev :
703 ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
704 ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
709 destruct vars; try destruct o; inversion H.
710 apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *)
714 (* holy cow this is ugly *)
715 Definition rcut Γ Δ Σ₃ lev Σ₁₂ :
717 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
718 ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
719 ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
738 set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q.
739 set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
744 apply rassoc' in q''.
749 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
753 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
754 | RArrange a b c d e l r => let case_RURule := tt in _
755 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
756 | RLit Γ Δ l _ => let case_RLit := tt in _
757 | RVar Γ Δ σ p => let case_RVar := tt in _
758 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
759 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
760 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
761 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
762 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
763 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
764 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
765 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
766 | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
767 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
768 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
769 | RVoid _ _ l => let case_RVoid := tt in _
770 | RBrak Σ a b c n m => let case_RBrak := tt in _
771 | REsc Σ a b c n m => let case_REsc := tt in _
772 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
773 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
774 end); intro X_; try apply ileaf in X_; simpl in X_.
776 destruct case_RURule.
777 apply ILeaf. simpl. intros.
778 set (@urule2expr a b _ _ e l r0 ξ) as q.
779 unfold ujudg2exprType.
780 unfold ujudg2exprType in q.
781 apply q with (vars:=vars).
783 apply X_ with (vars:=vars0).
788 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
793 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
798 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
803 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
807 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
808 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
809 set (@EVar _ _ _ Δ ξ v) as q.
815 destruct case_RGlobal.
816 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
822 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
824 destruct pf as [ vnew [ pf1 pf2 ]].
825 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
826 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
836 apply ELam with (ev:=vnew).
843 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
846 apply ileaf in X. simpl in X.
856 destruct vars. try destruct o; inversion H.
859 set (X1 ξ vars1 H5) as q1.
860 set (X2 ξ vars2 H6) as q2.
861 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
868 apply (EApp _ _ _ _ _ _ q1' q2').
895 set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
896 set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
903 refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
911 destruct vars; try destruct o; inversion H.
912 refine (X_ _ _ H2 >>>= fun X' => return _).
919 destruct case_RRight.
922 destruct vars; try destruct o; inversion H.
923 refine (X_ _ _ H1 >>>= fun X' => return _).
931 apply ILeaf; simpl; intros.
936 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
941 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
942 rewrite mapOptionTree_compose.
945 apply ileaf in X. simpl in *.
949 destruct case_RAppCo.
950 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
956 destruct case_RAbsCo.
957 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
962 destruct case_RLetRec.
963 apply ILeaf; simpl; intros.
964 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
965 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
966 refine (X_ ((update_xi ξ t (leaves varstypes)))
967 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
973 inversion X; subst; clear X.
975 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
977 apply (@letrec_helper Γ Δ t varstypes).
978 rewrite mapOptionTree_compose.
979 rewrite mapOptionTree_compose.
981 replace ((mapOptionTree unlev (y @@@ t))) with y.
983 clear pf1 X0 X1 pfdist pf2 vars varstypes.
984 induction y; try destruct a; auto.
993 apply ILeaf; simpl; intros.
1000 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1001 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1002 rename Σ into body_freevars_types.
1003 rename vars into all_freevars.
1004 rename X0 into body_expr.
1005 rename X into alts_exprs.
1007 destruct all_freevars; try destruct o; inversion H.
1008 rename all_freevars2 into body_freevars.
1009 rename all_freevars1 into alts_freevars.
1011 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1012 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1013 apply fix_indexing in alts_exprs'.
1014 simpl in alts_exprs'.
1015 apply unindex_tree in alts_exprs'.
1016 simpl in alts_exprs'.
1017 apply fix2 in alts_exprs'.
1018 apply treeM in alts_exprs'.
1020 refine ( alts_exprs' >>>= fun Y =>
1022 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1028 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1029 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1030 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
1031 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1032 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1035 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1036 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1037 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1039 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1040 apply closed2expr in cnd.
1044 refine (bind ξvars = manyFresh _ Σ ξ0; _).
1046 destruct ξvars as [vars ξpf].
1047 destruct ξpf as [ξ pf].
1048 refine (cnd ξ vars _ >>>= fun it => _).
1051 refine (return OK _).
1059 End HaskProofToStrong.