diff options
Diffstat (limited to 'src/array')
| -rw-r--r-- | src/array/Array_checker.v | 200 | ||||
| -rw-r--r-- | src/array/FArray.v | 270 |
2 files changed, 234 insertions, 236 deletions
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index de20723..f95c282 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool List Int63 PArray Psatz. +Require Import Bool List Int63 PArray Psatz ZArith. Require Import Misc State SMT_terms FArray SMT_classes. Import Form. @@ -193,7 +193,7 @@ Section certif. rho x = Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[ x]). Proof. intros x;apply wf_interp_form;trivial. Qed. - Definition wf := PArray.forallbi lt_form t_form. + Definition wf := aforallbi lt_form t_form. Hypothesis wf_t_i : wf. Notation atom := int (only parsing). @@ -226,14 +226,14 @@ Section certif. apply Typ.eqb_spec in Heq6a. apply Typ.eqb_spec in Heq6b. apply Typ.eqb_spec in Heq6c. - apply Int63Properties.eqb_spec in Heq6d. - apply Int63Properties.eqb_spec in Heq6e. + apply Int63.eqb_spec in Heq6d. + apply Int63.eqb_spec in Heq6e. pose proof (rho_interp (Lit.blit lres)) as Hrho. rewrite Heq2 in Hrho. simpl in Hrho. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. @@ -440,7 +440,7 @@ Section certif. subst t1 t2 t3 t4. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. assert (H15: b1 < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. discriminate. @@ -629,9 +629,9 @@ Section certif. apply Typ.eqb_spec in Heq11a. apply Typ.eqb_spec in Heq11b. - apply Int63Properties.eqb_spec in Heq11c. + apply Int63.eqb_spec in Heq11c. rewrite !andb_true_iff in Heq11d. - rewrite !Int63Properties.eqb_spec in Heq11d. + rewrite !Int63.eqb_spec in Heq11d. rewrite !Atom.t_interp_wf in isif; trivial. @@ -785,9 +785,9 @@ Section certif. apply Typ.eqb_spec in Heq11a. apply Typ.eqb_spec in Heq11b. - apply Int63Properties.eqb_spec in Heq11d. + apply Int63.eqb_spec in Heq11d. rewrite !andb_true_iff in Heq11c. - rewrite !Int63Properties.eqb_spec in Heq11c. + rewrite !Int63.eqb_spec in Heq11c. rewrite !Atom.t_interp_wf in isif; trivial. @@ -955,26 +955,22 @@ Section certif. apply Typ.eqb_spec in Heq15. apply Typ.eqb_spec in Heq15a. subst t3 t5 t4 t6 t7 t8. - rewrite !Int63Properties.eqb_spec in Heq1314. + rewrite !Int63.eqb_spec in Heq1314. unfold Lit.interp. rewrite Heq. unfold Var.interp. rewrite !wf_interp_form; trivial. rewrite Heq2. simpl. rewrite afold_left_or. unfold to_list. - rewrite Int63Properties.eqb_spec in Heq3. + rewrite Int63.eqb_spec in Heq3. rewrite Heq3. - (* for native-coq compatibility *) - assert (0 == 2 = false) as NCC. - { auto. } rewrite NCC. (* simpl. *) - rewrite foldi_down_gt; auto. + rewrite foldi_lt_r by reflexivity. + rewrite foldi_lt_r by reflexivity. + rewrite foldi_ge by reflexivity. + change (2 - 1) with 1; change (2 - 1 - 1) with 0. - (* simpl. *) - assert (2 - 1 = 1). { auto. } - rewrite H. - rewrite foldi_down_eq; auto. simpl. rewrite orb_false_r. assert (1 - 1 = 0) as Has2. { auto. } rewrite Has2. @@ -985,8 +981,8 @@ Section certif. pose proof (rho_interp (Lit.blit (a .[ 0]))). pose proof (rho_interp (Lit.blit (a .[ 1]))). - rewrite Heq5 in H0. rewrite Heq6 in H1. - simpl in H0, H1. + rewrite Heq5 in H. rewrite Heq6 in H0. + simpl in H, H0. unfold Lit.interp. rewrite andb_true_iff in Heq4. destruct Heq4 as (Heq4, Heq4a). @@ -994,32 +990,32 @@ Section certif. unfold Lit.interp in Hisa. rewrite Heq4 in Hisa. unfold Var.interp in Hisa. - rewrite Hisa in H0. symmetry in H0. + rewrite Hisa in H. symmetry in H. rewrite Heq4a. unfold Var.interp. - rewrite H1. + rewrite H0. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. (* b *) - pose proof (H2 b). assert (b < PArray.length t_atom). + pose proof (H1 b). assert (b < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. easy. - specialize (H3 H4). simpl in H3. - rewrite Heq7 in H3. simpl in H3. - rewrite !andb_true_iff in H3. destruct H3. destruct H3. - unfold get_type' in H3, H5, H6. unfold v_type in H3, H5, H6. + specialize (H2 H3). simpl in H2. + rewrite Heq7 in H2. simpl in H2. + rewrite !andb_true_iff in H2. destruct H2. destruct H2. + unfold get_type' in H2, H4, H5. unfold v_type in H2, H4, H5. case_eq (t_interp .[ b]). - intros v_typeb v_valb Htib. rewrite Htib in H3. + intros v_typeb v_valb Htib. rewrite Htib in H2. pose proof Htib as Htib''. - case_eq v_typeb; intros; rewrite H7 in H3; try now contradict H3. + case_eq v_typeb; intros; rewrite H6 in H2; try now contradict H2. case_eq (t_interp .[ b1]). - intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H6. + intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H5. pose proof Htib1 as Htib1''. case_eq (t_interp .[ b2]). - intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H5. + intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H4. pose proof Htib2 as Htib2''. rewrite Atom.t_interp_wf in Htib; trivial. rewrite Atom.t_interp_wf in Htib1; trivial. @@ -1028,33 +1024,33 @@ Section certif. rewrite !Atom.t_interp_wf in Htib; trivial. rewrite Htib1, Htib2 in Htib. unfold apply_binop in Htib. + apply Typ.eqb_spec in H4. apply Typ.eqb_spec in H5. - apply Typ.eqb_spec in H6. generalize dependent v_valb1. generalize dependent v_valb2. generalize dependent v_valb. - rewrite H5, H6, H7. rewrite !Typ.cast_refl. intros. + rewrite H4, H5, H6. rewrite !Typ.cast_refl. intros. specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_valb1 v_valb2) (v_valb)). - intros. specialize (H8 Htib). + intros. specialize (H7 Htib). (* c *) - pose proof (H2 c). assert (c < PArray.length t_atom). + pose proof (H1 c). assert (c < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. - specialize (H9 H10). simpl in H9. - rewrite Heq9 in H9. simpl in H9. - rewrite !andb_true_iff in H9. destruct H9. destruct H9. - unfold get_type' in H9, H11, H12. unfold v_type in H9, H11, H12. + specialize (H8 H9). simpl in H8. + rewrite Heq9 in H8. simpl in H8. + rewrite !andb_true_iff in H8. destruct H8. destruct H8. + unfold get_type' in H8, H10, H11. unfold v_type in H8, H10, H11. case_eq (t_interp .[ c]). - intros v_typec v_valc Htic. rewrite Htic in H9. + intros v_typec v_valc Htic. rewrite Htic in H8. pose proof Htic as Htic''. - case_eq v_typec; intros; rewrite H13 in H9; try now contradict H9. + case_eq v_typec; intros; rewrite H12 in H8; try now contradict H8. case_eq (t_interp .[ c1]). - intros v_typec1 v_valc1 Htic1. rewrite Htic1 in H12. + intros v_typec1 v_valc1 Htic1. rewrite Htic1 in H11. case_eq (t_interp .[ c2]). - intros v_typec2 v_valc2 Htic2. rewrite Htic2 in H11. + intros v_typec2 v_valc2 Htic2. rewrite Htic2 in H10. rewrite Atom.t_interp_wf in Htic; trivial. rewrite Atom.t_interp_wf in Htic1; trivial. rewrite Atom.t_interp_wf in Htic2; trivial. @@ -1062,33 +1058,33 @@ Section certif. rewrite !Atom.t_interp_wf in Htic; trivial. rewrite Htic1, Htic2 in Htic. simpl in Htic. - apply Typ.eqb_spec in H11. apply Typ.eqb_spec in H12. + apply Typ.eqb_spec in H10. apply Typ.eqb_spec in H11. generalize dependent v_valc1. generalize dependent v_valc2. generalize dependent v_valc. - rewrite H11, H12, H13. + rewrite H10, H11, H12. rewrite !Typ.cast_refl. intros. simpl in Htic. unfold Bval in Htic. specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t2 v_valc1 v_valc2) (v_valc)). - intros. specialize (H14 Htic). + intros. specialize (H13 Htic). (* c1 *) - pose proof (H2 c1). assert (c1 < PArray.length t_atom). + pose proof (H1 c1). assert (c1 < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq11. easy. - specialize (H15 H16). simpl in H15. - rewrite Heq11 in H15. simpl in H15. - rewrite !andb_true_iff in H15. destruct H15. destruct H15. - unfold get_type' in H15, H17, H18. unfold v_type in H15, H17, H18. + specialize (H14 H15). simpl in H14. + rewrite Heq11 in H14. simpl in H14. + rewrite !andb_true_iff in H14. destruct H14. destruct H14. + unfold get_type' in H14, H16, H17. unfold v_type in H14, H16, H17. case_eq (t_interp .[ c1]). - intros v_typec1' v_valc1' Htic1'. rewrite Htic1' in H15. + intros v_typec1' v_valc1' Htic1'. rewrite Htic1' in H14. pose proof Htic1' as Htic1'''. case_eq (t_interp .[ d1]). - intros v_typed1 v_vald1 Htid1. rewrite Htid1 in H18. + intros v_typed1 v_vald1 Htid1. rewrite Htid1 in H17. case_eq (t_interp .[ d2]). - intros v_typed2 v_vald2 Htid2. rewrite Htid2 in H17. + intros v_typed2 v_vald2 Htid2. rewrite Htid2 in H16. rewrite Atom.t_interp_wf in Htic1'; trivial. rewrite Atom.t_interp_wf in Htid1; trivial. rewrite Atom.t_interp_wf in Htid2; trivial. @@ -1096,35 +1092,35 @@ Section certif. rewrite !Atom.t_interp_wf in Htic1'; trivial. rewrite Htid1, Htid2 in Htic1'. simpl in Htic1'. - apply Typ.eqb_spec in H15. apply Typ.eqb_spec in H17. - apply Typ.eqb_spec in H18. + apply Typ.eqb_spec in H14. apply Typ.eqb_spec in H16. + apply Typ.eqb_spec in H17. generalize dependent v_vald1. generalize dependent v_vald2. generalize dependent v_valc1'. - rewrite H15, H17, H18. - unfold Bval. rewrite <- H15. + rewrite H14, H16, H17. + unfold Bval. rewrite <- H14. rewrite !Typ.cast_refl. intros. specialize (Atom.Bval_inj2 t_i t1 (select v_vald1 v_vald2) (v_valc1')). - intros. specialize (H19 Htic1'). + intros. specialize (H18 Htic1'). (* c2 *) - pose proof (H2 c2). assert (c2 < PArray.length t_atom). + pose proof (H1 c2). assert (c2 < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq12. easy. - specialize (H20 H21). simpl in H20. - rewrite Heq12 in H20. simpl in H20. - rewrite !andb_true_iff in H20. destruct H20. destruct H20. - unfold get_type' in H20, H22, H23. unfold v_type in H20, H22, H23. + specialize (H19 H20). simpl in H19. + rewrite Heq12 in H19. simpl in H19. + rewrite !andb_true_iff in H19. destruct H19. destruct H19. + unfold get_type' in H19, H21, H22. unfold v_type in H19, H21, H22. case_eq (t_interp .[ c2]). - intros v_typec2' v_valc2' Htic2'. rewrite Htic2' in H20. + intros v_typec2' v_valc2' Htic2'. rewrite Htic2' in H19. pose proof Htic2' as Htic2'''. case_eq (t_interp .[ e1]). - intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H23. + intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H22. case_eq (t_interp .[ e2]). - intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H22. + intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H21. pose proof Htie2 as Htie2''. rewrite Atom.t_interp_wf in Htic2'; trivial. rewrite Atom.t_interp_wf in Htie1; trivial. @@ -1133,35 +1129,35 @@ Section certif. rewrite !Atom.t_interp_wf in Htic2'; trivial. rewrite Htie1, Htie2 in Htic2'. simpl in Htic2'. - apply Typ.eqb_spec in H20. apply Typ.eqb_spec in H22. - apply Typ.eqb_spec in H23. + apply Typ.eqb_spec in H19. apply Typ.eqb_spec in H21. + apply Typ.eqb_spec in H22. generalize dependent v_valc1'. generalize dependent v_valc2'. generalize dependent v_vale1. generalize dependent v_vale2. - rewrite H22. rewrite H20 in *. rewrite H23. - unfold Bval. rewrite <- H20. + rewrite H21. rewrite H19 in *. rewrite H22. + unfold Bval. rewrite <- H19. rewrite !Typ.cast_refl. intros. specialize (Atom.Bval_inj2 t_i t1 (select v_vale1 v_vale2) (v_valc2')). - intros. specialize (H24 Htic2'). + intros. specialize (H23 Htic2'). (* d2 *) - pose proof (H2 d2). assert (d2 < PArray.length t_atom). + pose proof (H1 d2). assert (d2 < PArray.length t_atom). apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq14. easy. - specialize (H25 H26). simpl in H25. - rewrite Heq14 in H25. simpl in H25. - rewrite !andb_true_iff in H25. destruct H25. destruct H25. - unfold get_type' in H25, H27, H28. unfold v_type in H25, H27, H28. + specialize (H24 H25). simpl in H24. + rewrite Heq14 in H24. simpl in H24. + rewrite !andb_true_iff in H24. destruct H24. destruct H24. + unfold get_type' in H24, H26, H27. unfold v_type in H24, H26, H27. case_eq (t_interp .[ d2]). - intros v_typed2' v_vald2' Htid2'. rewrite Htid2' in H25. + intros v_typed2' v_vald2' Htid2'. rewrite Htid2' in H24. pose proof Htid2' as Htid2'''. case_eq (t_interp .[ f1]). - intros v_typef1 v_valf1 Htif1. rewrite Htif1 in H28. + intros v_typef1 v_valf1 Htif1. rewrite Htif1 in H27. case_eq (t_interp .[ f2]). - intros v_typef2 v_valf2 Htif2. rewrite Htif2 in H27. + intros v_typef2 v_valf2 Htif2. rewrite Htif2 in H26. rewrite Atom.t_interp_wf in Htid2'; trivial. rewrite Atom.t_interp_wf in Htif1; trivial. rewrite Atom.t_interp_wf in Htif2; trivial. @@ -1169,21 +1165,21 @@ Section certif. rewrite !Atom.t_interp_wf in Htid2'; trivial. rewrite Htif1, Htif2 in Htid2'. simpl in Htid2'. - apply Typ.eqb_spec in H25. apply Typ.eqb_spec in H27. - apply Typ.eqb_spec in H28. + apply Typ.eqb_spec in H24. apply Typ.eqb_spec in H26. + apply Typ.eqb_spec in H27. generalize dependent v_valf1. generalize dependent v_valf2. generalize dependent v_vald2'. - rewrite H25, H27, H28. - unfold Bval. rewrite <- H25. + rewrite H24, H26, H27. + unfold Bval. rewrite <- H24. rewrite !Typ.cast_refl. intros. specialize (Atom.Bval_inj2 t_i t0 (@diff _ _ (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) _ _ (Typ.dec_interp t_i v_typec2') _ (Typ.comp_interp t_i v_typec2') (Typ.inh_interp t_i t0) _ v_valf1 v_valf2) (v_vald2')). - intros. specialize (H29 Htid2'). + intros. specialize (H28 Htid2'). (* semantics *) @@ -1278,8 +1274,8 @@ Section certif. (interp_compdec_aux te))) | Typ.Tindex i => @existT Type (fun ty : Type => CompDec ty) - (te_carrier (@get typ_compdec t_i i)) - (te_compdec (@get typ_compdec t_i i)) + (te_carrier (@get typ_compdec t_i (of_Z (Z.of_N i)))) + (te_compdec (@get typ_compdec t_i (of_Z (Z.of_N i)))) | Typ.TZ => @existT Type (fun ty : Type => CompDec ty) BinNums.Z SMT_classes_instances.Z_compdec @@ -1339,8 +1335,8 @@ Section certif. (interp_compdec_aux te))) | Typ.Tindex i => @existT Type (fun ty : Type => CompDec ty) - (te_carrier (@get typ_compdec t_i i)) - (te_compdec (@get typ_compdec t_i i)) + (te_carrier (@get typ_compdec t_i (of_Z (Z.of_N i)))) + (te_compdec (@get typ_compdec t_i (of_Z (Z.of_N i)))) | Typ.TZ => @existT Type (fun ty : Type => CompDec ty) BinNums.Z SMT_classes_instances.Z_compdec @@ -1358,18 +1354,18 @@ Section certif. (Typ.ord_interp t_i v_typec1') (Typ.comp_interp t_i v_typec1') (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 v_valf2)). - intros. specialize (H5 Htid2'''). - rewrite <- H5. + intros. specialize (H4 Htid2'''). + rewrite <- H4. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)). intros. - unfold Atom.interp_form_hatom, interp_hatom in H0. - rewrite !Atom.t_interp_wf in H0; trivial. - rewrite Heq7 in H0. simpl in H0. - rewrite !Atom.t_interp_wf in H0; trivial. - rewrite Htib1, Htib2 in H0. simpl in H0. - rewrite !Typ.cast_refl in H0. simpl in H0. - apply Typ.i_eqb_spec_false in H0. + unfold Atom.interp_form_hatom, interp_hatom in H. + rewrite !Atom.t_interp_wf in H; trivial. + rewrite Heq7 in H. simpl in H. + rewrite !Atom.t_interp_wf in H; trivial. + rewrite Htib1, Htib2 in H. simpl in H. + rewrite !Typ.cast_refl in H. simpl in H. + apply Typ.i_eqb_spec_false in H. destruct Heq1314 as [Heq1314 | Heq1314]; @@ -1403,7 +1399,7 @@ Section certif. rewrite (Atom.Bval_inj2 t_i _ _ _ Htid2) in *. apply select_at_diff. - red in H0. red. intro. apply H0. auto. + red in H. red. intro. apply H. auto. Qed. End Correct. diff --git a/src/array/FArray.v b/src/array/FArray.v index 26617b8..69e56f9 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -44,7 +44,7 @@ Module Raw. Lemma eqb_elt_eq x y : eqb_elt x y = true <-> x = y. Proof. unfold eqb_elt. case (eq_dec x y); split; easy. Qed. - Hint Immediate eqb_key_eq eqb_elt_eq. + Hint Immediate eqb_key_eq eqb_elt_eq : smtcoq_array. Definition farray := list (key * elt). @@ -54,8 +54,8 @@ Module Raw. Definition ltk (a b : (key * elt)) := lt (fst a) (fst b). - Hint Unfold ltk eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold ltk eqk eqke : smtcoq_array. + Hint Extern 2 (eqke ?a ?b) => split : smtcoq_array. Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop). Proof. apply StrictOrder_OrdType. Qed. @@ -90,7 +90,7 @@ Module Raw. Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l. + Hint Immediate ltk_right_r ltk_right_l : smtcoq_array. Notation Sort := (sort ltk). Notation Inf := (lelistA (ltk)). @@ -100,7 +100,7 @@ Module Raw. Notation NoDupA := (NoDupA eqk). - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : smtcoq_array. Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. Proof. @@ -110,13 +110,13 @@ Module Raw. (* eqk, eqke are equalities *) Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. @@ -133,35 +133,35 @@ Module Raw. Proof. unfold ltk; eauto. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed. + Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. - apply lt_not_eq in H. auto. + apply lt_not_eq in H. auto with smtcoq_array. Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : smtcoq_array. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : smtcoq_array. + Hint Immediate eqk_sym eqke_sym : smtcoq_array. Global Instance eqk_equiv : Equivalence eqk. - Proof. split; eauto. Qed. + Proof. split; eauto with smtcoq_array. Qed. Global Instance eqke_equiv : Equivalence eqke. - Proof. split; eauto. Qed. + Proof. split; eauto with smtcoq_array. Qed. Global Instance ltk_strorder : StrictOrder ltk. Proof. split. unfold Irreflexive, Reflexive, complement. - intros. apply lt_not_eq in H; auto. + intros. apply lt_not_eq in H; auto with smtcoq_array. unfold Transitive. intros x y z. apply lt_trans. Qed. Global Instance eq_equiv : @Equivalence (key * elt) eq. Proof. - split; auto. + split; auto with smtcoq_array. unfold Transitive. apply eq_trans. Qed. @@ -173,13 +173,13 @@ Module Raw. Global Instance ltk_compatk : Proper (eqk==>eqk==>iff) ltk. Proof. intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute. - compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array. Qed. Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk. Proof. intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute. - compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array. Qed. Global Instance ltk_asym : Asymmetric ltk. @@ -194,8 +194,8 @@ Module Raw. destruct x, x'. simpl in *. intro. symmetry in H. - apply lt_not_eq in H. auto. - subst. auto. + apply lt_not_eq in H. auto with smtcoq_array. + subst. auto with smtcoq_array. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. @@ -208,8 +208,8 @@ Module Raw. intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; intros; subst; trivial. Qed. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. + Hint Resolve eqk_not_ltk : smtcoq_array. + Hint Immediate ltk_eqk eqk_ltk : smtcoq_array. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. @@ -217,17 +217,17 @@ Module Raw. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : smtcoq_array. Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. firstorder. - exists x; auto. + exists x; auto with smtcoq_array. induction H. destruct y. - exists e; auto. + exists e; auto with smtcoq_array. destruct IHInA as [e H0]. - exists e; auto. + exists e; auto with smtcoq_array. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. @@ -237,7 +237,7 @@ Module Raw. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. Proof. - destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto with smtcoq_array. Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. @@ -246,8 +246,8 @@ Module Raw. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : smtcoq_array. + Hint Resolve Inf_lt : smtcoq_array. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -261,11 +261,11 @@ Module Raw. intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. + eapply Sort_Inf_In; eauto with smtcoq_array. + red; simpl; auto with smtcoq_array. Qed. - Hint Resolve Sort_Inf_NotIn. + Hint Resolve Sort_Inf_NotIn : smtcoq_array. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA l. Proof. @@ -274,14 +274,14 @@ Module Raw. Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. Proof. - inversion 1; intros; eapply Sort_Inf_In; eauto. + inversion 1; intros; eapply Sort_Inf_In; eauto with smtcoq_array. Qed. Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto. - left; apply Sort_In_cons_1 with l; auto. + inversion_clear 2; auto with smtcoq_array. + left; apply Sort_In_cons_1 with l; auto with smtcoq_array. Qed. Lemma Sort_In_cons_3 : @@ -294,7 +294,7 @@ Module Raw. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. - inversion_clear H0; eauto. + inversion_clear H0; eauto with smtcoq_array. destruct H1; simpl in *; intuition. Qed. @@ -310,7 +310,7 @@ Module Raw. inversion_clear 1; compute in H0; intuition. Qed. - Hint Resolve In_inv_2 In_inv_3. + Hint Resolve In_inv_2 In_inv_3 : smtcoq_array. (** * FMAPLIST interface implementaion *) @@ -327,11 +327,11 @@ Module Raw. intro abs. inversion abs. Qed. - Hint Resolve empty_1. + Hint Resolve empty_1 : smtcoq_array. Lemma empty_sorted : Sort empty. Proof. - unfold empty; auto. + unfold empty; auto with smtcoq_array. Qed. Lemma MapsTo_inj : forall x e e' l (Hl:Sort l), @@ -363,7 +363,7 @@ Module Raw. + unfold eqk in H, H0. simpl in *. subst. inversion_clear HH. inversion_clear HH0. - unfold eqke in *. simpl in *. destruct H, H1; subst; auto. + unfold eqke in *. simpl in *. destruct H, H1; subst; auto with smtcoq_array. apply InA_eqke_eqk in H1. inversion_clear Hl. specialize (Sort_Inf_In H2 H3 H1). @@ -382,15 +382,15 @@ Module Raw. Proof. unfold Empty, MapsTo. intros m. - case m;auto. + case m;auto with smtcoq_array. intros (k,e) l inlist. - absurd (InA eqke (k, e) ((k, e) :: l));auto. + absurd (InA eqke (k, e) ((k, e) :: l));auto with smtcoq_array. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. Proof. intros m. - case m;auto. + case m;auto with smtcoq_array. intros p l abs. inversion abs. Qed. @@ -416,15 +416,15 @@ Module Raw. - simpl. case_eq (compare x k'); trivial. + intros _x0 e0. absurd (In x ((k', _x) :: l));try assumption. - apply Sort_Inf_NotIn with _x;auto. + apply Sort_Inf_NotIn with _x;auto with smtcoq_array. + intros _x0 e0. apply IHb. - elim (sort_inv sorted);auto. - elim (In_inv belong1);auto. + elim (sort_inv sorted);auto with smtcoq_array. + elim (In_inv belong1);auto with smtcoq_array. intro abs. - absurd (eq x k'); auto. + absurd (eq x k'); auto with smtcoq_array. symmetry in abs. - apply lt_not_eq in abs; auto. + apply lt_not_eq in abs; auto with smtcoq_array. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. @@ -432,10 +432,10 @@ Module Raw. intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo. induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail). revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail). - - exists _x; auto. - - induction IHb; auto. - + exists x0; auto. - + inversion_clear sorted; auto. + - exists _x; auto with smtcoq_array. + - induction IHb; auto with smtcoq_array. + + exists x0; auto with smtcoq_array. + + inversion_clear sorted; auto with smtcoq_array. Qed. Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m. @@ -461,8 +461,8 @@ Module Raw. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold MapsTo. - induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto). - case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto. + induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto with smtcoq_array). + case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto with smtcoq_array. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. @@ -473,11 +473,11 @@ Module Raw. - case_eq (compare x k'); intros _x0 e1; subst. + inversion_clear 2. * clear e1;compute in H0; destruct H0. - apply lt_not_eq in H; auto. now contradict H. + apply lt_not_eq in H; auto with smtcoq_array. now contradict H. * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. (* order. *) intros. - apply (lt_trans k') in _x0; auto. + apply (lt_trans k') in _x0; auto with smtcoq_array. apply lt_not_eq in _x0. now contradict _x0. + clear e1;inversion_clear 2. @@ -486,7 +486,7 @@ Module Raw. (* order. *) intros. apply lt_not_eq in H. now contradict H. - + clear e1; do 2 inversion_clear 1; auto. + + clear e1; do 2 inversion_clear 1; auto with smtcoq_array. compute in H2; destruct H2. (* order. *) subst. apply lt_not_eq in _x0. now contradict _x0. @@ -509,7 +509,7 @@ Module Raw. Proof. intros m x y e; generalize y; clear y. unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto with smtcoq_array. Qed. Lemma add_2 : forall m x y e e', @@ -517,14 +517,14 @@ Module Raw. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto; clear e0. - subst;auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto with smtcoq_array; clear e0. + subst;auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. (* order. *) subst. now contradict eqky'. - auto. - auto. + auto with smtcoq_array. + auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; intuition. Qed. @@ -533,10 +533,10 @@ Module Raw. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];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 H0; auto. + apply (In_inv_3 H0); compute; auto with smtcoq_array. + apply (In_inv_3 H0); compute; auto with smtcoq_array. + constructor 2; apply (In_inv_3 H0); compute; auto with smtcoq_array. + inversion_clear H0; auto with smtcoq_array. Qed. Lemma add_Inf : forall (m:farray)(x x':key)(e e':elt), @@ -550,7 +550,7 @@ Module Raw. compute in H0,H1. simpl; case (compare x x''); intuition. Qed. - Hint Resolve add_Inf. + Hint Resolve add_Inf : smtcoq_array. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). Proof. @@ -558,9 +558,9 @@ Module Raw. simpl; intuition. intros. destruct a as (x',e'). - simpl; case (compare x x'); intuition; inversion_clear Hm; auto. - constructor; auto. - apply Inf_eq with (x',e'); auto. + simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array. + constructor; auto with smtcoq_array. + apply Inf_eq with (x',e'); auto with smtcoq_array. Qed. (** * [remove] *) @@ -583,18 +583,18 @@ Module Raw. red; inversion 1; inversion H0. - apply Sort_Inf_NotIn with x0; auto. + apply Sort_Inf_NotIn with x0; auto with smtcoq_array. clear e0. inversion Hm. subst. - apply Sort_Inf_NotIn with x0; auto. + apply Sort_Inf_NotIn with x0; auto with smtcoq_array. clear e0;inversion_clear Hm. - assert (notin:~ In y (remove y l)) by auto. + assert (notin:~ In y (remove y l)) by auto with smtcoq_array. intros (x1,abs). inversion_clear abs. compute in H1; destruct H1. subst. apply lt_not_eq in _x; now contradict _x. - apply notin; exists x1; auto. + apply notin; exists x1; auto with smtcoq_array. Qed. @@ -602,41 +602,41 @@ Module Raw. ~ 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 MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. - inversion_clear 3; auto. + inversion_clear 3; auto with smtcoq_array. compute in H1; destruct H1. subst; now contradict H. - inversion_clear 1; inversion_clear 2; auto. + inversion_clear 1; inversion_clear 2; auto with smtcoq_array. Qed. 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 MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto. - inversion_clear 1; inversion_clear 1; auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array. + inversion_clear 1; inversion_clear 1; auto with smtcoq_array. Qed. Lemma remove_4_aux : forall m (Hm:Sort m) x y, ~ eq x y -> In y m -> In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto; + induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. rewrite In_alt. - inversion_clear 3; auto. + inversion_clear 3; auto with smtcoq_array. inversion H2. unfold eqk in H3. simpl in H3. subst. now contradict H0. apply In_alt. - exists x. auto. + exists x. auto with smtcoq_array. apply lt_not_eq in _x. intros. inversion_clear Hm. @@ -647,27 +647,27 @@ Module Raw. destruct (eq_dec k' y). exists x0. apply InA_cons_hd. - split; simpl; auto. + split; simpl; auto with smtcoq_array. inversion H3. unfold eqk in H4. simpl in H4; subst. now contradict n. assert ((exists e : elt, MapsTo y e (remove x l)) -> (exists e : elt, MapsTo y e ((k', x0) :: remove x l))). intros. destruct H6. exists x2. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. apply H6. - apply IHf; auto. + apply IHf; auto with smtcoq_array. apply In_alt. - exists x1. auto. + exists x1. auto with smtcoq_array. Qed. Lemma remove_4 : forall m (Hm:Sort m) x y, ~ eq x y -> In y m <-> In y (remove x m). Proof. split. - apply remove_4_aux; auto. + apply remove_4_aux; auto with smtcoq_array. revert H. generalize Hm; clear Hm. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac @@ -675,18 +675,18 @@ Module Raw. intros. destruct H0 as (e, H0). exists e. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. intros. apply lt_not_eq in _x0. inversion_clear Hm. apply In_inv in H0. destruct H0. exists _x. - apply InA_cons_hd. split; simpl; auto. + apply InA_cons_hd. split; simpl; auto with smtcoq_array. specialize (IHb H1 H H0). inversion IHb. exists x0. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. Qed. Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt), @@ -700,9 +700,9 @@ Module Raw. compute in H0. simpl; case (compare x x''); intuition. inversion_clear Hm. - apply Inf_lt with (x'',e''); auto. + apply Inf_lt with (x'',e''); auto with smtcoq_array. Qed. - Hint Resolve remove_Inf. + Hint Resolve remove_Inf : smtcoq_array. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). Proof. @@ -710,7 +710,7 @@ Module Raw. simpl; intuition. intros. destruct a as (x',e'). - simpl; case (compare x x'); intuition; inversion_clear Hm; auto. + simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array. Qed. (** * [elements] *) @@ -720,25 +720,25 @@ Module Raw. Lemma elements_1 : forall m x e, MapsTo x e m -> InA eqke (x,e) (elements m). Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_2 : forall m x e, InA eqke (x,e) (elements m) -> MapsTo x e m. Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_3 : forall m (Hm:Sort m), sort ltk (elements m). Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m). Proof. intros. apply Sort_NoDupA. - apply elements_3; auto. + apply elements_3; auto with smtcoq_array. Qed. (** * [fold] *) @@ -752,7 +752,7 @@ Module Raw. Lemma fold_1 : forall m (A:Type)(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; revert i; induction m as [ |[k e]]; simpl; auto. + intros; revert i; induction m as [ |[k e]]; simpl; auto with smtcoq_array. Qed. (** * [equal] *) @@ -776,7 +776,7 @@ Module Raw. Equivb cmp m m' -> equal cmp m m' = true. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto; unfold Equivb; intuition; subst. + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto with smtcoq_array; unfold Equivb; intuition; subst. - destruct (H0 x') as [_ H3]. assert (H2: In x' nil). { @@ -789,53 +789,53 @@ Module Raw. apply H3. exists e. now constructor. } elim H2. intros x0 Hx0. inversion Hx0. - - case_eq (compare x x'); simpl; subst;auto; unfold Equivb; + - case_eq (compare x x'); simpl; subst;auto with smtcoq_array; unfold Equivb; intuition; subst. + destruct (H0 x). assert (In x ((x',e')::l')). - apply H2; auto. - exists e; auto. + apply H2; auto with smtcoq_array. + exists e; auto with smtcoq_array. destruct (In_inv H4). (* order. *) clear H. apply lt_not_eq in l0; now contradict l0. inversion_clear Hm'. assert (Inf (x,e) l'). - apply Inf_lt with (x',e'); auto. + apply Inf_lt with (x',e'); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). + match goal with H: compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). - apply H1 with x'; auto. + apply H1 with x'; auto with smtcoq_array. rewrite cmp_e_e'; simpl. - apply IHl; auto. - inversion_clear Hm; auto. - inversion_clear Hm'; auto. + apply IHl; auto with smtcoq_array. + inversion_clear Hm; auto with smtcoq_array. + inversion_clear Hm'; auto with smtcoq_array. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x',e) ::l)). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H2 H4)); auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + destruct (In_inv (H2 H4)); auto with smtcoq_array. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). - destruct H as (e'', hyp); exists e''; auto. - apply MapsTo_eq with k; auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + apply MapsTo_eq with k; auto with smtcoq_array. destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H3 H4)); auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + destruct (In_inv (H3 H4)); auto with smtcoq_array. subst. inversion_clear Hm'. now elim (Sort_Inf_NotIn H5 H6). - apply H1 with k; destruct (eq_dec x' k); auto. + apply H1 with k; destruct (eq_dec x' k); auto with smtcoq_array. + destruct (H0 x'). assert (In x' ((x,e)::l)). - apply H3; auto. - exists e'; auto. + apply H3; auto with smtcoq_array. + exists e'; auto with smtcoq_array. destruct (In_inv H4). (* order. *) clear H; subst; apply lt_not_eq in l0; now contradict l0. inversion_clear Hm. assert (Inf (x',e') l). - apply Inf_lt with (x,e); auto. + apply Inf_lt with (x,e); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). Qed. @@ -843,7 +843,7 @@ Module Raw. equal cmp m m' = true -> Equivb cmp m m'. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto; unfold Equivb; + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto with smtcoq_array; unfold Equivb; intuition; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. - inversion H0. @@ -852,19 +852,19 @@ Module Raw. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). - exists e'; constructor; split; trivial; apply eq_trans with x; auto. + exists e'; constructor; split; trivial; apply eq_trans with x; auto with smtcoq_array. destruct (H k). destruct (H10 H9) as (e'',hyp). - exists e''; auto. + exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). - exists e; constructor; split; trivial; apply eq_trans with x'; auto. + exists e; constructor; split; trivial; apply eq_trans with x'; auto with smtcoq_array. destruct (H k). destruct (H11 H9) as (e'',hyp). - exists e''; auto. + exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H]. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. @@ -872,16 +872,16 @@ Module Raw. inversion_clear H0. + destruct H9; simpl in *; subst. inversion_clear H1. - * destruct H0; simpl in *; subst; auto. + * destruct H0; simpl in *; subst; auto with smtcoq_array. * elim (Sort_Inf_NotIn H4 H5). - exists e'0; apply MapsTo_eq with x'; auto. + exists e'0; apply MapsTo_eq with x'; auto with smtcoq_array. (* order. *) + inversion_clear H1. - * destruct H0; simpl in *; subst; auto. + * destruct H0; simpl in *; subst; auto with smtcoq_array. elim (Sort_Inf_NotIn H2 H3). - exists e0; apply MapsTo_eq with x'; auto. + exists e0; apply MapsTo_eq with x'; auto with smtcoq_array. (* order. *) - * apply H8 with k; auto. + * apply H8 with k; auto with smtcoq_array. Qed. (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *) @@ -895,18 +895,18 @@ Module Raw. inversion H0; subst. destruct x; destruct y; compute in H1, H2. split; intros. - apply equal_2; auto. + apply equal_2; auto with smtcoq_array. simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl. - apply equal_1; auto. - apply equal_2; auto. + apply equal_1; auto with smtcoq_array. + apply equal_2; auto with smtcoq_array. generalize (equal_1 H H0 H3). simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). - rewrite H2; simpl; auto. + rewrite H2; simpl; auto with smtcoq_array. Qed. End Array. @@ -1492,7 +1492,7 @@ Section FArray. intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. apply add_neq_mapsto_iff; auto. Qed. - Hint Resolve add_neq_o. + Hint Resolve add_neq_o : smtcoq_array. Lemma MapsTo_fun : forall m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. @@ -1854,6 +1854,8 @@ Arguments extensionality2 {_} {_} {_} {_} {_} {_} {_} {_} {_} _. Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. +Declare Scope farray_scope. + Notation "a '[' i ']'" := (select a i) (at level 1, format "a [ i ]") : farray_scope. Notation "a '[' i '<-' v ']'" := (store a i v) (at level 1, format "a [ i <- v ]") : farray_scope. |