diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-15 15:12:29 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-15 15:12:29 -0400 |
| commit | c2df47be85f640255dfdee86144932084dad059b (patch) | |
| tree | ab38578dac3d57a50fd4fb9360ce102995582542 /src/CompleteEdwardsCurve/Pre.v | |
| parent | 6fdfabe26eb56d6758cea16f026557df5083863d (diff) | |
proved an admit in field homomorphisms that turned out to be unprovable; I added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index c74e9a321..76dd97c72 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -100,14 +100,16 @@ Section RespectsFieldHomomorphism. d_ok : field_homomorphism. - Lemma morphism_unidiedAdd' : forall P Q:F*F, + Lemma morphism_unifiedAdd' : forall P Q:F*F, + (~ EQ (ADD ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) -> + (~ EQ (SUB ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) -> eqp (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q)) (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)). Proof. - intros [x1 y1] [x2 y2]. + intros [x1 y1] [x2 y2] Hnonzero1 Hnonzero2; cbv [unifiedAdd' phip eqp]; apply conj; - (rewrite_strat topdown hints field_homomorphism); reflexivity. + (rewrite_strat topdown hints field_homomorphism); try assumption; reflexivity. Qed. End RespectsFieldHomomorphism. |