From 7ce6bf4f7740de4c69877ec9179520bcaa0d014c Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 18 Feb 2022 17:10:13 +0100 Subject: Removed deprecated features --- src/Misc.v | 208 ++++++++++++------------- src/PArray/PArray.v | 40 ++--- src/SMT_terms.v | 68 ++++---- src/State.v | 50 +++--- src/Trace.v | 14 +- src/array/Array_checker.v | 58 +++---- src/bva/BVList.v | 2 +- src/bva/Bva_checker.v | 302 ++++++++++++++++++------------------ src/classes/SMT_classes_instances.v | 16 +- src/cnf/Cnf.v | 64 ++++---- src/euf/Euf.v | 38 ++--- src/lia/Lia.v | 30 ++-- src/spl/Assumptions.v | 8 +- src/spl/Operators.v | 88 +++++------ src/spl/Syntactic.v | 12 +- 15 files changed, 499 insertions(+), 499 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index 0317bda..86dc1aa 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -25,7 +25,7 @@ Proof. intros [ | ]; reflexivity. Qed. (** Lemmas about Int63 *) -Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i == j). +Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i =? j). Proof. intros; apply iff_reflect. symmetry;apply eqb_spec. @@ -43,7 +43,7 @@ Proof. Qed. Lemma le_eq : forall i j, - (j <= i) = true -> (j + 1 <= i) = false -> i = j. + (j <=? i) = true -> (j + 1 <=? i) = false -> i = j. Proof. intros i j; rewrite leb_spec; destruct (dec_Zle [|j+1|] [|i|]) as [H|H]. rewrite <- leb_spec in H; rewrite H; discriminate. @@ -59,18 +59,18 @@ Proof. rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption. Qed. -Lemma leb_0 : forall x, 0 <= x = true. +Lemma leb_0 : forall x, 0 <=? x = true. Proof. intros x;rewrite leb_spec;destruct (to_Z_bounded x);trivial. Qed. -Lemma leb_refl : forall n, n <= n = true. +Lemma leb_refl : forall n, n <=? n = true. Proof. intros n;rewrite leb_spec;apply Z.le_refl. Qed. Lemma lt_eq : forall i j, - (i < j + 1) = true -> (i < j) = false -> i = j. + (i (i i = j. Proof. intros i j. rewrite ltb_spec. destruct (dec_Zlt [|i|] [|j|]) as [H|H]. rewrite <- ltb_spec in H; rewrite H; discriminate. @@ -86,7 +86,7 @@ Proof. rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia. Qed. -Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true. +Lemma not_0_ltb : forall x, x <> 0 <-> 0 0)%Z;[ | lia]. @@ -95,34 +95,34 @@ Proof. assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | lia]. Qed. -Lemma ltb_0 : forall x, ~ (x < 0 = true). +Lemma ltb_0 : forall x, ~ (x y < z = true -> x < z = true. +Lemma ltb_trans : forall x y z, x y x y < z = true -> x < z = true. +Lemma leb_ltb_trans : forall x y z, x <=? y = true -> y x [|x+1|] = ([|x|] + 1)%Z. +Lemma to_Z_add_1 : forall x y, x [|x+1|] = ([|x|] + 1)%Z. Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;lia. @@ -133,12 +133,12 @@ Proof. intros; assert (Bx := to_Z_bounded x); rewrite add_spec, to_Z_1, Z.mod_small; lia. Qed. -Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true). +Lemma leb_not_gtb : forall n m, m <=? n = true -> ~(n [|x - y|] = ([|x|] - [|y|])%Z. +Lemma to_Z_sub_gt : forall x y, y <=? x = true -> [|x - y|] = ([|x|] - [|y|])%Z. Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia. Qed. -Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z. +Lemma to_Z_sub_1 : forall x y, y ([| x - 1|] = [|x|] - 1)%Z. Proof. intros;apply to_Z_sub_gt. generalize (leb_ltb_trans _ _ _ (leb_0 y) H). @@ -174,14 +174,14 @@ Proof. intros; apply (to_Z_sub_1 _ 0); rewrite ltb_spec; assumption. Qed. -Lemma ltb_leb_sub1 : forall x i, x <> 0 -> (i < x = true <-> i <= x - 1 = true). +Lemma ltb_leb_sub1 : forall x i, x <> 0 -> (i i <=? x - 1 = true). Proof. intros x i Hdiff. rewrite ltb_spec, leb_spec, to_Z_sub_1_diff;trivial. split;auto with zarith. Qed. -Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true. +Lemma minus_1_lt i : (i =? 0) = false -> i - 1 > i = (i1 >> i) lxor (i2 >> i). Proof. apply bit_ext; intros n. rewrite lxor_spec, !bit_lsr, lxor_spec. - case (_ <= _); auto. + case (_ <=? _); auto. Qed. Lemma bit_or_split i : i = (i>>1)<<1 lor bit i 0. @@ -215,21 +215,21 @@ Proof. case (Zle_lt_or_eq _ _ Hi). 2: replace 0%Z with [|0|]; auto; rewrite to_Z_eq. 2: intros H; rewrite <-H. - 2: replace (0 < 1) with true; auto. + 2: replace (0 Prop), P 0 -> - (forall i, (i < max_int) = true -> P i -> P (i + 1)) -> + (forall i, (i P i -> P (i + 1)) -> forall i, P i. Proof. intros P HP0 Hrec i. @@ -327,9 +327,9 @@ Proof. Qed. Lemma int_ind_bounded : forall (P : int -> Prop) min max, - min <= max = true -> + min <=? max = true -> P min -> - (forall i, min <= i = true -> i < max = true -> P i -> P (i + 1)) -> + (forall i, min <=? i = true -> i P i -> P (i + 1)) -> P max. Proof. intros P min max Hle Hmin Hrec. @@ -364,7 +364,7 @@ rewrite <- to_Z_eq. rewrite sub_spec, to_Z_1. rewrite 2!bit_0_spec. rewrite sub_spec, to_Z_1. -case_eq (i == 0). +case_eq (i =? 0). rewrite eqb_spec; intro Hi; rewrite Hi; reflexivity. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0. generalize (to_Z_bounded i). @@ -442,7 +442,7 @@ Fixpoint iter_int63_aux (n : nat) (i : int) (A : Type) (f : A -> A) : A -> A := match n with | O => fun x => x | S n => - if i == 0 then fun x => x + if i =? 0 then fun x => x else let g := iter_int63_aux n (i >> 1) A f in fun x => if bit i 0 then f (g (g x)) else g (g x) end. @@ -460,7 +460,7 @@ rewrite <- to_Z_eq, to_Z_0. generalize (to_Z_bounded i); lia. reflexivity. intros i a Hi; simpl. -case (i == 0); [ reflexivity | ]. +case (i =? 0); [ reflexivity | ]. rewrite IHn; [ | apply pow2_lsr; assumption]. rewrite IHn; [ | apply pow2_lsr; assumption]. case (bit i 0); reflexivity. @@ -484,20 +484,20 @@ intros n i A f; revert i; induction n; intros i a Hi. lia. } simpl. -replace (i == 0) with false. +replace (i =? 0) with false. { rewrite bit_sub1_0, sub1_lsr. { case_eq (bit i 0); simpl. { intros _. - case_eq (i == 1). + case_eq (i =? 1). { rewrite eqb_spec; intro H; rewrite H in *; clear i H. case n; reflexivity. } rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. - replace (i - 1 == 0) with false. + replace (i - 1 =? 0) with false. { reflexivity. } @@ -505,14 +505,14 @@ replace (i == 0) with false. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. } intro Hibit. - case_eq (i == 1). + case_eq (i =? 1). { rewrite eqb_spec; intro H; rewrite H in *; clear i H; discriminate. } rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. - replace (i - 1 == 0) with false. + replace (i - 1 =? 0) with false. { - case_eq (i == 2). + case_eq (i =? 2). { rewrite eqb_spec; intro H; rewrite H in *; clear i H. destruct n; [ lia | ]. @@ -559,7 +559,7 @@ symmetry. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0; lia. Qed. -Lemma iter_int63_S : forall i A f a, 0 < i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a). +Lemma iter_int63_S : forall i A f a, 0 iter_int63 i A f a = f (iter_int63 (i - 1) A f a). Proof. intros i A f a. rewrite ltb_spec, to_Z_0; intro Hi. @@ -575,7 +575,7 @@ Definition foldi (from to : int) (a : A) : A := - if to <= from then + if to <=? from then a else let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * A)%type) => @@ -583,14 +583,14 @@ Definition foldi ) (from, a) in r. Lemma foldi_ge : forall A f from to (a:A), - to <= from = true -> foldi f from to a = a. + to <=? from = true -> foldi f from to a = a. Proof. intros A f from to a; unfold foldi. intro H; rewrite H; reflexivity. Qed. Lemma foldi_lt_l : forall A f from to (a:A), - from < to = true -> foldi f from to a = foldi f (from + 1) to (f from a). + from foldi f from to a = foldi f (from + 1) to (f from a). Proof. intros A f from to a Hfromto. pose proof (to_Z_bounded from) as Hfrom. @@ -599,7 +599,7 @@ unfold foldi. rewrite leb_negb_gtb. rewrite Hfromto; simpl. rewrite ltb_spec in Hfromto. -case_eq (to <= from + 1). +case_eq (to <=? from + 1). rewrite leb_spec, to_Z_add_1_wB; [ | lia ]. intro Htofrom. assert (H : to = from + 1). @@ -620,7 +620,7 @@ rewrite ltb_spec, to_Z_0, sub_spec, Zmod_small; lia. Qed. Lemma foldi_lt_r : forall A f from to (a:A), - from < to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a). + from foldi f from to a = f (to - 1) (foldi f from (to - 1) a). Proof. intros A f from to a; rewrite ltb_spec; intro Hlt. assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). @@ -641,8 +641,8 @@ Proof. Qed. Lemma foldi_ind : forall A (P : int -> A -> Prop) f from to a, - from <= to = true -> P from a -> - (forall i a, from <= i = true -> i < to = true -> P i a -> P (i + 1) (f i a)) -> + from <=? to = true -> P from a -> + (forall i a, from <=? i = true -> i P i a -> P (i + 1) (f i a)) -> P to (foldi f from to a). Proof. intros A P f from to a Hle Hfrom IH. @@ -657,8 +657,8 @@ Proof. Qed. Lemma foldi_ind2 : forall A B (P : int -> A -> B -> Prop) f1 f2 from to a1 a2, - from <= to = true -> P from a1 a2 -> - (forall i a1 a2, from <= i = true -> i < to = true -> P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) -> + from <=? to = true -> P from a1 a2 -> + (forall i a1 a2, from <=? i = true -> i P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) -> P to (foldi f1 from to a1) (foldi f2 from to a2). Proof. intros A B P f1 f2 from to a1 a2 Hle Hfrom IH. @@ -673,7 +673,7 @@ Proof. Qed. Lemma foldi_eq_compat : forall A (f1 f2:int -> A -> A) min max a, - (forall i a, min <= i = true -> i < max = true -> f1 i a = f2 i a) -> + (forall i a, min <=? i = true -> i f1 i a = f2 i a) -> foldi f1 min max a = foldi f2 min max a. Proof. intros A f1 f2 min max a Hf. @@ -702,7 +702,7 @@ Proof. Qed. Lemma to_list_In : forall {A} (t: array A) i, - i < length t = true -> In (t.[i]) (to_list t). + i In (t.[i]) (to_list t). intros A t i; assert (Bt := to_Z_bounded (length t)); assert (Bi := to_Z_bounded i); rewrite ltb_spec; unfold to_list. rewrite <- in_rev. apply foldi_ind. @@ -719,13 +719,13 @@ Lemma to_list_In : forall {A} (t: array A) i, Qed. Lemma to_list_In_eq : forall {A} (t: array A) i x, - i < length t = true -> x = t.[i] -> In x (to_list t). + i x = t.[i] -> In x (to_list t). Proof. intros A t i x Hi ->. now apply to_list_In. Qed. Lemma In_to_list : forall {A} (t: array A) x, - In x (to_list t) -> exists i, i < length t = true /\ x = t.[i]. + In x (to_list t) -> exists i, i A -> B) t i, - i < length t = true -> (amapi f t).[i] = f i (t.[i]). + i (amapi f t).[i] = f i (t.[i]). Proof. intros A B f t. assert (Bt := to_Z_bounded (length t)). @@ -806,13 +806,13 @@ Proof. Qed. Lemma get_amap : forall {A B} (f:A -> B) t i, - i < length t = true -> (amap f t).[i] = f (t.[i]). + i (amap f t).[i] = f (t.[i]). Proof. intros; unfold amap; apply get_amapi; assumption. Qed. Lemma get_amapi_outofbound : forall {A B} (f:int -> A -> B) t i, - i < length t = false -> (amapi f t).[i] = f (length t) (default t). + i (amapi f t).[i] = f (length t) (default t). Proof. intros A B f t i H1; rewrite get_outofbound. apply default_amapi. @@ -820,7 +820,7 @@ Proof. Qed. Lemma get_amap_outofbound : forall {A B} (f:A -> B) t i, - i < length t = false -> (amap f t).[i] = f (default t). + i (amap f t).[i] = f (default t). Proof. intros; unfold amap; apply get_amapi_outofbound; assumption. Qed. @@ -845,7 +845,7 @@ Qed. (** Some properties about afold_left *) Definition afold_left A default (OP : A -> A -> A) (V : array A) := - if length V == 0 then default + if length V =? 0 then default else foldi (fun i a => OP a (V.[i])) 1 (length V) (V.[0]). Lemma afold_left_spec : forall A args op (e : A), @@ -863,7 +863,7 @@ Lemma afold_left_spec : forall A args op (e : A), Lemma afold_left_eq : forall A OP (def : A) V1 V2, length V1 = length V2 -> - (forall i, i < length V1 = true -> V1.[i] = V2.[i]) -> + (forall i, i V1.[i] = V2.[i]) -> afold_left _ def OP V1 = afold_left _ def OP V2. Proof. intros A OP def V1 V2 Heqlength HeqV. @@ -885,8 +885,8 @@ Qed. Lemma afold_left_ind : forall A OP def V (P : int -> A -> Prop), (length V = 0 -> P 0 def) -> - (0 < length V = true -> P 1 (V.[0])) -> - (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i + 1) (OP a (V.[i]))) -> + (0 P 1 (V.[0])) -> + (forall a i, 0 i P i a -> P (i + 1) (OP a (V.[i]))) -> P (length V) (afold_left A def OP V). Proof. intros A OP def V P HP0 HP1 HPOP. @@ -905,7 +905,7 @@ Qed. (** Some properties about afold_right *) Definition afold_right A default (OP : A -> A -> A) (V : array A) := - if length V == 0 then default + if length V =? 0 then default else foldi (fun i => OP (V.[length V - 1 - i])) 1 (length V) (V.[length V - 1]). Lemma afold_right_spec : forall A args op (e : A), @@ -927,7 +927,7 @@ Lemma afold_right_spec : forall A args op (e : A), Lemma afold_right_eq : forall A OP (def : A) V1 V2, length V1 = length V2 -> - (forall i, i < length V1 = true -> V1.[i] = V2.[i]) -> + (forall i, i V1.[i] = V2.[i]) -> afold_right _ def OP V1 = afold_right _ def OP V2. Proof. intros A OP def V1 V2 Heqlength HeqV. @@ -948,8 +948,8 @@ Qed. Lemma afold_right_ind : forall A OP def V (P : int -> A -> Prop), (length V = 0 -> P 0 def) -> - (0 < length V = true -> P (length V - 1) (V.[length V - 1])) -> - (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i - 1) (OP (V.[i - 1]) a)) -> + (0 P (length V - 1) (V.[length V - 1])) -> + (forall a i, 0 i P i a -> P (i - 1) (OP (V.[i - 1]) a)) -> P 0 (afold_right A def OP V). Proof. intros A OP def V P HP0 HP1 HPOP. @@ -972,7 +972,7 @@ Qed. (* Case andb *) Lemma afold_left_andb_false : forall i a, - i < length a = true -> + i a .[ i] = false -> afold_left bool true andb a = false. Proof. @@ -991,7 +991,7 @@ Qed. Lemma afold_left_andb_false_inv : forall a, afold_left bool true andb a = false -> - exists i, (i < length a = true) /\ (a .[ i] = false). + exists i, (i a.[i] = true) -> + (forall i, i a.[i] = true) -> afold_left bool true andb a = true. Proof. intros a H. @@ -1020,7 +1020,7 @@ Qed. Lemma afold_left_andb_true_inv : forall a, afold_left bool true andb a = true -> - forall i, i < length a = true -> a.[i] = true. + forall i, i a.[i] = true. Proof. intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i). revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind. @@ -1052,7 +1052,7 @@ Qed. (* Case orb *) Lemma afold_left_orb_true : forall i a, - i < length a = true -> + i a .[ i] = true -> afold_left bool false orb a = true. Proof. @@ -1071,7 +1071,7 @@ Qed. Lemma afold_left_orb_true_inv : forall a, afold_left bool false orb a = true -> - exists i, i < length a = true /\ a .[ i] = true. + exists i, i a.[i] = false) -> + (forall i, i a.[i] = false) -> afold_left bool false orb a = false. Proof. intros a H. @@ -1100,7 +1100,7 @@ Qed. Lemma afold_left_orb_false_inv : forall a, afold_left bool false orb a = false -> - forall i, i < length a = true -> a.[i] = false. + forall i, i a.[i] = false. Proof. intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i). revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind. @@ -1132,8 +1132,8 @@ Qed. (* Case implb *) Lemma afold_right_implb_false : forall a, - 0 < length a = true /\ - (forall i, i < length a - 1 = true -> a .[ i] = true) /\ + 0 a .[ i] = true) /\ a.[length a - 1] = false -> afold_right bool true implb a = false. Proof. @@ -1150,8 +1150,8 @@ Qed. Lemma afold_right_implb_false_inv : forall a, afold_right bool true implb a = false -> - 0 < length a = true /\ - (forall i, i < length a - 1 = true -> a .[ i] = true) /\ + 0 a .[ i] = true) /\ a.[length a - 1] = false. Proof. intros a H; assert (Ba := to_Z_bounded (length a)); split; [ | split ]. @@ -1185,7 +1185,7 @@ Proof. Qed. Lemma afold_right_implb_true_aux : forall a, - (exists i, i < length a - 1 = true /\ a.[i] = false) -> + (exists i, i afold_right bool true implb a = true. Proof. intros a [ i [ Hi Hai ] ]. @@ -1206,8 +1206,8 @@ Proof. Qed. Lemma afold_right_implb_true : forall a, - length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/ - (forall i, i < length a = true -> a.[i] = true) -> + length a = 0 \/ (exists i, i a.[i] = true) -> afold_right bool true implb a = true. Proof. intro a; assert (Ba := to_Z_bounded (length a)); case (reflect_eqb (length a) 0). @@ -1216,7 +1216,7 @@ Proof. intros [H1|[H1|H1]]. elim (Hneq H1). apply afold_right_implb_true_aux; auto. - assert (Heq : length a == 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq). + assert (Heq : length a =? 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq). unfold afold_right; rewrite Heq. revert Hneq; rewrite <- to_Z_eq, to_Z_0; intro Hneq. apply (foldi_ind _ (fun i a => a = true)). @@ -1230,12 +1230,12 @@ Qed. Lemma afold_right_implb_true_inv : forall a, afold_right bool true implb a = true -> - length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/ - (forall i, i < length a = true -> a.[i] = true). + length a = 0 \/ (exists i, i a.[i] = true). Proof. intros a H; cut (length a = 0 - \/ (exists i, 0 <= i = true /\ i < length a - 1 = true /\ a.[i] = false) - \/ (forall i, 0 <= i = true -> i < length a = true -> a.[i] = true)). + \/ (exists i, 0 <=? i = true /\ i i a.[i] = true)). clear H; intro H; destruct H as [ H | H ]. left; tauto. destruct H as [ H | H ]. @@ -1276,18 +1276,18 @@ Qed. (* Other cases *) Lemma afold_left_length_2 : forall A default OP t, - (length t == 2) = true -> + (length t =? 2) = true -> afold_left A default OP t = OP (t.[0]) (t.[1]). Proof. - intros A default OP t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity. + intros A default OP t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 =? 0) with false; reflexivity. Qed. Lemma afold_right_length_2 : forall A default OP t, - (length t == 2) = true -> + (length t =? 2) = true -> afold_right A default OP t = OP (t.[0]) (t.[1]). Proof. - intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity. + intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 =? 0) with false; reflexivity. Qed. @@ -1305,77 +1305,77 @@ Ltac tac_right := Lemma afold_left_xorb_false1 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = false -> t .[ 1] = false -> afold_left bool false xorb t = false. Proof. tac_left. Qed. Lemma afold_left_xorb_false2 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = true -> t .[ 1] = true -> afold_left bool false xorb t = false. Proof. tac_left. Qed. Lemma afold_left_xorb_true1 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = false -> t .[ 1] = true -> afold_left bool false xorb t = true. Proof. tac_left. Qed. Lemma afold_left_xorb_true2 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = true -> t .[ 1] = false -> afold_left bool false xorb t = true. Proof. tac_left. Qed. (* Lemma afold_right_implb_false : forall t f, *) -(* (PArray.length t == 2) = true -> *) +(* (PArray.length t =? 2) = true -> *) (* f (t .[ 0]) = true -> f (t .[ 1]) = false -> *) (* afold_right bool int true implb f t = false. *) (* Proof. tac_right. Qed. *) (* Lemma afold_right_implb_true1 : forall t f, *) -(* (PArray.length t == 2) = true -> *) +(* (PArray.length t =? 2) = true -> *) (* f (t .[ 0]) = false -> *) (* afold_right bool int true implb f t = true. *) (* Proof. tac_right. Qed. *) (* Lemma afold_right_implb_true2 : forall t f, *) -(* (PArray.length t == 2) = true -> *) +(* (PArray.length t =? 2) = true -> *) (* f (t.[1]) = true -> *) (* afold_right bool int true implb f t = true. *) (* Proof. tac_right. Qed. *) Lemma afold_left_eqb_false1 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = false -> t .[ 1] = true -> afold_left bool true eqb t = false. Proof. tac_left. Qed. Lemma afold_left_eqb_false2 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = true -> t .[ 1] = false -> afold_left bool true eqb t = false. Proof. tac_left. Qed. Lemma afold_left_eqb_true1 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = true -> t .[ 1] = true -> afold_left bool true eqb t = true. Proof. tac_left. Qed. Lemma afold_left_eqb_true2 : forall t, - (PArray.length t == 2) = true -> + (PArray.length t =? 2) = true -> t .[ 0] = false -> t .[ 1] = false -> afold_left bool true eqb t = true. Proof. tac_left. Qed. @@ -1573,7 +1573,7 @@ Definition aexistsbi {A:Type} (f:int->A->bool) (t:array A) := Lemma aexistsbi_false_spec : forall A (f : int -> A -> bool) t, aexistsbi f t = false <-> - forall i, i < length t = true -> f i (t.[i]) = false. + forall i, i f i (t.[i]) = false. Proof. intros A f t; unfold aexistsbi. split. @@ -1586,7 +1586,7 @@ Proof. Qed. Lemma aexistsbi_spec : forall A (f : int -> A -> bool) t, - aexistsbi f t = true <-> exists i, i < length t = true /\ f i (t.[i]) = true. + aexistsbi f t = true <-> exists i, i A->bool) (t:array A) := afold_left _ true andb (amapi f t). Lemma aforallbi_false_spec : forall A (f : int -> A -> bool) t, - aforallbi f t = false <-> exists i, i < length t = true /\ f i (t.[i]) = false. + aforallbi f t = false <-> exists i, i A -> bool) t, aforallbi f t = true <-> - forall i, i < length t = true -> f i (t.[i]) = true. + forall i, i f i (t.[i]) = true. Proof. intros A f t; unfold aforallbi. split. diff --git a/src/PArray/PArray.v b/src/PArray/PArray.v index 03f1abd..891db84 100644 --- a/src/PArray/PArray.v +++ b/src/PArray/PArray.v @@ -27,9 +27,9 @@ Module IntOrderedType <: OrderedType. Definition t := int. - Definition eq x y := (x == y) = true. + Definition eq x y := (x =? y) = true. - Definition lt x y := (x < y) = true. + Definition lt x y := (x x | None => d @@ -90,7 +90,7 @@ Definition default {A:Type} (t:array A) : A := Definition set {A:Type} (t:array A) (i:int) (a:A) : array A := let (td,l) := t in - if l <= i then + if l <=? i then t else let (t,d) := td in @@ -115,14 +115,14 @@ Definition max_length := max_int. Require FSets.FMapFacts. Module P := FSets.FMapFacts.WProperties_fun IntOrderedType Map. -Lemma get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. +Lemma get_outofbound : forall A (t:array A) i, (i t.[i] = default t. intros A t i; unfold get. destruct t as ((t, d), l). unfold length; intro Hi; rewrite Hi; clear Hi. reflexivity. Qed. -Lemma get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. +Lemma get_set_same : forall A t i (a:A), (i t.[i<-a].[i] = a. intros A t i a. destruct t as ((t, d), l). unfold set, get, length. @@ -143,7 +143,7 @@ Lemma get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. intros A t i j a Hij. destruct t as ((t, d), l). unfold set, get, length. -case (l <= i). +case (l <=? i). reflexivity. rewrite P.F.add_neq_o. reflexivity. @@ -156,17 +156,17 @@ Lemma default_set : forall A t i (a:A), default (t.[i<-a]) = default t. intros A t i a. destruct t as ((t, d), l). unfold default, set. -case (l <= i); reflexivity. +case (l <=? i); reflexivity. Qed. Lemma get_make : forall A (a:A) size i, (make size a).[i] = a. intros A a size i. unfold make, get. rewrite P.F.empty_o. -case (i < size); reflexivity. +case (i - (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> + (forall i, i t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. *) @@ -229,7 +229,7 @@ Qed. Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t. unfold default, get, set. destruct t as ((t, d), l). -case_eq (i < l). +case_eq (i default t -> (x < length t) = true. + t.[x] <> default t -> (x true - | Fnot2 _ l => Lit.blit l < i + | Fnot2 _ l => Lit.blit l - 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 + aforallbi (fun _ l => Lit.blit l (Lit.blit a (Lit.blit a List.forallb (fun l => Lit.blit l f1 j = f2 j) -> + (forall j, j f1 j = f2 j) -> lt_form i h -> interp_aux f1 h = interp_aux f2 h. Proof. @@ -161,11 +161,11 @@ Module Form. intros;rewrite default_set;trivial. Qed. - Lemma t_interp_wf : forall i, i < PArray.length t_form -> + Lemma t_interp_wf : forall i, i t_interp.[i] = interp_aux (PArray.get t_interp) (t_form.[i]). Proof. set (P' i t := length t = length t_form -> - forall j, j < i -> + forall j, j 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 aforallbi_spec in wf_t_i. @@ -179,7 +179,7 @@ Module Form. intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. rewrite H2;trivial. - assert (j < i). + assert (j [|i|]) by (intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0); auto with zarith. @@ -203,7 +203,7 @@ Module Form. Lemma wf_interp_form_lt : forall t_form, wf t_form -> - forall x, x < PArray.length t_form -> + forall x, x interp_state_var t_form x = interp t_form (t_form.[x]). Proof. unfold interp_state_var;intros. @@ -214,7 +214,7 @@ Module Form. forall t_form, PArray.default t_form = Ftrue -> wf t_form -> forall x, interp_state_var t_form x = interp t_form (t_form.[x]). Proof. - intros t Hd Hwf x;case_eq (x < PArray.length t);intros. + intros t Hd Hwf x;case_eq (x 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') + | 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 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 Int63.eqb la lb + top_eqb o o' && (t1 =? t1') && (t2 =? t2') && (t3 =? t3') + | Aapp a la, Aapp b lb => (a =? b) && list_beq Int63.eqb la lb | _, _ => false end. @@ -2226,15 +2226,15 @@ Qed. Definition lt_atom i a := match a with | Acop _ => true - | Auop _ h => h < i - | Abop _ h1 h2 => (h1 < i) && (h2 < i) - | Atop _ h1 h2 h3 => (h1 < i) && (h2 < i) && (h3 < i) - | Anop _ ha => List.forallb (fun h => h < i) ha - | Aapp f args => List.forallb (fun h => h < i) args + | Auop _ h => h (h1 (h1 List.forallb (fun h => h List.forallb (fun h => h f1 j = f2 j) -> + forall f1 f2 i, (forall j, j f1 j = f2 j) -> forall a, lt_atom i a -> interp_aux f1 a = interp_aux f2 a. Proof. @@ -2277,12 +2277,12 @@ Qed. intros;rewrite default_set;trivial. Qed. - Lemma t_interp_wf_lt : forall i, i < PArray.length t_atom -> + Lemma t_interp_wf_lt : forall i, i 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 -> + forall j, j 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 aforallbi_spec in wf_t_i. @@ -2296,7 +2296,7 @@ Qed. intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. rewrite H2;trivial. - assert (j < i). + assert (j [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. @@ -2313,7 +2313,7 @@ Qed. Lemma t_interp_wf : forall i, t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]). Proof. - intros i;case_eq (i< PArray.length t_atom);intros. + intros i;case_eq (i + j exists v : interp_t (v_type Typ.type interp_t (a .[ j])), a .[ j] = Bval (v_type Typ.type interp_t (a .[ j])) v) -> - forall l, List.forallb (fun h0 : int => h0 < h) l = true -> + forall l, List.forallb (fun h0 : int => h0 forall (f0: tval), exists v : interp_t @@ -2356,9 +2356,9 @@ Qed. exists true; auto. Qed. - Lemma check_aux_interp_aux_lt : forall h, h < length t_atom -> + Lemma check_aux_interp_aux_lt : forall h, h forall a, - (forall j, j < h -> + (forall j, j exists v, a.[j] = Bval (v_type _ _ (a.[j])) v) -> exists v, interp_aux (get a) (t_atom.[h]) = Bval (v_type _ _ (interp_aux (get a) (t_atom.[h]))) v. @@ -2485,19 +2485,19 @@ Qed. (k3 (Typ.interp t_i) z)); auto. (* N-ary operators *) - intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. + intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. intros acc _; exists (distinct (Typ.i_eqb t_i A) (rev acc)); auto. intro acc; rewrite andb_true_iff; intros [H1 H2]; destruct (IH _ H1) as [va Hva]; rewrite Hva; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ i])) A); simpl; try (exists true; auto); intro k; destruct (IHl (k interp_t va :: acc) H2) as [vb Hvb]; exists vb; auto. (* Application *) intros i l H; apply (check_aux_interp_aux_lt_aux a h IH l H (t_func.[i])). Qed. - Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom -> + Lemma check_aux_interp_hatom_lt : forall h, h 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 -> + forall j, j 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_ind;unfold P';intros. @@ -2508,7 +2508,7 @@ Qed. rewrite e, PArray.get_set_same. apply check_aux_interp_aux_lt; auto. rewrite H2; auto. - assert (j < i). + assert (j [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. @@ -2519,7 +2519,7 @@ Qed. Lemma check_aux_interp_hatom : forall h, exists v, t_interp.[h] = Bval (get_type h) v. Proof. - intros i;case_eq (i< PArray.length t_atom);intros. + intros i;case_eq (i l = l'. @@ -217,7 +217,7 @@ Module Lit. unfold interp, Var.interp;intros rho1 rho2 l Heq;rewrite Heq;trivial. Qed. - Lemma lxor_neg : forall l1 l2, (l1 lxor l2 == 1) = true -> l1 = Lit.neg l2. + Lemma lxor_neg : forall l1 l2, (l1 lxor l2 =? 1) = true -> l1 = Lit.neg l2. Proof. unfold Lit.neg; intros l1 l2;rewrite eqb_spec;intros Heq;rewrite <- Heq. rewrite lxorC, <- lxorA, lxor_nilpotent, lxor0_r;trivial. @@ -228,14 +228,14 @@ End Lit. Lemma compare_spec' : forall x y, match x ?= y with - | Lt => x < y + | Lt => x x = y - | Gt => y < x + | Gt => y false - | l :: c => (l == Lit._true) || has_true c + | l :: c => (l =? Lit._true) || has_true c end. @@ -343,9 +343,9 @@ Module C. | l2::c2' => match compare l1 l2 with | Eq => l1 :: resolve c1 c2' - | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2 + | Lt => if l1 lxor l2 =? 1 then or c1 c2' else l1 :: resolve c1 c2 | Gt => - if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux c2' + if l1 lxor l2 =? 1 then or c1 c2' else l2 :: resolve_aux c2' end end. @@ -359,13 +359,13 @@ Module C. induction c2;simpl;try discriminate. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto. - generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). simpl in Hc1;rewrite Hc1;trivial. simpl in H0;rewrite H0, orb_true_r;trivial. simpl;destruct (Lit.interp rho l1);simpl;auto. - generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). simpl in Hc1;rewrite Hc1;trivial. @@ -382,9 +382,9 @@ Module C. | l1::c1, l2::c2' => match compare l1 l2 with | Eq => l1 :: resolve c1 c2' - | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2 + | Lt => if l1 lxor l2 =? 1 then or c1 c2' else l1 :: resolve c1 c2 | Gt => - if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2' + if l1 lxor l2 =? 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2' end end. @@ -397,13 +397,13 @@ Module C. intros Hc1 Hc2. generalize (compare_spec' a i);destruct (a ?= i);intros;subst;simpl. destruct (Lit.interp rho i);simpl in *;auto. - generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros. + generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros. rewrite or_correct. rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). simpl in Hc1;rewrite Hc1;trivial. simpl in Hc2;rewrite Hc2, orb_true_r;trivial. simpl;destruct (Lit.interp rho a);simpl;auto. - generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros. + generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros. rewrite or_correct. rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). simpl in Hc1;rewrite Hc1;trivial. @@ -485,7 +485,7 @@ Module S. Proof. unfold valid, get;simpl;intros. destruct (reflect_eqb id id0);subst. - case_eq (id0 < length s);intros. + case_eq (id0 l1:: nil | l2 :: c' => match l1 ?= l2 with - | Lt => if l1 lxor l2 == 1 then C._true else l1 :: c + | Lt => if l1 lxor l2 =? 1 then C._true else l1 :: c | Eq => c - | Gt => if l1 lxor l2 == 1 then C._true else l2 :: insert l1 c' + | Gt => if l1 lxor l2 =? 1 then C._true else l2 :: insert l1 c' end end. @@ -558,10 +558,10 @@ Module S. intros rho Hwf l1;induction c;simpl;trivial. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. destruct (Lit.interp rho a);simpl in *;auto. - generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros;trivial. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros;trivial. rewrite C.interp_true;trivial. rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. - generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite C.interp_true;trivial. rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. simpl;rewrite orb_assoc,(orb_comm (Lit.interp rho l1)),<-orb_assoc,IHc;trivial. @@ -623,7 +623,7 @@ Module S. Proof. unfold valid, get, set_clause. intros rho s Hrho Hs pos c Hc id. destruct (reflect_eqb pos id);subst. - case_eq (id < length s); intro H. + case_eq (id (C.resolve (get s (r.[i])) c')) 1 len (get s (r.[0])) in (* S.set_clause *) internal_set s pos c. @@ -683,8 +683,8 @@ Module S. Definition subclause (cl1 cl2 : list _lit) := List.forallb (fun l1 => - (l1 == Lit._false) || (l1 == Lit.neg Lit._true) || - List.existsb (fun l2 => l1 == l2) cl2) cl1. + (l1 =? Lit._false) || (l1 =? Lit.neg Lit._true) || + List.existsb (fun l2 => l1 =? l2) cl2) cl1. Definition check_weaken (s:t) (cid:clause_id) (cl:list _lit) : C.t := if subclause (get s cid) cl then cl else C._true. diff --git a/src/Trace.v b/src/Trace.v index 1849c44..ad4c41e 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -61,7 +61,7 @@ Section trace. end) s a) (inl s) t in s'. Definition _checker_partial_ (s: S.t) (t: _trace_) (max:int) : S.t := - PArray.fold_left (fun s a => PArray.foldi_left (fun i s' a' => if i < max then check_step s' a' else s') s a) s t. + PArray.fold_left (fun s a => PArray.foldi_left (fun i s' a' => if i - (forall i : int, i < length d -> C.interp rho (to_list (d.[i]))). + (forall i : int, i C.interp rho (to_list (d.[i]))). Proof. unfold valid; intros rho d; split; intro H. intros i Hi; case_eq (C.interp rho (to_list (d .[ i]))); try reflexivity. @@ -210,7 +210,7 @@ Module Cnf_Checker. Local Open Scope list_scope. - Local Notation check_flatten t_form := (check_flatten t_form (fun i1 i2 => i1 == i2) (fun _ _ => false)) (only parsing). + Local Notation check_flatten t_form := (check_flatten t_form (fun i1 i2 => i1 =? i2) (fun _ _ => false)) (only parsing). Definition step_checker t_form s (st:step) := match st with @@ -290,7 +290,7 @@ Module Cnf_Checker. Definition checker_eq t_form l1 l2 l (c:certif) := negb (Lit.is_pos l) && match t_form.[Lit.blit l] with - | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2') + | Form.Fiff l1' l2' => (l1 =? l1') && (l2 =? l2') | _ => false end && checker t_form l c. @@ -504,7 +504,7 @@ Inductive step := Definition add_roots s d used_roots := match used_roots with | Some ur => foldi (fun i s => - let c := if (ur.[i]) < length d then (d.[ur.[i]])::nil else C._true in + let c := if (ur.[i]) foldi (fun i s => S.set_clause s i (d.[i]::nil)) 0 (length d) s end. @@ -521,7 +521,7 @@ Inductive step := S.valid rho (add_roots s d used_roots). Proof. intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto with smtcoq_core); case used_roots. - intro ur; apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] < length d). + intro ur; apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; unfold C.valid; simpl; specialize (H5 i); rewrite length_amap, get_amap in H5 by assumption; unfold rho; rewrite H5; auto with smtcoq_core. @@ -733,7 +733,7 @@ Inductive step := Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) := negb (Lit.is_pos l) && match t_form.[Lit.blit l] with - | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2') + | Form.Fiff l1' l2' => (l1 =? l1') && (l2 =? l2') | _ => false end && let (nclauses,_,_) := c in diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index 3e403b3..78f7101 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -40,7 +40,7 @@ Section certif. | Atop (TO_store ti2 te2) fa j v2 => if Typ.eqb ti1 ti2 && Typ.eqb te te1 && Typ.eqb te te2 && - (i == j) && (v == v2) + (i =? j) && (v =? v2) then lres::nil else C._true | _ => C._true @@ -57,7 +57,7 @@ Section certif. Definition store_of_me a b := match get_atom b with | Atop (TO_store ti te) a' i _ => - if (a' == a) then Some (ti, te, i) else None + if (a' =? a) then Some (ti, te, i) else None | _ => None end. @@ -77,8 +77,8 @@ Section certif. match store_of_me sa sa2, store_of_me sa2 sa with | Some (ti3, te3, i1), None | None, Some (ti3, te3, i1) => if Typ.eqb ti ti3 && Typ.eqb te te3 && - (((i1 == i) && (j1 == j) && (j2 == j)) || - ((i1 == j) && (j1 == i) && (j2 == i))) then + (((i1 =? i) && (j1 =? j) && (j2 =? j)) || + ((i1 =? j) && (j1 =? i) && (j2 =? i))) then cl else C._true | _, _ => C._true @@ -101,11 +101,11 @@ Section certif. | Abop (BO_select ti1 te1) a' d1, Abop (BO_select ti2 te2) b' d2 => Typ.eqb ti ti1 && Typ.eqb ti ti2 && Typ.eqb te te1 && Typ.eqb te te2 && - (a == a') && (b == b') && (d1 == d2) && + (a =? a') && (b =? b') && (d1 =? d2) && match get_atom d1 with | Abop (BO_diffarray ti3 te3) a3 b3 => Typ.eqb ti ti3 && Typ.eqb te te3 && - (a3 == a) && (b3 == b) + (a3 =? a) && (b3 =? b) | _ => false end | _, _ => false @@ -116,7 +116,7 @@ Section certif. if Lit.is_pos lres then match get_form (Lit.blit lres) with | For args => - if PArray.length args == 2 then + if PArray.length args =? 2 then let l1 := args.[0] in let l2 := args.[1] in if Lit.is_pos l1 && negb (Lit.is_pos l2) then @@ -213,7 +213,7 @@ Section certif. intros [ ] c1 c2 c3 Heq5. (* roweq *) - case_eq (Typ.eqb t0 t2 && Typ.eqb t t1 && - Typ.eqb t t3 && (b2 == c2) && (a2 == c3)); simpl; intros Heq6; try (now apply C.interp_true). + Typ.eqb t t3 && (b2 =? c2) && (a2 =? c3)); simpl; intros Heq6; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq. @@ -235,7 +235,7 @@ Section certif. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. - pose proof (H a). assert (a < PArray.length t_atom). + pose proof (H a). assert (a nil | ai :: a' => ai :: top_k_bools a' (k - 1) diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 24917a8..5c14bab 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -96,7 +96,7 @@ Section Checker. | Auop (UO_BVbitOf N p) a' => (* TODO: Do not need to check [Nat.eqb l (N.to_nat N)] at every iteration *) - if (a == a') (* We bit blast the right bv *) + if (a =? a') (* We bit blast the right bv *) && (Nat.eqb i p) (* We consider bits after bits *) && (Nat.eqb n (N.to_nat N)) (* The bv has indeed type BV n *) then check_bb a bs (S i) n @@ -133,7 +133,7 @@ Section Checker. Fixpoint check_not (bs br : list _lit) := match bs, br with | nil, nil => true - | b::bs, r::br => (r == Lit.neg b) && check_not bs br + | b::bs, r::br => (r =? Lit.neg b) && check_not bs br | _, _ => false end. @@ -146,7 +146,7 @@ Section Checker. | FbbT a bs, FbbT r br => match get_atom r with | Auop (UO_BVnot N) a' => - if (a == a') && check_not bs br && + if (a =? a') && check_not bs br && (N.of_nat (length bs) =? N)%N then lres::nil else C._true @@ -174,25 +174,25 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_form (Lit.blit bres), bvop with | Fand args, BO_BVand n => - ((if PArray.length args == 2 then + ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVand (n-1)) | For args, BO_BVor n => - ((if PArray.length args == 2 then + ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVor (n-1)) | Fxor a1 a2, BO_BVxor n => - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)), + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_BVxor (n-1)) | Fiff a1 a2, (BO_eq (Typ.TBV n)) => - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)), + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_eq (Typ.TBV n)) | _, _ => (false, bvop) @@ -218,21 +218,21 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVand n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (@check_symopp bs1 bs2 bsres (BO_BVand n)) && (N.of_nat (length bs1) =? n)%N then lres::nil else C._true | Abop (BO_BVor n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_symopp bs1 bs2 bsres (BO_BVor n)) && (N.of_nat (length bs1) =? n)%N then lres::nil else C._true | Abop (BO_BVxor n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_symopp bs1 bs2 bsres (BO_BVxor n)) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -268,7 +268,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres @@ -284,7 +284,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres @@ -306,7 +306,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_eq (Typ.TBV n)) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_eq bs1 bs2 [lbb]) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -340,12 +340,12 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := Fixpoint eq_carry_lit (carry : carry) (c : _lit) := if Lit.is_pos c then match carry with - | Clit l => l == c + | Clit l => l =? c | Cand c1 c2 => match get_form (Lit.blit c) with | Fand args => - if PArray.length args == 2 then + if PArray.length args =? 2 then (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1])) (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *) else false @@ -363,7 +363,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Cor c1 c2 => match get_form (Lit.blit c) with | For args => - if PArray.length args == 2 then + if PArray.length args =? 2 then (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1])) (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *) else false @@ -381,7 +381,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := else (* c can be negative only when it is literal false *) match carry with - | Clit l => l == c + | Clit l => l =? c | _ => false end. @@ -400,7 +400,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := (* This is the way LFSC computes carries *) let carry' := Cor (Cand (Clit b1) (Clit b2)) (Cand (Cxor (Clit b1) (Clit b2)) carry) in - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))) + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))) && eq_carry_lit carry c && check_add bs1 bs2 bsres carry' | _ => false @@ -422,7 +422,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVadd n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_add bs1 bs2 bsres (Clit Lit._false)) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -458,7 +458,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | FbbT a bs, FbbT r br => match get_atom r with | Auop (UO_BVneg n) a' => - if (a == a') && check_neg bs br && + if (a =? a') && check_neg bs br && (N.of_nat (length bs) =? n)%N then lres::nil else C._true @@ -545,7 +545,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVmult n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_mult bs1 bs2 bsres) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -590,7 +590,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_BVult n) a1' a2' => - if ((a1 == a1') && (a2 == a2')) + if ((a1 =? a1') && (a2 =? a2')) && (check_ult bs1 bs2 lbb) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? n)%N @@ -636,7 +636,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_BVslt n) a1' a2' => - if ((a1 == a1') && (a2 == a2')) + if ((a1 =? a1') && (a2 =? a2')) && (check_slt bs1 bs2 lbb) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? n)%N @@ -691,7 +691,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVconcat n m) a1' a2' => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_concat bs1 bs2 bsres) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? m)%N @@ -771,7 +771,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := else false. Definition check_extract3 (bs bsres: list _lit) (i j: N) : bool := - forallb2 (fun l1 l2 => l1 == l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres. + forallb2 (fun l1 l2 => l1 =? l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres. (** Checker for bitvector extraction *) @@ -783,7 +783,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | O => match j, bsres with | O, nil => true - | S j', b :: bsres' => (bx == b) && check_extract2 x' bsres' i j' + | S j', b :: bsres' => (bx =? b) && check_extract2 x' bsres' i j' | _, _ => false end | S i' => @@ -804,7 +804,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVextr i n0 n1) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_extract bs bsres i (n0 + i)) && (N.of_nat (length bs) =? n1)%N && (N.leb (n0 + i) n1) @@ -847,7 +847,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVzextn n i) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_zextend bs bsres i) && (N.of_nat (length bs) =? n)%N then lres::nil @@ -889,7 +889,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVsextn n i) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_sextend bs bsres i) && (N.of_nat (length bs) =? n)%N then lres::nil @@ -938,7 +938,7 @@ Definition shl_lit_be (a: list _lit) (b: list bool): list _lit := | Abop (BO_BVshl n) a1' a2' => match (get_atom a2) with | (Acop (CO_BV bv2 n2)) => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && check_shl bs1 bv2 bsres && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bv2) =? n)%N @@ -989,7 +989,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit := | Abop (BO_BVshr n) a1' a2' => match (get_atom a2) with | (Acop (CO_BV bv2 n2)) => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && check_shr bs1 bv2 bsres && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bv2) =? n)%N @@ -1211,7 +1211,7 @@ Proof. (* a *) pose proof (H a). - assert (H1: a < PArray.length t_atom). + assert (H1: a a = b. Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed. -Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. Qed. @@ -1937,9 +1937,9 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. exact H. now contradict H. now contradict H. @@ -1947,9 +1947,9 @@ Proof. intros. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -1964,9 +1964,9 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. exact H. now contradict H. now contradict H. @@ -1974,9 +1974,9 @@ Proof. intros. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -1991,14 +1991,14 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H. + case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H. exact H. now contradict H. now contradict H. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H. + case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -2041,20 +2041,20 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. (* apply length_to_list in H4. *) unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2100,19 +2100,19 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. @@ -2164,19 +2164,19 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. @@ -2226,20 +2226,20 @@ Proof. intro bs1. intros. rewrite H3 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros H5. + case_eq (PArray.length a =? 2). intros H5. rewrite H5 in H1. rewrite eqb_spec in H5. apply to_list_two in H5. unfold forallb. rewrite H5. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6. rewrite andb_true_iff in H6. destruct H6 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, H2. unfold Var.interp. now rewrite andb_true_r. intros H6. rewrite H6 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7. rewrite andb_true_iff in H7. destruct H7 as (H7 & H8). rewrite eqb_spec in H7, H8. rewrite H7, H8. rewrite andb_true_r. @@ -2310,12 +2310,12 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold C.interp. unfold existsb. rewrite orb_false_r. @@ -2325,7 +2325,7 @@ Proof. intro bs1. now unfold Var.interp. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2369,21 +2369,21 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold C.interp. unfold existsb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite orb_false_r. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite orb_false_r. @@ -2433,12 +2433,12 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold C.interp, existsb. @@ -2446,7 +2446,7 @@ Proof. intro bs1. rewrite Heq1, Heq2. unfold Var.interp. now rewrite orb_false_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite orb_false_r. @@ -2494,20 +2494,20 @@ Proof. intro bs1. intros. rewrite H3 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros H5. + case_eq (PArray.length a =? 2). intros H5. rewrite H5 in H1. rewrite eqb_spec in H5. apply to_list_two in H5. unfold forallb. rewrite H5. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6. rewrite andb_true_iff in H6. destruct H6 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold C.interp, Lit.interp, existsb. rewrite Heq1, H2. unfold Var.interp. now rewrite orb_false_r. intros H6. rewrite H6 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7. rewrite andb_true_iff in H7. destruct H7 as (H7 & H8). rewrite eqb_spec in H7, H8. rewrite H7, H8. rewrite orb_false_r. @@ -2576,7 +2576,7 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros i Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. @@ -2585,7 +2585,7 @@ Proof. intro bs1. now unfold Var.interp. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2629,14 +2629,14 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2686,14 +2686,14 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2740,14 +2740,14 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2796,8 +2796,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2834,8 +2834,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2871,8 +2871,8 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case (PArray.length a == 2) in *. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *. + case (PArray.length a =? 2) in *. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -2924,8 +2924,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2961,8 +2961,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2998,8 +2998,8 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case (PArray.length a == 2) in *. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *. + case (PArray.length a =? 2) in *. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -3051,7 +3051,7 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -3088,7 +3088,7 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -3124,7 +3124,7 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in *. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -3204,7 +3204,7 @@ Proof. intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVand *) - - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -3227,7 +3227,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a if i == last then l else Lit.neg l) args. + amapi (fun i l => if i =? last then l else Lit.neg l) args. (* Register or_of_imp as PrimInline. *) Lemma length_or_of_imp : forall args, @@ -31,21 +31,21 @@ Lemma length_or_of_imp : forall args, Proof. intro; unfold or_of_imp; apply length_amapi. Qed. Lemma get_or_of_imp : forall args i, - i < (PArray.length args) - 1 -> (or_of_imp args).[i] = Lit.neg (args.[i]). + i (or_of_imp args).[i] = Lit.neg (args.[i]). Proof. - unfold or_of_imp; intros args i H; case_eq (0 < PArray.length args). + unfold or_of_imp; intros args i H; case_eq (0 +Lemma get_or_of_imp2 : forall args i, 0 i = (PArray.length args) - 1 -> (or_of_imp args).[i] = args.[i]. Proof. unfold or_of_imp; intros args i Heq Hi; rewrite get_amapi; subst i. @@ -55,7 +55,7 @@ Qed. Lemma afold_right_impb p a : (forall x, p (Lit.neg x) = negb (p x)) -> - (PArray.length a == 0) = false -> + (PArray.length a =? 0) = false -> (afold_right bool true implb (amap p a)) = List.existsb p (to_list (or_of_imp a)). Proof. @@ -97,7 +97,7 @@ Proof. case_eq (List.existsb p (to_list (or_of_imp a))); auto. rewrite existsb_exists. intros [x [H4 H5]]. apply In_to_list in H4. destruct H4 as [i [H4 ->]]. - case_eq (i < PArray.length a - 1); intro Heq. + case_eq (i if Lit.is_pos l then C._true - else if PArray.length args == 0 then C._true + else if PArray.length args =? 0 then C._true else let args := or_of_imp args in l :: to_list args @@ -193,7 +193,7 @@ Section CHECKER. if Lit.is_pos l then to_list args else C._true | Fimp args => - if PArray.length args == 0 then C._true else + if PArray.length args =? 0 then C._true else if Lit.is_pos l then let args := or_of_imp args in to_list args @@ -271,15 +271,15 @@ Section CHECKER. let x := Lit.blit l in match get_hash x with | For args => - if i < PArray.length args then Lit.lit x::Lit.neg (args.[i])::nil + if i - if i < PArray.length args then Lit.nlit x::(args.[i])::nil + if i let len := PArray.length args in - if i < len then - if i == len - 1 then Lit.lit x::Lit.neg (args.[i])::nil + if i C._true @@ -297,15 +297,15 @@ Section CHECKER. let x := Lit.blit l in match get_hash x with | For args => - if (i < PArray.length args) && negb (Lit.is_pos l) then Lit.neg (args.[i])::nil + if (i - if (i < PArray.length args) && (Lit.is_pos l) then (args.[i])::nil + if (i let len := PArray.length args in - if (i < len) && negb (Lit.is_pos l) then - if i == len - 1 then Lit.neg (args.[i])::nil + if (i C._true @@ -362,7 +362,7 @@ Section CHECKER. tauto_check). - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r. - rewrite afold_left_or, orb_comm;apply orb_negb_r. - - case_eq (PArray.length a == 0); auto using C.interp_true. + - case_eq (PArray.length a =? 0); auto using C.interp_true. intro Hl; simpl. unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl. rewrite (afold_right_impb (Lit.interp_neg _) Hl), orb_comm;try apply orb_negb_r. @@ -381,7 +381,7 @@ Section CHECKER. Proof. unfold check_BuildProj,C.valid;intros l i. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; - case_eq (i < PArray.length a);intros Hlt;auto using C.interp_true;simpl. + case_eq (i ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + assert (H1: i ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. Qed. End CHECKER. diff --git a/src/euf/Euf.v b/src/euf/Euf.v index 6b97f94..fae0cfd 100644 --- a/src/euf/Euf.v +++ b/src/euf/Euf.v @@ -40,23 +40,23 @@ Section certif. | nil => let xres := Lit.blit res in get_eq xres (fun t1' t2' => - if ((t1 == t1') && (t2 == t2')) || - ((t1 == t2') && (t2 == t1')) then + if ((t1 =? t1') && (t2 =? t2')) || + ((t1 =? t2') && (t2 =? t1')) then Lit.lit xres :: clause else C._true) | leq::eqs => let xeq := Lit.blit leq in get_eq xeq (fun t t' => - if t2 == t' then + if t2 =? t' then check_trans_aux t1 t eqs res (Lit.nlit xeq :: clause) else - if t2 == t then + if t2 =? t then check_trans_aux t1 t' eqs res (Lit.nlit xeq :: clause) else - if t1 == t' then + if t1 =? t' then check_trans_aux t t2 eqs res (Lit.nlit xeq :: clause) else - if t1 == t then + if t1 =? t then check_trans_aux t' t2 eqs res (Lit.nlit xeq :: clause) else C._true) end. @@ -66,7 +66,7 @@ Section certif. | nil => let xres := Lit.blit res in get_eq xres (fun t1 t2 => - if t1 == t2 then Lit.lit xres :: nil else C._true) + if t1 =? t2 then Lit.lit xres :: nil else C._true) | leq :: eqs => let xeq := Lit.blit leq in get_eq xeq @@ -79,12 +79,12 @@ Section certif. | nil, nil, nil => c | eq::eqs, t1::l, t2::r => match eq with - | None => if t1 == t2 then build_congr eqs l r c else C._true + | None => if t1 =? t2 then build_congr eqs l r c else C._true | Some leq => let xeq := Lit.blit leq in get_eq xeq (fun t1' t2' => - if ((t1 == t1') && (t2 == t2')) || - ((t1 == t2') && (t2 == t1')) then + if ((t1 =? t1') && (t2 =? t2')) || + ((t1 =? t2') && (t2 =? t1')) then build_congr eqs l r (Lit.nlit xeq :: c) else C._true) end @@ -104,7 +104,7 @@ Section certif. build_congr eqs (a::nil) (b::nil) (Lit.lit xeq :: nil) else C._true | Atom.Aapp f1 args1, Atom.Aapp f2 args2 => - if f1 == f2 then build_congr eqs args1 args2 (Lit.lit xeq :: nil) + if f1 =? f2 then build_congr eqs args1 args2 (Lit.lit xeq :: nil) else C._true | _, _ => C._true end). @@ -126,7 +126,7 @@ Section certif. (a::nil) (b::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil) else C._true | Atom.Aapp p a, Atom.Aapp p' b => - if p == p' then + if p =? p' then build_congr eqs a b (Lit.nlit xPA :: Lit.lit xPB :: nil) else C._true | _, _ => C._true @@ -215,7 +215,7 @@ Section certif. destruct b;trivial with smtcoq_euf. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite Misc.aforallbi_spec;intros. - assert (i < length t_atom). + assert (i - if PArray.length a == 3 then + if PArray.length a =? 3 then let a_eq_b := a.[0] in let not_a_le_b := a.[1] in let not_b_le_a := a.[2] in get_eq a_eq_b (fun a b => get_not_le not_a_le_b (fun a' b' => get_not_le not_b_le_a (fun b'' a'' => - if (a == a') && (a == a'') && (b == b') && (b == b'') + if (a =? a') && (a =? a'') && (b =? b') && (b =? b'') then (Lit.lit (Lit.blit l))::nil else - if (a == b') && (a == b'') && (b == a') && (b == a'') + if (a =? b') && (a =? b'') && (b =? a') && (b =? a'') then (Lit.lit (Lit.blit l))::nil else C._true))) else C._true @@ -668,7 +668,7 @@ Section certif. Lemma build_pexpr_atom_aux_correct : forall (build_pexpr : vmap -> hatom -> vmap * PExpr Z) h i, (forall h' vm vm' pe, - h' < h -> + h' Typ.eqb (get_type t_i t_func t_atom h') Typ.TZ -> build_pexpr vm h' = (vm',pe) -> wf_vmap vm -> @@ -681,7 +681,7 @@ Section certif. bounded_pexpr (fst vm') pe /\ t_interp.[h'] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe))-> forall a vm vm' pe, - h < i -> + h lt_atom h a -> check_atom a Typ.TZ -> build_pexpr_atom_aux build_pexpr vm a = (vm',pe) -> @@ -933,7 +933,7 @@ Transparent build_z_atom. t_interp.[h] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). Proof. intros. - case_eq (h < length t_atom);intros. + case_eq (h forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem + if forallb2 (fun id c => forallb2 (fun i j => i =? j) (S.get s id) (S.sort_uniq c)) prem_id prem then concl else C._true. @@ -89,7 +89,7 @@ Section Checker_correct. t_form). Lemma interp_check_clause c1 : forall c2, - forallb2 (fun i j => i == j) c1 c2 -> C.interp rho c1 = C.interp rho c2. + forallb2 (fun i j => i =? j) c1 c2 -> C.interp rho c1 = C.interp rho c2. Proof. induction c1 as [ |l1 c1 IHc1]; simpl; intros [ |l2 c2]; simpl; auto; try discriminate. unfold is_true. rewrite andb_true_iff. intros [H1 H2]. @@ -97,7 +97,7 @@ Section Checker_correct. Qed. Lemma valid_check_clause cid c : - forallb2 (fun i j => i == j) (S.get s cid) (S.sort_uniq c) -> + forallb2 (fun i j => i =? j) (S.get s cid) (S.sort_uniq c) -> interp_uf rho c. Proof. intro H. rewrite <- interp_equiv, <- S.sort_uniq_correct; auto. @@ -131,7 +131,7 @@ Section Checker_correct. - unfold C.valid. now rewrite interp_equiv. - now apply C.interp_true. - now apply C.interp_true. - - case_eq (forallb2 (fun i j => i == j) (S.get s pid) (S.sort_uniq p)); + - case_eq (forallb2 (fun i j => i =? j) (S.get s pid) (S.sort_uniq p)); simpl; intro Heq; [ |now apply C.interp_true]. apply IHpids. apply H. apply (valid_check_clause _ _ Heq). Qed. diff --git a/src/spl/Operators.v b/src/spl/Operators.v index 540de3f..95bbe8e 100644 --- a/src/spl/Operators.v +++ b/src/spl/Operators.v @@ -35,7 +35,7 @@ Section Operators. Fixpoint check_in x l := match l with | nil => false - | t::q => if x == t then true else check_in x q + | t::q => if x =? t then true else check_in x q end. @@ -43,7 +43,7 @@ Section Operators. Proof. intro x; induction l as [ |t q IHq]; simpl. split; intro H; try discriminate; elim H. - case_eq (x == t). + case_eq (x =? t). rewrite eqb_spec; intro; subst t; split; auto. intro H; rewrite IHq; split; auto; intros [H1|H1]; auto; rewrite H1, eqb_refl in H; discriminate. Qed. @@ -54,7 +54,7 @@ Section Operators. | nil => true | b::q => if aexistsbi (fun _ (x:option (int*int)) => match x with - | Some (a',b') => ((a == a') && (b == b')) || ((a == b') && (b == a')) + | Some (a',b') => ((a =? a') && (b =? b')) || ((a =? b') && (b =? a')) | None => false end ) t then check_diseqs_complete_aux a q t else false @@ -63,13 +63,13 @@ Section Operators. Lemma check_diseqs_complete_aux_spec : forall a dist t, check_diseqs_complete_aux a dist t = true <-> - forall y, In y dist -> exists i, i < length t /\ + forall y, In y dist -> exists i, i match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t); try discriminate; rewrite aexistsbi_spec; intros [i [H1 H2]]; rewrite IHq; clear IHq; intros H3 y [H4|H4]; auto; subst y; exists i; split; auto; generalize H2; case (t .[ i]); try discriminate; intros [a' b']; rewrite orb_true_iff, !andb_true_iff, !Int63.eqb_spec; intros [[H4 H5]|[H4 H5]]; subst a' b'; auto. - intro H1; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t). + case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t); try discriminate; rewrite aexistsbi_spec; intros [i [H1 H2]]; rewrite IHq; clear IHq; intros H3 y [H4|H4]; auto; subst y; exists i; split; auto; generalize H2; case (t .[ i]); try discriminate; intros [a' b']; rewrite orb_true_iff, !andb_true_iff, !Int63.eqb_spec; intros [[H4 H5]|[H4 H5]]; subst a' b'; auto. + intro H1; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t). intros _; rewrite IHq; clear IHq; intros y Hy; apply H1; auto. rewrite aexistsbi_false_spec; destruct (H1 b (or_introl (refl_equal b))) as [i [H2 H3]]; intro H; rewrite <- (H _ H2); destruct H3 as [H3|H3]; rewrite H3; rewrite !eqb_refl; auto; rewrite orb_true_r; auto. Qed. @@ -77,15 +77,15 @@ Section Operators. Lemma check_diseqs_complete_aux_false_spec : forall a dist t, check_diseqs_complete_aux a dist t = false <-> - exists y, In y dist /\ forall i, i < length t -> + exists y, In y dist /\ forall i, i (t.[i] <> Some (a,y) /\ t.[i] <> Some (y,a)). Proof. intros a dist t; induction dist as [ |b q IHq]; simpl; split; try discriminate. intros [y [H _]]; elim H. - case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t). + case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t). intros _; rewrite IHq; clear IHq; intros [y [H3 H4]]; exists y; auto. rewrite aexistsbi_false_spec; intros H _; exists b; split; auto; intros i Hi; split; intro H1; generalize (H _ Hi); rewrite H1, !eqb_refl; try discriminate; rewrite orb_true_r; discriminate. - intros [y [H1 H2]]; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t); auto; rewrite aexistsbi_spec; intros [i [H3 H4]]; rewrite IHq; clear IHq; exists y; destruct H1 as [H1|H1]; auto; subst y; case_eq (t.[i]); [intros [a' b'] Heq|intro Heq]; rewrite Heq in H4; try discriminate; rewrite orb_true_iff, !andb_true_iff, !eqb_spec in H4; destruct H4 as [[H4 H5]|[H4 H5]]; subst a' b'; generalize (H2 _ H3); rewrite Heq; intros [H4 H5]; [elim H4|elim H5]; auto. + intros [y [H1 H2]]; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t); auto; rewrite aexistsbi_spec; intros [i [H3 H4]]; rewrite IHq; clear IHq; exists y; destruct H1 as [H1|H1]; auto; subst y; case_eq (t.[i]); [intros [a' b'] Heq|intro Heq]; rewrite Heq in H4; try discriminate; rewrite orb_true_iff, !andb_true_iff, !eqb_spec in H4; destruct H4 as [[H4 H5]|[H4 H5]]; subst a' b'; generalize (H2 _ H3); rewrite Heq; intros [H4 H5]; [elim H4|elim H5]; auto. Qed. @@ -98,7 +98,7 @@ Section Operators. Lemma check_diseqs_complete_spec : forall dist t, check_diseqs_complete dist t = true <-> - forall x y, In2 x y dist -> exists i, i < length t /\ + forall x y, In2 x y dist -> exists i, i - exists x y, In2 x y dist /\ forall i, i < length t -> + exists x y, In2 x y dist /\ forall i, i (t.[i] <> Some (x,y) /\ t.[i] <> Some (y,x)). Proof. intros dist t; induction dist as [ |a q IHq]; simpl; split; try discriminate. @@ -135,7 +135,7 @@ Section Operators. | Fatom a => match get_atom a with | Atom.Abop (Atom.BO_eq A) h1 h2 => - if (Typ.eqb ty A) && (negb (h1 == h2)) && (check_in h1 dist) && (check_in h2 dist) then + if (Typ.eqb ty A) && (negb (h1 =? h2)) && (check_in h1 dist) && (check_in h2 dist) then Some (h1,h2) else None @@ -150,14 +150,14 @@ Section Operators. Lemma check_diseqs_spec : forall A dist diseq, check_diseqs A dist diseq = true <-> - ((forall i, i < length diseq -> + ((forall i, i let t := diseq.[i] in ~ Lit.is_pos t /\ exists a, get_form (Lit.blit t) = Fatom a /\ exists h1 h2, get_atom a = Atom.Abop (Atom.BO_eq A) h1 h2 /\ h1 <> h2 /\ (In2 h1 h2 dist \/ In2 h2 h1 dist)) /\ - (forall x y, In2 x y dist -> exists i, i < length diseq /\ + (forall x y, In2 x y dist -> exists i, i *) (* match get_atom a with *) (* | Atom.Abop (Atom.BO_eq A) h1 h2 => *) - (* (Typ.eqb ty A) && (negb (h1 == h2)) && (check_in h1 dist) && (check_in h2 dist) *) + (* (Typ.eqb ty A) && (negb (h1 =? h2)) && (check_in h1 dist) && (check_in h2 dist) *) (* | _ => false *) (* end *) (* | _ => false *) @@ -195,7 +195,7 @@ intros. destruct H0; now contradict H0. (* Lemma check_diseqs_spec : forall A dist diseq, *) - (* check_diseqs A dist diseq <-> forall i, i < length diseq -> *) + (* check_diseqs A dist diseq <-> forall i, i *) (* let t := diseq.[i] in *) (* ~ Lit.is_pos t /\ *) (* exists a, get_form (Lit.blit t) = Fatom a /\ *) @@ -204,7 +204,7 @@ intros. destruct H0; now contradict H0. (* Proof. *) (* intros A dist diseq; unfold check_diseqs; unfold is_true at 1; rewrite PArray.forallb_spec; split. *) (* intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try discriminate; case (get_form (Lit.blit (diseq .[ i]))); try discriminate; intros a H1; split; try discriminate; exists a; split; auto; generalize H1; clear H1; case (get_atom a); try discriminate; intros [ | | | | | | |B] h1 h2; try discriminate; rewrite !andb_true_iff; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; intros [[[H1 H4] H2] H3]; change (is_true (Typ.eqb A B)) in H1; rewrite Typ.eqb_spec in H1; subst B; exists h1; exists h2; split; auto; assert (H5: h1 <> h2) by (intro H; rewrite H, eqb_refl in H4; discriminate); split; auto; rewrite <- In2_In; auto. *) - (* intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try (intros [H _]; elim H; reflexivity); intros [_ [a [H1 [h1 [h2 [H2 [H3 H4]]]]]]]; rewrite H1, H2; rewrite !andb_true_iff; rewrite <- (In2_In H3) in H4; destruct H4 as [H4 H5]; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; repeat split; auto; case_eq (h1 == h2); auto; try (rewrite Typ.eqb_refl; auto); rewrite eqb_spec; intro; subst h1; elim H3; auto. *) + (* intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try (intros [H _]; elim H; reflexivity); intros [_ [a [H1 [h1 [h2 [H2 [H3 H4]]]]]]]; rewrite H1, H2; rewrite !andb_true_iff; rewrite <- (In2_In H3) in H4; destruct H4 as [H4 H5]; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; repeat split; auto; case_eq (h1 =? h2); auto; try (rewrite Typ.eqb_refl; auto); rewrite eqb_spec; intro; subst h1; elim H3; auto. *) (* Qed. *) @@ -231,7 +231,7 @@ intros. destruct H0; now contradict H0. match get_form f1, get_form f2 with | Fatom ha, Fatom hb => match get_atom ha, get_atom hb with - | Atom.Anop (Atom.NO_distinct ty) (x::y::nil), Atom.Abop (Atom.BO_eq ty') x' y' => (Typ.eqb ty ty') && (((x == x') && (y == y')) || ((x == y') && (y == x'))) + | Atom.Anop (Atom.NO_distinct ty) (x::y::nil), Atom.Abop (Atom.BO_eq ty') x' y' => (Typ.eqb ty ty') && (((x =? x') && (y =? y')) || ((x =? y') && (y =? x'))) | _, _ => false end | _, _ => false @@ -287,12 +287,12 @@ intros. destruct H0; now contradict H0. Proof. intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H2]]]; rewrite check_diseqs_spec in H2; destruct H2 as [H2 H3]; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. intros l H4; case_eq (distinct (Typ.i_eqb t_i A) (rev l)). - rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by exact Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H11: a < length t_atom). - case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H11; rewrite (get_outofbound _ _ _ H11) in H6; rewrite default_t_atom in H6; inversion H6. + rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by exact Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H11: a rho f1 = negb (rho f2). Proof. - intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 < length t_form) by (case_eq (f1 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); assert (H6: f2 < length t_form) by (case_eq (f2 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H2; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H7: hb < length t_atom) by (case_eq (hb < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H4; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate); generalize (wt_t_atom _ H7); rewrite H4; simpl; case (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) hb); try discriminate; simpl; rewrite andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A)); rewrite !Typ.eqb_spec; intros [H8 H9]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom x), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom y); rewrite H8, H9; intros [v1 HH1] [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; auto with smtcoq_spl_op smtcoq_core; rewrite Typ.i_eqb_sym; auto with smtcoq_spl_op smtcoq_core. + intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 afold_left bool int true andb (Lit.interp rho) diseq. *) (* Proof. *) (* intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H]]]; rewrite check_diseqs_spec in H; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. *) - (* intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H10: a < length t_atom). *) - (* case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H10; rewrite (get_outofbound _ _ _ H10) in H6; rewrite default_t_atom in H6; inversion H6. *) + (* intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H10: a var -> bool. Definition check_lit l1 l2 := - (l1 == l2) || ((Bool.eqb (Lit.is_pos l1) (Lit.is_pos l2)) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((Bool.eqb (Lit.is_pos l1) (negb (Lit.is_pos l2))) && (check_distinct_two_args (Lit.blit l1) (Lit.blit l2))). + (l1 =? l2) || ((Bool.eqb (Lit.is_pos l1) (Lit.is_pos l2)) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((Bool.eqb (Lit.is_pos l1) (negb (Lit.is_pos l2))) && (check_distinct_two_args (Lit.blit l1) (Lit.blit l2))). (* Definition check_lit l1 l2 := *) - (* (l1 == l2) || ((Lit.is_pos l1) && (Lit.is_pos l2) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((negb (Lit.is_pos l1)) && (negb (Lit.is_pos l2)) && (check_var (Lit.blit l2) (Lit.blit l1))). *) + (* (l1 =? l2) || ((Lit.is_pos l1) && (Lit.is_pos l2) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((negb (Lit.is_pos l1)) && (negb (Lit.is_pos l2)) && (check_var (Lit.blit l2) (Lit.blit l1))). *) Definition check_form_aux a b := match a, b with | Fatom ha, Fand diseq => check_distinct ha diseq - | Fatom a, Fatom b => a == b + | Fatom a, Fatom b => a =? b | Ftrue, Ftrue => true | Ffalse, Ffalse => true - | Fnot2 i1 l1, Fnot2 i2 l2 => (i1 == i2) && (check_lit l1 l2) - | Fand a1, Fand a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) - | For a1, For a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) - | Fimp a1, Fimp a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) - (* (length a1 == length a2) && (aforallbi (fun i l => if i < length a1 - 1 then check_lit (a2.[i]) l else check_lit l (a2.[i])) a1) *) + | Fnot2 i1 l1, Fnot2 i2 l2 => (i1 =? i2) && (check_lit l1 l2) + | Fand a1, Fand a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) + | For a1, For a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) + | Fimp a1, Fimp a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) + (* (length a1 =? length a2) && (aforallbi (fun i l => if i check_lit l1 j1 && check_lit l2 j2 (* check_lit l1 j1 && check_lit j1 l1 && check_lit l2 j2 && check_lit j2 l2 *) (* (* let a := check_lit l1 j1 in *) *) @@ -450,16 +450,16 @@ intros. destruct H0; now contradict H0. (* rewrite <- H1; eauto with smtcoq_core. *) (* eapply interp_check_lit; eauto with smtcoq_core. *) (* (* Implication *) *) - (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite aforallbi_spec in H2; intro H3; apply afold_right_implb_true; case_eq (length a1 == 0); intro Heq. *) + (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite aforallbi_spec in H2; intro H3; apply afold_right_implb_true; case_eq (length a1 =? 0); intro Heq. *) (* left; rewrite eqb_spec in Heq; rewrite <- H1; auto with smtcoq_core. *) (* destruct (afold_right_implb_true_inv _ _ _ H3) as [H4|[[i [H4 H5]]|H4]]. *) (* rewrite H4 in Heq; discriminate. *) - (* right; left; exists i; rewrite <- H1; split; auto with smtcoq_core; case_eq (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; intro H6; assert (H7: i < length a1 = true). *) + (* right; left; exists i; rewrite <- H1; split; auto with smtcoq_core; case_eq (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; intro H6; assert (H7: i (i < length a2 - 1) && (negb (Lit.interp rho l))) a2). *) + (* right; case_eq (aexistsbi (fun i l => (i (h1 == h2) || check_form_aux cont (get_form h1) (get_form h2)) + (fun _ cont h1 h2 => (h1 =? h2) || check_form_aux cont (get_form h1) (get_form h2)) 0 (PArray.length t_form) (fun h1 h2 => false) h1 h2. Definition check_form := check_form_aux check_hform. diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v index eb512ee..ea55500 100644 --- a/src/spl/Syntactic.v +++ b/src/spl/Syntactic.v @@ -77,7 +77,7 @@ Section CheckAtom. match o1, o2 with | NO_distinct t1, NO_distinct t2 => Typ.eqb t1 t2 && list_beq check_hatom l1 l2 end - | Aapp f1 aargs, Aapp f2 bargs =>(f1 == f2) && list_beq check_hatom aargs bargs + | Aapp f1 aargs, Aapp f2 bargs =>(f1 =? f2) && list_beq check_hatom aargs bargs | _, _ => false end. @@ -191,7 +191,7 @@ Section CheckAtom. Definition check_hatom h1 h2 := foldi - (fun _ cont h1 h2 => (h1 == h2) || check_atom_aux cont (t_atom.[h1]) (t_atom.[h2])) + (fun _ cont h1 h2 => (h1 =? h2) || check_atom_aux cont (t_atom.[h1]) (t_atom.[h2])) 0 (PArray.length t_atom) (fun h1 h2 => false) h1 h2. Definition check_atom := check_atom_aux check_hatom. @@ -269,7 +269,7 @@ Section CheckAtom. | Val _ _, Val _ _ => False end. Proof. - unfold wt; unfold is_true at 1; rewrite aforallbi_spec; intros Hwt Hwf Hdef h1 h2; unfold check_neg_hatom; case_eq (get_atom h1); try discriminate; intros b1 t11 t12 H1; case_eq (get_atom h2); try discriminate; intros b2 t21 t22 H2; assert (H7: h1 < length t_atom) by (apply PArray.get_not_default_lt; rewrite H1, Hdef; discriminate); generalize (Hwt _ H7); rewrite H1; simpl; generalize H1; case b1; try discriminate; clear H1 b1; simpl; intro H1; case (get_type' t_i (t_interp t_i t_func t_atom) h1); try discriminate; simpl; rewrite andb_true_iff; intros [H30 H31]; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t11) Typ.TZ)) in H30; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t12) Typ.TZ)) in H31; rewrite Typ.eqb_spec in H30, H31; generalize (check_aux_interp_hatom _ t_func _ Hwf t11), (check_aux_interp_hatom _ t_func _ Hwf t12); rewrite H30, H31; intros [v1 Hv1] [v2 Hv2]; generalize H2; case b2; try discriminate; clear H2 b2; intro H2; unfold is_true; rewrite andb_true_iff; intros [H3 H4]; generalize (check_hatom_correct Hwf Hdef _ _ H3), (check_hatom_correct Hwf Hdef _ _ H4); unfold interp_hatom; intros H5 H6; rewrite t_interp_wf; auto; rewrite H1; simpl; rewrite Hv1, Hv2; simpl; rewrite t_interp_wf; auto; rewrite H2; simpl; rewrite <- H5; rewrite <- H6, Hv1, Hv2; simpl. + unfold wt; unfold is_true at 1; rewrite aforallbi_spec; intros Hwt Hwf Hdef h1 h2; unfold check_neg_hatom; case_eq (get_atom h1); try discriminate; intros b1 t11 t12 H1; case_eq (get_atom h2); try discriminate; intros b2 t21 t22 H2; assert (H7: h1 check_atom a1 a2 | Ftrue, Ftrue => true @@ -371,7 +371,7 @@ Section FLATTEN. | Fxor l1 l2, Fxor lf1 lf2 => frec l1 lf1 && frec l2 lf2 | Fimp args1, Fimp args2 => - if PArray.length args1 == PArray.length args2 then + if PArray.length args1 =? PArray.length args2 then aforallbi (fun i l => frec l (args2.[i])) args1 else false | Fiff l1 l2, Fiff lf1 lf2 => -- cgit