proposition: Lemma unsat_match s th1 th2 : sym_match s th1 th2 -> unsat th2 -> unsat th1.
proof: Proof. pose I_ si mi := si ++ filter [predC si] (iota 0 mi). have SsP mi si ri (Ii := I_ si mi): uniq si && all (gtn ri) si -> (ri <= mi)%N -> [/\ {in Ii, forall i, i < mi}%N, uniq Ii & size Ii = mi]. - case/andP=> Usi /allP/=ltsi le_ri_mi; have uIm := iota_uniq 0 mi. have uIi: uniq Ii by rewrite cat_uniq Usi -all_predC filter_all filter_uniq. have defIi: Ii =i iota 0 mi. move=> i; rewrite mem_cat mem_filter orb_andr orbN mem_iota. by apply: orb_idl => /ltsi/leq_trans->. split=> // [i|]; first by rewrite defIi mem_iota. by rewrite (perm_size (uniq_perm _ _ defIi)) ?size_iota. have lt_nth ri si i: (nth ri si i < ri)%N -> (i < size si)%N. by rewrite !ltnNge; apply: contra => le_si; rewrite nth_default. case: s => [si sj sk] /= sym12 Uth2 m m_th1; case/and3P: (m_th1) sym12. case: th_bbox (th_bboxP (bbox_refl (th_bbox th1))) => ri rj rijP. case/andP=> /= leri lerj lerk _ /and4P[Ssi Ssj /andP[Usk /allP/=lesrk] sym12]. have{Ssi}-/SsP/(_ leri)[ltIi uIi szIi] := Ssi. have{Ssj} /SsP/(_ lerj)[ltIj uIj szIj] := Ssj. pose smL ij := m (nth ri (I_ si m.1) ij.1, nth rj (I_ sj m.2) ij.2)%N. pose smR := [seq m`_k | k <- sk]. have [[lb_m ZmL Dm] [o1m ZmR]] := (LmodelP m, RmodelP m). have{lb_m} smLP: is_Lmodel m smL. split=> // [ij | ij1 ij2 /andP[lti1 ltj1] /andP[lti2 ltj2]]; first exact: ZmL. by rewrite Dm ?inE /dot_ref/= ?nth_uniq ?ltIi ?ltIj ?mem_nth ?szIi ?szIj. have{lesrk} ubk k: k \in sk -> (k < size m)%N by move=> /lesrk/leq_trans->. have smRP: is_Rmodel smR. have ssmR: {subset smR <= (m : seq _)}. by move=> _ /mapP[k s_k ->]; rewrite mem_nth ?ubk. split=> [|xi /ssmR/ZmR//]; have [Um _] := orthonormalP o1m. apply: sub_orthonormal o1m; rewrite ?map_inj_in_uniq //. by apply: can_in_inj (index^~ m) _ => k s_k; rewrite /= index_uniq ?ubk. apply: (Uth2 (Model smLP smRP)); apply/satP=> [][[i2 j2] kvs2] /(allP sym12). case/andP=> -> /hasP[[[i1 j1] kvs1] th1_cl1 /andP[/eqP[Di1 Dj1] /allP s_kv12]]. have:= rijP _ th1_cl1; rewrite Di1 Dj1 => /andP[/lt_nth lti1 /lt_nth ltj1]. rewrite !inE -szIi -szIj !size_cat !(leq_trans _ (leq_addr _ _)) //. split=> // kv /s_kv12 kvs1_kv1; rewrite size_map /sat_lit /=. have /lt_nth ltk := th_dimP (leqnn _) _ th1_cl1 _ kvs1_kv1; split=> //. rewrite (nth_map (th_dim th1)) // /smL !nth_cat lti1 ltj1 -Di1 -Dj1. by have [_ _ /(_ _ kvs1_kv1)[]] := satP m_th1 _ th1_cl1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)