diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-02 12:48:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-02 15:48:09 -0400 |
| commit | 7f20cf022c139dac1379dd249dd9b42998d6aced (patch) | |
| tree | ec326b091999ad3a097c552a8eb0a1be9ba40153 | |
| parent | 2fc3ff8afe6396c2866874980e3721dda2505839 (diff) | |
improve some fragile proofs (built on 8.4)
| -rw-r--r-- | src/Encoding/PointEncodingPre.v | 4 | ||||
| -rw-r--r-- | src/Experiments/Ed25519.v | 10 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 2 |
3 files changed, 8 insertions, 8 deletions
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index ed69441c1..71b239698 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -271,8 +271,8 @@ Section PointEncodingPre. cbv [option_eq Tuple.fieldwise Tuple.fieldwise' fst snd] in H; destruct H | H : Bool.eqb _ _ = _ |- _ => apply Bool.eqb_prop in H - | H : ?b = sign_bit ?x |- sign_bit ?y = ?b => erewrite <-sign_bit_subst by eassumption; congruence - | H : ?b <> sign_bit ?x |- sign_bit ?y <> ?b => erewrite <-sign_bit_subst by eassumption; congruence + | H : ?b = sign_bit ?x |- sign_bit ?y = ?b => erewrite <-sign_bit_subst by eassumption; instantiate; congruence + | H : ?b <> sign_bit ?x |- sign_bit ?y <> ?b => erewrite <-sign_bit_subst by eassumption; instantiate; congruence | |- sign_bit _ = whd ?w => destruct (whd w) | |- negb _ = false => apply Bool.negb_false_iff | |- _ => solve [auto using Bool.eqb_prop, diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 8b6e709a5..0fa27be66 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -598,8 +598,8 @@ Proof. rewrite Tuple.to_list_from_list. apply Conversion.convert_bounded. } { destruct w; - repeat match goal with p : _ * Z |- _ => destruct p end. - simpl Tuple.to_list in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + cbv [Tuple.to_list Tuple.to_list'] in *. rewrite Pow2BaseProofs.bounded_iff in *. (* TODO : Is there a better way to do this? *) pose proof (H0 0). @@ -611,7 +611,7 @@ Proof. pose proof (H0 6). pose proof (H0 7). clear H0. - cbv [GF25519.wire_widths nth_default nth_error] in *. + cbv [GF25519.wire_widths nth_default nth_error value] in *. repeat rewrite combine_ZNWord by (rewrite ?Znat.Nat2Z.inj_add; simpl Z.of_nat; repeat apply lor_shiftl_bounds; omega). cbv - [ZNWord Z.lor Z.shiftl]. rewrite Z.shiftl_0_l. @@ -626,12 +626,12 @@ Lemma initial_bounds : forall x n, (Tuple.to_list (length PseudoMersenneBaseParams.limb_widths) (GF25519BoundedCommon.proj1_fe25519 x)) n < 2 ^ GF25519.int_width - - (if PeanoNat.Nat.eq_dec n 0 + (if Decidable.dec (n=0)%nat then 0 else Z.shiftr (2 ^ GF25519.int_width) (nth_default 0 PseudoMersenneBaseParams.limb_widths - (Init.Nat.pred n))))%Z. + (pred n))))%Z. Proof. intros. cbv [GF25519BoundedCommon.fe25519] in *. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 773fea8fd..d630698e7 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -243,7 +243,7 @@ Proof. | _ => solve [ reflexivity | congruence | eauto 99 ] | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) | _ => progress eapply Proper_test_and_op - | _ => progress eapply conj + | _ => progress split | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) | _ => intro end. |