diff options
Diffstat (limited to 'src/SMT_terms.v')
| -rw-r--r-- | src/SMT_terms.v | 373 |
1 files changed, 220 insertions, 153 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 66936cf..8c4ffa6 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) @@ -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). Fixpoint lt_form i h {struct 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 @@ -273,27 +275,31 @@ Module Typ. Fixpoint interp_compdec_aux (t:type) : {ty: Type & CompDec ty} := match t with | TFArray ti te => + let iti := interp_compdec_aux ti in + let ite := interp_compdec_aux te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in existT (fun ty : Type => CompDec ty) - (@farray (type_compdec (projT2 (interp_compdec_aux ti))) - (type_compdec (projT2 (interp_compdec_aux te))) - (@ord_of_compdec _ (projT2 (interp_compdec_aux ti))) - (@inh_of_compdec _ (projT2 (interp_compdec_aux te)))) - (FArray_compdec - (type_compdec (projT2 (interp_compdec_aux ti))) - (type_compdec (projT2 (interp_compdec_aux te)))) + (@farray tti + tte + (@ord_of_compdec tti cti) + (@inh_of_compdec tte cte)) + (FArray_compdec tti tte) | 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 | TBV n => existT (fun ty : Type => CompDec ty) (BITVECTOR_LIST.bitvector n) (BV_compdec n) end. - Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) := - projT2 (interp_compdec_aux t). + Definition interp (t:type) : Type := type_compdec (projT2 (interp_compdec_aux t)). - Definition interp (t:type) : Type := type_compdec (interp_compdec t). + Definition interp_compdec (t:type) : CompDec (interp t) := + projT2 (interp_compdec_aux t). Definition interp_ftype (t:ftype) := @@ -301,40 +307,17 @@ Module Typ. (interp (snd t)) (fst t). - Definition dec_interp (t:type) : DecType (interp t). - Proof. - unfold interp. - destruct (interp_compdec t) as [x c]. simpl. - apply EqbToDecType. - Defined. - - Instance ord_interp (t:type) : OrdType (interp t). - Proof. - unfold interp. - destruct (interp_compdec t) as [x c]. simpl. - apply Ordered. - Defined. - - Instance comp_interp (t:type) : Comparable (interp t). - Proof. - unfold interp, ord_interp. - destruct (interp_compdec t) as [x c]. simpl. - apply Comp. - Defined. - + Global Instance dec_interp (t:type) : DecType (interp t) := + (@EqbToDecType _ (@eqbtype_of_compdec (interp t) (interp_compdec t))). - Definition inh_interp (t:type) : Inhabited (interp t). - unfold interp. - destruct (interp_compdec t). - apply Inh. - Defined. + Global Instance ord_interp (t:type) : OrdType (interp t) := + @ord_of_compdec (interp t) (interp_compdec t). - Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _). + Global Instance comp_interp (t:type) : Comparable (interp t) := + @comp_of_compdec (interp t) (interp_compdec t). - - Hint Resolve - dec_interp comp_interp ord_interp - inh_interp interp_compdec : typeclass_instances. + Global Instance inh_interp (t:type) : Inhabited (interp t) := + @inh_of_compdec (interp t) (interp_compdec t). (* Boolean equality over interpretation of a btype *) @@ -379,7 +362,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 +379,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 +488,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 +526,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 +534,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 +582,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 +617,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 +787,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 +836,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 +863,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 +965,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. @@ -1523,13 +1506,25 @@ Qed. apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s) | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select | BO_diffarray ti te => - apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te)) + let iti := Typ.interp_compdec_aux t_i ti in + let ite := Typ.interp_compdec_aux t_i te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in + apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@EqbToDecType _ (@eqbtype_of_compdec tte cte)) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tti cti) (@inh_of_compdec tte cte)) end. Definition interp_top o := match o with | TO_store ti te => - apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te)) + let iti := Typ.interp_compdec_aux t_i ti in + let ite := Typ.interp_compdec_aux t_i te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in + apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tte cte)) end. Fixpoint compute_interp ty acc l := @@ -1964,9 +1959,9 @@ Qed. rewrite !Typ.cast_refl. intros. exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t'))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) + (Typ.dec_interp t_i t') + (Typ.ord_interp t_i t') + (Typ.comp_interp t_i t') (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto. (* Ternary operatores *) @@ -1988,11 +1983,7 @@ Qed. intros. rewrite !Typ.cast_refl. intros. - exists ((@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti'))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') - (Typ.inh_interp t_i te') x1 x2 x3)); auto. + exists (@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') (Typ.dec_interp t_i ti') (Typ.ord_interp t_i ti') (Typ.comp_interp t_i ti') (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') (Typ.inh_interp t_i te') x1 x2 x3); auto. (* N-ary operators *) destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). @@ -2228,9 +2219,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 +2253,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 +2363,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 *) @@ -2467,12 +2464,7 @@ Qed. simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ]; simpl; try (exists true; reflexivity). - exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _(Typ.interp_compdec t_i ti))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) - (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) - (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto. + exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (Typ.dec_interp t_i ti) (Typ.ord_interp t_i ti) (Typ.comp_interp t_i ti) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto. (* Ternary operators *) intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3]; @@ -2486,9 +2478,9 @@ Qed. case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ]; simpl; try (exists true; reflexivity). exists (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) + (Typ.dec_interp t_i ti) + (Typ.ord_interp t_i ti) + (Typ.comp_interp t_i ti) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y) (k3 (Typ.interp t_i) z)); auto. @@ -2503,22 +2495,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 +2551,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 @@ -2614,6 +2608,79 @@ End PredefinedArrays. *) +(* Register constants for OCaml access *) +Register Typ.type as SMTCoq.SMT_terms.Typ.type. +Register Typ.TFArray as SMTCoq.SMT_terms.Typ.TFArray. +Register Typ.Tindex as SMTCoq.SMT_terms.Typ.Tindex. +Register Typ.TZ as SMTCoq.SMT_terms.Typ.TZ. +Register Typ.Tbool as SMTCoq.SMT_terms.Typ.Tbool. +Register Typ.Tpositive as SMTCoq.SMT_terms.Typ.Tpositive. +Register Typ.TBV as SMTCoq.SMT_terms.Typ.TBV. +Register Typ.interp as SMTCoq.SMT_terms.Typ.interp. +Register Typ.dec_interp as SMTCoq.SMT_terms.Typ.dec_interp. +Register Typ.ord_interp as SMTCoq.SMT_terms.Typ.ord_interp. +Register Typ.comp_interp as SMTCoq.SMT_terms.Typ.comp_interp. +Register Typ.inh_interp as SMTCoq.SMT_terms.Typ.inh_interp. +Register Typ.i_eqb as SMTCoq.SMT_terms.Typ.i_eqb. +Register Atom.tval as SMTCoq.SMT_terms.Atom.tval. +Register Atom.Tval as SMTCoq.SMT_terms.Atom.Tval. +Register Atom.CO_xH as SMTCoq.SMT_terms.Atom.CO_xH. +Register Atom.CO_Z0 as SMTCoq.SMT_terms.Atom.CO_Z0. +Register Atom.CO_BV as SMTCoq.SMT_terms.Atom.CO_BV. +Register Atom.UO_xO as SMTCoq.SMT_terms.Atom.UO_xO. +Register Atom.UO_xI as SMTCoq.SMT_terms.Atom.UO_xI. +Register Atom.UO_Zpos as SMTCoq.SMT_terms.Atom.UO_Zpos. +Register Atom.UO_Zneg as SMTCoq.SMT_terms.Atom.UO_Zneg. +Register Atom.UO_Zopp as SMTCoq.SMT_terms.Atom.UO_Zopp. +Register Atom.UO_BVbitOf as SMTCoq.SMT_terms.Atom.UO_BVbitOf. +Register Atom.UO_BVnot as SMTCoq.SMT_terms.Atom.UO_BVnot. +Register Atom.UO_BVneg as SMTCoq.SMT_terms.Atom.UO_BVneg. +Register Atom.UO_BVextr as SMTCoq.SMT_terms.Atom.UO_BVextr. +Register Atom.UO_BVzextn as SMTCoq.SMT_terms.Atom.UO_BVzextn. +Register Atom.UO_BVsextn as SMTCoq.SMT_terms.Atom.UO_BVsextn. +Register Atom.BO_Zplus as SMTCoq.SMT_terms.Atom.BO_Zplus. +Register Atom.BO_Zminus as SMTCoq.SMT_terms.Atom.BO_Zminus. +Register Atom.BO_Zmult as SMTCoq.SMT_terms.Atom.BO_Zmult. +Register Atom.BO_Zlt as SMTCoq.SMT_terms.Atom.BO_Zlt. +Register Atom.BO_Zle as SMTCoq.SMT_terms.Atom.BO_Zle. +Register Atom.BO_Zge as SMTCoq.SMT_terms.Atom.BO_Zge. +Register Atom.BO_Zgt as SMTCoq.SMT_terms.Atom.BO_Zgt. +Register Atom.BO_eq as SMTCoq.SMT_terms.Atom.BO_eq. +Register Atom.BO_BVand as SMTCoq.SMT_terms.Atom.BO_BVand. +Register Atom.BO_BVor as SMTCoq.SMT_terms.Atom.BO_BVor. +Register Atom.BO_BVxor as SMTCoq.SMT_terms.Atom.BO_BVxor. +Register Atom.BO_BVadd as SMTCoq.SMT_terms.Atom.BO_BVadd. +Register Atom.BO_BVmult as SMTCoq.SMT_terms.Atom.BO_BVmult. +Register Atom.BO_BVult as SMTCoq.SMT_terms.Atom.BO_BVult. +Register Atom.BO_BVslt as SMTCoq.SMT_terms.Atom.BO_BVslt. +Register Atom.BO_BVconcat as SMTCoq.SMT_terms.Atom.BO_BVconcat. +Register Atom.BO_BVshl as SMTCoq.SMT_terms.Atom.BO_BVshl. +Register Atom.BO_BVshr as SMTCoq.SMT_terms.Atom.BO_BVshr. +Register Atom.BO_select as SMTCoq.SMT_terms.Atom.BO_select. +Register Atom.BO_diffarray as SMTCoq.SMT_terms.Atom.BO_diffarray. +Register Atom.TO_store as SMTCoq.SMT_terms.Atom.TO_store. +Register Atom.NO_distinct as SMTCoq.SMT_terms.Atom.NO_distinct. +Register Atom.atom as SMTCoq.SMT_terms.Atom.atom. +Register Atom.Acop as SMTCoq.SMT_terms.Atom.Acop. +Register Atom.Auop as SMTCoq.SMT_terms.Atom.Auop. +Register Atom.Abop as SMTCoq.SMT_terms.Atom.Abop. +Register Atom.Atop as SMTCoq.SMT_terms.Atom.Atop. +Register Atom.Anop as SMTCoq.SMT_terms.Atom.Anop. +Register Atom.Aapp as SMTCoq.SMT_terms.Atom.Aapp. +Register Form.form as SMTCoq.SMT_terms.Form.form. +Register Form.Fatom as SMTCoq.SMT_terms.Form.Fatom. +Register Form.Ftrue as SMTCoq.SMT_terms.Form.Ftrue. +Register Form.Ffalse as SMTCoq.SMT_terms.Form.Ffalse. +Register Form.Fnot2 as SMTCoq.SMT_terms.Form.Fnot2. +Register Form.Fand as SMTCoq.SMT_terms.Form.Fand. +Register Form.For as SMTCoq.SMT_terms.Form.For. +Register Form.Fxor as SMTCoq.SMT_terms.Form.Fxor. +Register Form.Fimp as SMTCoq.SMT_terms.Form.Fimp. +Register Form.Fiff as SMTCoq.SMT_terms.Form.Fiff. +Register Form.Fite as SMTCoq.SMT_terms.Form.Fite. +Register Form.FbbT as SMTCoq.SMT_terms.Form.FbbT. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) |