diff options
| -rw-r--r-- | src/Algebra.v | 73 | ||||
| -rw-r--r-- | src/Tactics/Nsatz.v | 40 |
2 files changed, 104 insertions, 9 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 6dc188e2c..d7b684760 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -225,7 +225,21 @@ Module Group. intros ? Hx Ho. assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity). rewrite Ho, right_identity in Hxo. intuition. - Qed. + Qed. + + Lemma neq_inv_nonzero : forall x, x <> inv x -> x <> id. + Proof. + intros ? Hx Hi; apply Hx. + rewrite Hi. + symmetry; apply inv_id. + Qed. + + Lemma inv_neq_nonzero : forall x, inv x <> x -> x <> id. + Proof. + intros ? Hx Hi; apply Hx. + rewrite Hi. + apply inv_id. + Qed. Section ZeroNeqOne. Context {one} `{is_zero_neq_one T eq id one}. @@ -420,12 +434,22 @@ Module IntegralDomain. Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}. Lemma mul_nonzero_nonzero_cases (x y : T) - : eq (mul x y) zero -> eq x zero \/ eq y zero. + : eq (mul x y) zero -> eq x zero \/ eq y zero. Proof. pose proof mul_nonzero_nonzero x y. destruct (eq_dec x zero); destruct (eq_dec y zero); intuition. Qed. + Lemma mul_nonzero_nonzero_iff (x y : T) + : ~eq (mul x y) zero <-> ~eq x zero /\ ~eq y zero. + Proof. + split. + { intro H0; split; intro H1; apply H0; rewrite H1. + { apply Ring.mul_0_r. } + { apply Ring.mul_0_l. } } + { intros [? ?] ?; edestruct mul_nonzero_nonzero_cases; eauto with nocore. } + Qed. + Global Instance Integral_domain : @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring. @@ -540,6 +564,51 @@ Ltac field_simplify_eq_hyps := Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. +(*** Inequalities over fields *) +Ltac assert_expr_by_nsatz H ty := + let H' := fresh in + rename H into H'; assert (H : ty) + by (try (intro; apply H'); nsatz); + clear H'. +Ltac test_not_constr_eq_assert_expr_by_nsatz y zero H ty := + first [ constr_eq y zero; fail 1 y "is already" zero + | assert_expr_by_nsatz H ty ]. +Ltac canonicalize_field_inequalities_step' eq zero opp add sub := + match goal with + | [ H : not (eq ?x (opp ?y)) |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (add x y) zero)) + | [ H : (eq ?x (opp ?y) -> False)%type |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (add x y) zero -> False)%type + | [ H : not (eq ?x ?y) |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (sub x y) zero)) + | [ H : (eq ?x ?y -> False)%type |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (sub x y) zero)) + end. +Ltac canonicalize_field_inequalities' eq zero opp add sub := repeat canonicalize_field_inequalities_step' eq zero opp add sub. +Ltac canonicalize_field_equalities_step' eq zero opp add sub := + lazymatch goal with + | [ H : eq ?x (opp ?y) |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (add x y) zero) + | [ H : eq ?x ?y |- _ ] + => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (sub x y) zero) + end. +Ltac canonicalize_field_equalities' eq zero opp add sub := repeat canonicalize_field_equalities_step' eq zero opp add sub. + +(** These are the two user-facing tactics. They put (in)equalities + into the form [_ <> 0] / [_ = 0]. *) +Ltac canonicalize_field_inequalities := + let fld := guess_field in + lazymatch type of fld with + | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => canonicalize_field_inequalities' eq zero opp add sub + end. +Ltac canonicalize_field_equalities := + let fld := guess_field in + lazymatch type of fld with + | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => canonicalize_field_equalities' eq zero opp add sub + end. + (*** Polynomial equations over fields *) diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v index 8fa8c4a86..97b9da1ad 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Nsatz.v @@ -72,6 +72,16 @@ Ltac nsatz_rewrite_and_revert domain := end end. +(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz] + cannot handle duplicate hypotheses. So we clear them. *) +Ltac nsatz_clear_duplicates_for_bug_4851 domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ => + repeat match goal with + | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H' + end + end. + Ltac nsatz_nonzero := try solve [apply Integral_domain.integral_domain_one_zero |apply Integral_domain.integral_domain_minus_one_zero @@ -81,6 +91,7 @@ Ltac nsatz_domain_sugar_power domain sugar power := let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) lazymatch type of domain with | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => + nsatz_clear_duplicates_for_bug_4851 domain; nsatz_rewrite_and_revert domain; let reified_package := nsatz_reify_equations eq zero in let fv := nsatz_get_free_variables reified_package in @@ -115,13 +126,28 @@ Tactic Notation "nsatz" constr(n) := Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat. -Ltac nsatz_contradict := - unfold not; - intros; - let domain := nsatz_guess_domain in +(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] + contradicts any hypothesis of the form [?x' <> ?y'], we turn this + problem about inequalities into one about equalities and give it + to [nsatz]. *) +Ltac nsatz_contradict_single_hypothesis domain := lazymatch type of domain with | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => - assert (eq one zero) as Hbad; - [nsatz; nsatz_nonzero - |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] + unfold not in *; + match goal with + | [ H : eq _ _ -> False |- eq _ _ -> False ] + => intro; apply H; nsatz + end end. + +Ltac nsatz_contradict := + let domain := nsatz_guess_domain in + nsatz_contradict_single_hypothesis domain + || (unfold not; + intros; + lazymatch type of domain with + | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => + assert (eq one zero) as Hbad; + [nsatz; nsatz_nonzero + |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] + end). |