diff options
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 75 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 6 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.mli | 3 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 24 | ||||
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 16 | ||||
| -rw-r--r-- | contrib/rtauto/Bintree.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 202 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 240 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 85 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 299 |
10 files changed, 522 insertions, 434 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 2dbf1d107..119b155d0 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -322,7 +322,7 @@ let h_reduce_with_zeta = let rewrite_until_var arg_num eq_ids : tactic = let test_var g = let _,args = destApp (pf_concl g) in - isVar args.(arg_num) + not (isConstruct args.(arg_num)) in let rec do_rewrite eq_ids g = if test_var g @@ -532,9 +532,9 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = match kind_of_term new_term_value_eq with | App(f,[| _;_;args2 |]) -> args2 | _ -> -(* observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ *) -(* pr_lconstr_env (pf_env g') new_term_value_eq *) -(* ); *) + observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ + pr_lconstr_env (pf_env g') new_term_value_eq + ); anomaly "cannot compute new term value" in let fun_body = @@ -622,9 +622,9 @@ let build_proof let term_eq = make_refl_eq type_of_term t in - tclTHENSEQ + tclTHENSEQ [ - h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps); + h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; pattern_option [[-1],t] None; h_simplest_case t; @@ -744,7 +744,7 @@ let build_proof ] g | Rel _ -> anomaly "Free var in goal conclusion !" and build_proof do_finalize dyn_infos g = -(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) +(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> @@ -813,8 +813,9 @@ type static_fix_info = nb_realargs : int } -let prove_rec_hyp fix_info = - { proving_tac = + + +let prove_rec_hyp_for_struct fix_info = (fun eq_hyps -> tclTHEN (rewrite_until_var (fix_info.idx - 1) eq_hyps) (fun g -> @@ -824,6 +825,9 @@ let prove_rec_hyp fix_info = in refine rec_hyp_proof g )) + +let prove_rec_hyp fix_info = + { proving_tac = prove_rec_hyp_for_struct fix_info ; is_valid = fun _ -> true } @@ -831,7 +835,26 @@ let prove_rec_hyp fix_info = exception Not_Rec - +let generalize_non_dep hyp g = + let hyps = [hyp] in + let env = Global.env () in + let hyp_typ = pf_type_of g (mkVar hyp) in + let to_revert,_ = + Environ. fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> + if List.mem hyp hyps + or List.exists (occur_var_in_decl env hyp) keep + or occur_var env hyp hyp_typ + or Termops.is_section_variable hyp (* should be dangerous *) + then (clear,decl::keep) + else (hyp::clear,keep)) + ~init:([],[]) (pf_env g) + in + observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); + tclTHEN + (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert))) + (observe_tac "thin" (thin to_revert)) + g + let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic = fun goal -> (* observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ *) @@ -974,7 +997,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : try if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; let nparams = List.length !params in - let args_as_constr = List.map mkVar args in + let args_as_constr = List.map mkVar args in let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in let other_args_as_constr = List.map mkVar other_args in let rec_num,new_body = @@ -982,7 +1005,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : let f = fnames.(idx') in let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" in - let name_of_f = Name ( id_of_label (con_label f)) in + let name_of_f = Name (id_of_label (con_label f)) in let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in let idx'' = list_index name_of_f (Array.to_list na) - 1 in let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in @@ -1002,11 +1025,11 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : (* observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); *) let do_prove branches applied_body = build_proof - interactive_proof - (Array.to_list fnames) - (Idmap.map prove_rec_hyp ptes_to_fixes) - branches - applied_body + interactive_proof + (Array.to_list fnames) + (Idmap.map prove_rec_hyp ptes_to_fixes) + branches + applied_body in let replace_and_prove = tclTHENS @@ -1025,11 +1048,18 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : info = applied_body_with_real_args; eq_hyps = []; } ]; - let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in - let id_as_induction_constr = Tacexpr.ElimOnConstr id in + let id = + try + List.nth (List.rev args_as_constr) (rec_num) + with _ -> anomaly ("Cannot find recursive argument of function ! ") + in (tclTHENSEQ - [new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) - intros_reflexivity + [ + keep (!params@(List.map destVar args_as_constr)); + observe_tac "generalizing" (generalize_non_dep (destVar id)); + observe_tac "new_destruct" + (h_case (id,Rawterm.NoBindings)); + observe_tac "intros_reflexivity" intros_reflexivity ]) ] in @@ -1077,7 +1107,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : let fix_info = Idmap.find (destVar pte) !pte_to_fix in fix_info.nb_realargs with Not_found -> (* Not a recursive function *) - nb_prod (pf_concl g) + nb_lam (Util.out_some !fbody_with_params) +(* nb_prod (pf_concl g) *) in observe_tac "" (tclTHEN (tclDO nb_real_args (observe_tac "intro" intro)) diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 072c3d518..fc5200202 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -439,6 +439,8 @@ let get_funs_constant mp dp = with Not_Rec -> () in l_const + +exception No_graph_found let make_scheme fas = let env = Global.env () @@ -451,8 +453,10 @@ let make_scheme fas = let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in let first_fun_kn = - (* Fixme: take into accour funs_mp and funs_dp *) + try + (* Fixme: take into account funs_mp and funs_dp *) fst (destInd (id_to_constr first_fun_rel_id)) + with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map fst this_block_funs_indexes in diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli index 929c3db51..8b4faaf44 100644 --- a/contrib/funind/functional_principles_types.mli +++ b/contrib/funind/functional_principles_types.mli @@ -24,5 +24,8 @@ val generate_functional_principle : val compute_new_princ_type_from_rel : constr array -> sorts array -> types -> types + +exception No_graph_found + val make_scheme : (identifier*identifier*Rawterm.rawsort) list -> unit val make_case_scheme : (identifier*identifier*Rawterm.rawsort) -> unit diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 2bad9bb50..bd48266a4 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -82,8 +82,13 @@ let choose_dest_or_ind scheme_info = TACTIC EXTEND newfunind - ["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] -> + ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> [ + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in let f,args = decompose_app c in fun g -> let princ = @@ -192,15 +197,26 @@ VERNAC ARGUMENT EXTEND fun_scheme_args END VERNAC COMMAND EXTEND NewFunctionalScheme - ["New" "Functional" "Scheme" fun_scheme_args(fas) ] -> + ["Functional" "Scheme" fun_scheme_args(fas) ] -> [ - Functional_principles_types.make_scheme fas + try + Functional_principles_types.make_scheme fas + with Functional_principles_types.No_graph_found -> + match fas with + | (_,fun_name,_)::_ -> + begin + make_graph fun_name; + try Functional_principles_types.make_scheme fas + with Functional_principles_types.No_graph_found -> + Util.error ("Cannot generate induction principle(s)") + end + | _ -> assert false (* we can only have non empty list *) ] END VERNAC COMMAND EXTEND NewFunctionalCase - ["New" "Functional" "Case" fun_scheme_arg(fas) ] -> + ["Functional" "Case" fun_scheme_arg(fas) ] -> [ Functional_principles_types.make_case_scheme fas ] diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index a12f1f01f..2c7e4d33c 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -772,11 +772,6 @@ let invfun_verif c l dorew gl = else error "wrong number of arguments for the function" -TACTIC EXTEND functional_induction - [ "functional" "induction" constr(c) ne_constr_list(l) ] - -> [ invfun_verif c l true ] -END - (* Construction of the functional scheme. *) @@ -847,15 +842,20 @@ let declareFunScheme f fname mutflist = +TACTIC EXTEND functional_induction + [ "old" "functional" "induction" constr(c) ne_constr_list(l) ] + -> [ invfun_verif c l true ] +END + VERNAC COMMAND EXTEND FunctionalScheme - [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" + [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident(c) "with" ne_ident_list(l) ] -> [ declareFunScheme c na l ] -| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] +| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] -> [ declareFunScheme c na [] ] END - + diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v index ee66f02a9..8827da100 100644 --- a/contrib/rtauto/Bintree.v +++ b/contrib/rtauto/Bintree.v @@ -18,7 +18,7 @@ Open Scope positive_scope. Ltac clean := try (simpl; congruence). Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. -Functional Scheme Pcompare_ind := Induction for Pcompare. +Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop. Lemma Prect : forall P : positive -> Type, P 1 -> @@ -31,13 +31,13 @@ Qed. Lemma Gt_Eq_Gt : forall p q cmp, (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt. -apply (Pcompare_ind (fun p q cmp => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt)); +apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt)); simpl;auto;congruence. Qed. Lemma Gt_Lt_Gt : forall p q cmp, (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt. -apply (Pcompare_ind (fun p q cmp => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt)); +apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt)); simpl;auto;congruence. Qed. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 17be9405c..af5cee4fa 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -469,7 +469,7 @@ Ltac omega_bal := match goal with (** * Insertion *) -Fixpoint add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with +Function add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with | Leaf => Node (Leaf _) x e (Leaf _) 1 | Node l y e' r h => match X.compare x y with @@ -482,17 +482,17 @@ Fixpoint add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s wi Lemma add_avl_1 : forall elt (m:t elt) x e, avl m -> avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1. Proof. - intros elt m x e; functional induction add elt x e m; intros; inv avl; simpl in *. + intros elt m x e; functional induction (add x e m); intros; inv avl; simpl in *. intuition; try constructor; simpl; auto; try omega_max. (* LT *) - destruct H; auto. + destruct IHt; auto. split. apply bal_avl; auto; omega_max. omega_bal. (* EQ *) intuition; omega_max. (* GT *) - destruct H; auto. + destruct IHt; auto. split. apply bal_avl; auto; omega_max. omega_bal. @@ -507,12 +507,12 @@ Hint Resolve add_avl. Lemma add_in : forall elt (m:t elt) x y e, avl m -> (In y (add x e m) <-> X.eq y x \/ In y m). Proof. - intros elt m x y e; functional induction add elt x e m; auto; intros. + intros elt m x y e; functional induction (add x e m); auto; intros. intuition_in. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (H H1); intuition_in. + rewrite (IHt H2); intuition_in. (* EQ *) inv avl. firstorder_in. @@ -520,30 +520,30 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (H H2); intuition_in. + rewrite (IHt H3); intuition_in. Qed. Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m). Proof. - intros elt m x e; functional induction add elt x e m; + intros elt m x e; functional induction (add x e m); intros; inv bst; inv avl; auto; apply bal_bst; auto. (* lt_tree -> lt_tree (add ...) *) - red; red in H4. + red; red in H5. intros. - rewrite (add_in x y0 e H0) in H1. + rewrite (add_in x y0 e H1) in H2. intuition. eauto. (* gt_tree -> gt_tree (add ...) *) - red; red in H4. + red; red in H5. intros. - rewrite (add_in x y0 e H6) in H1. + rewrite (add_in x y0 e H7) in H2. intuition. apply lt_eq with x; auto. Qed. Lemma add_1 : forall elt (m:t elt) x y e, avl m -> X.eq x y -> MapsTo y e (add x e m). Proof. - intros elt m x y e; functional induction add elt x e m; + intros elt m x y e; functional induction (add x e m); intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; eauto. Qed. @@ -574,25 +574,26 @@ Qed. for [t=Leaf], we pre-unpack [t] (and forget about [h]). *) -Fixpoint remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := +Function remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := match l with | Leaf => (r,(x,e)) - | Node ll lx le lr lh => let (l',m) := remove_min ll lx le lr in (bal l' x e r, m) + | Node ll lx le lr lh => let (l',m) := (remove_min ll lx le lr : t elt*(key*elt)) in (bal l' x e r, m) end. Lemma remove_min_avl_1 : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> avl (fst (remove_min l x e r)) /\ 0 <= height (Node l x e r h) - height (fst (remove_min l x e r)) <= 1. Proof. - intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv avl; simpl in *; split; auto. avl_nns; omega_max. (* l = Node *) - inversion_clear H0. - destruct (H lh); auto. + inversion_clear H1. + destruct (IHp lh); auto. split; simpl in *. - apply bal_avl; auto; omega_max. - omega_bal. + rewrite_all H0. simpl in *. + apply bal_avl; subst;auto; omega_max. + rewrite_all H0;simpl in *;omega_bal. Qed. Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> @@ -605,16 +606,17 @@ Lemma remove_min_in : forall elt (l:t elt) x e r h y, avl (Node l x e r h) -> (In y (Node l x e r h) <-> X.eq y (fst (snd (remove_min l x e r))) \/ In y (fst (remove_min l x e r))). Proof. - intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. intuition_in. (* l = Node *) - inversion_clear H0. - generalize (remove_min_avl H1). - rewrite H_eq_0; simpl; intros. + inversion_clear H1. + generalize (remove_min_avl H2). + + rewrite_all H0; simpl; intros. rewrite bal_in; auto. - generalize (H lh y H1). + generalize (IHp lh y H2). intuition. - inversion_clear H8; intuition. + inversion_clear H9; intuition. Qed. Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> @@ -622,49 +624,50 @@ Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h ((X.eq y (fst (snd (remove_min l x e r))) /\ e' = (snd (snd (remove_min l x e r)))) \/ MapsTo y e' (fst (remove_min l x e r)))). Proof. - intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. intuition_in; subst; auto. (* l = Node *) - inversion_clear H0. - generalize (remove_min_avl H1). - rewrite H_eq_0; simpl; intros. + inversion_clear H1. + generalize (remove_min_avl H2). + rewrite_all H0; simpl; intros. rewrite bal_mapsto; auto; unfold create. - destruct (H lh y e'). + simpl in *;destruct (IHp lh y e'). auto. intuition. - inversion_clear H3; intuition. - inversion_clear H10; intuition. + inversion_clear H4; intuition. + inversion_clear H11; intuition. Qed. Lemma remove_min_bst : forall elt (l:t elt) x e r h, bst (Node l x e r h) -> avl (Node l x e r h) -> bst (fst (remove_min l x e r)). Proof. - intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H0; inversion_clear H1. + inversion_clear H1; inversion_clear H2. apply bal_bst; auto. - firstorder. + rewrite_all H0;simpl in *;firstorder. intro; intros. - generalize (remove_min_in y H0). - rewrite H_eq_0; simpl. + generalize (remove_min_in y H1). + rewrite_all H0; simpl in *. destruct 1. - apply H4; intuition. + apply H5; intuition. Qed. Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, bst (Node l x e r h) -> avl (Node l x e r h) -> gt_tree (fst (snd (remove_min l x e r))) (fst (remove_min l x e r)). Proof. - intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H0; inversion_clear H1. + inversion_clear H1; inversion_clear H2. intro; intro. - generalize (H lh H2 H0); clear H8 H7 H. - generalize (remove_min_avl H0). - generalize (remove_min_in (fst m) H0). - rewrite H_eq_0; simpl; intros. - rewrite (bal_in x e y H7 H6) in H1. - destruct H. + rewrite_all H0;simpl in *. + generalize (IHp lh H3 H1); clear H9 H8 IHp. + generalize (remove_min_avl H1). + generalize (remove_min_in (fst m) H1). + rewrite H0; simpl; intros. + rewrite (bal_in x e y H9 H7) in H2. + destruct H8. firstorder. apply lt_eq with x; auto. apply X.lt_trans with x; auto. @@ -677,13 +680,13 @@ Qed. [|height t1 - height t2| <= 2]. *) -Definition merge elt (s1 s2 : t elt) := match s1,s2 with +Function merge (elt:Set) (s1 s2 : t elt) : tree elt := match s1,s2 with | Leaf, _ => s2 | _, Leaf => s1 | _, Node l2 x2 e2 r2 h2 => - let (s2',m) := remove_min l2 x2 e2 r2 in - let (x,e) := m in - bal s1 x e s2' + match remove_min l2 x2 e2 r2 with + (s2',(x,e)) => bal s1 x e s2' + end end. Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> @@ -691,12 +694,13 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> avl (merge s1 s2) /\ 0<= height (merge s1 s2) - max (height s1) (height s2) <=1. Proof. - intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros;subst. split; auto; avl_nns; omega_max. + destruct _x;try contradiction;clear H1. split; auto; avl_nns; simpl in *; omega_max. - generalize (remove_min_avl_1 H0). - rewrite H_eq_1; simpl; destruct 1. - rewrite H_eq_2; simpl. + destruct _x;try contradiction;clear H1. + generalize (remove_min_avl_1 H4). +rewrite H2; simpl;destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -712,49 +716,53 @@ Qed. Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (In y (merge s1 s2) <-> In y s1 \/ In y s2). Proof. - intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + intros elt s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros. intuition_in. intuition_in. - rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto]. + destruct _x;try contradiction;clear H1. +(* rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *) + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. rewrite bal_in; auto. - generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_in y0 H2); rewrite H_eq_1; simpl; intro. - rewrite H3; intuition. + generalize (remove_min_avl H4); rewrite H2; simpl; auto. + generalize (remove_min_in y H4); rewrite H2; simpl; intro. + rewrite H1; intuition. Qed. Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2). Proof. - intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + intros elt s1 s2; functional induction (@merge elt s1 s2); subst; simpl in *; intros. intuition_in. intuition_in. - rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto]. + destruct _x;try contradiction;clear H1. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. rewrite bal_mapsto; auto; unfold create. - generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_mapsto y0 e0 H2); rewrite H_eq_1; simpl; intro. - rewrite H3; intuition (try subst; auto). - inversion_clear H3; intuition. + generalize (remove_min_avl H4); rewrite H2; simpl; auto. + generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro. + rewrite H1; intuition (try subst; auto). + inversion_clear H1; intuition. Qed. Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> bst (merge s1 s2). Proof. - intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros; auto. - rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. + intros elt s1 s2; functional induction (@merge elt s1 s2); subst;simpl in *; intros; auto. + apply bal_bst; auto. - generalize (remove_min_bst H1); rewrite H_eq_1; simpl in *; auto. + destruct _x;try contradiction. + generalize (remove_min_bst H3); rewrite H2; simpl in *; auto. + destruct _x;try contradiction. intro; intro. - apply H3; auto. - generalize (remove_min_in x H2); rewrite H_eq_1; simpl; intuition. - generalize (remove_min_gt_tree H1); rewrite H_eq_1; simpl; auto. + apply H5; auto. + generalize (remove_min_in x H4); rewrite H2; simpl; intuition. + destruct _x;try contradiction. + generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto. Qed. (** * Deletion *) -Fixpoint remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with +Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with | Leaf => Leaf _ | Node l y e r h => match X.compare x y with @@ -767,22 +775,22 @@ Fixpoint remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. Proof. - intros elt s x; functional induction remove elt x s; simpl; intros. + intros elt s x; functional induction (@remove elt x s); subst;simpl; intros. split; auto; omega_max. (* LT *) inv avl. - destruct (H H1). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) inv avl. - generalize (merge_avl_1 H0 H1 H2). + generalize (merge_avl_1 H1 H2 H3). intuition omega_max. (* GT *) inv avl. - destruct (H H2). + destruct (IHt H2). split. apply bal_avl; auto. omega_max. @@ -798,32 +806,32 @@ Hint Resolve remove_avl. Lemma remove_in : forall elt (s:t elt) x y, bst s -> avl s -> (In y (remove x s) <-> ~ X.eq y x /\ In y s). Proof. - intros elt s x; functional induction remove elt x s; simpl; intros. + intros elt s x; functional induction (@remove elt x s); simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite bal_in; auto. - generalize (H y0 H1); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H2); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H9; eauto. + elim H10; eauto. (* GT *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite bal_in; auto. - generalize (H y0 H6); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H7); intuition; [ order | order | intuition_in ]. Qed. Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s). Proof. - intros elt s x; functional induction remove elt x s; simpl; intros. + intros elt s x; functional induction (@remove elt x s); subst;simpl; intros. auto. (* LT *) inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H1) in H0; auto. - destruct H0; eauto. + rewrite (remove_in x y0 H1) in H; auto. + destruct H; eauto. (* EQ *) inv avl; inv bst. apply merge_bst; eauto. @@ -831,8 +839,8 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H6) in H0; auto. - destruct H0; eauto. + rewrite (remove_in x y0 H6) in H; auto. + destruct H; eauto. Qed. Lemma remove_1 : forall elt (m:t elt) x y, bst m -> avl m -> X.eq x y -> ~ In y (remove x m). @@ -911,7 +919,7 @@ Qed. (** The [mem] function is deciding appartness. It exploits the [bst] property to achieve logarithmic complexity. *) -Fixpoint mem (x:key)(m:t elt) { struct m } : bool := +Function mem (x:key)(m:t elt) { struct m } : bool := match m with | Leaf => false | Node l y e r _ => match X.compare x y with @@ -925,7 +933,7 @@ Implicit Arguments mem. Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. Proof. intros s x. - functional induction mem x s; inversion_clear 1; auto. + functional induction (mem x s); inversion_clear 1; auto. intuition_in. intuition_in; firstorder; absurd (X.lt x y); eauto. intuition_in; firstorder; absurd (X.lt y x); eauto. @@ -934,10 +942,10 @@ Qed. Lemma mem_2 : forall s x, mem x s = true -> In x s. Proof. intros s x. - functional induction mem x s; firstorder; intros; try discriminate. + functional induction (mem x s); firstorder; intros; try discriminate. Qed. -Fixpoint find (x:key)(m:t elt) { struct m } : option elt := +Function find (x:key)(m:t elt) { struct m } : option elt := match m with | Leaf => None | Node l y e r _ => match X.compare x y with @@ -950,7 +958,7 @@ Fixpoint find (x:key)(m:t elt) { struct m } : option elt := Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. Proof. intros m x e. - functional induction find x m; inversion_clear 1; auto. + functional induction (find x m); inversion_clear 1; auto. intuition_in. intuition_in; firstorder; absurd (X.lt x y); eauto. intuition_in; auto. @@ -962,7 +970,7 @@ Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. - functional induction find x m; firstorder; intros; try discriminate. + functional induction (find x m); subst;firstorder; intros; try discriminate. inversion H; subst; auto. Qed. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 4b2761f10..128ed45d2 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -96,7 +96,7 @@ Qed. (** * [mem] *) -Fixpoint mem (k : key) (s : t elt) {struct s} : bool := +Function mem (k : key) (s : t elt) {struct s} : bool := match s with | nil => false | (k',_) :: l => @@ -110,33 +110,33 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool := Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true. Proof. intros m Hm x; generalize Hm; clear Hm. - functional induction mem x m;intros sorted belong1;trivial. + functional induction (mem x m);intros sorted belong1;trivial. - inversion belong1. inversion H. + inversion belong1. inversion H0. - absurd (In k ((k', e) :: l));try assumption. - apply Sort_Inf_NotIn with e;auto. + absurd (In x ((k', _x) :: l));try assumption. + apply Sort_Inf_NotIn with _x;auto. - apply H. + apply IHb. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. - absurd (X.eq k k');auto. + absurd (X.eq x k');auto. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. - functional induction mem x m; intros sorted hyp;try ((inversion hyp);fail). - exists e; auto. - induction H; auto. - exists x; auto. + functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). + exists _x; auto. + induction IHb; auto. + exists x0; auto. inversion_clear sorted; auto. Qed. (** * [find] *) -Fixpoint find (k:key) (s: t elt) {struct s} : option elt := +Function find (k:key) (s: t elt) {struct s} : option elt := match s with | nil => None | (k',x)::s' => @@ -150,31 +150,31 @@ Fixpoint find (k:key) (s: t elt) {struct s} : option elt := Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold PX.MapsTo. - functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto. + functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. Proof. intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction find x m;simpl; subst; try clear H_eq_1. + functional induction (find x m);simpl; subst; try clear H_eq_1. inversion 2. inversion_clear 2. - compute in H0; destruct H0; order. - generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. + clear H0;compute in H1; destruct H1;order. + clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order. - inversion_clear 2. + clear H0;inversion_clear 2. compute in H0; destruct H0; intuition congruence. generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. - do 2 inversion_clear 1; auto. - compute in H3; destruct H3; order. + clear H0; do 2 inversion_clear 1; auto. + compute in H2; destruct H2; order. Qed. (** * [add] *) -Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt := +Function add (k : key) (x : elt) (s : t elt) {struct s} : t elt := match s with | nil => (k,x) :: nil | (k',y) :: l => @@ -189,7 +189,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y. unfold PX.MapsTo. - functional induction add x e m;simpl;auto. + functional induction (add x e m);simpl;auto. Qed. Lemma add_2 : forall m x y e e', @@ -197,25 +197,29 @@ Lemma add_2 : forall m x y e e', Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. - functional induction add x e' m;simpl;auto; clear H_eq_1. - intros y' e' eqky'; inversion_clear 1; destruct H0; simpl in *. + functional induction (add x e' m) ;simpl;auto; clear H0. + subst;auto. + + intros y' e'' eqky'; inversion_clear 1; destruct H1; simpl in *. order. auto. auto. - intros y' e' eqky'; inversion_clear 1; intuition. + intros y' e'' eqky'; inversion_clear 1; intuition. Qed. + Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. - functional induction add x e' m;simpl; intros. - apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H0); compute; auto. - constructor 2; apply (In_inv_3 H0); compute; auto. - inversion_clear H1; auto. + functional induction (add x e' m);simpl; intros. + apply (In_inv_3 H1); compute; auto. + subst s;apply (In_inv_3 H2); compute; auto. + constructor 2; apply (In_inv_3 H2); compute; auto. + inversion_clear H2; auto. Qed. + Lemma add_Inf : forall (m:t elt)(x x':key)(e e':elt), Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m). Proof. @@ -242,7 +246,7 @@ Qed. (** * [remove] *) -Fixpoint remove (k : key) (s : t elt) {struct s} : t elt := +Function remove (k : key) (s : t elt) {struct s} : t elt := match s with | nil => nil | (k',x) :: l => @@ -256,30 +260,36 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt := Lemma remove_1 : forall m (Hm:Sort m) x y, X.eq x y -> ~ In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - functional induction remove x m;simpl;intros;subst;try clear H_eq_1. + functional induction (remove x m);simpl;intros;subst. red; inversion 1; inversion H1. - apply Sort_Inf_NotIn with x; auto. - constructor; compute; order. + apply Sort_Inf_NotIn with x0; auto. + clear H0;constructor; compute; order. - inversion_clear Hm. - apply Sort_Inf_NotIn with x; auto. - apply Inf_eq with (k',x);auto; compute; apply X.eq_trans with k; auto. + clear H0;inversion_clear Hm. + apply Sort_Inf_NotIn with x0; auto. + apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. - inversion_clear Hm. - assert (notin:~ In y (remove k l)) by auto. - intros (x0,abs). + clear H0;inversion_clear Hm. + assert (notin:~ In y (remove x l)) by auto. + intros (x1,abs). inversion_clear abs. - compute in H3; destruct H3; order. - apply notin; exists x0; auto. + compute in H2; destruct H2; order. + apply notin; exists x1; auto. Qed. + Lemma remove_2 : forall m (Hm:Sort m) x y e, ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction remove x m;auto; try clear H_eq_1. + functional induction (remove x m);subst;auto; + match goal with + | [H: X.compare _ _ = _ |- _ ] => clear H + | _ => idtac + end. + inversion_clear 3; auto. compute in H1; destruct H1; order. @@ -290,7 +300,7 @@ Lemma remove_3 : forall m (Hm:Sort m) x y e, MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction remove x m;auto. + functional induction (remove x m);subst;auto. inversion_clear 1; inversion_clear 1; auto. Qed. @@ -341,8 +351,7 @@ Qed. (** * [fold] *) -Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A := - fun acc => +Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} : A := match m with | nil => acc | (k,e)::m' => fold f m' (f k e acc) @@ -351,12 +360,12 @@ Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A := Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. - intros; functional induction fold A f m i; auto. + intros; functional induction (fold f m i); auto. Qed. (** * [equal] *) -Fixpoint equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool := +Function equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool := match m, m' with | nil, nil => true | (x,e)::l, (x',e')::l' => @@ -375,56 +384,52 @@ Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equal cmp m m' -> equal cmp m m' = true. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - functional induction equal cmp m m'; simpl; auto; unfold Equal; - intuition; subst; try clear H_eq_3. + functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal; + intuition; subst; match goal with + | [H: X.compare _ _ = _ |- _ ] => clear H + | _ => idtac + end. - destruct p as (k,e). - destruct (H0 k). - destruct H2. - exists e; auto. - inversion H2. - destruct (H0 x). - destruct H. - exists e; auto. - inversion H. - destruct (H0 x). - assert (In x ((x',e')::l')). - apply H; auto. - exists e; auto. - destruct (In_inv H3). - order. - inversion_clear Hm'. - assert (Inf (x,e) l'). - apply Inf_lt with (x',e'); auto. - elim (Sort_Inf_NotIn H5 H7 H4). - - assert (cmp e e' = true). + assert (cmp_e_e':cmp e e' = true). apply H2 with x; auto. - rewrite H0; simpl. - apply H; auto. + rewrite cmp_e_e'; simpl. + apply IHb; auto. inversion_clear Hm; auto. inversion_clear Hm'; auto. unfold Equal; intuition. - destruct (H1 k). + destruct (H0 k). assert (In k ((x,e) ::l)). - destruct H3 as (e'', hyp); exists e''; auto. - destruct (In_inv (H4 H6)); auto. + destruct H as (e'', hyp); exists e''; auto. + destruct (In_inv (H1 H4)); auto. inversion_clear Hm. - elim (Sort_Inf_NotIn H8 H9). - destruct H3 as (e'', hyp); exists e''; auto. + elim (Sort_Inf_NotIn H6 H7). + destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - destruct (H1 k). + destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H3 as (e'', hyp); exists e''; auto. - destruct (In_inv (H5 H6)); auto. + destruct H as (e'', hyp); exists e''; auto. + destruct (In_inv (H3 H4)); auto. inversion_clear Hm'. - elim (Sort_Inf_NotIn H8 H9). - destruct H3 as (e'', hyp); exists e''; auto. + elim (Sort_Inf_NotIn H6 H7). + destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. apply H2 with k; destruct (eq_dec x k); auto. + + destruct (X.compare x x'); try contradiction;clear H2. + destruct (H0 x). + assert (In x ((x',e')::l')). + apply H; auto. + exists e; auto. + destruct (In_inv H3). + order. + inversion_clear Hm'. + assert (Inf (x,e) l'). + apply Inf_lt with (x',e'); auto. + elim (Sort_Inf_NotIn H5 H7 H4). + destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. @@ -435,43 +440,70 @@ Proof. assert (Inf (x',e') l). apply Inf_lt with (x,e); auto. elim (Sort_Inf_NotIn H5 H7 H4). + + destruct _x; + destruct _x0;try contradiction. + + clear H1;destruct p as (k,e). + destruct (H0 k). + destruct H1. + exists e; auto. + inversion H1. + + destruct p as (x,e). + destruct (H0 x). + destruct H. + exists e; auto. + inversion H. + + destruct p;destruct p0;contradiction. Qed. + Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equal cmp m m'. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - functional induction equal cmp m m'; simpl; auto; unfold Equal; - intuition; try discriminate; subst; try clear H_eq_3; - try solve [inversion H0]; destruct (andb_prop _ _ H0); clear H0; - inversion_clear Hm; inversion_clear Hm'. - - destruct (H H0 H5 H3). - destruct (In_inv H1). + functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal; + intuition; try discriminate; subst; match goal with + | [H: X.compare _ _ = _ |- _ ] => clear H + | _ => idtac + end. + + inversion H0. + + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHb H1 H3 H6). + destruct (In_inv H0). exists e'; constructor; split; trivial; apply X.eq_trans with x; auto. - destruct (H7 k). - destruct (H10 H9) as (e'',hyp). + destruct (H k). + destruct (H9 H8) as (e'',hyp). exists e''; auto. - destruct (H H0 H5 H3). - destruct (In_inv H1). + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHb H1 H3 H6). + destruct (In_inv H0). exists e; constructor; split; trivial; apply X.eq_trans with x'; auto. - destruct (H7 k). - destruct (H11 H9) as (e'',hyp). + destruct (H k). + destruct (H10 H8) as (e'',hyp). exists e''; auto. - destruct (H H0 H6 H4). - inversion_clear H1. - destruct H10; simpl in *; subst. + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHb H1 H4 H7). + inversion_clear H0. + destruct H9; simpl in *; subst. inversion_clear H2. - destruct H10; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H6 H7). + destruct H9; simpl in *; subst; auto. + elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with k; auto; order. inversion_clear H2. - destruct H1; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H0 H5). - exists e1; apply MapsTo_eq with k; auto; order. - apply H9 with k; auto. + destruct H0; simpl in *; subst; auto. + elim (Sort_Inf_NotIn H1 H3). + exists e0; apply MapsTo_eq with k; auto; order. + apply H8 with k; auto. Qed. (** This lemma isn't part of the spec of [Equal], but is used in [FMapAVL] *) diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index dc034bf83..415e0c113 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -91,7 +91,7 @@ Qed. (** * [mem] *) -Fixpoint mem (k : key) (s : t elt) {struct s} : bool := +Function mem (k : key) (s : t elt) {struct s} : bool := match s with | nil => false | (k',_) :: l => if X.eq_dec k k' then true else mem k l @@ -100,30 +100,30 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool := Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true. Proof. intros m Hm x; generalize Hm; clear Hm. - functional induction mem x m;intros NoDup belong1;trivial. - inversion belong1. inversion H. + functional induction (mem x m);intros NoDup belong1;trivial. + inversion belong1. inversion H0. inversion_clear NoDup. inversion_clear belong1. inversion_clear H3. compute in H4; destruct H4. elim H; auto. - apply H0; auto. - exists x; auto. + apply IHb; auto. + exists x0; auto. Qed. Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. - functional induction mem x m; intros NoDup hyp; try discriminate. - exists e; auto. + functional induction (mem x m); intros NoDup hyp; try discriminate. + exists _x; auto. inversion_clear NoDup. - destruct H0; auto. - exists x; auto. + destruct IHb; auto. + exists x0; auto. Qed. (** * [find] *) -Fixpoint find (k:key) (s: t elt) {struct s} : option elt := +Function find (k:key) (s: t elt) {struct s} : option elt := match s with | nil => None | (k',x)::s' => if X.eq_dec k k' then Some x else find k s' @@ -132,23 +132,23 @@ Fixpoint find (k:key) (s: t elt) {struct s} : option elt := Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold PX.MapsTo. - functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto. + functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. Qed. Lemma find_1 : forall m (Hm:NoDupA m) x e, MapsTo x e m -> find x m = Some e. Proof. intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction find x m;simpl; subst; try clear H_eq_1. + functional induction (find x m);simpl; subst; try clear H_eq_1. inversion 2. do 2 inversion_clear 1. compute in H3; destruct H3; subst; trivial. - elim H0; apply InA_eqk with (k,e); auto. + elim H; apply InA_eqk with (x,e); auto. do 2 inversion_clear 1; auto. - compute in H4; destruct H4; elim H; auto. + compute in H3; destruct H3; elim _x; auto. Qed. (* Not part of the exported specifications, used later for [combine]. *) @@ -166,7 +166,7 @@ Qed. (** * [add] *) -Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt := +Function add (k : key) (x : elt) (s : t elt) {struct s} : t elt := match s with | nil => (k,x) :: nil | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l @@ -175,28 +175,28 @@ Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt := Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y; unfold PX.MapsTo. - functional induction add x e m;simpl;auto. + functional induction (add x e m);simpl;auto. Qed. Lemma add_2 : forall m x y e e', ~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). Proof. intros m x y e e'; generalize y e; clear y e; unfold PX.MapsTo. - functional induction add x e' m;simpl;auto. - intros y' e' eqky'; inversion_clear 1. - destruct H1; simpl in *. + functional induction (add x e' m);simpl;auto. + intros y' e'' eqky'; inversion_clear 1. + destruct H2; simpl in *. elim eqky'; apply X.eq_trans with k'; auto. auto. - intros y' e' eqky'; inversion_clear 1; intuition. + intros y' e'' eqky'; inversion_clear 1; intuition. Qed. Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. - functional induction add x e' m;simpl;auto. - intros; apply (In_inv_3 H0); auto. - constructor 2; apply (In_inv_3 H1); auto. + functional induction (add x e' m);simpl;auto. + intros; apply (In_inv_3 H1); auto. + constructor 2; apply (In_inv_3 H2); auto. inversion_clear 2; auto. Qed. @@ -204,12 +204,12 @@ Lemma add_3' : forall m x y e e', ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m. Proof. intros m x y e e'. generalize y e; clear y e. - functional induction add x e' m;simpl;auto. + functional induction (add x e' m);simpl;auto. inversion_clear 2. - compute in H1; elim H; auto. - inversion H1. - constructor 2; inversion_clear H1; auto. compute in H2; elim H0; auto. + inversion H2. + constructor 2; inversion_clear H2; auto. + compute in H3; elim H1; auto. inversion_clear 2; auto. Qed. @@ -257,7 +257,7 @@ Qed. (** * [remove] *) -Fixpoint remove (k : key) (s : t elt) {struct s} : t elt := +Function remove (k : key) (s : t elt) {struct s} : t elt := match s with | nil => nil | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l @@ -266,23 +266,23 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt := Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - functional induction remove x m;simpl;intros;auto. + functional induction (remove x m);simpl;intros;auto. - red; inversion 1; inversion H1. + red; inversion 1; inversion H2. inversion_clear Hm. subst. - swap H1. - destruct H3 as (e,H3); unfold PX.MapsTo in H3. + swap H2. + destruct H as (e,H); unfold PX.MapsTo in H. apply InA_eqk with (y,e); auto. - compute; apply X.eq_trans with k; auto. + compute; apply X.eq_trans with x; auto. intro H2. destruct H2 as (e,H2); inversion_clear H2. compute in H3; destruct H3. - elim H; apply X.eq_trans with y; auto. + elim _x; apply X.eq_trans with y; auto. inversion_clear Hm. - elim (H0 H4 H1). + elim (IHt0 H4 H1). exists e; auto. Qed. @@ -290,10 +290,10 @@ Lemma remove_2 : forall m (Hm:NoDupA m) x y e, ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction remove x m;auto. + functional induction (remove x m);auto. inversion_clear 3; auto. - compute in H2; destruct H2. - elim H0; apply X.eq_trans with k'; auto. + compute in H3; destruct H3. + elim H1; apply X.eq_trans with k'; auto. inversion_clear 1; inversion_clear 2; auto. Qed. @@ -302,7 +302,7 @@ Lemma remove_3 : forall m (Hm:NoDupA m) x y e, MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction remove x m;auto. + functional induction (remove x m);auto. do 2 inversion_clear 1; auto. Qed. @@ -310,7 +310,7 @@ Lemma remove_3' : forall m (Hm:NoDupA m) x y e, InA eqk (y,e) (remove x m) -> InA eqk (y,e) m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. - functional induction remove x m;auto. + functional induction (remove x m);auto. do 2 inversion_clear 1; auto. Qed. @@ -347,8 +347,7 @@ Qed. (** * [fold] *) -Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A := - fun acc => +Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc : A) {struct m} : A := match m with | nil => acc | (k,e)::m' => fold f m' (f k e acc) @@ -357,7 +356,7 @@ Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A := Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. - intros; functional induction fold A f m i; auto. + intros; functional induction (@fold A f m i); auto. Qed. (** * [equal] *) diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 3c6f49394..5b912f8b2 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -287,7 +287,7 @@ Qed. (** The [mem] function is deciding appartness. It exploits the [bst] property to achieve logarithmic complexity. *) -Fixpoint mem (x:elt)(s:t) { struct s } : bool := +Function mem (x:elt)(s:t) { struct s } : bool := match s with | Leaf => false | Node l y r _ => match X.compare x y with @@ -300,7 +300,7 @@ Fixpoint mem (x:elt)(s:t) { struct s } : bool := Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. Proof. intros s x. - functional induction mem x s; inversion_clear 1; auto. + functional induction (mem x s); inversion_clear 1; auto. inversion_clear 1. inversion_clear 1; auto; absurd (X.lt x y); eauto. inversion_clear 1; auto; absurd (X.lt y x); eauto. @@ -309,7 +309,7 @@ Qed. Lemma mem_2 : forall s x, mem x s = true -> In x s. Proof. intros s x. - functional induction mem x s; auto; intros; try discriminate. + functional induction (mem x s); auto; intros; try discriminate. Qed. (** * Singleton set *) @@ -472,7 +472,7 @@ Ltac omega_bal := match goal with (** * Insertion *) -Fixpoint add (x:elt)(s:t) { struct s } : t := match s with +Function add (x:elt)(s:t) { struct s } : t := match s with | Leaf => Node Leaf x Leaf 1 | Node l y r h => match X.compare x y with @@ -485,17 +485,17 @@ Fixpoint add (x:elt)(s:t) { struct s } : t := match s with Lemma add_avl_1 : forall s x, avl s -> avl (add x s) /\ 0 <= height (add x s) - height s <= 1. Proof. - intros s x; functional induction add x s; intros; inv avl; simpl in *. + intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *. intuition; try constructor; simpl; auto; try omega_max. (* LT *) - destruct H; auto. + destruct IHt; auto. split. apply bal_avl; auto; omega_max. omega_bal. (* EQ *) intuition; omega_max. (* GT *) - destruct H; auto. + destruct IHt; auto. split. apply bal_avl; auto; omega_max. omega_bal. @@ -510,12 +510,12 @@ Hint Resolve add_avl. Lemma add_in : forall s x y, avl s -> (In y (add x s) <-> X.eq y x \/ In y s). Proof. - intros s x; functional induction add x s; auto; intros. + intros s x; functional induction (add x s); auto; intros. intuition_in. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (H y0 H1); intuition_in. + rewrite (IHt y0 H2); intuition_in. (* EQ *) inv avl. intuition. @@ -523,24 +523,24 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (H y0 H2); intuition_in. + rewrite (IHt y0 H3); intuition_in. Qed. Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s). Proof. - intros s x; functional induction add x s; auto; intros. + intros s x; functional induction (add x s); auto; intros. inv bst; inv avl; apply bal_bst; auto. (* lt_tree -> lt_tree (add ...) *) - red; red in H4. + red; red in H5. intros. - rewrite (add_in l x y0 H0) in H1. + rewrite (add_in l x y0 H1) in H2. intuition. eauto. inv bst; inv avl; apply bal_bst; auto. (* gt_tree -> gt_tree (add ...) *) - red; red in H4. + red; red in H5. intros. - rewrite (add_in r x y0 H6) in H1. + rewrite (add_in r x y0 H7) in H2. intuition. apply MX.lt_eq with x; auto. Qed. @@ -688,22 +688,22 @@ Qed. for [t=Leaf], we pre-unpack [t] (and forget about [h]). *) -Fixpoint remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := +Function remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := match l with | Leaf => (r,x) - | Node ll lx lr lh => let (l',m) := remove_min ll lx lr in (bal l' x r, m) + | Node ll lx lr lh => let (l',m) := (remove_min ll lx lr : t*elt) in (bal l' x r, m) end. Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> avl (fst (remove_min l x r)) /\ 0 <= height (Node l x r h) - height (fst (remove_min l x r)) <= 1. Proof. - intros l x r; functional induction remove_min l x r; simpl in *; intros. + intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv avl; simpl in *; split; auto. avl_nns; omega_max. (* l = Node *) - inversion_clear H0. - destruct (H lh); auto. + inversion_clear H. + rewrite H0 in IHp;simpl in IHp;destruct (IHp lh); auto. split; simpl in *. apply bal_avl; auto; omega_max. omega_bal. @@ -719,29 +719,30 @@ Lemma remove_min_in : forall l x r h y, avl (Node l x r h) -> (In y (Node l x r h) <-> X.eq y (snd (remove_min l x r)) \/ In y (fst (remove_min l x r))). Proof. - intros l x r; functional induction remove_min l x r; simpl in *; intros. + intros l x r; functional induction (remove_min l x r); simpl in *; intros. intuition_in. (* l = Node *) - inversion_clear H0. - generalize (remove_min_avl ll lx lr lh H1). - rewrite H_eq_0; simpl; intros. + inversion_clear H1. + generalize (remove_min_avl ll lx lr lh H2). + rewrite H0; simpl; intros. rewrite bal_in; auto. - generalize (H lh y H1). + rewrite H0 in IHp;generalize (IHp lh y H2). intuition. - inversion_clear H8; intuition. + inversion_clear H9; intuition. Qed. Lemma remove_min_bst : forall l x r h, bst (Node l x r h) -> avl (Node l x r h) -> bst (fst (remove_min l x r)). Proof. - intros l x r; functional induction remove_min l x r; simpl in *; intros. + intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H0; inversion_clear H1. + inversion_clear H; inversion_clear H1. + rewrite_all H0;simpl in *. apply bal_bst; auto. firstorder. intro; intros. - generalize (remove_min_in ll lx lr lh y H0). - rewrite H_eq_0; simpl. + generalize (remove_min_in ll lx lr lh y H). + rewrite H0; simpl. destruct 1. apply H4; intuition. Qed. @@ -750,16 +751,16 @@ Lemma remove_min_gt_tree : forall l x r h, bst (Node l x r h) -> avl (Node l x r h) -> gt_tree (snd (remove_min l x r)) (fst (remove_min l x r)). Proof. - intros l x r; functional induction remove_min l x r; simpl in *; intros. + intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H0; inversion_clear H1. + inversion_clear H; inversion_clear H1. intro; intro. - generalize (H lh H2 H0); clear H8 H7 H. - generalize (remove_min_avl ll lx lr lh H0). - generalize (remove_min_in ll lx lr lh m H0). - rewrite H_eq_0; simpl; intros. - rewrite (bal_in l' x r y H7 H6) in H1. - destruct H. + generalize (IHp lh H2 H); clear H8 H7 IHp. + generalize (remove_min_avl ll lx lr lh H). + generalize (remove_min_in ll lx lr lh m H). + rewrite H0; simpl; intros. + rewrite (bal_in l' x r y H8 H6) in H1. + destruct H7. firstorder. apply MX.lt_eq with x; auto. apply X.lt_trans with x; auto. @@ -772,7 +773,7 @@ Qed. [|height t1 - height t2| <= 2]. *) -Definition merge s1 s2 := match s1,s2 with +Function merge (s1 s2 :t) : t:= match s1,s2 with | Leaf, _ => s2 | _, Leaf => s1 | _, Node l2 x2 r2 h2 => @@ -784,11 +785,12 @@ Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 -> avl (merge s1 s2) /\ 0<= height (merge s1 s2) - max (height s1) (height s2) <=1. Proof. - intros s1 s2; functional induction merge s1 s2; simpl in *; intros. + intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros. split; auto; avl_nns; omega_max. split; auto; avl_nns; simpl in *; omega_max. + destruct _x;try contradiction;clear H1. generalize (remove_min_avl_1 l2 x2 r2 h2 H0). - rewrite H_eq_1; simpl; destruct 1. + rewrite H2; simpl; destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -804,32 +806,34 @@ Qed. Lemma merge_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (In y (merge s1 s2) <-> In y s1 \/ In y s2). Proof. - intros s1 s2; functional induction merge s1 s2; simpl in *; intros. + intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros. intuition_in. intuition_in. - replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H_eq_1; auto]. + destruct _x;try contradiction;clear H1. + replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto]. rewrite bal_in; auto. - generalize (remove_min_avl l2 x2 r2 h2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y); rewrite H_eq_1; simpl; intro. - rewrite H3; intuition. + generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y); rewrite H2; simpl; intro. + rewrite H1; intuition. Qed. Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> bst (merge s1 s2). Proof. - intros s1 s2; functional induction merge s1 s2; simpl in *; intros; auto. + intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto. + destruct _x;try contradiction;clear H1. apply bal_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2); rewrite H_eq_1; simpl in *; auto. + generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto. intro; intro. - apply H3; auto. - generalize (remove_min_in l2 x2 r2 h2 m); rewrite H_eq_1; simpl; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H_eq_1; simpl; auto. + apply H5; auto. + generalize (remove_min_in l2 x2 r2 h2 m); rewrite H2; simpl; intuition. + generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H2; simpl; auto. Qed. (** * Deletion *) -Fixpoint remove (x:elt)(s:tree) { struct s } : t := match s with +Function remove (x:elt)(s:tree) { struct s } : t := match s with | Leaf => Leaf | Node l y r h => match X.compare x y with @@ -842,22 +846,22 @@ Fixpoint remove (x:elt)(s:tree) { struct s } : t := match s with Lemma remove_avl_1 : forall s x, avl s -> avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. Proof. - intros s x; functional induction remove x s; simpl; intros. + intros s x; functional induction (remove x s); subst;simpl; intros. intuition; omega_max. (* LT *) inv avl. - destruct (H H1). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) inv avl. - generalize (merge_avl_1 l r H0 H1 H2). + generalize (merge_avl_1 l r H1 H2 H3). intuition omega_max. (* GT *) inv avl. - destruct (H H2). + destruct (IHt H2). split. apply bal_avl; auto. omega_max. @@ -873,32 +877,32 @@ Hint Resolve remove_avl. Lemma remove_in : forall s x y, bst s -> avl s -> (In y (remove x s) <-> ~ X.eq y x /\ In y s). Proof. - intros s x; functional induction remove x s; simpl; intros. + intros s x; functional induction (remove x s); subst;simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite bal_in; auto. - generalize (H y0 H1); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H9; eauto. (* GT *) - inv avl; inv bst; clear H_eq_0. + inv avl; inv bst; clear H0. rewrite bal_in; auto. - generalize (H y0 H6); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H6); intuition; [ order | order | intuition_in ]. Qed. Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s). Proof. - intros s x; functional induction remove x s; simpl; intros. + intros s x; functional induction (remove x s); simpl; intros. auto. (* LT *) inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in l x y0) in H0; auto. - destruct H0; eauto. + rewrite (remove_in l x y0) in H1; auto. + destruct H1; eauto. (* EQ *) inv avl; inv bst. apply merge_bst; eauto. @@ -906,13 +910,13 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in r x y0) in H0; auto. - destruct H0; eauto. + rewrite (remove_in r x y0) in H1; auto. + destruct H1; eauto. Qed. (** * Minimum element *) -Fixpoint min_elt (s:t) : option elt := match s with +Function min_elt (s:t) : option elt := match s with | Leaf => None | Node Leaf y _ _ => Some y | Node l _ _ _ => min_elt l @@ -920,46 +924,48 @@ end. Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s. Proof. - intro s; functional induction min_elt s; simpl. + intro s; functional induction (min_elt s); subst; simpl. inversion 1. inversion 1; auto. intros. - destruct t0; auto. + destruct l; auto. Qed. Lemma min_elt_2 : forall s x y, bst s -> min_elt s = Some x -> In y s -> ~ X.lt y x. Proof. - intro s; functional induction min_elt s; simpl. + intro s; functional induction (min_elt s); subst;simpl. inversion_clear 2. inversion_clear 1. inversion 1; subst. inversion_clear 1; auto. inversion_clear H5. + destruct l;try contradiction. inversion_clear 1. - destruct t0. + simpl. + destruct l1. inversion 1; subst. - assert (X.lt x y) by (apply H3; auto). + assert (X.lt x _x) by (apply H3; auto). inversion_clear 1; auto; order. - assert (X.lt t1 y) by auto. + assert (X.lt t _x) by auto. inversion_clear 2; auto; - (assert (~ X.lt t1 x) by auto); order. + (assert (~ X.lt t x) by auto); order. Qed. Lemma min_elt_3 : forall s, min_elt s = None -> Empty s. Proof. - intro s; functional induction min_elt s; simpl. + intro s; functional induction (min_elt s); subst;simpl. red; auto. inversion 1. - destruct t0. - inversion 1. - intros H0; destruct (H H0 t1); auto. + destruct l;try contradiction. + clear H0;intro H0. + destruct (IHo H0 t); auto. Qed. (** * Maximum element *) -Fixpoint max_elt (s:t) : option elt := match s with +Function max_elt (s:t) : option elt := match s with | Leaf => None | Node _ y Leaf _ => Some y | Node _ _ r _ => max_elt r @@ -967,40 +973,38 @@ end. Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s. Proof. - intro s; functional induction max_elt s; simpl. + intro s; functional induction (max_elt s); subst;simpl. inversion 1. inversion 1; auto. - intros. - destruct t2; auto. + destruct r;try contradiction; auto. Qed. Lemma max_elt_2 : forall s x y, bst s -> max_elt s = Some x -> In y s -> ~ X.lt x y. Proof. - intro s; functional induction max_elt s; simpl. + intro s; functional induction (max_elt s); subst;simpl. inversion_clear 2. inversion_clear 1. inversion 1; subst. inversion_clear 1; auto. inversion_clear H5. + destruct r;try contradiction. inversion_clear 1. - destruct t2. - inversion 1; subst. - assert (X.lt y x) by (apply H4; auto). - inversion_clear 1; auto; order. - assert (X.lt y t1) by auto. +(* inversion 1; subst. *) +(* assert (X.lt y x) by (apply H4; auto). *) +(* inversion_clear 1; auto; order. *) + assert (X.lt _x0 t) by auto. inversion_clear 2; auto; - (assert (~ X.lt x t1) by auto); order. + (assert (~ X.lt x t) by auto); order. Qed. Lemma max_elt_3 : forall s, max_elt s = None -> Empty s. Proof. - intro s; functional induction max_elt s; simpl. + intro s; functional induction (max_elt s); subst;simpl. red; auto. inversion 1. - destruct t2. - inversion 1. - intros H0; destruct (H H0 t1); auto. + destruct r;try contradiction. + clear H0;intros H0; destruct (IHo H0 t); auto. Qed. (** * Any element *) @@ -1022,7 +1026,7 @@ Qed. Same as [merge] but does not assume anything about heights. *) -Definition concat s1 s2 := +Function concat (s1 s2 : t) : t := match s1, s2 with | Leaf, _ => s2 | _, Leaf => s1 @@ -1033,46 +1037,39 @@ Definition concat s1 s2 := Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2). Proof. - intros s1 s2; functional induction concat s1 s2; auto. - intros; change (avl (join (Node t t0 t1 i) m s2')). - rewrite <- H_eq_ in H; rewrite <- H_eq_. - apply join_avl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H_eq_1; simpl; auto. + intros s1 s2; functional induction (concat s1 s2); subst;auto. + destruct _x;try contradiction;clear H1. + intros; apply join_avl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto. Qed. Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> bst (concat s1 s2). Proof. - intros s1 s2; functional induction concat s1 s2; auto. - intros; change (bst (join (Node t t0 t1 i) m s2')). - rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; - rewrite <- H_eq_ in H3; rewrite <- H_eq_. - apply join_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite H_eq_1; simpl; auto. + intros s1 s2; functional induction (concat s1 s2); subst ;auto. + destruct _x;try contradiction;clear H1. + intros; apply join_bst; auto. + generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 m H3); rewrite H2; simpl; auto. destruct 1; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto. Qed. Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> (In y (concat s1 s2) <-> In y s1 \/ In y s2). Proof. - intros s1 s2; functional induction concat s1 s2. + intros s1 s2; functional induction (concat s1 s2);subst;simpl. intuition. inversion_clear H5. - intuition. + destruct _x;try contradiction;clear H1;intuition. inversion_clear H5. - intros. - change (In y (join (Node t t0 t1 i) m s2') <-> - In y (Node t t0 t1 i) \/ In y (Node l2 x2 r2 h2)). - rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; - rewrite <- H_eq_ in H3; rewrite <- H_eq_. - rewrite (join_in s1 m s2' y H0). - generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite H_eq_1; simpl. + destruct _x;try contradiction;clear H1; intros. + rewrite (join_in (Node _x1 t _x2 i) m s2' y H0). + generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl. intro EQ; rewrite EQ; intuition. Qed. @@ -1084,7 +1081,7 @@ Qed. - [present] is [true] if and only if [s] contains [x]. *) -Fixpoint split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with +Function split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with | Leaf => (Leaf, (false, Leaf)) | Node l y r h => match X.compare x y with @@ -1101,101 +1098,99 @@ Fixpoint split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with Lemma split_avl : forall s x, avl s -> avl (fst (split x s)) /\ avl (snd (snd (split x s))). Proof. - intros s x; functional induction split x s. + intros s x; functional induction (split x s);subst;simpl in *. auto. - destruct p; simpl in *. - inversion_clear 1; intuition. + rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. simpl; inversion_clear 1; auto. - destruct p; simpl in *. - inversion_clear 1; intuition. + rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. Qed. Lemma split_in_1 : forall s x y, bst s -> avl s -> (In y (fst (split x s)) <-> In y s /\ X.lt y x). Proof. - intros s x; functional induction split x s. + intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. - rewrite (H y0 H1 H5); clear H H_eq_0. + rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H9. + rewrite (IHp y0 H2 H6); clear IHp H0. intuition. inversion_clear H0; auto; order. (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0. intuition. order. intuition_in; order. (* GT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. rewrite join_in; auto. - generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition. - rewrite (H y0 H2 H6); clear H. + generalize (split_avl r x H7); rewrite H1; simpl; intuition. + rewrite (IHp y0 H3 H7); clear H1. intuition; [ eauto | eauto | intuition_in ]. Qed. Lemma split_in_2 : forall s x y, bst s -> avl s -> (In y (snd (snd (split x s))) <-> In y s /\ X.lt x y). Proof. - intros s x; functional induction split x s. + intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. rewrite join_in; auto. - generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition. - rewrite (H y0 H1 H5); clear H H_eq_0. + generalize (split_avl l x H6); rewrite H1; simpl; intuition. + rewrite (IHp y0 H2 H6); clear IHp H0. intuition; [ order | order | intuition_in ]. (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0. intuition; [ order | intuition_in; order ]. (* GT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. - rewrite (H y0 H2 H6); clear H H_eq_0. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite (IHp y0 H3 H7); clear IHp H0. intuition; intuition_in; order. Qed. Lemma split_in_3 : forall s x, bst s -> avl s -> (fst (snd (split x s)) = true <-> In x s). Proof. - intros s x; functional induction split x s. + intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. - rewrite H; auto. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite IHp; auto. intuition_in; absurd (X.lt x y); eauto. (* EQ *) simpl in *; inversion_clear 1; inversion_clear 1; intuition. (* GT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. - rewrite H; auto. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite IHp; auto. intuition_in; absurd (X.lt y x); eauto. Qed. Lemma split_bst : forall s x, bst s -> avl s -> bst (fst (split x s)) /\ bst (snd (snd (split x s))). Proof. - intros s x; functional induction split x s. + intros s x; functional induction (split x s);subst;simpl in *. intuition. (* LT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition. + generalize (split_avl l x H6); rewrite H1; simpl; intuition. intro; intro. - generalize (split_in_2 l x y0 H1 H5); rewrite H_eq_1; simpl; intuition. + generalize (split_in_2 l x y0 H2 H6); rewrite H1; simpl; intuition. (* EQ *) simpl in *; inversion_clear 1; inversion_clear 1; intuition. (* GT *) - destruct p; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition. + generalize (split_avl r x H7); rewrite H1; simpl; intuition. intro; intro. - generalize (split_in_1 r x y0 H2 H6); rewrite H_eq_1; simpl; intuition. + generalize (split_in_1 r x y0 H3 H7); rewrite H1; simpl; intuition. Qed. (** * Intersection *) - Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with +Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with | Leaf,_ => Leaf | _,Leaf => Leaf | Node l1 x1 r1 h1, _ => |