diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-24 23:52:06 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 23:52:06 -0400 |
| commit | ec33e34bb2928cbaee1895417e19d744497fdf3b (patch) | |
| tree | 94a0dd156a2da76507efcd1a9330779cb7d3a1f1 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | dfcae14436538ff9196b92061603ed832947f6af (diff) | |
Proper proofs for all ModularBaseSystem operations except [sub]
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 2d5f5a0c5..371da7767 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -265,24 +265,49 @@ Section FieldOperationProofs. rewrite !encode_rep. assumption. Qed. - Global Instance opp_Proper : Proper (Logic.eq ==> eq ==> eq) opp. - Admitted. - Global Instance add_Proper : Proper (eq ==> eq ==> eq) add. - Admitted. + Proof. + repeat intro. + cbv beta delta [eq] in *. + erewrite !add_rep; cbv [rep] in *; try reflexivity; assumption. + Qed. - Global Instance sub_Proper : Proper (Logic.eq ==> eq ==> eq ==> eq) sub. + Global Instance sub_Proper : Proper (eq ==> eq ==> eq ==> eq) sub. + Proof. Admitted. + Global Instance opp_Proper : Proper (eq ==> eq ==> eq) opp. + Proof. + cbv [opp]; repeat intro. + apply sub_Proper; assumption || reflexivity. + Qed. + Global Instance mul_Proper : Proper (eq ==> eq ==> eq) mul. - Admitted. + Proof. + repeat intro. + cbv beta delta [eq] in *. + erewrite !mul_rep; cbv [rep] in *; try reflexivity; assumption. + Qed. + + Check pow. + Global Instance pow_Proper : Proper (eq ==> Logic.eq ==> eq) pow. + Proof. + repeat intro. + cbv beta delta [eq] in *. + erewrite !pow_rep; cbv [rep] in *; subst; try reflexivity. + congruence. + Qed. Global Instance inv_Proper chain chain_correct : Proper (eq ==> eq) (inv chain chain_correct). - Admitted. + Proof. + cbv [inv]; repeat intro. + apply pow_Proper; assumption || reflexivity. + Qed. Global Instance div_Proper : Proper (eq ==> eq ==> eq) div. - Admitted. - + Proof. + cbv [div]; repeat intro; congruence. + Qed. Section FieldProofs. Context (modulus_gt_2 : 2 < modulus) |