proposition: Lemma InterpRaster_correct2 : forall n m (t l b r:Q) x y (bitmap: raster n m), raster_well_formed bitmap -> In (x,y) (CentersOfPixels bitmap (l,t) (r,b)) -> exists p, Is_true (RasterIndex bitmap (fst p) (snd p)) /\ x=f l r n (Z.of_nat (snd p)) /\ y=f t b m (Z.of_nat (fst p)).
proof: Proof. intros n m t l b r x y bitmap. unfold CentersOfPixels, InterpRow, UniformPartition. fold (f l r n). fold (f t b m). generalize (f l r n) (f t b m). clear t l b r f. intros q q0 wf H. apply in_flat_map in H. destruct H as [[s v] [H H0]]. destruct bitmap as [bitmap]. simpl. destruct wf. apply In_nth with (d:=(q0 0%Z, nth 0 bitmap nil)) in H. destruct H as [i [ilt H]]. rewrite combine_length, map_length, iterateN_succ_length in ilt. assert (i < Pos.to_nat m)%nat. { apply (Nat.lt_le_trans _ _ _ ilt), Nat.le_min_l. } clear ilt. rewrite combine_nth in H. 2: rewrite map_length, iterateN_succ_length, H1; reflexivity. inversion H. clear H. subst s. subst v. simpl in H0. rewrite map_map in H0. apply in_map_iff in H0. destruct H0 as [[s b] [H H0]]. unfold fst in H. inversion H. clear H. subst s. clear H6 y. apply filter_In in H0. destruct H0. unfold snd in H0. subst b. apply In_nth with (d:= (q 0%Z,true)) in H. destruct H as [j [jlt H]]. rewrite Forall_forall in H2. rewrite combine_nth in H. inversion H. clear H H4 x. rewrite combine_length, map_length, iterateN_succ_length in jlt. assert (j < Pos.to_nat n)%nat. { apply (Nat.lt_le_trans _ _ _ jlt). apply Nat.le_min_l. } clear jlt. exists (i,j). split. - simpl. rewrite (nth_indep _ false true). rewrite (nth_indep _ nil (nth 0 bitmap nil)). unfold Is_true. rewrite H5. trivial. rewrite H1. exact H3. rewrite H2. exact H. apply nth_In. rewrite H1. exact H3. - simpl. split. rewrite map_nth. apply f_equal. apply iterateN_succ_nth. exact H. rewrite map_nth. apply f_equal. apply iterateN_succ_nth, H3. - rewrite map_length, iterateN_succ_length. rewrite H2. reflexivity. apply nth_In. rewrite H1. exact H3. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.raster.Raster CoRN.reals.fast.Interval CoRN.metric2.FinEnum CoRN.metric2.ProductMetric CoRN.logic.Classic