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 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
767 | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
768 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
769 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
770 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
771 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
772 | RVoid _ _ l => let case_RVoid := tt in _
773 | RBrak Σ a b c n m => let case_RBrak := tt in _
774 | REsc Σ a b c n m => let case_REsc := tt in _
775 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
776 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
777 end); intro X_; try apply ileaf in X_; simpl in X_.
779 destruct case_RURule.
780 apply ILeaf. simpl. intros.
781 set (@urule2expr a b _ _ e l r0 ξ) as q.
782 unfold ujudg2exprType.
783 unfold ujudg2exprType in q.
784 apply q with (vars:=vars).
786 apply X_ with (vars:=vars0).
791 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
796 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
801 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
806 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
810 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
811 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
812 set (@EVar _ _ _ Δ ξ v) as q.
818 destruct case_RGlobal.
819 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
825 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
827 destruct pf as [ vnew [ pf1 pf2 ]].
828 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
829 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
839 apply ELam with (ev:=vnew).
846 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
849 apply ileaf in X. simpl in X.
853 apply ILeaf; simpl; intros.
858 destruct vars; inversion H.
859 destruct o; inversion H3.
860 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
872 destruct vars. try destruct o; inversion H.
875 set (X1 ξ vars1 H5) as q1.
876 set (X2 ξ vars2 H6) as q2.
877 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
884 apply (EApp _ _ _ _ _ _ q1' q2').
890 destruct case_RWhere.
893 destruct vars; try destruct o; inversion H.
894 destruct vars2; try destruct o; inversion H2.
897 assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
898 refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
901 destruct pf as [ vnew [ pf1 pf2 ]].
902 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
908 refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
917 refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
926 apply ELet with (ev:=vnew)(tv:=σ₁).
946 set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
947 set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
954 refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
962 destruct vars; try destruct o; inversion H.
963 refine (X_ _ _ H2 >>>= fun X' => return _).
970 destruct case_RRight.
973 destruct vars; try destruct o; inversion H.
974 refine (X_ _ _ H1 >>>= fun X' => return _).
982 apply ILeaf; simpl; intros.
987 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
992 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
993 rewrite mapOptionTree_compose.
996 apply ileaf in X. simpl in *.
1000 destruct case_RAppCo.
1001 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
1007 destruct case_RAbsCo.
1008 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
1013 destruct case_RLetRec.
1014 apply ILeaf; simpl; intros.
1015 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
1016 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
1017 refine (X_ ((update_xi ξ t (leaves varstypes)))
1018 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
1024 inversion X; subst; clear X.
1026 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
1028 apply (@letrec_helper Γ Δ t varstypes).
1029 rewrite mapOptionTree_compose.
1030 rewrite mapOptionTree_compose.
1032 replace ((mapOptionTree unlev (y @@@ t))) with y.
1034 clear pf1 X0 X1 pfdist pf2 vars varstypes.
1035 induction y; try destruct a; auto.
1043 destruct case_RCase.
1044 apply ILeaf; simpl; intros.
1051 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1052 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1053 rename Σ into body_freevars_types.
1054 rename vars into all_freevars.
1055 rename X0 into body_expr.
1056 rename X into alts_exprs.
1058 destruct all_freevars; try destruct o; inversion H.
1059 rename all_freevars2 into body_freevars.
1060 rename all_freevars1 into alts_freevars.
1062 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1063 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1064 apply fix_indexing in alts_exprs'.
1065 simpl in alts_exprs'.
1066 apply unindex_tree in alts_exprs'.
1067 simpl in alts_exprs'.
1068 apply fix2 in alts_exprs'.
1069 apply treeM in alts_exprs'.
1071 refine ( alts_exprs' >>>= fun Y =>
1073 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1079 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1080 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1081 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
1082 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1083 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1086 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1087 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1088 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1090 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1091 apply closed2expr in cnd.
1095 refine (bind ξvars = manyFresh _ Σ ξ0; _).
1097 destruct ξvars as [vars ξpf].
1098 destruct ξpf as [ξ pf].
1099 refine (cnd ξ vars _ >>>= fun it => _).
1102 refine (return OK _).
1110 End HaskProofToStrong.