diff options
Diffstat (limited to 'src/SMT_terms.v')
-rw-r--r-- | src/SMT_terms.v | 194 |
1 files changed, 102 insertions, 92 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index f88c0c4..f536bd6 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool Int63 PArray BinNat BinPos ZArith SMT_classes_instances. +Require Import Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances. Require Import Misc State BVList. (* FArray Equalities DecidableTypeEx. *) Require FArray. Require List . @@ -79,10 +79,10 @@ Module Form. | Fatom a => interp_atom a | Ftrue => true | Ffalse => false - | Fnot2 i l => fold (fun b => negb (negb b)) 1 i (Lit.interp interp_var l) - | Fand args => afold_left _ _ true andb (Lit.interp interp_var) args - | For args => afold_left _ _ false orb (Lit.interp interp_var) args - | Fimp args => afold_right _ _ true implb (Lit.interp interp_var) args + | Fnot2 i l => foldi (fun _ b => negb (negb b)) 0 i (Lit.interp interp_var l) + | Fand args => afold_left _ true andb (amap (Lit.interp interp_var) args) + | For args => afold_left _ false orb (amap (Lit.interp interp_var) args) + | Fimp args => afold_right _ true implb (amap (Lit.interp interp_var) args) | Fxor a b => xorb (Lit.interp interp_var a) (Lit.interp interp_var b) | Fiff a b => Bool.eqb (Lit.interp interp_var a) (Lit.interp interp_var b) | Fite a b c => @@ -98,19 +98,19 @@ Module Form. Section Interp_get. - Variable t_form : PArray.array form. + Variable t_form : array form. - Definition t_interp : PArray.array bool := - PArray.foldi_left (fun i t_b hf => - t_b.[i <- interp_aux (PArray.get t_b) hf]) - (PArray.make (PArray.length t_form) true) t_form. + Definition t_interp : array bool := + foldi (fun i t_b => + t_b.[i <- interp_aux (get t_b) (t_form.[i])]) 0 (length t_form) + (make (length t_form) true). Definition lt_form i h := match h with | Fatom _ | Ftrue | Ffalse => true | Fnot2 _ l => Lit.blit l < i | Fand args | For args | Fimp args => - PArray.forallb (fun l => Lit.blit l < i) args + aforallbi (fun _ l => Lit.blit l < i) args | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i) | Fite a b c => (Lit.blit a < i) && (Lit.blit b < i) && (Lit.blit c < i) | FbbT _ ls => List.forallb (fun l => Lit.blit l < i) ls @@ -123,41 +123,42 @@ Module Form. interp_aux f1 h = interp_aux f2 h. Proof. destruct h;simpl;intros;trivial; - try (apply afold_left_eq;unfold is_true in H0; - rewrite PArray.forallb_spec in H0;intros; + try (try apply afold_left_eq; try apply afold_right_eq;unfold is_true in H0; + rewrite ?forallb_spec, ?aforallbi_spec, ?andb_true_iff in H0;intros; + rewrite ?length_amap; try rewrite length_amap in H1; + rewrite ?get_amap by assumption; auto using Lit.interp_eq_compat with smtcoq_core). - f_equal;auto using Lit.interp_eq_compat. - - apply afold_right_eq;unfold is_true in H0; - rewrite PArray.forallb_spec in H0;intros; - auto using Lit.interp_eq_compat with smtcoq_core. - - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. - - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. - - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. + - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. + - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. + - decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. - replace (List.map (Lit.interp f2) l) with (List.map (Lit.interp f1) l); auto. unfold is_true in H0. rewrite List.forallb_forall in H0. - apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto with smtcoq_core. + apply List.map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto with smtcoq_core. Qed. - Definition wf := PArray.forallbi lt_form t_form. + Definition wf := aforallbi lt_form t_form. Hypothesis wf_t_i : wf. Lemma length_t_interp : length t_interp = length t_form. Proof. - unfold t_interp;apply PArray.foldi_left_Ind with (P := fun i a => length a = length t_form). + unfold t_interp. + assert (Bt := to_Z_bounded (length t_form)). + apply (foldi_ind _ (fun i a => length a = length t_form)). + rewrite leb_spec, to_Z_0; lia. + rewrite length_make, leb_length; reflexivity. intros;rewrite length_set;trivial. - rewrite length_make, ltb_length;trivial. Qed. Lemma default_t_interp : default t_interp = true. Proof. - unfold t_interp;apply PArray.foldi_left_Ind with - (P := fun i a => default a = true). - intros;rewrite default_set;trivial. + unfold t_interp. + assert (Bt := to_Z_bounded (length t_form)). + apply (foldi_ind _ (fun i a => default a = true)). + rewrite leb_spec, to_Z_0; lia. apply default_make. + intros;rewrite default_set;trivial. Qed. Lemma t_interp_wf : forall i, i < PArray.length t_form -> @@ -167,26 +168,27 @@ Module Form. forall j, j < i -> t.[j] = interp_aux (PArray.get t) (t_form.[j])). assert (P' (length t_form) t_interp). - unfold is_true, wf in wf_t_i;rewrite PArray.forallbi_spec in wf_t_i. - unfold t_interp;apply foldi_left_Ind;unfold P';intros. - rewrite length_set in H1. - destruct (Int63Properties.reflect_eqb j i). - rewrite e, PArray.get_set_same. - apply lt_form_interp_form_aux with (2:= wf_t_i i H). + unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i. + unfold t_interp;apply foldi_ind;unfold P';intros. + apply leb_0. + elim (ltb_0 _ H0). + rewrite length_set in H2. + destruct (reflect_eqb j i). + rewrite e, get_set_same. + apply lt_form_interp_form_aux with (2:= wf_t_i i H0). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. - rewrite H1;trivial. + rewrite H2;trivial. assert (j < i). assert ([|j|] <> [|i|]) by (intros Heq1;elim n;apply to_Z_inj;trivial). - generalize H2;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H); + generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0); auto with zarith. - rewrite get_set_other, H0;auto. + rewrite get_set_other, H1;auto. apply lt_form_interp_form_aux with - (2:= wf_t_i j (ltb_trans _ _ _ H3 H)). + (2:= wf_t_i j (ltb_trans _ _ _ H4 H0)). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);apply ltb_trans with j; [ rewrite Heq| ];trivial. - elim (ltb_0 _ H0). apply H;apply length_t_interp. Qed. @@ -252,7 +254,7 @@ Module Typ. Import FArray. - Notation index := int (only parsing). + Notation index := N (only parsing). Inductive type := | TFArray : type -> type -> type @@ -283,7 +285,7 @@ Module Typ. (type_compdec (projT2 (interp_compdec_aux te)))) | Tindex i => existT (fun ty : Type => CompDec ty) - (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i])) + (te_carrier (t_i .[of_Z (Z.of_N i)])) (te_compdec (t_i .[of_Z (Z.of_N i)])) | TZ => existT (fun ty : Type => CompDec ty) Z Z_compdec | Tbool => existT (fun ty : Type => CompDec ty) bool bool_compdec | Tpositive => existT (fun ty : Type => CompDec ty) positive Positive_compdec @@ -379,7 +381,7 @@ Module Typ. reflect (x = y) (eqb_of_compdec c x y). Proof. intros x y. - apply reflect_eqb. + apply SMT_classes.reflect_eqb. Qed. @@ -396,7 +398,7 @@ Module Typ. Definition i_eqb_eqb (t:type) : interp t -> interp t -> bool := match t with - | Tindex i => eqb_of_compdec (t_i.[i]).(te_compdec) + | Tindex i => eqb_of_compdec (t_i.[of_Z (Z.of_N i)]).(te_compdec) | TZ => Z.eqb (* Zeq_bool *) | Tbool => Bool.eqb | Tpositive => Pos.eqb @@ -505,7 +507,7 @@ Module Typ. Fixpoint cast (A B: type) : cast_result A B := match A as C, B as D return cast_result C D with | Tindex i, Tindex j => - match Int63Op.cast i j with + match N_cast i j with | Some k => Cast (fun P => k (fun y => P (Tindex y))) | None => NoCast end @@ -543,7 +545,7 @@ Module Typ. Proof. destruct A;simpl;trivial. do 2 rewrite cast_refl. easy. - rewrite Int63Properties.cast_refl;trivial. + rewrite N_cast_refl;trivial. rewrite N_cast_refl;trivial. Qed. @@ -551,7 +553,7 @@ Module Typ. (* Remark : I use this definition because eqb will not be used only in the interpretation *) Fixpoint eqb (A B: type) : bool := match A, B with - | Tindex i, Tindex j => i == j + | Tindex i, Tindex j => N.eqb i j | TZ, TZ => true | Tbool, Tbool => true | Tpositive, Tpositive => true @@ -599,7 +601,7 @@ Module Typ. rewrite andb_false_iff in H. destruct H; apply cast_diff in H; rewrite H; auto. case (cast A1 B1); auto. - intros H. rewrite (Int63Properties.cast_diff _ _ H);trivial. + rewrite N.eqb_neq. intro Heq. now rewrite N_cast_diff. rewrite N.eqb_neq. intro Heq. now rewrite N_cast_diff. Qed. @@ -634,7 +636,7 @@ Module Typ. apply (reflect_iff _ _ (reflect_eqb x1 y1)) in H. apply (reflect_iff _ _ (reflect_eqb x2 y2)) in H0. subst; auto. - apply iff_reflect;rewrite Int63Properties.eqb_spec;split;intros H;[inversion H | subst]; trivial. + apply iff_reflect. rewrite N.eqb_eq. split;intros H;[inversion H | subst]; trivial. apply iff_reflect. rewrite N.eqb_eq. split;intros H;[inversion H | subst]; trivial. Qed. @@ -804,7 +806,7 @@ Module Atom. | UO_Zpos, UO_Zpos | UO_Zneg, UO_Zneg | UO_Zopp, UO_Zopp => true - | UO_BVbitOf s1 n, UO_BVbitOf s2 m => Nat_eqb n m && N.eqb s1 s2 + | UO_BVbitOf s1 n, UO_BVbitOf s2 m => Nat.eqb n m && N.eqb s1 s2 | UO_BVnot s1, UO_BVnot s2 => N.eqb s1 s2 | UO_BVneg s1, UO_BVneg s2 => N.eqb s1 s2 | UO_BVextr i0 n00 n01, UO_BVextr i1 n10 n11 => N.eqb i0 i1 && N.eqb n00 n10 && N.eqb n01 n11 @@ -853,10 +855,10 @@ Module Atom. | Acop o, Acop o' => cop_eqb o o' | Auop o t, Auop o' t' => uop_eqb o o' && (t == t') | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 == t1') && (t2 == t2') - | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63Native.eqb t t' + | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63.eqb t t' | Atop o t1 t2 t3, Atop o' t1' t2' t3' => top_eqb o o' && (t1 == t1') && (t2 == t2') && (t3 == t3') - | Aapp a la, Aapp b lb => (a == b) && list_beq Int63Native.eqb la lb + | Aapp a la, Aapp b lb => (a == b) && list_beq Int63.eqb la lb | _, _ => false end. @@ -880,7 +882,7 @@ Module Atom. Lemma reflect_uop_eqb : forall o1 o2, reflect (o1 = o2) (uop_eqb o1 o2). Proof. intros [ | | | | | s1 n1 | s1 | s1 | s1 | s1 | s1 ] [ | | | | |s2 n2 | s2 | s2 | s2 | s2 | s2 ];simpl; try constructor;trivial; try discriminate. - - apply iff_reflect. case_eq (Nat_eqb n1 n2). + - apply iff_reflect. case_eq (Nat.eqb n1 n2). + case_eq ((s1 =? s2)%N). * rewrite N.eqb_eq, beq_nat_true_iff. intros -> ->. split; reflexivity. @@ -982,26 +984,26 @@ Qed. (* Constants *) preflect (reflect_cop_eqb c c0);constructor;subst;trivial. (* Unary operators *) - preflect (reflect_uop_eqb u u0); preflect (Int63Properties.reflect_eqb i i0); + preflect (reflect_uop_eqb u u0); preflect (Misc.reflect_eqb i i0); constructor;subst;trivial. (* Binary operators *) preflect (reflect_bop_eqb b b0); - preflect (Int63Properties.reflect_eqb i i1); - preflect (Int63Properties.reflect_eqb i0 i2); + preflect (Misc.reflect_eqb i i1); + preflect (Misc.reflect_eqb i0 i2); constructor;subst;trivial. (* Ternary operators *) preflect (reflect_top_eqb t t0). - preflect (Int63Properties.reflect_eqb i i2). - preflect (Int63Properties.reflect_eqb i0 i3). - preflect (Int63Properties.reflect_eqb i1 i4). + preflect (Misc.reflect_eqb i i2). + preflect (Misc.reflect_eqb i0 i3). + preflect (Misc.reflect_eqb i1 i4). constructor;subst;trivial. (* N-ary operators *) preflect (reflect_nop_eqb n n0); - preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); + preflect (reflect_list_beq _ _ Misc.reflect_eqb l l0); constructor; subst; reflexivity. (* Application *) - preflect (Int63Properties.reflect_eqb i i0); - preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); + preflect (Misc.reflect_eqb i i0); + preflect (reflect_list_beq _ _ Misc.reflect_eqb l l0); constructor;subst;trivial. Qed. @@ -2228,9 +2230,9 @@ Qed. Variable t_atom : PArray.array atom. - Definition t_interp : PArray.array bval := - PArray.foldi_left (fun i t_a a => t_a.[i <- interp_aux (PArray.get t_a) a]) - (PArray.make (PArray.length t_atom) (interp_cop CO_xH)) t_atom. + Definition t_interp : array bval := + foldi (fun i t_a => t_a.[i <- interp_aux (get t_a) (t_atom.[i])]) 0 (length t_atom) + (make (length t_atom) (interp_cop CO_xH)). Definition lt_atom i a := match a with @@ -2262,52 +2264,58 @@ Qed. unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite Hf, IHl;trivial. Qed. - Definition wf := PArray.forallbi lt_atom t_atom. + Definition wf := aforallbi lt_atom t_atom. Hypothesis wf_t_i : wf. Lemma length_t_interp : length t_interp = length t_atom. Proof. - unfold t_interp;apply PArray.foldi_left_Ind with - (P := fun i a => length a = length t_atom). + unfold t_interp. + assert (Bt := to_Z_bounded (length t_atom)). + apply (foldi_ind _ (fun i a => length a = length t_atom)). + rewrite leb_spec, to_Z_0; lia. + rewrite length_make, leb_length;trivial. intros;rewrite length_set;trivial. - rewrite length_make, ltb_length;trivial. Qed. Lemma default_t_interp : default t_interp = interp_cop CO_xH. Proof. - unfold t_interp;apply PArray.foldi_left_Ind with - (P := fun i a => default a = interp_cop CO_xH). - intros;rewrite default_set;trivial. + unfold t_interp. + assert (Bt := to_Z_bounded (length t_atom)). + apply (foldi_ind _ (fun i a => default a = interp_cop CO_xH)). + rewrite leb_spec, to_Z_0; lia. apply default_make. + intros;rewrite default_set;trivial. Qed. Lemma t_interp_wf_lt : forall i, i < PArray.length t_atom -> t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]). Proof. + assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> forall j, j < i -> t.[j] = interp_aux (PArray.get t) (t_atom.[j])). assert (P' (length t_atom) t_interp). - unfold is_true, wf in wf_t_i;rewrite PArray.forallbi_spec in wf_t_i. - unfold t_interp;apply foldi_left_Ind;unfold P';intros. - rewrite length_set in H1. - destruct (Int63Properties.reflect_eqb j i). + unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i. + unfold t_interp;apply foldi_ind;unfold P';intros. + rewrite leb_spec, to_Z_0; lia. + elim (ltb_0 _ H0). + rewrite length_set in H2. + destruct (Misc.reflect_eqb j i). rewrite e, PArray.get_set_same. - apply lt_interp_aux with (2:= wf_t_i i H). + apply lt_interp_aux with (2:= wf_t_i i H0). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. - rewrite H1;trivial. + rewrite H2;trivial. assert (j < i). assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). - generalize H2;unfold is_true;rewrite !ltb_spec, - (to_Z_add_1 _ _ H);auto with zarith. - rewrite get_set_other, H0;auto. - apply lt_interp_aux with (2:= wf_t_i j (ltb_trans _ _ _ H3 H)). + generalize H3;unfold is_true;rewrite !ltb_spec, + (to_Z_add_1 _ _ H0);auto with zarith. + rewrite get_set_other, H1;auto. + apply lt_interp_aux with (2:= wf_t_i j (ltb_trans _ _ _ H4 H0)). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);apply ltb_trans with j; [ rewrite Heq| ];trivial. - elim (ltb_0 _ H0). apply H;apply length_t_interp. Qed. @@ -2366,7 +2374,7 @@ Qed. exists v, interp_aux (get a) (t_atom.[h]) = Bval (v_type _ _ (interp_aux (get a) (t_atom.[h]))) v. Proof. - unfold wf, is_true in wf_t_i; rewrite forallbi_spec in wf_t_i. + unfold wf, is_true in wf_t_i; rewrite aforallbi_spec in wf_t_i. intros h Hh a IH; generalize (wf_t_i h Hh). case (t_atom.[h]); simpl. (* Constants *) @@ -2503,22 +2511,24 @@ Qed. Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom -> exists v, t_interp.[h] = Bval (get_type h) v. Proof. + assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> forall j, j < i -> exists v, t.[j] = Bval (v_type Typ.type interp_t (t.[j])) v). assert (P' (length t_atom) t_interp). - unfold t_interp;apply foldi_left_Ind;unfold P';intros. - rewrite length_set in H1. - destruct (Int63Properties.reflect_eqb j i). + unfold t_interp;apply foldi_ind;unfold P';intros. + rewrite leb_spec, to_Z_0; lia. + elim (ltb_0 _ H0). + rewrite length_set in H2. + destruct (Misc.reflect_eqb j i). rewrite e, PArray.get_set_same. apply check_aux_interp_aux_lt; auto. - rewrite H1; auto. + rewrite H2; auto. assert (j < i). assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). - generalize H2;unfold is_true;rewrite !ltb_spec, - (to_Z_add_1 _ _ H);auto with zarith. + generalize H3;unfold is_true;rewrite !ltb_spec, + (to_Z_add_1 _ _ H0);auto with zarith. rewrite get_set_other;auto. - elim (ltb_0 _ H0). apply H;apply length_t_interp. Qed. @@ -2557,7 +2567,7 @@ Qed. Definition wt t_atom := let t_interp := t_interp t_atom in let get_type := get_type' t_interp in - PArray.forallbi (fun i h => check_aux get_type h (get_type i)) t_atom. + aforallbi (fun i h => check_aux get_type h (get_type i)) t_atom. Definition interp_hatom (t_atom : PArray.array atom) := let t_a := t_interp t_atom in |