proposition: Lemma InterpRaster_correct1 : forall n m (t l b r:Q) (bitmap: raster n m) i j, raster_well_formed bitmap -> Is_true (RasterIndex bitmap i j) -> In (f l r n (Z.of_nat j), f t b m (Z.of_nat i)) (CentersOfPixels bitmap (l,t) (r,b)).
proof: Proof. intros n m t l b r 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. unfold RasterIndex. intros. pose proof (RasterIndex_in i j _ H H0) as [iin jin]. destruct bitmap as [bitmap], H. apply in_flat_map. exists (nth i (map q0 (iterateN_succ 0 m)) (q0 0%Z), nth i bitmap nil). split. - rewrite <- (combine_nth (map q0 (iterateN_succ 0 m)) bitmap i (q0 0%Z) nil). apply nth_In. rewrite combine_length, map_length, iterateN_succ_length. apply Nat.min_case. exact iin. rewrite H. exact iin. rewrite map_length, iterateN_succ_length, H. reflexivity. - rewrite map_map. replace (q0 (Z.of_nat i)) with (nth i (map q0 (iterateN_succ 0 m)) (q0 0%Z)). apply In_map_snd_const. replace (q (Z.of_nat j)) with (nth j (map q (iterateN_succ 0 n)) (q 0%Z)). apply In_filtered_list. 2: exact H0. rewrite map_length, iterateN_succ_length. rewrite Forall_forall in H1. rewrite (H1 (nth i bitmap nil)). apply Nat.le_refl. apply nth_In. rewrite H. exact iin. rewrite map_nth. apply f_equal. apply iterateN_succ_nth, jin. rewrite map_nth. apply f_equal. apply iterateN_succ_nth, iin. 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