proposition: Lemma coarse_extends_in (r : grect) : coarse_in r m -> has r m -> forall p, inset r p -> extends_in r p.
proof: Proof. move=> r0Emh m_r p r0p; set r0 := r in r0Emh r0p; pose m0 := predI r0 m. have [r_m0 r0_r]: subpred m0 r /\ subpred r r0 by split=> [q /andP[]|]. have r_p: r p := insetW r0p; move: {2}_.+1 (ltnSn (garea r)) => n le_r_n. elim: n => // n IHn in r (r0) p m0 le_r_n m_r r_p r_m0 r0_r r0p r0Emh *. have [m_p | m'p] := boolP (p \in m). by exists m => // [|q m_q]; [left | apply/orP; right]. have ext_hex d (ed := gedge d) : halfg d = p -> ~~ has (ehex d) m -> extends_in (gchop_rect r ed) (halfg ed) -> extends_in r p. - move=> Dp d'm [xm xmP rm_xm xm_ed]. have ext1d: ext1_hex xm d. rewrite /ext1_hex !inE xm_ed; apply/hasPn=> q /rm_xm/orP[|/(hasPn d'm)//]. by rewrite !in_gchop_rect /= gchop_edge negb_and orbC => /andP[_ ->]. do [exists (ext1_matte ext1d); rewrite ?inE ?Dp ?eqxx //] => [|q]. right with d xm; rewrite // in_mring inE gedge2 Dp xm_ed. apply/(contra (rm_xm p)); rewrite inE in_gchop_rect /= gchop_edge. by rewrite -Dp gchop_halfg andbF Dp. rewrite !inE => /predU1P[->|/rm_xm]; first by rewrite Dp r_p. by rewrite inE in_gchop_rect orb_andl => /andP[]. have{IHn} IHp d: halfg d = p -> has (predD r0 (gchop1 d)) m -> extends_in r p. move=> Dp m_r0d; pose r01 := gchop1_rect r0 d. have r01p: inset r01 p. apply/insetP=> q p1q; rewrite in_gchop1_rect /= (insetP r0p) //=. by have:= p1q; rewrite -Dp gtouch_chop1 => /andP[]. have [m_r01 | r01'm] := boolP (has r01 m). pose r1 := gchop1_rect r d; have r_r1: subpred r1 r := @gchop_rect_sub r _. apply/(extends_in_sub r_r1)/(IHn r1 r01)=> //. - have [q m_q /andP[d'q r0q]] := hasP m_r0d. apply: leq_trans (n) _ le_r_n; apply: (@ltn_garea_subrect q) => //=. by rewrite in_gchop1_rect /= r_m0 ?d'q //= r0q. - have [q m_q] := hasP m_r01; rewrite in_gchop1_rect => /andP[r0q d_q]. by apply/hasP; exists q; rewrite // in_gchop1_rect /= r_m0 //= r0q. - by rewrite in_gchop1_rect /= r_p -Dp gchop_chop1 ?gchop_halfg. - by move=> q; rewrite !(inE, in_gchop1_rect) andbAC => /andP[/r_m0->]. - by move=> q; rewrite !in_gchop1_rect /= => /andP[/r0_r->]. by move=> q1 q2 /gchop_rect_sub; apply: r0Emh. apply: ext_hex (Dp) (contra _ r01'm) _. by apply/sub_has=> q; rewrite in_gchop_rect Dp => /andP[/(insetP r01p)]. set r1 := gchop_rect r _; have r_r1: subpred r1 r := @gchop_rect_sub r _. have m_r1: has r1 m. have [q m_q /andP[d'q r0q]] := hasP m_r0d. apply/hasP; exists q; rewrite ?in_gchop_rect //= r_m0 /= ?r0q //. by rewrite gchop_edge (contra _ d'q) => // /gchop_chop1. apply (IHn _ r0) => //; last 2 [by move=> q /r_r1/r0_r]. - apply: leq_trans (n) _ le_r_n; apply: (@ltn_garea_subrect p) => //=. by rewrite in_gchop_rect /= r_p gchop_edge -Dp gchop_halfg. - by have [q _] := hasP m_r1; apply: gchop_rect_edge; rewrite gedge2 Dp. - move=> q m0q; rewrite in_gchop_rect /= r_m0 // gchop_edge. case/andP: m0q => r0q /(hasPn r01'm); apply: contra => d_q. by rewrite in_gchop1_rect /= r0q gchop_chop1. set ed := gedge d; case Ded: (halfg ed) => [x y]. case Dr0: r0 => [x0 x1 y0 y1] /=; rewrite -!ler_subr_addr !ltr_subr_addr. have r0efd i: r0 (halfg (gedge (iter i gface (gedge ed)))). by rewrite (insetP r0p) // -Dp -(halfg_iter_face i) gedge2 gtouch_edge. have /= (d2 := gedge (gface (gface ed))): gchop_rect r0 d2 (halfg d2). have [q m_q /andP[d'q r0q]] := hasP m_r0d; apply: gchop_rect_edge (q) _. by rewrite gedge2 (insetP r0p) // !halfg_face -Dp gtouch_edge. by rewrite in_gchop_rect /= r0q gchop_edge. rewrite in_gchop_rect /= gchop_halfg andbT; have [] := (r0efd 1, r0efd 3)%N. rewrite !(Ded, halfg_edge, halfg_face, oddg_edge, oddg_face) -!addrA Dr0. by case: oddgP; do ![case/andP | move-> | clear 1]. pose nd (q : gpoint) : gpoint := q *+ 2 + iter 3 ccw (oddg q). have h_nd q: halfg (nd q) = q by rewrite halfg_eq //= !ccw_odd. have o_nd q: oddg (nd q) = ccw (ccw (ccw (oddg q))). by rewrite oddg_eq //= !ccw_odd. have hEnd q: halfg (gedge (nd q)) = gnode q. by rewrite halfg_edge h_nd o_nd ccw4. have ndN q: nd (gnode q) = gedge (gnode (gedge (nd q))). rewrite -[gedge (nd q)]halfgK hEnd -[gnode q in RHS]h_nd. by rewrite oddg_edge o_nd -oddg_node -o_nd -gface_def gfaceK. have ndFE q: nd (gface (gedge q)) = gedge (gface (nd q)). by rewrite -[q in RHS]gedgeK ndN gnodeK gedge2. have m_nd4 q: r0 q -> has (equad (nd q)) m -> q \in m. move=> r0q /hasP[q1 m_q1 q4q1]; rewrite -[_ \in m](r0Emh _ q1) {m_q1}//. apply/esym/eqP; rewrite -[_ == _]/(_ && _) !eq_le -andbA; apply/and4P. move: q4q1; rewrite !(inE, in_gchop_rect) /gchop halfg_face -[halfg _]halfgK. rewrite h_nd oddg_face o_nd ccw4; case: (halfg q) q1 => x y [x1 y1] /=. rewrite -!(ltz_addr1 (_ %/ _)%Z) !ltz_divLR ?lez_divRL // !mulrDl !mulz2. by case: oddgP; rewrite /= ?addr0 ?addrK !(addrA _ 1 1) !ltz_addr1; do ![case/andP | move-> | clear 1]. have gchop1F3E d: gchop1 (iter 3 gface (gedge d)) = gchop1 (gface d). by rewrite -gchop1_shift gface4 gedge2. have ehex_shift_quad q q' (efq := gedge (gface q)): ehex q q' || ehex (gface efq) q' ==> equad q q' || equad efq q'. - have chop1idl q1 q2 b: gchop1 q1 q2 && b && gchop q1 q2 = gchop q1 q2 && b. by rewrite andbAC (andb_idl (@gchop_chop1 _ _)). rewrite !(inE, in_gchop_rect) !gtouch_chop1 /= !andbT gface4 !chop1idl. do 2!rewrite [in _ && _ && _]andbCA chop1idl; rewrite gchop_shift gchop1F3E. case: (gchop q _); rewrite //= orbC andbC andbCA; case: (gchop1 _ _) => //=. rewrite andbT gchop_edge -[gface q as fq in gface (gface fq)]gedge2. by case: (gchop _ _); rewrite ?orbF; case: orP => //= -[]/andP[/gchop_chop1]. have r0_np: r0 (gnode p). by rewrite (insetP r0p) // -hEnd -[p in gtouch p]h_nd gtouch_edge. have r0_fep: r0 (gface (gedge p)). rewrite -[gface _]h_nd -[nd _]gedge2 (insetP r0p) //. by rewrite -[p in gtouch p]gedgeK -hEnd gtouch_edge. have p4'm: ~~ has (equad (nd p)) m by apply/(contra _ m'p)/m_nd4/r0_r. have [m_p6 | p6'm] := boolP (has (ehex (nd p)) m). have{m_p6} m_efp: halfg (gedge (gface (nd p))) \in m. have [q m_q p6_q] := hasP m_p6; apply/m_nd4/hasP; rewrite -ndFE h_nd //. have:= ehex_shift_quad (nd p) q; rewrite p6_q /= ndFE. by rewrite (negPf (hasPn p4'm q m_q)); exists q. have [m_fp6 | /ext_hex] := boolP (has (ehex (gface (nd p))) m); last first. rewrite halfg_face; apply=> //. by exists m => // [|q m_q]; [left | apply/orP; right]. have m_ep: halfg (gedge (nd p)) \in m. have [q m_q p6_q] := hasP m_fp6; apply/m_nd4/hasP; rewrite hEnd //. have:= ehex_shift_quad (nd (gnode p)) q; rewrite -ndFE gnodeK /= p6_q orbT. by rewrite (negPf (hasPn p4'm q m_q)) orbF; exists q. have ext2p: ext2_quad m (nd p) by apply/and3P. exists (ext2_matte ext2p); last by rewrite inE h_nd eqxx. right with (nd p) m => //; first by left. by rewrite in_mring inE gedge2 h_nd m_ep. by move=> q /predU1P[->|m_q]; [rewrite h_nd inE r_p | apply/orP; right]. have [m_p | {}m'p] := boolP (has (gtouch p) m); last first. suffices: has [pred q | has (predD r0 (gchop1 q)) m] (traject gface (nd p) 4). case/hasP/sig2W=> _ /trajectP/sig2_eqW[i _ ->]. by apply: IHp; rewrite halfg_iter_face. have [q m_q r_q] := hasP m_r; apply: contraR m'p; rewrite -all_predC => m'p. apply/hasP; exists q => //; rewrite -[p]h_nd gtouch_chop1. by apply: sub_all m'p => ? /hasPn/(_ q m_q); rewrite negb_and negbK orbC r0_r. apply: ext_hex (h_nd p) (p6'm) _. have [m_nd | m'nd] := boolP (gnode p \in m). by exists m => [|q m_q|]; [left | rewrite !inE m_q orbT | rewrite hEnd]. have nd4'm: ~~ has (equad (nd (gnode p))) m by apply: contra m'nd => /m_nd4->. have r0_n2p: r0 (gnode (gnode p)). rewrite -[gnode _]addrA oddg_node (insetP r0p) //. by case: oddgP; case: (p) => x y; rewrite /= !lter_add2. have m_n2p: gnode (gnode p) \in m. have [q m_q p9q] := hasP m_p; apply/m_nd4/hasP=> //; exists q => //. have ep_q: gchop (gedge (nd p)) q. rewrite gchop_edge; apply: contra p6'm => p_q. by apply/hasP; exists q; rewrite // in_gchop_rect /= h_nd p9q. have /implyP := ehex_shift_quad (nd (gnode (gnode p))) q. rewrite ndN gnodeK gedge2 (negPf (hasPn nd4'm q m_q)) orbF => -> //. apply/orP; right; rewrite in_gchop_rect /= ndN gnodeK ep_q gtouch_chop1 /=. rewrite gchop1F3E gchop_chop1 //= -gchop1F3E gedge2 !andbT andbC. by rewrite -[p]h_nd gtouch_chop1 in p9q; case/and5P: p9q => /gchop_chop1-> ->. have r_np: r (gnode p). have: r (gnode (gnode p)) by rewrite r_m0 //= r0_n2p. rewrite /gnode oddg_node -addrA; case: (p) (r) r_p => x y [x0 x1 y0 y1]. by case: oddgP; rewrite /= !addr0; do ![case/andP | move-> | clear 1]. have ext1nd: ext1_hex m (nd (gnode p)). rewrite /ext1_hex !inE hEnd m_n2p; apply/hasP => -[q m_q nd4q]. have := ehex_shift_quad (nd (gnode p)) q; rewrite -ndFE gnodeK nd4q /=. by case/norP; rewrite (hasPn nd4'm) ?(hasPn p4'm). exists (ext1_matte ext1nd) => [|q|]; last by rewrite inE h_nd hEnd eqxx. right with (nd (gnode p)) m => //; first by left. by rewrite in_mring inE hEnd m_n2p gedge2 h_nd m'nd. rewrite !inE => /predU1P[] ->; last by rewrite orbT. by rewrite h_nd in_gchop_rect /= r_np -hEnd gchop_halfg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)