diff options
Diffstat (limited to 'cparser/validator/Alphabet.v')
| -rw-r--r-- | cparser/validator/Alphabet.v | 35 |
1 files changed, 17 insertions, 18 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index db850860..2d7f8ff9 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -199,7 +199,7 @@ Next Obligation. apply Zcompare_antisym. Qed. Next Obligation. destruct c. unfold compare31 in *. rewrite Z.compare_eq_iff in *. congruence. -eapply Zcompare_Lt_trans. apply H. apply H0. +eapply Zcompare_Lt_trans. apply H. apply H0. eapply Zcompare_Gt_trans. apply H. apply H0. Qed. Next Obligation. @@ -214,28 +214,27 @@ pose proof (inj_bound_spec x). match goal with |- In x (fst ?p) => destruct p as [] eqn:? end. replace inj_bound with i in H. revert l i Heqp x H. -apply iter_nat_invariant; intros. +induction (Z.abs_nat (phi inj_bound)); intros. inversion Heqp; clear Heqp; subst. -destruct x; specialize (H _ _ (eq_refl _) x0); simpl in *. -rewrite phi_incr in H0. -pose proof (phi_bounded i). -pose proof (phi_bounded (inj x0)). -destruct (Z_lt_le_dec (Zsucc (phi i)) (2 ^ Z_of_nat size)%Z). -rewrite Zmod_small in H0 by omega. -apply Zlt_succ_le, Zle_lt_or_eq in H0. -destruct H0; eauto. -left. -rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; reflexivity. -replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega. -rewrite Z_mod_same_full in H0. +rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega. +simpl in Heqp. +destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *. +inversion Heqp. subst. clear Heqp. +rewrite phi_incr in H. +pose proof (phi_bounded i0). +pose proof (phi_bounded (inj x)). +destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z). +rewrite Zmod_small in H by omega. +apply Zlt_succ_le, Zle_lt_or_eq in H. +destruct H; simpl; auto. left. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. +replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega. +rewrite Z_mod_same_full in H. exfalso; omega. -exfalso; inversion Heqp; subst; - pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega. -clear H. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega. -clear H H0. +clear H H0 H1. do 2 rewrite <- inj_Zabs_nat. f_equal. revert l i Heqp. |