proposition: Lemma RasterizeQ2_in : forall points (i j : Z) n m (r:raster n m), In (i,j) points -> raster_well_formed r -> (Z.to_nat i < Pos.to_nat m)%nat -> (Z.to_nat j < Pos.to_nat n)%nat -> Is_true (RasterIndex (fold_left (fun (rast:raster n m) (p:Z*Z) => setRaster rast true (Z.to_nat (fst p)) (Z.to_nat (snd p))) points r) (Z.to_nat i) (Z.to_nat j)).
proof: Proof. assert (forall points i j n m (r:raster n m), Is_true (RasterIndex r (Z.to_nat i) (Z.to_nat j)) -> raster_well_formed r -> Is_true (RasterIndex (fold_left (fun (rast:raster n m) (p:Z*Z) => setRaster rast true (Z.to_nat (fst p)) (Z.to_nat (snd p))) points r) (Z.to_nat i) (Z.to_nat j))). { induction points. - intros. exact H. - intros. simpl. apply IHpoints. apply setRaster_carry. exact H0. exact H. apply setRaster_wf, H0. } induction points. - intros. exfalso. inversion H0. - intros. simpl. destruct H0. + subst a. simpl. apply H. apply Is_true_eq_left, setRaster_correct1. exact H1. exact H2. exact H3. apply setRaster_wf, H1. + apply IHpoints. exact H0. apply setRaster_wf, H1. exact H2. exact H3. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround