diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Conversion_tactics.v | 14 | ||||
-rw-r--r-- | src/Misc.v | 6 | ||||
-rw-r--r-- | src/SMT_terms.v | 14 | ||||
-rw-r--r-- | src/lia/Lia.v | 5 | ||||
-rw-r--r-- | src/trace/coqTerms.ml | 5 |
5 files changed, 20 insertions, 24 deletions
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index 7109b11..3972ecb 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -6,14 +6,6 @@ Require Import ZArith. (********************************************************************) (********************************************************************) -(* SMTCoq utilise Zeq_bool *) -Lemma Zeq_bool_Zeqb a b : Z.eqb a b = Zeq_bool a b. -Proof. - case_eq (a =? b)%Z. - - rewrite Z.eqb_eq. intros ->. symmetry. now rewrite <- Zeq_is_eq_bool. - - rewrite Z.eqb_neq. intro H. case_eq (Zeq_bool a b); auto. now rewrite <- Zeq_is_eq_bool. -Qed. - (* Généralise fun x => f (g x) *) Ltac generalize_fun f g := repeat @@ -92,7 +84,7 @@ Ltac pos_rewriting := | |-context [Pos.mul (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.mul (Z2Pos X) (Z2Pos Y)) with (Z2Pos (X * Y)) | |-context [Pos.ltb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.ltb (Z2Pos X) (Z2Pos Y)) with (Z.ltb X Y) | |-context [Pos.leb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.leb (Z2Pos X) (Z2Pos Y)) with (Z.leb X Y) - | |-context [Pos.eqb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.eqb (Z2Pos X) (Z2Pos Y)) with (Z.eqb X Y);rewrite Zeq_bool_Zeqb + | |-context [Pos.eqb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.eqb (Z2Pos X) (Z2Pos Y)) with (Z.eqb X Y) end. (* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *) @@ -184,7 +176,7 @@ Ltac N_rewriting := | |-context [N.mul (Z2N ?X) (Z2N ?Y) ] => replace (N.mul (Z2N X) (Z2N Y)) with (Z2N (X * Y)) by (apply Z2N.inj_mul; N_solve_pos) | |-context [N.ltb (Z2N ?X) (Z2N ?Y) ] => replace (N.ltb (Z2N X) (Z2N Y)) with (Z.ltb X Y) by (apply N_inj_ltb; N_solve_pos) | |-context [N.leb (Z2N ?X) (Z2N ?Y) ] => replace (N.leb (Z2N X) (Z2N Y)) with (Z.leb X Y) by (apply N_inj_leb; N_solve_pos) - | |-context [N.eqb (Z2N ?X) (Z2N ?Y) ] => replace (N.eqb (Z2N X) (Z2N Y)) with (Z.eqb X Y) by (apply N_inj_eqb; N_solve_pos);rewrite Zeq_bool_Zeqb + | |-context [N.eqb (Z2N ?X) (Z2N ?Y) ] => replace (N.eqb (Z2N X) (Z2N Y)) with (Z.eqb X Y) by (apply N_inj_eqb; N_solve_pos) end. (* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *) @@ -278,7 +270,7 @@ Ltac nat_rewriting := | |-context [Nat.mul (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.mul (Z2Nat X) (Z2Nat Y)) with (Z2Nat (X * Y)) by (apply Z2Nat.inj_mul; nat_solve_pos) | |-context [Nat.ltb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.ltb (Z2Nat X) (Z2Nat Y)) with (Z.ltb X Y) by (apply nat_inj_ltb; nat_solve_pos) | |-context [Nat.leb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.leb (Z2Nat X) (Z2Nat Y)) with (Z.leb X Y) by (apply nat_inj_leb; nat_solve_pos) - | |-context [Nat.eqb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.eqb (Z2Nat X) (Z2Nat Y)) with (Z.eqb X Y) by (apply nat_inj_eqb; nat_solve_pos);rewrite Zeq_bool_Zeqb + | |-context [Nat.eqb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.eqb (Z2Nat X) (Z2Nat Y)) with (Z.eqb X Y) by (apply nat_inj_eqb; nat_solve_pos) end. (* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *) @@ -1008,3 +1008,9 @@ Implicit Arguments forallb2 [A B]. coq-load-path: ((rec "." "SMTCoq")) End: *) + +Lemma neg_eq_true_eq_false b : b = false <-> b <> true. +Proof. destruct b; intuition. Qed. + +Lemma is_true_iff e : e = true <-> is_true e. +Proof. now unfold is_true. Qed. diff --git a/src/SMT_terms.v b/src/SMT_terms.v index a99c158..42b1314 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -302,7 +302,7 @@ Module Typ. Definition i_eqb (t:type) : interp t -> interp t -> bool := match t with | Tindex i => (t_i.[i]).(te_eqb) - | TZ => Zeq_bool + | TZ => Z.eqb | Tbool => Bool.eqb | Tpositive => Peqb end. @@ -311,7 +311,7 @@ Module Typ. Proof. destruct t;simpl;intros. symmetry;apply reflect_iff;apply te_reflect. - symmetry;apply Zeq_is_eq_bool. + apply Z.eqb_eq. apply Bool.eqb_true_iff. apply Peqb_eq. Qed. @@ -321,11 +321,11 @@ Module Typ. intros;apply iff_reflect;symmetry;apply i_eqb_spec. Qed. - Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x. - Proof. - intros t x y; case_eq (i_eqb t x y); case_eq (i_eqb t y x); auto. - change (i_eqb t x y = true) with (is_true (i_eqb t x y)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H1; discriminate|elim H2; auto]. - change (i_eqb t y x = true) with (is_true (i_eqb t y x)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H2; discriminate|elim H1; auto]. + Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x. + Proof. + intros t x y; case_eq (i_eqb t x y); intro H1; symmetry; + [ | rewrite neg_eq_true_eq_false in *; intro H2; apply H1]; + rewrite is_true_iff in *; now rewrite i_eqb_spec in *. Qed. End Interp_Equality. diff --git a/src/lia/Lia.v b/src/lia/Lia.v index d8e89f3..dbd3b9c 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -1006,7 +1006,8 @@ Transparent build_z_atom. symmetry;apply Zgt_is_gt_bool. destruct t0;inversion H13;clear H13;subst. simpl. - symmetry;apply (Zeq_is_eq_bool (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). + apply (Z.eqb_eq (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). + Qed. Lemma build_formula_correct : @@ -1474,7 +1475,7 @@ Transparent build_z_atom. case_eq (vb <=? va); intros; subst. apply Zle_bool_imp_le in H2. apply Zle_bool_imp_le in H3. - apply Zeq_bool_neq in H. + apply Z.eqb_neq in H. (*pour la beauté du geste!*) lia. rewrite H3 in H1; simpl in H1; elim diff_true_false; trivial. rewrite H2 in H0; simpl in H1; elim diff_true_false; trivial. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 6c76f9d..1874d5f 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -52,10 +52,7 @@ let cltb = gen_constant z_modules "ltb" let cleb = gen_constant z_modules "leb" let cgeb = gen_constant z_modules "geb" let cgtb = gen_constant z_modules "gtb" -(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec - Z.eqb *) -(* let ceqbZ = gen_constant z_modules "eqb" *) -let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool" +let ceqbZ = gen_constant z_modules "eqb" (* Booleans *) let bool_modules = [["Coq";"Bool";"Bool"]] |