diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-12 13:26:32 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-12 13:26:32 -0500 |
| commit | b86dd1827e7da918148a650cc82d70dacaf3a545 (patch) | |
| tree | 87dbfc7633965025a4e48d5064cd58b51489820d /src/Experiments | |
| parent | 10f2123449727ff9887068fba8e2bcc55053c799 (diff) | |
Remove extra admitted lemmas in 8.4
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index fb663b281..e13d1ba72 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1227,7 +1227,7 @@ Proof. rewrite Tuple.to_list_from_list. rewrite <-Conversion.convert_correct by (auto || rewrite Tuple.to_list; reflexivity). rewrite <-Pow2BaseProofs.decode_bitwise_spec by (auto || cbv [In]; intuition omega). - cbv [Tuple.to_list Tuple.to_list' length fst snd Pow2Base.decode_bitwise Pow2Base.decode_bitwise' nth_default nth_error ]. + cbv [Tuple.to_list Tuple.to_list' length fst snd Pow2Base.decode_bitwise Pow2Base.decode_bitwise' nth_default nth_error value ]. clear. apply Z.bits_inj'. intros. @@ -1268,8 +1268,7 @@ Proof. replace m with n by omega; reflexivity | |- Z.testbit ?w ?n = (Z.testbit ?w ?m || _)%bool => replace m with n by omega - end; - admit. (* TODO(jadep): there are goal left here on 8.4 *) + end. } match goal with |- option_eq _ (option_map _ (if Z_lt_dec ?a ?b then Some _ else None)) (if (?X =? 1)%Z then None else Some _) => |