(*
Definition TInt : HaskType nil ★.
assert (tyConKind' intPrimTyCon = ★).
- admit.
rewrite <- H.
unfold HaskType; intros.
apply TCon.
| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
[Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ]
+| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
| RCase : forall Γ Δ lev tc Σ avars tbranches
(alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
Rule
| RApp _ _ _ _ _ _ _ => "App"
| RLet _ _ _ _ _ _ _ => "Let"
| RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
- | RLetRec _ _ _ _ _ => "LetRec"
+ | RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
| REsc _ _ _ _ _ _ => "Esc"
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_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
intros.
induction l1.
reflexivity.
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).
Qed.
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_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+ /\ mapOptionTree (update_ξ ξ 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_ξ ξ lev
+ (leaves vt2)) _ _; return _).
apply FreshMon.
simpl.
rewrite pf21.
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.
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'.
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_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+ /\ mapOptionTree (update_ξ ξ 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.
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.
apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
Defined.
- Definition letrec_helper Γ Δ l varstypes ξ' :
+ Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
ITree (LeveledHaskType Γ ★)
(fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
(mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
- -> ELetRecBindings Γ Δ ξ' l
- (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) 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.
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.
-
- simpl; apply ELR_branch.
- apply IHvarstypes1.
- simpl in X.
- inversion X; auto.
- apply IHvarstypes2.
- simpl in X.
- inversion X; auto.
-
+ apply ELR_branch.
+ apply IHvarstypes1; inversion X; auto.
+ apply IHvarstypes2; inversion X; auto.
Defined.
- Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
- induction t; auto.
- simpl.
- rewrite IHt; auto.
- Qed.
-
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 &
+ 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))}.
+
intros.
simpl in X.
destruct pcb.
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' ○ ξ) _
+ refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _
>>>= fun ξvars => _). apply FreshMon.
rewrite H.
rewrite <- mapOptionTree_compose.
reflexivity.
- destruct ξvars as [ exprvars [pf1 pf2 ]].
+ destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]].
set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
+
+ assert (distinct (vec2list exprvars')) as pfdistinct'.
+ unfold exprvars'.
+ rewrite vec2list_list2vec.
+ apply pfdistinct.
+
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 map_preserves_length with (f:=
+ (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ)
+ (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ)
+ (@weakL' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev)
+ (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))).
rewrite <- mapleaves.
- rewrite pf2.
+ rewrite pf2.
+ rewrite <- mapleaves'.
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.
+ clear pfdistinct'.
+ rewrite <- H' in exprvars'.
+ clear H'.
+ assert (distinct (vec2list exprvars')) as pfdistinct'.
+ admit.
+
+ set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') 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'.
| 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 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_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *.
refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
apply FreshMon.
simpl.
apply ILeaf.
simpl in *; intros.
destruct vars; try destruct o; inversion H.
- refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
+ refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *.
+ set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
inversion X_.
apply ileaf in X.
apply ileaf in X0.
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_ξ ξ 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).
+ apply (@letrec_helper Γ Δ t varstypes).
+ rewrite <- pf2 in X1.
+ rewrite mapOptionTree_compose.
+ apply X1.
+ apply ileaf in X0.
+ apply X0.
destruct case_RCase.
apply ILeaf; simpl; intros.
apply ileaf in X0.
simpl in X0.
set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
- refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
+ refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev 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.
apply FreshMon.
end)); clear closed2expr'; intros; subst.
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_ξ ξ 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.
+ Defined.
+
Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
{zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
(* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
- { scbwv_sac : @StrongAltCon tc
- ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
- ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
- ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list
- (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes))
+ { scbwv_sac : @StrongAltCon tc
+ ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
+ ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)
+ ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
+ ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
}.
Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
| EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
| ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
| EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
- | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
- | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
+ | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
+ | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
| EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l))
| EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
| ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l,
(weakLT' (tbranches@@l)) } ->
Expr Γ Δ ξ (tbranches @@ l)
- | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
+ | ELetRec : ∀ Γ Δ ξ l τ vars,
+ let ξ' := update_ξ ξ l (leaves vars) in
ELetRecBindings Γ Δ ξ' l vars ->
Expr Γ Δ ξ' (τ@@l) ->
Expr Γ Δ ξ (τ@@l)
(* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *)
with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type :=
| ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l []
- | ELR_leaf : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))]
+ | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
Context {VV:Type}{eqd_vv:EqDecidable VV}.
(* maintenance of Xi *)
- Definition dropVar (lv:list VV)(v:VV) : ??VV :=
- if fold_left
- (fun a b:bool => if a then true else if b then true else false)
- (map (fun lvv => if eqd_dec lvv v then true else false) lv)
- false
- then None
- else Some v.
+ Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
+ match lv with
+ | nil => Some v
+ | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
+ end.
(* later: use mapOptionTreeAndFlatten *)
Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e
+ | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
end.
|}.
Defined.
-Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
+
+Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v e => [ξ v]
+ | ELR_leaf Γ Δ ξ lev v t e => [t]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
end.
-
+(*
Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v e => [v]
+ | ELR_leaf Γ Δ ξ lev v _ _ e => [v]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
end.
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
+Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)]
+ | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
end.
-
+*)
Lemma stripping_nothing_is_inert
{Γ:TypeEnv}
fold stripOutVars.
simpl.
fold (stripOutVars nil).
- rewrite IHtree1.
- rewrite IHtree2.
+ rewrite <- IHtree1 at 2.
+ rewrite <- IHtree2 at 2.
reflexivity.
Qed.
-
+Ltac eqd_dec_refl X :=
+ destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
+ [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
Definition arrangeContext
(Γ:TypeEnv)(Δ:CoercionEnv Γ)
[Γ >> Δ > mapOptionTree ξ ctx |- τ]
[Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
- induction ctx; simpl in *.
+ induction ctx.
- refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
+ refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
(* nonempty leaf *)
destruct case_Some.
unfold stripOutVars in *; simpl.
unfold dropVar.
unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
- destruct (eqd_dec v v'); simpl in *.
+ destruct (eqd_dec v' v); subst.
+
(* where the leaf is v *)
apply inr.
subst.
refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
Defined.
+Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
+ unfold stripOutVars.
+ rewrite <- mapTree_compose.
+ induction t; try destruct a0.
+ simpl.
+ induction x.
+ reflexivity.
+ admit.
+ subst.
+ reflexivity.
+ simpl in *.
+ rewrite <- IHt1.
+ rewrite <- IHt2.
+ reflexivity.
+ Qed.
+
+Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
+ induction x.
+ simpl.
+ admit.
+ rewrite strip_lemma.
+ rewrite IHx.
+ rewrite <- strip_lemma.
+ admit.
+ Qed.
+
+Lemma distinct_app1 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1.
+ admit.
+ Qed.
+
+Lemma distinct_app2 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l2.
+ admit.
+ Qed.
+
+Lemma strip_distinct x y : distinct (app (leaves y) x) -> stripOutVars x y = y.
+ admit.
+ Qed.
+
Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
+ distinct (leaves v) ->
ND (@URule Γ Δ)
[Γ >> Δ>(mapOptionTree ξ ctx) |- z]
[Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
- induction v.
+ induction v; intros.
destruct a.
unfold mapOptionTree in *.
simpl in *.
simpl in IHv2'.
fold (mapOptionTree ξ) in IHv2'.
fold X in IHv2'.
- set (nd_comp (IHv1 _ _) IHv2') as qq.
+ set (nd_comp (IHv1 _ _ (distinct_app1 _ _ _ H)) (IHv2' (distinct_app2 _ _ _ H))) as qq.
eapply nd_comp.
apply qq.
clear qq IHv2' IHv2 IHv1.
-
- assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
- admit.
- rewrite H.
- clear H.
-
- (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
- assert ((stripOutVars (leaves v2) v1) = v1).
- admit.
- rewrite H.
- clear H.
+ rewrite strip_twice_lemma.
+ rewrite (strip_distinct (leaves v2) v1).
apply nd_rule.
apply RCossa.
+ auto.
Defined.
-Definition update_ξ'' {Γ} ξ tree lev :=
-(update_ξ ξ
- (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
- (leaves tree))).
-
-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
- mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
+ mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
= mapOptionTree ξ (stripOutVars (v :: nil) tree).
induction tree; simpl in *; try reflexivity; auto.
- unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
+ unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ lev ((v,t)::nil))) in *.
destruct a; simpl; try reflexivity.
unfold update_ξ.
simpl.
assert (q=eqd_dec v v0).
reflexivity.
destruct q.
+(*
reflexivity.
rewrite <- H.
reflexivity.
rewrite <- IHtree1.
rewrite <- IHtree2.
reflexivity.
+*)
+admit.
+admit.
+admit.
Qed.
-
Lemma updating_stripped_tree_is_inert'
{Γ} lev
(ξ:VV -> LeveledHaskType Γ ★)
tree tree2 :
- mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
+ mapOptionTree (update_ξ ξ lev (leaves tree)) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
= mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
-admit.
- Qed.
-
-Lemma updating_stripped_tree_is_inert''
- {Γ}
- (ξ:VV -> LeveledHaskType Γ ★)
- v tree lev :
- mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
- = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree).
-admit.
+ admit.
Qed.
-(*
-Lemma updating_stripped_tree_is_inert'''
- {Γ}
- (ξ:VV -> LeveledHaskType Γ)
-{T}
- (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
-:
- mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
- = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
-admit.
+Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
+ mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
+ (stripOutVars (vec2list (scbwv_exprvars x)) t)
+ =
+ mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) t).
+ intros.
+ unfold scbwv_ξ.
+ unfold scbwv_varstypes.
+ admit.
Qed.
-*)
(* IDEA: use multi-conclusion proofs instead *)
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
- | lrsp_leaf : forall v e,
- (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
- LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
+ | lrsp_leaf : forall v t e ,
+ (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
+ LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
| lrsp_cons : forall t1 t2 b1 b2,
LetRecSubproofs Γ Δ ξ lev t1 b1 ->
LetRecSubproofs Γ Δ ξ lev t2 b2 ->
LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
-Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
- eLetRecTypes branches =
- mapOptionTree (update_ξ'' ξ tree lev)
- (mapOptionTree (@fst _ _) tree).
- intros.
- induction branches.
- reflexivity.
- simpl.
- unfold update_ξ.
- unfold mapOptionTree; simpl.
-admit.
-admit.
- Qed.
-Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
-mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-=
-(*
-((mapOptionTreeAndFlatten
-(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
- (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
-*)
-((mapOptionTreeAndFlatten pcb_freevars
- (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
-admit.
-Qed.
-Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
- admit.
- Qed.
-Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
-admit.
-Qed.
-
-Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
- : LetRecSubproofs Γ Δ ξ lev tree branches ->
- ND Rule []
- [ Γ > Δ >
- mapOptionTree ξ (eLetRecContext branches)
- |-
- eLetRecTypes branches
- ].
- intro X.
- induction X; intros; simpl in *.
+Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
+ LetRecSubproofs Γ Δ ξ lev tree branches ->
+ ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
+ |- eLetRecTypes branches @@@ lev ].
+ intro X; induction X; intros; simpl in *.
apply nd_rule.
apply REmptyGroup.
set (ξ v) as q in *.
destruct q.
simpl in *.
- assert (h0=lev).
- admit.
- rewrite H.
apply n.
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
Defined.
-
-Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
- mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
-admit.
- Qed.
-
-
-
Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
forall branches body,
- ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
- LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
+ ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
+ LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
(* NOTE: how we interpret stuff here affects the order-of-side-effects *)
- simpl.
intro branches.
intro body.
intro pf.
intro lrsp.
- set ((update_ξ ξ
- (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
- (leaves tree)))) as ξ' in *.
+ set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
set (mapOptionTree (@fst _ _) tree) as pctx.
set (mapOptionTree ξ' pctx) as passback.
- set (fun a b => @RLetRec Γ Δ a b passback) as z.
+ set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
clear z.
unfold ξ' in *.
set (@updating_stripped_tree_is_inert') as zz.
- unfold update_ξ'' in *.
rewrite zz in q'.
clear zz.
clear ξ'.
- simpl in q'.
-
+ Opaque stripOutVars.
+ simpl.
+ rewrite <- mapOptionTree_compose in q'.
+ cut ((mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree) = (mapOptionTree (@snd _ _) tree @@@ lev)).
+ intro H'.
+ rewrite <- H'.
eapply nd_comp; [ idtac | apply q' ].
+ clear H'.
clear q'.
- unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
-
simpl.
set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
-
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
- rewrite cheat1 in q.
- set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
- unfold update_ξ'' in *.
- rewrite <- zz in q.
+ cut ((eLetRecTypes branches @@@ lev) = mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree).
+ intro H''.
+ rewrite <- H''.
apply q.
+ admit.
+ admit.
+ admit.
Defined.
+Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)),
+ distinct (map (@fst _ _) varstypes) ->
+ map (update_ξ ξ lev varstypes) (map (@fst _ _) varstypes) =
+ map (fun t => t@@ lev) (map (@snd _ _) varstypes).
+ intros.
+ induction varstypes.
+ reflexivity.
+ destruct a.
+ inversion H.
+ subst.
+ admit.
+ Qed.
-Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
- mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
- (stripOutVars (vec2list (scbwv_exprvars x)) t)
- =
- mapOptionTree (weakLT' ○ ξ)
- (stripOutVars (vec2list (scbwv_exprvars x)) t).
+Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
admit.
Qed.
+Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
+ admit.
+ Defined.
-Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
-(x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
-(e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
- (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) ,
-mapOptionTree (weakLT' ○ ξ)
- (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
-unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
-=
-mapOptionTree (weakLT' ○ ξ)
- (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
- mapOptionTree
- (update_ξ (weakLT' ○ ξ)
- (vec2list
- (vec_map
- (fun
- x0 : VV *
- HaskType
- (app (vec2list (sac_ekinds x)) Γ)
- ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩)
- (vec_zip (scbwv_exprvars x)
- (sac_types x Γ atypes)))))
- (unleaves (vec2list (scbwv_exprvars x)))
-.
-admit.
-Qed.
+Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2.
+ admit.
+ Defined.
+Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
+ forall scb:StrongCaseBranchWithVVs _ _ tc atypes,
+ forall l ξ, vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb) =
+ vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes).
+ intros.
+ unfold scbwv_ξ.
+ unfold scbwv_varstypes.
+ set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
+ (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) as q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite fst_zip in q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite snd_zip in q.
+ rewrite vec2list_map_list2vec in q.
+ apply vec2list_injective.
+ apply q.
+ apply scbwv_exprvars_distinct.
+ Qed.
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
+ mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
+ = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
+ intros.
+ simpl.
+ Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
+ hack.
+ induction alts'.
+ simpl.
+ destruct a.
+ unfold mkProofCaseBranch.
+ simpl.
+ reflexivity.
+ reflexivity.
+ simpl.
+ rewrite IHalts'1.
+ rewrite IHalts'2.
+ reflexivity.
+ rewrite H.
+ reflexivity.
+ Qed.
Definition expr2proof :
| ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
(fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
| ELetRec Γ Δ ξ lev t tree branches ebody =>
- let ξ' := update_ξ'' ξ tree lev in
+ let ξ' := update_ξ ξ lev (leaves tree) in
let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
-((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
+ ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
(branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
: LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
| ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
- | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
+ | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
end
) _ _ _ _ tree branches)
(weakLT' (tbranches@@l)) })
: ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
- | T_Leaf None => let case_nil := tt in _
- | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
+ | T_Leaf None => let case_nil := tt in _
| T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
+ | T_Leaf (Some x) =>
+ match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with
+ existT scbx ex =>
+ (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
+ end
end) alts')
in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
end
-); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+ ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
destruct case_EGlobal.
apply nd_rule.
destruct case_ELam; intros.
unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
- set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
+ set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
apply UND_to_ND in pfx.
unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
unfold ξ' in pfx.
- fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
+ fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx.
rewrite updating_stripped_tree_is_inert in pfx.
unfold update_ξ in pfx.
destruct (eqd_dec v v).
clear pf_body.
fold (@mapOptionTree VV).
fold (mapOptionTree ξ).
- set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
+ set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
unfold ξ' in n.
apply e'.
destruct case_leaf.
- unfold pcb_judg.
+ clear o x alts alts' e.
+ eapply nd_comp; [ apply e' | idtac ].
+ clear e'.
+ set (existT
+ (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes =>
+ Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))) scbx ex) as stuff.
+ set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
+ simpl in n.
+ apply n.
+ clear n.
+
+ rewrite mapleaves'.
simpl.
- repeat rewrite <- mapOptionTree_compose in *.
- set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
- (unleaves (vec2list (scbwv_exprvars (projT1 x))))
- (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
- _ _
- ))) as q.
- rewrite cheat4 in q.
- rewrite cheat3.
- unfold weakCK'' in q.
- simpl in q.
- rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q.
- Ltac cheater Q :=
- match goal with
- [ Q:?Y |- ?Z ] =>
- assert (Y=Z) end.
- cheater q.
- admit.
- rewrite <- H.
- clear H.
- apply q.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- updating_stripped_tree_is_inert''' with (l:=l).
+ replace (vec2list (scbwv_exprvars scbx)) with (leaves (unleaves (vec2list (scbwv_exprvars scbx)))).
+ rewrite <- mapleaves'.
+ rewrite vec2list_map_list2vec.
+ unfold sac_Γ.
+ rewrite <- (scbwv_coherent scbx l ξ).
+ rewrite <- vec2list_map_list2vec.
+ rewrite mapleaves'.
+ apply arrangeContextAndWeaken''.
+ rewrite leaves_unleaves.
+ apply (scbwv_exprvars_distinct scbx).
+ apply leaves_unleaves.
destruct case_nil.
apply nd_id0.
apply b2'.
destruct case_ECase.
- rewrite cheat2.
+ rewrite case_lemma.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
rewrite <- mapOptionTree_compose.
apply dcsp.
apply e'.
- destruct case_ELetRec; simpl in *; intros.
- set (@letRecSubproofsToND') as q.
- simpl in q.
- apply q.
- clear q.
+ destruct case_ELetRec; intros.
+ unfold ξ'0 in *.
+ clear ξ'0.
+ unfold ξ'1 in *.
+ clear ξ'1.
+ apply letRecSubproofsToND'.
apply e'.
apply subproofs.
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
- | ELR_leaf _ _ ξ' cv v e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite
+ | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
Fixpoint update_ξ
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
- (vt:list (VV * LeveledHaskType Γ ★))
+ (lev:HaskLevel Γ)
+ (vt:list (VV * HaskType Γ ★))
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
- | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
end.
+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+ not (In v (map (@fst _ _) varstypes)) ->
+ (update_ξ ξ lev varstypes) v = ξ v.
+ intros.
+ induction varstypes.
+ reflexivity.
+ simpl.
+ destruct a.
+ destruct (eqd_dec v0 v).
+ subst.
+ simpl in H.
+ assert False.
+ apply H.
+ auto.
+ inversion H0.
+ apply IHvarstypes.
+ unfold not; intros.
+ apply H.
+ simpl.
+ auto.
+ Defined.
(***************************************************************************************************)
| WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr ebody >>= fun tbody =>
weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
- let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
+ let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
let ig' := update_ig ig ((ev:CoreVar)::nil) in
weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
| WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil))
+ weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
(update_ig ig ((v:CoreVar)::nil)) τ lev ebody
>>= fun ebody' =>
OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
(ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
| WELetRec rb e =>
- let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in
+ let ξ' := update_ξ ξ lev _ in
let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
let binds :=
(fix binds (t:Tree ??(WeakExprVar * WeakExpr))
mkStrongAltConPlusJunk' tc ac >>= fun sac =>
list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
>>= fun exprvars' =>
- let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
+ (let case_pf := tt in _) >>= fun pf =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
(sacpj_ψ sac _ _ avars' ψ)
(scbwv_ξ scb ξ lev)
weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
- end)).
+ end)); try clear binds.
destruct case_some.
apply (addErrorMessage "case_some").
destruct e''; try apply (Error error_message).
apply OK.
apply ELR_leaf.
+ unfold ξ'.
+ simpl.
+ induction (leaves (varsTypes rb φ)).
+ simpl; auto.
+ destruct (ξ c).
+ simpl.
apply e1.
+ destruct case_pf.
+ set (distinct_decidable (vec2list exprvars')) as dec.
+ destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
+ apply OK; auto.
+
destruct case_case.
exists scb.
apply ebranch'.
projects / coq-hetmet.git / commitdiff