diff options
| -rw-r--r-- | src/Algebra.v | 79 | ||||
| -rw-r--r-- | src/Tactics/Nsatz.v | 3 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 7 |
3 files changed, 73 insertions, 16 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 99fb2deb8..7f4fe06cc 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -580,6 +580,10 @@ Ltac field_nonzero_mul_split := repeat match goal with | [ H : ?R (?mul ?x ?y) ?zero |- _ ] => apply IntegralDomain.mul_nonzero_nonzero_cases in H; destruct H + | [ |- not (?R (?mul ?x ?y) ?zero) ] + => apply IntegralDomain.mul_nonzero_nonzero_iff; split + | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ] + => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H end. Ltac common_denominator := @@ -607,6 +611,28 @@ Ltac common_denominator_all := repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end. (** Now we have more conservative versions that don't simplify non-division structure. *) +Ltac deduplicate_nonfraction_pieces mul := + repeat match goal with + | [ x0 := ?v, x1 := context[?v] |- _ ] + => progress change v with x0 in x1 + | [ x := mul ?a ?b |- _ ] + => not is_var a; + let a' := fresh x in + pose a as a'; change a with a' in x + | [ x := mul ?a ?b |- _ ] + => not is_var b; + let b' := fresh x in + pose b as b'; change b with b' in x + | [ x0 := ?v, x1 := ?v |- _ ] + => change x1 with x0 in *; clear x1 + | [ x := ?v |- _ ] + => is_var v; subst x + | [ x0 := mul ?a ?b, x1 := mul ?a ?b' |- _ ] + => subst x0 x1 + | [ x0 := mul ?a ?b, x1 := mul ?a' ?b |- _ ] + => subst x0 x1 + end. + Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont := idtac; let one_arg_recr := @@ -656,7 +682,8 @@ Ltac set_nonfraction_pieces_in_by H nonzero_tac := => let T := type of H in set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac - ltac:(fun T' => change T' in H) + ltac:(fun T' => change T' in H); + deduplicate_nonfraction_pieces mul end. Ltac set_nonfraction_pieces_by nonzero_tac := idtac; @@ -666,31 +693,53 @@ Ltac set_nonfraction_pieces_by nonzero_tac := => let T := get_goal in set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac - ltac:(fun T' => change T') + ltac:(fun T' => change T'); + deduplicate_nonfraction_pieces mul end. Ltac set_nonfraction_pieces_in H := set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)). Ltac set_nonfraction_pieces := set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)). Ltac conservative_common_denominator_in H := - set_nonfraction_pieces_in H; - [ .. - | common_denominator_in H; - [ repeat split; try assumption.. - | ] ]; - repeat match goal with H := _ |- _ => subst H end. + idtac; + let fld := guess_field in + let div := lazymatch type of fld with + | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => div + end in + lazymatch type of H with + | appcontext[div] + => set_nonfraction_pieces_in H; + [ .. + | common_denominator_in H; + [ repeat split; try assumption.. + | ] ]; + repeat match goal with H := _ |- _ => subst H end + | ?T => fail 0 "no division in" H ":" T + end. Ltac conservative_common_denominator := - set_nonfraction_pieces; - [ .. - | common_denominator; - [ repeat split; try assumption.. - | ] ]; - repeat match goal with H := _ |- _ => subst H end. + idtac; + let fld := guess_field in + let div := lazymatch type of fld with + | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => div + end in + lazymatch goal with + | |- appcontext[div] + => set_nonfraction_pieces; + [ .. + | common_denominator; + [ repeat split; try assumption.. + | ] ]; + repeat match goal with H := _ |- _ => subst H end + | |- ?G + => fail 0 "no division in goal" G + end. Ltac conservative_common_denominator_all := try conservative_common_denominator; [ .. - | repeat match goal with [H: _ |- _ _ _ ] => progress conservative_common_denominator_in H; [] end ]. + | repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end ]. Inductive field_simplify_done {T} : T -> Type := Field_simplify_done : forall H, field_simplify_done H. diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v index 84d472e54..04f35c200 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Nsatz.v @@ -85,7 +85,8 @@ Ltac nsatz_clear_duplicates_for_bug_4851 domain := Ltac nsatz_nonzero := try solve [apply Integral_domain.integral_domain_one_zero |apply Integral_domain.integral_domain_minus_one_zero - |trivial]. + |trivial + |assumption]. Ltac nsatz_domain_sugar_power domain sugar power := let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index e8876fee2..2324e1b34 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -111,3 +111,10 @@ Ltac destruct_trivial_step := | [ H : True |- _ ] => clear H || destruct H end. Ltac destruct_trivial := repeat destruct_trivial_step. + +Ltac clear_duplicates_step := + match goal with + | [ H : ?T, H' : ?T |- _ ] => clear H' + | [ H := ?T, H' := ?T |- _ ] => clear H' + end. +Ltac clear_duplicates := repeat clear_duplicates_step. |