Merge branch 'master' into add-file

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.