proposition: Lemma collect_congs : forall (A B C D : CONGpoint) (HCong : CTCong A B C D) pa pb pc pd ss (interp : positive -> CONGpoint), interp pa = A -> interp pb = B -> interp pc = C -> interp pd = D -> ss_ok ss interp -> ss_ok (SSP.add (SP.add (pa,pb) (SP.add (pc,pd) SP.empty)) ss) interp.
proof: Proof. intros A B C D HCong pa pb pc pd ss interp HA HB HC HD HSS. revert A B C D pa pb pc pd HA HB HC HD HCong. cut (forall A B C D pa pb pc pd, interp pa = A -> interp pb = B -> interp pc = C -> interp pd = D -> CTCong A B C D -> Pos.le pa pb -> Pos.le pc pd -> ss_ok (SSP.add (SP.add (pa, pb) (SP.add (pc, pd) SP.empty)) ss) interp). intros Haux A B C D pa pb pc pd HA HB HC HD HCong. revert C D pc pd HC HD HCong. cut (forall C D pc pd, interp pc = C -> interp pd = D -> CTCong A B C D -> Pos.le pc pd -> ss_ok (SSP.add (SP.add (pa, pb) (SP.add (pc, pd) SP.empty)) ss) interp). intros Haux' C D pc pd HC HD HCong. case_eq (Pos.leb pc pd); intro Hpcpd. apply Pos.leb_le in Hpcpd. apply Haux' with C D; assumption. apply Pos.leb_gt, Pos.lt_le_incl in Hpcpd. assert (Heq : SP.Equal (SP.add (pc, pd) SP.empty) (SP.add (pd, pc) SP.empty)) by (apply SPWP.Dec.F.add_m; [apply eq_pseudo_refl|apply SPWP.equal_refl]). intro s. rewrite Heq. apply Haux' with D C; trivial. apply CTcong_right_comm, HCong. intros C D pc pd HC HD HCong Hpcpd. case_eq (Pos.leb pa pb); intro Hpapb. apply Pos.leb_le in Hpapb. apply Haux with A B C D; assumption. apply Pos.leb_gt, Pos.lt_le_incl in Hpapb. assert (Heq : SP.Equal (SP.add (pa, pb) (SP.add (pc, pd) SP.empty)) (SP.add (pb, pa) (SP.add (pc, pd) SP.empty))) by (apply SPWP.Dec.F.add_m; [apply eq_pseudo_refl|apply SPWP.equal_refl]). intro s. rewrite Heq. apply Haux with B A C D; trivial. apply CTcong_left_comm, HCong. intros A B C D pa pb pc pd HA HB HC HD HCong Hpapb Hpcpd s Hs. cut (forall p1 p2 p3 p4, SP.mem (p1, p2) s && SP.mem (p3, p4) s = true -> Pos.le p1 p2 -> Pos.le p3 p4 -> CTCong (interp p1) (interp p2) (interp p3) (interp p4)). intros Haux p1 p2. cut (forall p3 p4, SP.mem (p1, p2) s && SP.mem (p3, p4) s = true -> Pos.le p3 p4 -> CTCong (interp p1) (interp p2) (interp p3) (interp p4)). intros Haux' p3 p4 Hmem. case_eq (Pos.leb p3 p4); intro Hp3p4. apply Pos.leb_le in Hp3p4. apply Haux'; assumption. apply Pos.leb_gt, Pos.lt_le_incl in Hp3p4. apply CTcong_right_comm, Haux'; trivial. assert (Heq : SP.mem (p4, p3) s = SP.mem (p3, p4) s) by (apply SPWP.Dec.F.mem_m; [apply eq_pseudo_refl|apply SPWP.equal_refl]). rewrite Heq. assumption. intros p3 p4 Hmem Hp3p4. case_eq (Pos.leb p1 p2); intro Hp1p2. apply Pos.leb_le in Hp1p2. apply Haux; assumption. apply Pos.leb_gt, Pos.lt_le_incl in Hp1p2. apply CTcong_left_comm, Haux; trivial. assert (Heq : SP.mem (p2, p1) s = SP.mem (p1, p2) s) by (apply SPWP.Dec.F.mem_m; [apply eq_pseudo_refl|apply SPWP.equal_refl]). rewrite Heq. assumption. intros p1 p2 p3 p4 Hmem Hp1p2 Hp3p4. elim (SPWP.Dec.F.eq_dec (p1,p2) (p3,p4)); intro Hp1p3. apply eq_le2__eq2 in Hp1p3; trivial. destruct Hp1p3. subst. apply CTcong_refl. apply SSPWEqP.MP.Dec.F.mem_2 in Hs. apply SSPWEqP.MP.Dec.F.add_iff in Hs. rewrite andb_true_iff in Hmem. destruct Hmem as [Hmem1 Hmem2]. elim Hs; intro HsE. assert (HmemR : forall p q, SP.mem (p,q) (SP.add (pa, pb) (SP.add (pc, pd) SP.empty)) = SP.mem (p,q) s) by (intros; apply SPWP.Dec.F.mem_m; [unfold Pos.eq|]; auto). rewrite <- HmemR in Hmem1. rewrite <- HmemR in Hmem2. clear HmemR. elim (SPWP.Dec.F.eq_dec (pa,pb) (p1,p2)); intro Hpap1. apply eq_le2__eq2 in Hpap1; trivial. destruct Hpap1 as [Hpap1 Hpbp2]. rewrite Hpap1, Hpbp2 in *. rewrite SPWP.Dec.F.add_neq_b in Hmem2; trivial. rewrite <- SPWP.singleton_equal_add in Hmem2. apply SPWP.Dec.F.mem_iff in Hmem2. apply SPWP.Dec.F.singleton_1 in Hmem2. apply eq_le2__eq2 in Hmem2; trivial. destruct Hmem2 as [Hpcp3 Hpdp4]. rewrite Hpcp3, Hpdp4 in *; rewrite HA, HB, HC, HD. assumption. rewrite SPWP.Dec.F.add_neq_b in Hmem1; trivial. rewrite <- SPWP.singleton_equal_add in Hmem1. apply SPWP.Dec.F.mem_iff in Hmem1. apply SPWP.Dec.F.singleton_1 in Hmem1. apply eq_le2__eq2 in Hmem1; trivial. destruct Hmem1 as [Hpcp1 Hpdp2]. rewrite Hpcp1, Hpdp2 in *. rewrite SPWP.add_add in Hmem2. rewrite SPWP.Dec.F.add_neq_b in Hmem2; trivial. rewrite <- SPWP.singleton_equal_add in Hmem2. apply SPWP.Dec.F.mem_iff in Hmem2. apply SPWP.Dec.F.singleton_1 in Hmem2. apply eq_le2__eq2 in Hmem2; trivial. destruct Hmem2 as [Hpap3 Hpbp4]. rewrite Hpap3, Hpbp4 in *; rewrite HA, HB, HC, HD. apply CTcong_sym, HCong. apply HSS with s. apply SSPWEqP.MP.Dec.F.mem_1. assumption. rewrite Hmem1; rewrite Hmem2; reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets