diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-23 00:58:59 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-23 00:58:59 -0400 |
| commit | 93d6ee9bccc984b5eaa1d7e6f8bc2319697b6afb (patch) | |
| tree | 7ed237501b9318843d76d28c012f3e7c66e4d181 /src/Algebra.v | |
| parent | 64b0d8f59df25a0f115b1d33f4e46d88a63b8b17 (diff) | |
Generalize field_from_redundant_representation
Note that the old version did not need phi', but the new version does
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index fb34e488e..e10552f9c 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -929,8 +929,10 @@ Module Field. {phi'_inv : forall a, phi' (inv a) = INV (phi' a)} (phi'_div : forall a b, phi' (div a b) = DIV (phi' a) (phi' b)). - Local Instance field_from_redundant_representation - : @field H eq zero one opp add sub mul inv div. + Lemma field_and_homomorphism_from_redundant_representation + : @field H eq zero one opp add sub mul inv div + /\ @Ring.is_homomorphism F EQ ONE ADD MUL H eq one add mul phi + /\ @Ring.is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'. Proof. repeat match goal with | [ H : field |- _ ] => destruct H; try clear H @@ -956,8 +958,8 @@ Module Field. | [ |- eq _ _ ] => apply phi'_eq | [ H : (~eq _ _)%type |- _ ] => pose proof (fun pf => H (proj1 (@phi'_eq _ _) pf)); clear H | [ H : EQ _ _ |- _ ] => rewrite H - | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div by reflexivity - | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div in H by reflexivity + | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id by reflexivity + | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id in H by reflexivity | _ => solve [ eauto ] end. Qed. |