X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=2ea0c4a1e4cfaea4311bcda04a7090166d87d53f;hp=65c638eb2d9bddbd41bbb1965d58271c3ab8618a;hb=171beb27508a340b24ab14837e72451d0b500805;hpb=17ed8145b371ce578db7fdd67aced8dd2013e623 diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 65c638e..2ea0c4a 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. @@ -25,19 +26,13 @@ Section HaskProofToStrong. Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★. - Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type := - match j with - mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) - end. - Definition judg2exprType (j:Judg) : Type := match j with - (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ) + (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> + FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ) end. - Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ. + Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l. intros. inversion X; auto. Defined. @@ -47,8 +42,8 @@ Section HaskProofToStrong. apply X0. Defined. - Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) l1 l2 q, - update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) l1 q. + Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q, + update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q. intros. induction l1. reflexivity. @@ -58,14 +53,6 @@ Section HaskProofToStrong. reflexivity. Qed. - Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t). - intros. - induction t. - destruct a; auto. - simpl; rewrite H; auto. - simpl; rewrite IHt1; rewrite IHt2; auto. - Qed. - Lemma quark {T} (l1:list T) l2 vf : (In vf (app l1 l2)) <-> (In vf l1) \/ (In vf l2). @@ -133,30 +120,53 @@ Section HaskProofToStrong. reflexivity. Qed. + Lemma fresh_lemma'' Γ + : forall types ξ lev, + FreshM { varstypes : _ + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. + admit. + Defined. + Lemma fresh_lemma' Γ - : forall types vars Σ ξ, Σ = mapOptionTree ξ vars -> + : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars -> FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ - /\ mapOptionTree (update_ξ ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }. + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ + /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. induction types. intros; destruct a. refine (bind vf = fresh (leaves vars) ; return _). apply FreshMon. destruct vf as [ vf vf_pf ]. - exists [(vf,l)]. + exists [(vf,h)]. split; auto. simpl. - set (helper VV _ vars vf ξ l vf_pf) as q. + set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q. rewrite q. symmetry; auto. simpl. destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto. + split; auto. + apply distinct_cons. + intro. + inversion H0. + apply distinct_nil. refine (return _). exists []; auto. - intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _). + split. + simpl. + symmetry; auto. + split. + simpl. + reflexivity. + simpl. + apply distinct_nil. + intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _). apply FreshMon. - destruct x2 as [vt2 [pf21 pf22]]. - refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _). + destruct x2 as [vt2 [pf21 [pf22 pfdist]]]. + refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev + (leaves vt2)) _ _; return _). apply FreshMon. simpl. rewrite pf21. @@ -166,7 +176,7 @@ Section HaskProofToStrong. destruct x1 as [vt1 [pf11 pf12]]. exists (vt1,,vt2); split; auto. - set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q. set (mapOptionTree_extensional _ _ q) as q'. rewrite q'. clear q' q. @@ -174,7 +184,7 @@ Section HaskProofToStrong. reflexivity. simpl. - set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q. + set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q. set (mapOptionTree_extensional _ _ q) as q'. rewrite q'. rewrite q'. @@ -182,23 +192,27 @@ Section HaskProofToStrong. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose in *. - rewrite pf12. + split. + destruct pf12. + rewrite H. inversion pf11. rewrite <- mapOptionTree_compose. reflexivity. + + admit. Defined. - Lemma fresh_lemma Γ ξ vars Σ Σ' + Lemma fresh_lemma Γ ξ vars Σ Σ' lev : Σ = mapOptionTree ξ vars -> FreshM { vars' : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ ((vars',Σ')::nil)) vars = Σ - /\ mapOptionTree (update_ξ ξ ((vars',Σ')::nil)) [vars'] = [Σ'] }. + | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ + /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. intros. - set (fresh_lemma' Γ [Σ'] vars Σ ξ H) as q. + set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q. refine (q >>>= fun q' => return _). apply FreshMon. clear q. - destruct q' as [varstypes [pf1 pf2]]. + destruct q' as [varstypes [pf1 [pf2 pfdist]]]. destruct varstypes; try destruct o; try destruct p; simpl in *. destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]. inversion pf2; subst. @@ -209,309 +223,535 @@ Section HaskProofToStrong. inversion pf2. Defined. - Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), - FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. - intros. - set (fresh_lemma' Γ Σ [] [] ξ0 (refl_equal _)) as q. - refine (q >>>= fun q' => return _). - apply FreshMon. - clear q. - destruct q' as [varstypes [pf1 pf2]]. - exists (mapOptionTree (@fst _ _) varstypes). - exists (update_ξ ξ0 (leaves varstypes)). - symmetry; auto. - Defined. - - Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★), - ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j. - - refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : - ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j := - match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with - | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RCanL t a => let case_RCanL := tt in _ - | RCanR t a => let case_RCanR := tt in _ - | RuCanL t a => let case_RuCanL := tt in _ - | RuCanR t a => let case_RuCanR := tt in _ - | RAssoc t a b c => let case_RAssoc := tt in _ - | RCossa t a b c => let case_RCossa := tt in _ - | RExch t a b => let case_RExch := tt in _ - | RWeak t a => let case_RWeak := tt in _ - | RCont t a => let case_RCont := tt in _ + Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type := + forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ). + + Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), + ujudg2exprType Γ ξ Δ h t l -> + ujudg2exprType Γ ξ Δ j t l + . + intros Γ Δ. + refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} : + ujudg2exprType Γ ξ Δ h t l -> + ujudg2exprType Γ ξ Δ j t l := + match r as R in Arrange H C return + ujudg2exprType Γ ξ Δ H t l -> + ujudg2exprType Γ ξ Δ C t l + with + | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r) + | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r) + | AId a => let case_AId := tt in _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in _ + | AuAssoc a b c => let case_AuAssoc := tt in _ + | AExch a b => let case_AExch := tt in _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) end); clear urule2expr; intros. - destruct case_RCanL. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 ([],,vars)). + destruct case_AId. + apply X. + + destruct case_ACanL. + simpl; unfold ujudg2exprType; intros. + simpl in X. + apply (X ([],,vars)). simpl; rewrite <- H; auto. - destruct case_RCanR. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 (vars,,[])). + destruct case_ACanR. + simpl; unfold ujudg2exprType; intros. + simpl in X. + apply (X (vars,,[])). simpl; rewrite <- H; auto. - destruct case_RuCanL. - apply ILeaf; simpl; intros. + destruct case_AuCanL. + simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. - inversion X. - simpl in X0. - apply (X0 vars2); auto. + simpl in X. + apply (X vars2); auto. - destruct case_RuCanR. - apply ILeaf; simpl; intros. + destruct case_AuCanR. + simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. - inversion X. - simpl in X0. - apply (X0 vars1); auto. - - destruct case_RAssoc. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. + simpl in X. + apply (X vars1); auto. + + destruct case_AAssoc. + simpl; unfold ujudg2exprType; intros. + simpl in X. destruct vars; try destruct o; inversion H. destruct vars1; try destruct o; inversion H. - apply (X0 (vars1_1,,(vars1_2,,vars2))). + apply (X (vars1_1,,(vars1_2,,vars2))). subst; auto. - destruct case_RCossa. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. + destruct case_AuAssoc. + simpl; unfold ujudg2exprType; intros. + simpl in X. destruct vars; try destruct o; inversion H. destruct vars2; try destruct o; inversion H. - apply (X0 ((vars1,,vars2_1),,vars2_2)). + apply (X ((vars1,,vars2_1),,vars2_2)). subst; auto. - destruct case_RLeft. - destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. - destruct o; [ idtac | apply INone ]. - destruct u; simpl in *. - apply ILeaf; simpl; intros. + destruct case_AExch. + simpl; unfold ujudg2exprType ; intros. + simpl in X. destruct vars; try destruct o; inversion H. - set (fun q => ileaf (e ξ q)) as r'. - simpl in r'. - apply r' with (vars:=vars2). - clear r' e. - clear r0. - induction h0. - destruct a. - destruct u. + apply (X (vars2,,vars1)). + inversion H; subst; auto. + + destruct case_AWeak. + simpl; unfold ujudg2exprType; intros. + simpl in X. + apply (X []). + auto. + + destruct case_ACont. + simpl; unfold ujudg2exprType ; intros. + simpl in X. + apply (X (vars,,vars)). + simpl. + rewrite <- H. + auto. + + destruct case_ALeft. + intro vars; unfold ujudg2exprType; intro H. + destruct vars; try destruct o; inversion H. + apply (fun q => e ξ q vars2 H2). + clear r0 e H2. simpl in X. - apply ileaf in X. - apply ILeaf. simpl. - simpl in X. + unfold ujudg2exprType. intros. apply X with (vars:=vars1,,vars). - simpl. rewrite H0. rewrite H1. + simpl. reflexivity. - apply INone. - apply IBranch. - apply IHh0_1. inversion X; auto. - apply IHh0_2. inversion X; auto. - auto. - - destruct case_RRight. - destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. - destruct o; [ idtac | apply INone ]. - destruct u; simpl in *. - apply ILeaf; simpl; intros. + + destruct case_ARight. + intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. - set (fun q => ileaf (e ξ q)) as r'. - simpl in r'. - apply r' with (vars:=vars1). - clear r' e. - clear r0. - induction h0. - destruct a. - destruct u. + apply (fun q => e ξ q vars1 H1). + clear r0 e H2. simpl in X. - apply ileaf in X. - apply ILeaf. simpl. - simpl in X. + unfold ujudg2exprType. intros. apply X with (vars:=vars,,vars2). - simpl. rewrite H0. - rewrite H2. + inversion H. + simpl. reflexivity. - apply INone. - apply IBranch. - apply IHh0_1. inversion X; auto. - apply IHh0_2. inversion X; auto. - auto. - - destruct case_RExch. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - destruct vars; try destruct o; inversion H. - apply (X0 (vars2,,vars1)). - inversion H; subst; auto. - - destruct case_RWeak. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 []). - auto. - - destruct case_RCont. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 (vars,,vars)). - simpl. - rewrite <- H. - auto. - Defined. - Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ : - ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c. - intro it. - induction c. - destruct a. - destruct u; simpl in *. - apply ileaf in it. - apply ILeaf. - simpl in *. - intros; apply it with (vars:=vars); auto. - apply INone. - apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto. - Defined. + destruct case_AComp. + apply e2. + apply e1. + apply X. + Defined. - Definition letrec_helper Γ Δ l varstypes ξ' : - ITree (LeveledHaskType Γ ★) - (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t) - (mapOptionTree (ξ' ○ (@fst _ _)) varstypes) - -> ELetRecBindings Γ Δ ξ' l - (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) varstypes). + Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : + ITree (HaskType Γ ★) + (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l) + (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes) + -> ELetRecBindings Γ Δ ξ' l varstypes. intros. induction varstypes. destruct a; simpl in *. destruct p. - destruct l0 as [τ l']. simpl. apply ileaf in X. simpl in X. - destruct (eqd_dec (unlev (ξ' v)) τ). - rewrite <- e. apply ELR_leaf. + rename h into τ. + destruct (eqd_dec (unlev (ξ' v)) τ). + rewrite <- e. destruct (ξ' v). simpl. destruct (eqd_dec h0 l). rewrite <- e0. + simpl in X. + subst. apply X. - apply (Prelude_error "level mismatch; should never happen"). - apply (Prelude_error "letrec type mismatch; should never happen"). + apply (Prelude_error "level mismatch; should never happen"). + apply (Prelude_error "letrec type mismatch; should never happen"). apply ELR_nil. + apply ELR_branch. + apply IHvarstypes1; inversion X; auto. + apply IHvarstypes2; inversion X; auto. + Defined. - simpl; apply ELR_branch. - apply IHvarstypes1. - simpl in X. - inversion X; auto. - apply IHvarstypes2. - simpl in X. - inversion X; auto. + Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }. + refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with + | INone => T_Leaf None + | ILeaf x y => T_Leaf (Some _) + | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2) + end). + exists x; auto. + Defined. + Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x }) + : ITree { x:X & F x } (fun x => J (projT1 x)) t + -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t). + intro it. + induction it; simpl in *. + apply INone. + apply ILeaf. + apply f. + simpl; apply IBranch; auto. Defined. - Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t. - induction t; auto. + Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }). + refine (fix rec t := match t with + | T_Leaf None => T_Leaf None + | T_Leaf (Some x) => T_Leaf (Some _) + | T_Branch b1 b2 => T_Branch (rec b1) (rec b2) + end). + destruct x as [x fx]. + refine (bind fx' = fx ; return _). + apply FreshMon. + exists x. + apply fx'. + Defined. + + Definition case_helper tc Γ Δ lev tbranches avars ξ : + forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac}, + prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> + ((fun sac => FreshM + { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac + & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) + (weakT' tbranches) (weakL' lev) }) (projT1 pcb)). + intro pcb. + intro X. + simpl in X. simpl. - rewrite IHt; auto. - Qed. + destruct pcb as [sac pcb]. + simpl in *. + + destruct X. + destruct s as [vars vars_pf]. - Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) : - forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars, - judg2exprType (pcb_judg pcb) -> - (pcb_freevars pcb) = mapOptionTree ξ Σ -> - FreshM - {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars & - Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}. + refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars + (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _). + apply FreshMon. + rewrite vars_pf. + rewrite <- mapOptionTree_compose. + reflexivity. + destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]]. + set (mapOptionTree (@fst _ _) localvars) as localvars'. + + set (list2vec (leaves localvars')) as localvars''. + cut (length (leaves localvars') = sac_numExprVars sac). intro H''. + rewrite H'' in localvars''. + cut (distinct (vec2list localvars'')). intro H'''. + set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb. + + refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _). + apply FreshMon. + simpl. + unfold scbwv_xi. + rewrite vars_pf. + rewrite <- mapOptionTree_compose. + clear localvars_pf1. + simpl. + rewrite mapleaves'. + + admit. + + exists scb. + apply ileaf in q. + apply q. + + admit. + admit. + Defined. + + Definition gather_branch_variables + Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon & + ProofCaseBranch tc Γ Δ lev tbranches avars sac}) + : + forall vars, + mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars + -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts) + -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) + { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' }) + alts. + induction alts; + intro vars; + intro pf; + intro source. + destruct a; [ idtac | apply INone ]. + simpl in *. + apply ileaf in source. + apply ILeaf. + destruct s as [sac pcb]. + simpl in *. + split. intros. - simpl in X. - destruct pcb. + eapply source. + apply H. + clear source. + + exists vars. + auto. + + simpl in pf. + destruct vars; try destruct o; simpl in pf; inversion pf. + simpl in source. + inversion source. + subst. + apply IBranch. + apply (IHalts1 vars1 H0 X); auto. + apply (IHalts2 vars2 H1 X0); auto. + + Defined. + + Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), + FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. + intros Γ Σ. + induction Σ; intro ξ. + destruct a. + destruct l as [τ l]. + set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q. + refine (q >>>= fun q' => return _). + apply FreshMon. + clear q. + destruct q' as [varstypes [pf1 [pf2 distpf]]]. + exists (mapOptionTree (@fst _ _) varstypes). + exists (update_xi ξ l (leaves varstypes)). + symmetry; auto. + refine (return _). + exists []. + exists ξ; auto. + refine (bind f1 = IHΣ1 ξ ; _). + apply FreshMon. + destruct f1 as [vars1 [ξ1 pf1]]. + refine (bind f2 = IHΣ2 ξ1 ; _). + apply FreshMon. + destruct f2 as [vars2 [ξ2 pf22]]. + refine (return _). + exists (vars1,,vars2). + exists ξ2. + simpl. + rewrite pf22. + rewrite pf1. + admit. (* freshness assumption *) + Defined. + + Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p : + forall (X_ : ITree Judg judg2exprType + ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])), + ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p]. + intros. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + + refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). + apply FreshMon. + + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + inversion X_. + apply ileaf in X. + apply ileaf in X0. simpl in *. - set (sac_types pcb_scb _ avars) as boundvars. - refine (fresh_lemma' _ (unleaves (map (fun x => x@@(weakL' lev)) (vec2list boundvars))) Σ - (mapOptionTree weakLT' pcb_freevars) - (weakLT' ○ ξ) _ - >>>= fun ξvars => _). apply FreshMon. - rewrite H. - rewrite <- mapOptionTree_compose. + + refine (X ξ vars1 _ >>>= fun X0' => _). + apply FreshMon. + simpl. + auto. + + refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). + apply FreshMon. + simpl. + rewrite pf2. + rewrite pf1. reflexivity. - destruct ξvars as [ exprvars [pf1 pf2 ]]. - set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'. - assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'. - rewrite <- mapOptionTree_compose in pf2. - simpl in pf2. - rewrite mapleaves. - rewrite <- map_preserves_length. - rewrite map_preserves_length with (f:=update_ξ (weakLT' ○ ξ) (leaves exprvars) ○ (@fst _ _)). - rewrite <- mapleaves. - rewrite pf2. - rewrite leaves_unleaves. - rewrite vec2list_map_list2vec. - rewrite vec2list_len. - reflexivity. - rewrite <- H' in exprvars'. - clear H'. - - set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars') as scb. - set (scbwv_ξ scb ξ lev) as ξ'. - refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon. - simpl. - unfold ξ'. - unfold scbwv_ξ. - simpl. - rewrite <- vec2list_map_list2vec. - rewrite <- pf1. - admit. - - apply ileaf in X'. - simpl in X'. - exists scb. - unfold weakCK''. - unfold ξ' in X'. - apply X'. + apply FreshMon. + + apply ILeaf. + apply ileaf in X1'. + apply ileaf in X0'. + simpl in *. + apply ELet with (ev:=vnew)(tv:=σ₁). + apply X0'. + apply X1'. + Defined. + + Definition vartree Γ Δ Σ lev ξ : + forall vars, Σ @@@ lev = mapOptionTree ξ vars -> + ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ. + induction Σ; intros. + destruct a. + intros; simpl in *. + apply ILeaf. + destruct vars; try destruct o; inversion H. + set (EVar Γ Δ ξ v) as q. + rewrite <- H1 in q. + apply q. + intros. + apply INone. + intros. + destruct vars; try destruct o; inversion H. + apply IBranch. + eapply IHΣ1. + apply H1. + eapply IHΣ2. + apply H2. Defined. - Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) := - match t with - | T_Leaf None => return [] - | T_Leaf (Some x) => bind x' = x ; return [x'] - | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2') - end. - Lemma itree_mapOptionTree : forall T T' F (f:T->T') t, - ITree _ F (mapOptionTree f t) -> - ITree _ (F ○ f) t. + Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. intros. - induction t; try destruct a; simpl in *. - apply ILeaf. - inversion X; auto. - apply INone. - apply IBranch. - apply IHt1; inversion X; auto. - apply IHt2; inversion X; auto. - Defined. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + apply X0. + Defined. + + Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *. + intros. + set (X ξ vars H) as q. + simpl in q. + refine (q >>>= fun q' => return _). + apply FreshMon. + inversion q'. + auto. + Defined. + + Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + eapply X with (vars:=[],,vars). + rewrite H; reflexivity. + Defined. + + Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev : + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + eapply X with (vars:=vars2). + auto. + Defined. + + Definition rassoc Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars2; try destruct o; inversion H2. + apply X with (vars:=(vars1,,vars2_1),,vars2_2). + subst; reflexivity. + Defined. + + Definition rassoc' Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=vars1_1,,(vars1_2,,vars2)). + subst; reflexivity. + Defined. + + Definition swapr Γ Δ Σ₁ a b c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars1; try destruct o; inversion H1. + apply X with (vars:=(vars1_2,,vars1_1),,vars2). + subst; reflexivity. + Defined. + + Definition rdup Γ Δ Σ₁ a c lev : + ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev]. + intros. + apply ileaf in X. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *) + subst; reflexivity. + Defined. + + (* holy cow this is ugly *) + Definition rcut Γ Δ Σ₃ lev Σ₁₂ : + forall Σ₁ Σ₂, + ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] -> + ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev]. + + induction Σ₁₂. + intros. + destruct a. + + eapply rlet. + apply IBranch. + apply X. + apply X0. + + simpl in X0. + apply rdrop'' in X0. + apply rdrop'''. + apply X0. + + intros. + simpl in X0. + apply rassoc in X0. + set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q. + set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'. + apply rassoc' in q. + apply swapr in q. + apply rassoc in q. + set (q' q) as q''. + apply rassoc' in q''. + apply rdup in q''. + apply q''. + Defined. Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j. intros h j r. refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with - | RURule a b c d e => let case_RURule := tt in _ + | RArrange a b c d e l r => let case_RURule := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ p => let case_RVar := tt in _ @@ -524,27 +764,27 @@ Section HaskProofToStrong. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _ - | REmptyGroup _ _ => let case_REmptyGroup := tt in _ + | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ + | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ + | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ - | RLetRec Γ Δ lri x y => let case_RLetRec := tt in _ + | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _ end); intro X_; try apply ileaf in X_; simpl in X_. - destruct case_RURule. - destruct d; try destruct o. - apply ILeaf; destruct u; simpl; intros. - set (@urule2expr a b _ _ e ξ) as q. - set (fun z => ileaf (q z)) as q'. - simpl in q'. - apply q' with (vars:=vars). - clear q' q. - apply bridge. - apply X_. + destruct case_RURule. + apply ILeaf. simpl. intros. + set (@urule2expr a b _ _ e l r0 ξ) as q. + unfold ujudg2exprType. + unfold ujudg2exprType in q. + apply q with (vars:=vars). + intros. + apply X_ with (vars:=vars0). + auto. auto. - apply no_urules_with_empty_conclusion in e; inversion e; auto. - apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto. destruct case_RBrak. apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. @@ -567,22 +807,24 @@ Section HaskProofToStrong. destruct case_RVar. apply ILeaf; simpl; intros; refine (return ILeaf _ _). - destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2. - apply EVar. + destruct vars; simpl in H; inversion H; destruct o. inversion H1. + set (@EVar _ _ _ Δ ξ v) as q. + rewrite <- H2 in q. + simpl in q. + apply q. inversion H. destruct case_RGlobal. apply ILeaf; simpl; intros; refine (return ILeaf _ _). apply EGlobal. - apply wev. destruct case_RLam. apply ILeaf. simpl in *; intros. - refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)). + refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ ((⟨vnew, tx @@ x ⟩) :: nil)) as ξ' in *. + set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *. refine (X_ ξ' (vars,,[vnew]) _ >>>= _). apply FreshMon. simpl. @@ -606,19 +848,6 @@ Section HaskProofToStrong. apply ileaf in X. simpl in X. apply X. - destruct case_RBindingGroup. - apply ILeaf; simpl; intros. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - destruct vars; inversion H. - destruct o; inversion H3. - refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _). - apply FreshMon. - apply FreshMon. - apply IBranch; auto. - destruct case_RApp. apply ILeaf. inversion X_. @@ -641,38 +870,101 @@ Section HaskProofToStrong. apply (EApp _ _ _ _ _ _ q1' q2'). destruct case_RLet. + eapply rlet. + apply X_. + + destruct case_RWhere. apply ILeaf. simpl in *; intros. - destruct vars; try destruct o; inversion H. - refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)). + destruct vars; try destruct o; inversion H. + destruct vars2; try destruct o; inversion H2. + clear H2. + + assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. + refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)). apply FreshMon. + destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. simpl in *. - refine (X0 ξ vars2 _ >>>= fun X0' => _). - apply FreshMon. - auto. - refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _). + + refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _). apply FreshMon. - rewrite H1. simpl. + inversion pf1. + rewrite H3. + rewrite H4. rewrite pf2. - rewrite pf1. - rewrite H1. reflexivity. - refine (return _). + + refine (X0 ξ vars2_1 _ >>>= fun X1' => _). + apply FreshMon. + reflexivity. + apply FreshMon. + apply ILeaf. apply ileaf in X0'. apply ileaf in X1'. simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₂). - apply X0'. + apply ELet with (ev:=vnew)(tv:=σ₁). apply X1'. + apply X0'. + + destruct case_RCut. + inversion X_. + subst. + clear X_. + induction Σ₃. + destruct a. + subst. + eapply rcut. + apply X. + apply X0. - destruct case_REmptyGroup. + apply ILeaf. + simpl. + intros. + refine (return _). + apply INone. + set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1. + set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2. + apply ileaf in q1. + apply ileaf in q2. + simpl in *. + apply ILeaf. + simpl. + intros. + refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _). + apply FreshMon. + apply FreshMon. + apply IBranch; auto. + + destruct case_RLeft. + apply ILeaf. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H2 >>>= fun X' => return _). + apply FreshMon. + apply IBranch. + eapply vartree. + apply H1. + apply X'. + + destruct case_RRight. + apply ILeaf. + simpl; intros. + destruct vars; try destruct o; inversion H. + refine (X_ _ _ H1 >>>= fun X' => return _). + apply FreshMon. + apply IBranch. + apply X'. + eapply vartree. + apply H2. + + destruct case_RVoid. apply ILeaf; simpl; intros. refine (return _). apply INone. @@ -706,34 +998,33 @@ Section HaskProofToStrong. destruct case_RLetRec. apply ILeaf; simpl; intros. - refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon. - destruct ξvars as [ varstypes [ pf1 pf2 ]]. - refine (X_ ((update_ξ ξ (leaves varstypes))) + refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. + destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. + refine (X_ ((update_xi ξ t (leaves varstypes))) (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. rewrite pf1. auto. apply ILeaf. - destruct x as [τ l]. inversion X; subst; clear X. - (* getting rid of this will require strengthening RLetRec *) - assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH. - admit. - - apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes)); - rewrite mapleaves; rewrite <- map_compose; simpl; - [ idtac - | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ]. - - clear X0. - rewrite <- mapOptionTree_compose in X1. - set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *. - rewrite <- mapleaves. - rewrite HHH. - - apply (letrec_helper _ _ _ _ _ X1). + apply (@ELetRec _ _ _ _ _ _ _ varstypes). + auto. + apply (@letrec_helper Γ Δ t varstypes). + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite pf2. + replace ((mapOptionTree unlev (y @@@ t))) with y. + apply X0. + clear pf1 X0 X1 pfdist pf2 vars varstypes. + induction y; try destruct a; auto. + rewrite IHy1 at 1. + rewrite IHy2 at 1. + reflexivity. + apply ileaf in X1. + simpl in X1. + apply X1. destruct case_RCase. apply ILeaf; simpl; intros. @@ -742,45 +1033,47 @@ Section HaskProofToStrong. subst. apply ileaf in X0. simpl in X0. - set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *. - refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _). - apply FreshMon. - destruct vars; try destruct o; inversion H; clear H. - rename vars1 into varsalts. - rename vars2 into varsΣ. - - refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto. + (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free + * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *) + rename Σ into body_freevars_types. + rename vars into all_freevars. + rename X0 into body_expr. + rename X into alts_exprs. + + destruct all_freevars; try destruct o; inversion H. + rename all_freevars2 into body_freevars. + rename all_freevars1 into alts_freevars. + + set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q. + set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'. + apply fix_indexing in alts_exprs'. + simpl in alts_exprs'. + apply unindex_tree in alts_exprs'. + simpl in alts_exprs'. + apply fix2 in alts_exprs'. + apply treeM in alts_exprs'. + + refine ( alts_exprs' >>>= fun Y => + body_expr ξ _ _ + >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto. apply FreshMon. - destruct ξvars as [varstypes [pf1 pf2]]. - - apply treeM. - apply itree_mapOptionTree in X. - refine (itree_to_tree (itmap _ X)). - intros. - eapply case_helper. - apply X1. - instantiate (1:=varsΣ). - rewrite <- H2. - admit. apply FreshMon. + apply H2. Defined. - Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c. - refine (( - fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j := - match pn in @ClosedND _ _ J return ITree _ judg2exprType J with - | cnd_weak => let case_nil := tt in INone _ _ - | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd') - | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2) - end)); clear closed2expr'; intros; subst. - Defined. + Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j := + match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with + | scnd_weak _ => let case_nil := tt in fun _ => INone _ _ + | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q) + | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q) + end. - Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) - {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> - FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). + Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★) + {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] -> + FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}). intro pf. - set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. + set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd. apply closed2expr in cnd. apply ileaf in cnd. simpl in *. @@ -794,7 +1087,10 @@ Section HaskProofToStrong. auto. refine (return OK _). exists ξ. - apply (ileaf it). + apply ileaf in it. + simpl in it. + apply it. + apply INone. Defined. End HaskProofToStrong.