From b86dd1827e7da918148a650cc82d70dacaf3a545 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 12 Nov 2016 13:26:32 -0500 Subject: Remove extra admitted lemmas in 8.4 --- src/Experiments/Ed25519.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/Experiments') 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 _) => -- cgit v1.2.3