From dfff69ef604e02703575cb1cb15b2f77eda5f0f4 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Thu, 28 Mar 2019 15:24:33 +0100 Subject: Re-implementation of zify The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite --- plugins/micromega/ZifyBool.v | 255 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 plugins/micromega/ZifyBool.v (limited to 'plugins/micromega/ZifyBool.v') diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v new file mode 100644 index 0000000000..ec37c2003f --- /dev/null +++ b/plugins/micromega/ZifyBool.v @@ -0,0 +1,255 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 0 <= x <= 1) ; cstr := Z_of_bool_bound}. +Add InjTyp Inj_bool_Z. + +(** Boolean operators *) + +Instance Op_andb : BinOp andb := + { TBOp := Z.min ; + TBOpInj := ltac: (destruct n,m; reflexivity)}. +Add BinOp Op_andb. + +Instance Op_orb : BinOp orb := + { TBOp := Z.max ; + TBOpInj := ltac:(destruct n,m; reflexivity)}. +Add BinOp Op_orb. + +Instance Op_negb : UnOp negb := + { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. +Add UnOp Op_negb. + +Instance Op_eq_bool : BinRel (@eq bool) := + {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. +Add BinRel Op_eq_bool. + +Instance Op_true : CstOp true := + { TCst := 1 ; TCstInj := eq_refl }. + +Instance Op_false : CstOp false := + { TCst := 0 ; TCstInj := eq_refl }. + + +(** Comparisons are encoded using the predicates [isZero] and [isLeZero].*) + +Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0). + +Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0). + +(* Some intermediate lemma *) + +Lemma Z_eqb_isZero : forall n m, + Z_of_bool (n =? m) = isZero (n - m). +Proof. + intros ; unfold isZero. + destruct ( n =? m) eqn:EQ. + - simpl. rewrite Z.eqb_eq in EQ. + rewrite EQ. rewrite Z.sub_diag. + reflexivity. + - + destruct (n - m =? 0) eqn:EQ'. + rewrite Z.eqb_neq in EQ. + rewrite Z.eqb_eq in EQ'. + apply Zminus_eq in EQ'. + congruence. + reflexivity. +Qed. + +Lemma Z_leb_sub : forall x y, x <=? y = ((x - y) <=? 0). +Proof. + intros. + destruct (x <=?y) eqn:B1 ; + destruct (x - y <=?0) eqn:B2 ; auto. + - rewrite Z.leb_le in B1. + rewrite Z.leb_nle in B2. + rewrite Z.le_sub_0 in B2. tauto. + - rewrite Z.leb_nle in B1. + rewrite Z.leb_le in B2. + rewrite Z.le_sub_0 in B2. tauto. +Qed. + +Lemma Z_ltb_leb : forall x y, x isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}. + +Instance Op_Zleb : BinOp Z.leb := + { TBOp := fun x y => isLeZero (x-y) ; + TBOpInj := + ltac: (intros;unfold isLeZero; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_Zleb. + +Instance Op_Zgeb : BinOp Z.geb := + { TBOp := fun x y => isLeZero (y-x) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z.geb_leb; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_Zgeb. + +Instance Op_Zltb : BinOp Z.ltb := + { TBOp := fun x y => isLeZero (x+1-y) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z_ltb_leb; + rewrite <- Z_leb_sub; + reflexivity) }. + +Instance Op_Zgtb : BinOp Z.gtb := + { TBOp := fun x y => isLeZero (y-x+1) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z.gtb_ltb; + rewrite Z_ltb_leb; + rewrite Z_leb_sub; + rewrite Z.add_sub_swap; + reflexivity) }. +Add BinOp Op_Zgtb. + +(** Comparison over nat *) + + +Lemma Z_of_nat_eqb_iff : forall n m, + (n =? m)%nat = (Z.of_nat n =? Z.of_nat m). +Proof. + intros. + rewrite Nat.eqb_compare. + rewrite Z.eqb_compare. + rewrite Nat2Z.inj_compare. + reflexivity. +Qed. + +Lemma Z_of_nat_leb_iff : forall n m, + (n <=? m)%nat = (Z.of_nat n <=? Z.of_nat m). +Proof. + intros. + rewrite Nat.leb_compare. + rewrite Z.leb_compare. + rewrite Nat2Z.inj_compare. + reflexivity. +Qed. + +Lemma Z_of_nat_ltb_iff : forall n m, + (n isZero (Z.sub x y) ; + TBOpInj := ltac:( + intros; simpl; + rewrite <- Z_eqb_isZero; + f_equal; apply Z_of_nat_eqb_iff) }. +Add BinOp Op_nat_eqb. + +Instance Op_nat_leb : BinOp Nat.leb := + { TBOp := fun x y => isLeZero (x-y) ; + TBOpInj := ltac:( + intros; + rewrite Z_of_nat_leb_iff; + unfold isLeZero; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_nat_leb. + +Instance Op_nat_ltb : BinOp Nat.ltb := + { TBOp := fun x y => isLeZero (x+1-y) ; + TBOpInj := ltac:( + intros; + rewrite Z_of_nat_ltb_iff; + unfold isLeZero; + rewrite Z_ltb_leb; + rewrite <- Z_leb_sub; + reflexivity) }. +Add BinOp Op_nat_ltb. + +(** Injected boolean operators *) + +Lemma Z_eqb_ZSpec_ok : forall x, x <> isZero x. +Proof. + intros. + unfold isZero. + destruct (x =? 0) eqn:EQ. + - apply Z.eqb_eq in EQ. + simpl. congruence. + - apply Z.eqb_neq in EQ. + simpl. auto. +Qed. + +Instance Z_eqb_ZSpec : UnOpSpec isZero := + {| UPred := fun n r => n <> r ; USpec := Z_eqb_ZSpec_ok |}. +Add Spec Z_eqb_ZSpec. + +Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0. +Proof. + intros. + unfold isLeZero. + destruct (x <=? 0) eqn:EQ. + - apply Z.leb_le in EQ. + simpl. intuition congruence. + - simpl. + apply Z.leb_nle in EQ. + apply Zorder.Znot_le_gt in EQ. + tauto. +Qed. + +Instance leZeroSpec : UnOpSpec isLeZero := + {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}. +Add Spec leZeroSpec. -- cgit v1.2.3