rewrite app_comm_cons.
reflexivity.
*)
-admit.
+ admit.
Qed.
Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
| 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_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
- end.
-
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
- match elrb with
- | ELR_nil Γ Δ ξ lev => []
- | 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}
reflexivity.
Qed.
-(* IDEA: use multi-conclusion proofs instead *)
+(* TODO: use multi-conclusion proofs instead *)
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v t e ,
|- (mapOptionTree (@snd _ _) tree) @@@ lev ].
intro X; induction X; intros; simpl in *.
apply nd_rule.
- apply REmptyGroup.
+ apply RVoid.
set (ξ v) as q in *.
destruct q.
simpl in *.
apply n.
- eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
Defined.
simpl.
set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
- eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
rewrite ξlemma.
destruct case_ELet; intros; simpl in *.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply nd_prod; [ idtac | apply pf_let].
- clear pf_let.
- eapply nd_comp; [ apply pf_body | idtac ].
- clear pf_body.
+ apply nd_prod.
+ apply pf_let.
+ clear pf_let.
+ eapply nd_comp; [ apply pf_body | idtac ].
+ clear pf_body.
fold (@mapOptionTree VV).
fold (mapOptionTree ξ).
set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.