From dc786cea07fc7c2f9323d57a60d4731ebe97a577 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 30 Jun 2020 15:49:07 +0200 Subject: Remove one axiom --- src/Misc.v | 18 ++++++ src/cnf/Cnf.v | 202 ++++++++++++++++++++++++++++++++++++++++++---------------- 2 files changed, 165 insertions(+), 55 deletions(-) (limited to 'src') diff --git a/src/Misc.v b/src/Misc.v index 24e27c0..66e9b73 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -59,6 +59,18 @@ Proof. Qed. +Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true. +Proof. + intro Hl. rewrite ltb_spec, (to_Z_sub_1 _ 0). + - lia. + - rewrite ltb_spec. rewrite eqb_false_spec in Hl. + assert (0%Z <> [|i|]) + by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto). + destruct (to_Z_bounded i) as [H1 _]. + clear -H H1. change [|0|] with 0%Z. lia. +Qed. + + Lemma foldi_down_ZInd2 : forall A (P: Z -> A -> Prop) (f:int -> A -> A) max min a, (max < min = true -> P ([|min|])%Z a) -> @@ -142,6 +154,12 @@ Proof. unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia. 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). +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]. Proof. diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index d6a6640..23aa979 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import PArray List Bool ZArith. +Require Import PArray List Bool ZArith Psatz. Require Import Misc State SMT_terms BVList. Import Form. @@ -53,6 +53,62 @@ Proof. rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); omega. Qed. +Lemma afold_right_impb p a : + (forall x, p (Lit.neg x) = negb (p x)) -> + (PArray.length a == 0) = false -> + (afold_right bool int true implb p a) = + List.existsb p (to_list (or_of_imp a)). +Proof. + intros Hp Hl. + case_eq (afold_right bool int true implb p a); intro Heq; symmetry. + - apply afold_right_implb_true_inv in Heq. + destruct Heq as [Heq|[[i [Hi Heq]]|Heq]]. + + rewrite Heq in Hl. discriminate. + + rewrite existsb_exists. exists (Lit.neg (a .[ i])). split. + * { + apply (to_list_In_eq _ i). + - rewrite length_or_of_imp. apply (ltb_trans _ (PArray.length a - 1)); auto. + now apply minus_1_lt. + - now rewrite get_or_of_imp. + } + * now rewrite Hp, Heq. + + rewrite existsb_exists. exists (a.[(PArray.length a) - 1]). split. + * { + apply (to_list_In_eq _ (PArray.length a - 1)). + - rewrite length_or_of_imp. + now apply minus_1_lt. + - symmetry. apply get_or_of_imp2; auto. + unfold is_true. rewrite ltb_spec. rewrite eqb_false_spec in Hl. + assert (0%Z <> [|PArray.length a|]) + by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto). + destruct (to_Z_bounded (PArray.length a)) as [H1 _]. + clear -H H1. change [|0|] with 0%Z. lia. + } + * { + apply Heq. now apply minus_1_lt. + } + - apply afold_right_implb_false_inv in Heq. + destruct Heq as [H1 [H2 H3]]. + case_eq (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. + + assert (H6 := H2 _ Heq). now rewrite (get_or_of_imp Heq), Hp, H6 in H5. + + assert (H6:i = PArray.length a - 1). + { + clear -H4 Heq H1. + rewrite length_or_of_imp in H4. + apply to_Z_inj. rewrite (to_Z_sub_1 _ 0); auto. + rewrite ltb_spec in H4; auto. + rewrite ltb_negb_geb in Heq. + case_eq (PArray.length a - 1 <= i); intro H2; rewrite H2 in Heq; try discriminate. + clear Heq. rewrite leb_spec in H2. rewrite (to_Z_sub_1 _ 0) in H2; auto. + lia. + } + rewrite get_or_of_imp2 in H5; auto. + rewrite H6, H3 in H5. discriminate. +Qed. + Section CHECKER. @@ -91,6 +147,7 @@ Section CHECKER. else l :: PArray.to_list args | Fimp args => if Lit.is_pos l then C._true + else if PArray.length args == 0 then C._true else let args := or_of_imp args in l :: PArray.to_list args @@ -128,6 +185,7 @@ Section CHECKER. if Lit.is_pos l then PArray.to_list args else C._true | Fimp args => + if PArray.length args == 0 then C._true else if Lit.is_pos l then let args := or_of_imp args in PArray.to_list args @@ -287,10 +345,6 @@ Section CHECKER. match goal with |- context [Lit.interp rho ?x] => destruct (Lit.interp rho x);trivial end. - Axiom afold_right_impb : forall a, - (afold_right bool int true implb (Lit.interp rho) a) = - C.interp rho (to_list (or_of_imp a)). - Axiom Cinterp_neg : forall cl, C.interp rho (map Lit.neg cl) = negb (forallb (Lit.interp rho) cl). @@ -298,12 +352,15 @@ Section CHECKER. Proof. unfold check_BuildDef,C.valid;intros l. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; - case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; - unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; - tauto_check. - rewrite afold_left_and, Cinterp_neg;apply orb_negb_r. - rewrite afold_left_or, orb_comm;apply orb_negb_r. - rewrite afold_right_impb, orb_comm;apply orb_negb_r. + case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; + try (unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; + tauto_check). + - rewrite afold_left_and, 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. + 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. Qed. Lemma valid_check_BuildDef2 : forall l, C.valid rho (check_BuildDef2 l). @@ -320,30 +377,60 @@ Section CHECKER. 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. - - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. - simpl;rewrite afold_left_and. - case_eq (forallb (Lit.interp rho) (to_list a));trivial. - rewrite forallb_forall;intros Heq;rewrite Heq;trivial. - apply to_list_In; auto. - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. - simpl;rewrite afold_left_or. - - unfold C.interp;case_eq (existsb (Lit.interp rho) (to_list a));trivial. - rewrite <-not_true_iff_false, existsb_exists, Lit.interp_neg. - case_eq (Lit.interp rho (a .[ i]));trivial. - intros Heq Hex;elim Hex;exists (a.[i]);split;trivial. - apply to_list_In; auto. - case_eq (i == PArray.length a - 1);intros Heq;simpl; - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl; - rewrite afold_right_impb; case_eq (C.interp rho (to_list (or_of_imp a)));trivial; - unfold C.interp;rewrite <-not_true_iff_false, existsb_exists; - try rewrite Lit.interp_neg; case_eq (Lit.interp rho (a .[ i]));trivial; - intros Heq' Hex;elim Hex. - exists (a.[i]);split;trivial. - assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq; rewrite <- (get_or_of_imp2 H1 Heq); apply to_list_In; rewrite length_or_of_imp; auto. - exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq';split;trivial. - assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq; 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; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. + simpl;rewrite afold_left_and. + case_eq (forallb (Lit.interp rho) (to_list a));trivial. + rewrite forallb_forall;intros Heq;rewrite Heq;trivial. + apply to_list_In; auto. + - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. + simpl;rewrite afold_left_or. + unfold C.interp;case_eq (existsb (Lit.interp rho) (to_list a));trivial. + rewrite <-not_true_iff_false, existsb_exists, Lit.interp_neg. + case_eq (Lit.interp rho (a .[ i]));trivial. + intros Heq Hex;elim Hex;exists (a.[i]);split;trivial. + apply to_list_In; auto. + - assert (Hl : (PArray.length a == 0) = false) + by (rewrite eqb_false_spec; intro H1; rewrite H1 in Hlt; now elim (ltb_0 i)). + case_eq (i == PArray.length a - 1);intros Heq;simpl; + rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl. + + rewrite Lit.interp_neg, orb_false_r. + rewrite (afold_right_impb (Lit.interp_neg _) Hl). + case_eq (Lit.interp rho (a .[ i])); intro Hi. + * rewrite orb_false_r, existsb_exists. + exists (a .[ i]). split; auto. + { + apply (to_list_In_eq _ i). + - now rewrite length_or_of_imp. + - symmetry. apply get_or_of_imp2. + + clear -Hl. rewrite eqb_false_spec in Hl. + unfold is_true. rewrite ltb_spec. change [|0|] with 0%Z. + assert (H:[|PArray.length a|] <> 0%Z) + by (intro H; apply Hl; now apply to_Z_inj). + destruct (to_Z_bounded (PArray.length a)) as [H1 _]. + lia. + + now rewrite Int63Properties.eqb_spec in Heq. + } + * now rewrite orb_true_r. + + rewrite orb_false_r. + case_eq (Lit.interp rho (a .[ i])); intro Hi. + * now rewrite orb_true_r. + * rewrite (afold_right_impb (Lit.interp_neg _) Hl). + rewrite orb_false_r, existsb_exists. + exists (Lit.neg (a .[ i])). + { + split. + - apply (to_list_In_eq _ i). + + now rewrite length_or_of_imp. + + symmetry. apply get_or_of_imp. + clear -Hlt Heq. + unfold is_true. rewrite ltb_spec. rewrite (to_Z_sub_1 _ i); auto. + rewrite eqb_false_spec in Heq. + assert (H:[|i|] <> ([|PArray.length a|] - 1)%Z) + by (intro H; apply Heq, to_Z_inj; rewrite (to_Z_sub_1 _ i); auto). + clear Heq. + rewrite ltb_spec in Hlt. lia. + - now rewrite Lit.interp_neg, Hi. + } Qed. Hypothesis Hs : S.valid rho s. @@ -358,9 +445,11 @@ Section CHECKER. destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; tauto_check. - rewrite afold_left_and, Cinterp_neg, orb_false_r;trivial. - rewrite afold_left_or, orb_false_r;trivial. - rewrite afold_right_impb, orb_false_r;trivial. + - rewrite afold_left_and, Cinterp_neg, orb_false_r;trivial. + - rewrite afold_left_or, orb_false_r;trivial. + - case_eq (PArray.length a == 0); auto using C.interp_true. + intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl). + - case_eq (PArray.length a == 0); auto using C.interp_true. Qed. Lemma valid_check_ImmBuildDef2 : forall cid, C.valid rho (check_ImmBuildDef2 cid). @@ -384,23 +473,26 @@ Section CHECKER. case_eq (i < PArray.length a); intros Hlt;auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; rewrite !orb_false_r. - rewrite afold_left_and. - rewrite forallb_forall;intros H;apply H;auto. - apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false, afold_left_or. - unfold C.interp;rewrite existsb_exists, Lit.interp_neg. - case_eq (Lit.interp rho (a .[ i]));trivial. - intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial. - apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false, afold_right_impb. - case_eq (i == PArray.length a - 1);intros Heq';simpl; - unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r, - existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial; - intros Heq2 Hex;elim Hex. - exists (a.[i]);split;trivial. - assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. - exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. - assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; 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; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + - rewrite afold_left_and. + rewrite forallb_forall;intros H;apply H;auto. + apply to_list_In; auto. + - rewrite negb_true_iff, <-not_true_iff_false, afold_left_or. + unfold C.interp;rewrite existsb_exists, Lit.interp_neg. + case_eq (Lit.interp rho (a .[ i]));trivial. + intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial. + apply to_list_In; auto. + - rewrite negb_true_iff, <-not_true_iff_false. + assert (Hl:(PArray.length a == 0) = false) + by (rewrite eqb_false_spec; intro H; rewrite H in Hlt; now apply (ltb_0 i)). + rewrite (afold_right_impb (Lit.interp_neg _) Hl). + case_eq (i == PArray.length a - 1);intros Heq';simpl; + unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r, + existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial; + intros Heq2 Hex;elim Hex. + exists (a.[i]);split;trivial. + assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. + exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. + assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; 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; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. Qed. End CHECKER. -- cgit