diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-23 20:52:50 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-23 20:52:57 -0400 |
| commit | fc1f842a2797ed2318cb304d5f123e72ec9bc78e (patch) | |
| tree | c46df2e07355230d1731937cb04f429448cf9b16 /src/ModularArithmetic/ModularBaseSystemListProofs.v | |
| parent | 1d67ceeb14375a2832162568cd285e5c65c0cb16 (diff) | |
Created separate definitions for cmovne and cmovl for reification
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemListProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 23ec30cf7..3a6ffbeac 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -289,7 +289,7 @@ Section ModulusComparisonProofs. Lemma ge_modulus'_0 : forall {A} f us i, ge_modulus' (A := A) f us 0 i = f 0. Proof. - induction i; intros; simpl; break_if; auto. + induction i; intros; simpl; cbv [cmovne cmovl]; break_if; auto. Qed. Lemma ge_modulus'_01 : forall {A} f us i b, @@ -297,8 +297,8 @@ Section ModulusComparisonProofs. (ge_modulus' (A := A) f us b i = f 0 \/ ge_modulus' (A := A) f us b i = f 1). Proof. induction i; intros; - try intuition (subst; cbv [ge_modulus' LetIn.Let_In]; break_if; tauto). - simpl; cbv [LetIn.Let_In]. + try intuition (subst; cbv [ge_modulus' LetIn.Let_In cmovl cmovne]; break_if; tauto). + simpl; cbv [LetIn.Let_In cmovl cmovne]. break_if; apply IHi; tauto. Qed. @@ -317,7 +317,7 @@ Section ModulusComparisonProofs. induction i; repeat match goal with | |- _ => progress intros; simpl in * - | |- _ => progress cbv [LetIn.Let_In] in * + | |- _ => progress cbv [LetIn.Let_In cmovne cmovl] in * | |- _ =>erewrite (ge_modulus'_0 (@id Z)) in * | H : (?x <= 0)%nat |- _ => progress replace x with 0%nat in * by omega | |- _ => break_if @@ -335,7 +335,7 @@ Section ModulusComparisonProofs. Proof. induction i; repeat match goal with - | |- _ => progress (intros; cbv [LetIn.Let_In id]) + | |- _ => progress (intros; cbv [LetIn.Let_In id cmovne cmovl]) | |- _ => progress (simpl compare' in * ) | |- _ => progress specialize_by omega | |- _ => (progress rewrite ?Z.compare_eq_iff, |