(Joint Center)Library PFsection3

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg matrix poly finset.
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
Require Import gfunctor center gproduct cyclic pgroup abelian frobenius.
Require Import mxalgebra mxrepresentation vector falgebra fieldext galois.
Require Import ssrnum rat algC algnum classfun character.
Require Import integral_char inertia vcharacter.
Require Import PFsection1 PFsection2.

This file covers Peterfalvi, Section 3: TI-Subsets with Cyclic Normalizers
Given a direct product decomposition defW : W1 \x W2 = W, we define here: cyclicTIset defW == the set complement of W1 and W2 in W; this (locally) V definition is usually Let-bound to V. := W :\: (W1 :|: W2). cyclicTI_hypothesis G defW <-> W is a cyclic of odd order that is the normaliser in G of its non-empty TI subset V = cyclicTIset defW = W :\: (W1 :|: W2).
  • > This is Peterfalvi, Hypothesis (3.1), or Feit-Thompson (13.1).
cyclicTIirr defW i j == the irreducible character of W coinciding with (locally) w_ i j chi_i and 'chi_j on W1 and W2, respectively. This notation is usually Let-bound to w_ i j. := 'chi_(dprod_Iirr defW (i, j)). cfCyclicTIset defW i j == the virtual character of 'Z[irr W, V] coinciding (locally) alpha_ i j with 1 - chi_i and 1 - 'chi_j on W1 and W2, respectively. This definition is denoted by alpha_ i j in this file, and is only used in the proof if Peterfalvi (13.9) in the sequel. := cfDprod defW (1 - 'chi_i) (1 - 'chi_j). = 1 - w_ i 0 - w_ 0 j + w_ i j. cfCyclicTIsetBase defW := the tuple of all the alpha_ i j, for i, j != 0. (locally) cfWVbase This is a basis of 'CF(W, V); this definition is not used outside this file. For ctiW : cyclicTI_hypothesis defW G we also define cyclicTIiso ctiW == a linear isometry from 'CF(W) to 'CF(G) that (locally) sigma that extends induction on 'CF(W, V), maps the w_ i j to virtual characters, and w_ 0 0 to 1. This definition is usually Let-bound to sigma, and only depends extensionally on W, V and G. (locally) eta_ i j := sigma (w_ i j), as in sections 13 and 14 of tha Peterfalv text. cyclicTI_NC ctiW phi == the number of eta_ i j constituents of phi. (locally) NC phi := #| [set ij | ' [phi, eta_ ij .1 ij.2] != 0]|. The construction of sigma involves a large combinatorial proof, for which it is worthwhile to use reflection techniques to automate mundane and repetitive arguments. We isolate the necessary boilerplate in a separate CyclicTIisoReflexion module.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Section Definitions.

Variables (gT : finGroupType) (G W W1 W2 : {set gT}).

Definition cyclicTIset of W1 \x W2 = W := W :\: (W1 :|: W2).

Definition cyclicTI_hypothesis (defW : W1 \x W2 = W) :=
  [/\ cyclic W, odd #|W| & normedTI (cyclicTIset defW) G W].

End Definitions.

These is defined as a Notation which clients can bind with a Section Let that can be folded easily.
Notation cyclicTIirr defW i j := 'chi_(dprod_Iirr defW (i, j)).

Module CyclicTIisoReflexion.

Support for carrying out the combinatorial parts of the proof of Theorem (3.5) by reflection. Specifically, we need to show that in a rectangular array of virtual characters of norm 3, of even dimensions, and such that the dot product of two entries is 1 if they are on the same row or column, the entries of each column contain a "pivot" normal virtual character orthogonal to all other columns. The proof never needs to consider more than a 4 x 2 rectangle, but frequently renumbers lines, columns and orthonormal components in order to do so. We want to use reflection to automate this renumbering; we also want to automate the evaluation of the dot product constaints for partially described entries of the matrix. To do so we define a "theory" data structure to store a reifed form of such partial descriptions: a set of "clauses", each consisting in an index (i, j) into the array, and a collection of "literals" (k, v) representing constraints ' [b_(i, j), x`_k] = v%:~R, with v = 0, 1 or -1. A clause with exactly three nonzero literals defines b_(i, j) exactly. We define special notation for the concrete instances that appear in reflected proofs; for example |= & b11 = -x1 + x2 + x3 & x1, ~x2 in b12 & ? in b31 denotes the "theory" of arrays whose two left entries decomposes into x1 + x2 + x3 for some orthonormal x1, x2, and x3, such that the second top entry has x1 is a signed component but is orthogonal to x2, and which have an (unconstrained) first entry in the third column. (The concrete encoding shifts indices to start at 0.) The "models" in which such theories are interpreted supply the dimensions of the array, which must be even, nonequal and at least 2, the function mapping indices to array entries, which must be virtual characters with the requisite norms and dot products, and an orthonormal sequence of virtual characters that will be used to interpret the xij; a model coerces to any of these three components. We are primarily interested in two predicates: sat m th <=> the interpretation of th in m is well-defined (no out of bound indices) and valid (all constraints true). unsat th <-> forall m, ~ sat m th While the main theorem of this section, column_pivot, can be seen as an instance of "sat", all the principal combinatorial lemmas use "unsat", whose universal quantifier allows symmetry reductions. We present the set of lemmas implementing reflection-assisted proofs of "unsat th" as a small domain-specific proof language consisting of the following tactics: consider bij ::= add a clause for bij, which must not appear in th, changing the goal to unsat th & ? in bij. bij must be within a 4 x 2 bounding box, and th must be symmetric if bij "breaks" the 2 x 2 box. fill bij ::= add an x(k.+1) literal to the bij clause in th, where x1, ..., xk are all the normal characters appearing in th, and the clause for bij exists and contains assumptions for all of x1, ..., xk, at two of which are nonzero. uwlog Dcl: cl [by tac] ::= add the clause cl to th, replacing an existing clause for the same matrix entry. This produces a side goal of unsat th, but with an additional assumption Dcl : unsat th+cl, which can be resolved with the optional "by tac". uhave lit in bij as T(ij, kl) ::= adds the literal lit (one of xk, -xk, or ~xk) to an existing clause for bij in th, using the reflection lemma T(ij, kl) to rule out the other possibilities for xk. Here T can be either O (general dot product evaluation) or L (specific line/column constraints following from (3.5.2)). uhave lit, lit' in bij as T(ij, kl) ::= adds both lit and lit'. uhave lit | lit' in bij as T(ij, kl) ::= produces two subgoals, where lit (resp. lit') is added to the ... in bij clause in th, using T(ij, kl) to eliminate the third literal. (lit and lit' must constrain the same component). uhave lit | lit' | lit'' in bij ::= produces three subgoals, where lit (resp. lit', lit'') is added to the bij clause in th; lit, lit', lit'' should be a permutation of xk,
  • xk, and ~xk for some k.
uwlog Ebij: lit | lit' in bij as T(ij, kl) ::= adds lit to the bij clause in th, but produces a side goal where lit' has been added instead, with an additional assumption Ebij: th + (lit in bij); T(ij, kl) is used to rule out the third value. counter to T(ij, kl) ::= use T(ij, kl) to conclude that unsat th. uexact Hth' ::= use Hth' : unsat th', where th' is a subset of th (with the same order of literals) to conclude. symmetric to Hth' ::= use Hth' : unsat th', where th' is a permutation of a subset of th (preserving columns, and with at most one row exchange) to conclude.

Import ssrint.

Clause left-hand side, a reference to a value of beta; in the reference model m, (i, j) stands for beta_ (inord i.+1) (inord j.+1).
Definition ref := (nat × nat)%type.
Implicit Type ij : ref.
Definition Ref b_ij : ref := edivn (b_ij - 11) 10. (* Ref 21 = (1, 0). *)
Notation "''b' ij" := (Ref ij) (at level 0, ij at level 0, format "''b' ij").
Notation b11 := 'b11. Notation b12 := 'b12.
Notation b21 := 'b21. Notation b22 := 'b22.
Notation b31 := 'b31. Notation b32 := 'b32.
Notation b41 := 'b41. Notation b42 := 'b42.

Definition bbox := (nat × nat)%type. (* bounding box for refs. *)
Implicit Type bb : bbox.
Identity Coercion pair_of_bbox : bbox >-> prod.

Definition sub_bbox bb1 bb2 := (bb1.1 bb2.1)%N && (bb1.2 bb2.2)%N.
Definition wf_ref bb := [pred ij : ref | (ij.1 < bb.1)%N && (ij.2 < bb.2)%N].
Definition dot_ref ij1 ij2 := ((ij1.1 == ij2.1).+1 × (ij1.2 == ij2.2).+1 - 1)%N.

Lemma bbox_refl bb : sub_bbox bb bb.

Clause right-hand side litteral, denoting the projection of the left-hand side on an irreducible character of G: in a valid model m, (k, v) stands for the component m`_k *~ v = (model_xi m)`_k, and for the projection constraint ' [m i j, m`_k] == v%:~R.
Definition lit := (nat × int)%type. (* +x1 = (0,1) ~x2 = (1,0) -x3 = (2, -1)  *)
Implicit Types (kv : lit) (kvs : seq lit).
Definition Lit k1 v : lit := if (0 + k1)%N is k.+1 then (k, v) else (k1, v).
Notation "+x k" := (Lit k 1) (at level 0, k at level 0, format "+x k").
Notation "-x k" := (Lit k (-1)) (at level 0, k at level 0, format "-x k").
Notation "~x k" := (Lit k 0) (at level 0, k at level 0, format "~x k").
Notation x1 := +x1. Notation x2 := +x2.
Notation x3 := +x3. Notation x4 := +x4.
Notation x5 := +x5. Notation x6 := +x6.
Notation x7 := +x7. Notation x8 := +x8.

Definition AndLit kvs kv := kv :: kvs.
Definition AddLit := AndLit.
Notation "(*dummy*)" := (Prop Prop) (at level 0) : defclause_scope.
Infix "+" := AddLit : defclause_scope.
Definition SubLit kvs kv := AddLit kvs (kv.1, - kv.2).
Infix "-" := SubLit : defclause_scope.
Coercion LastLit kv := [:: kv].

Fixpoint norm_cl kvs : nat :=
  (if kvs is (_, v) :: kvs1 then `|v| ^ 2 + norm_cl kvs1 else 0)%N.

Definition clause := (ref × seq lit)%type.
Implicit Type cl : clause.
Definition Clause ij kvs : clause := (ij, kvs).
Notation "& kv1 , .. , kvn 'in' ij" :=
  (Clause ij (AndLit .. (AndLit nil kv1) .. kvn))
  (at level 200, ij, kv1, kvn at level 0,
   format "& kv1 , .. , kvn 'in' ij").
Notation "& ? 'in' ij" := (Clause ij nil)
  (at level 200, ij at level 0, format "& ? 'in' ij").
Definition DefClause := Clause.
Notation "& ij = kvs" := (DefClause ij kvs)
  (at level 200, ij at level 0, format "& ij = kvs").

Definition theory := seq clause.
Implicit Type th : theory.
Definition AddClause th cl : theory := cl :: th.
Notation "|= cl1 .. cln" := (AddClause .. (AddClause nil cl1) .. cln)
  (at level 8, cl1, cln at level 200,
   format "|= '[hv' cl1 '/' .. '/' cln ']'").

Transpose (W1 / W2 symmetry).

Definition tr (ij : nat × nat) : ref := (ij.2, ij.1).
Definition tr_th th : theory := [seq (tr cl.1, cl.2) | cl <- th].

Lemma trK : involutive tr.
Lemma tr_thK : involutive tr_th.

Index range of a theory.

Fixpoint th_bbox th : bbox :=
  if th is (i, j, _) :: th1 then
    let: (ri, rj) := th_bbox th1 in (maxn i.+1 ri, maxn j.+1 rj)
  else (0, 0)%N.

Lemma th_bboxP th bb :
  reflect {in th, cl, cl.1 \in wf_ref bb} (sub_bbox (th_bbox th) bb).
Implicit Arguments th_bboxP [th bb].

Fixpoint th_dim th : nat :=
  if th is (_, kvs) :: th1 then
    foldr (fun kvmaxn kv.1.+1) (th_dim th1) kvs
  else 0%N.

Lemma th_dimP th bk :
  reflect {in th, cl, {in cl.2, kv, kv.1 < bk}}%N
          (th_dim th bk)%N.
Implicit Arguments th_dimP [th bk].

Theory and clause lookup.

CoInductive get_spec T (P : TProp) (Q : Prop) : option TProp :=
  | GetSome x of P x : get_spec P Q (Some x)
  | GetNone of Q : get_spec P Q None.

Fixpoint get_cl ij (th : theory) : option clause :=
  if th is cl :: th1 then if cl.1 == ij then Some cl else get_cl ij th1
  else None.

Lemma get_clP ij (th : theory) :
  get_spec (fun cl : clausecl \in th cl.1 = ij) True (get_cl ij th).

Fixpoint get_lit (k0 : nat) kvs : option int :=
  if kvs is (k, v) :: kvs1 then if k == k0 then Some v else get_lit k0 kvs1
  else None.

Lemma get_litP k0 kvs :
  get_spec (fun v(k0, v) \in kvs) (k0 \notin unzip1 kvs) (get_lit k0 kvs).

Theory extension.

Fixpoint set_cl cl2 th : wrapped theory :=
  if th is cl :: th1 then
    let: Wrap th2 := set_cl cl2 th1 in
    if cl.1 == cl2.1 then Wrap (AddClause th2 cl2) else Wrap (AddClause th2 cl)
  else Wrap nil.

Definition ext_cl th cl k v :=
  let: (ij, kvs) := cl in set_cl (Clause ij (AndLit kvs (Lit k.+1 v))) th.

Definition wf_ext_cl cl k rk := (k \notin unzip1 cl.2) && (k < rk)%N.

Definition wf_fill k kvs := (size kvs == k) && (norm_cl kvs < 3)%N.

Lemma ext_clP cl1 th k v (cl1k := (cl1.1, (k, v) :: cl1.2)) :
    cl1 \in th
  exists2 th1, ext_cl th cl1 k v = Wrap th1
        & cl1k \in th1
         th1 =i [pred cl | if cl.1 == cl1.1 then cl == cl1k else cl \in th].

Satisfiability tests.

Definition sat_test (rO : rel clause) ij12 th :=
  if get_cl (Ref ij12.1) th is Some cl1 then
    oapp (rO cl1) true (get_cl (Ref ij12.2) th)
  else true.

This reflects the application of (3.5.1) for an arbitrary pair of entries.
Definition Otest cl1 cl2 :=
  let: (ij1, kvs1) := cl1 in let: (ij2, kvs2) := cl2 in
  let fix loop s1 s2 kvs2 :=
    if kvs2 is (k, v2) :: kvs2 then
      if get_lit k kvs1 is Some v1 then loop (v1 × v2 + s1) s2 kvs2 else
      loop s1 s2.+1 kvs2
    else (s1, if norm_cl kvs1 == 3 then 0%N else s2) in
  let: (s1, s2) := loop 0 0%N kvs2 in
  (norm_cl kvs2 == 3) ==> (`|s1 - dot_ref ij1 ij2| s2)%N.

Matching up to a permutation of the rows, columns, and base vectors.

Definition sub_match th1 th2 :=
  let match_cl cl1 cl2 :=
    if cl2.1 == cl1.1 then subseq cl1.2 cl2.2 else false in
  all [pred cl1 | has (match_cl cl1) th2] th1.

Definition wf_consider ij th (ri := (th_bbox th).1) :=
  (ij.1 < 2 + ((2 < ri) || sub_match th (tr_th th)).*2)%N && (ij.2 < 2)%N.

CoInductive sym := Sym (si : seq nat) (sj : seq nat) (sk : seq nat).

Definition sym_match s th1 th2 :=
  let: Sym si sj sk := s in let: (ri, rj, rk) := (th_bbox th1, th_dim th1) in
  let is_sym r s := uniq s && all (gtn r) s in
  let match_cl cl2 :=
    let: (i2, j2, kvs2) := cl2 in let ij := (nth ri si i2, nth rj sj j2) in
    let match_lit kvs1 kv := (nth rk sk kv.1, kv.2) \in kvs1 in
    let match_cl1 cl1 :=
      let: (ij1, kvs1) := cl1 in (ij1 == ij) && all (match_lit kvs1) kvs2 in
    uniq (unzip1 kvs2) && has match_cl1 th1 in
  [&& is_sym ri si, is_sym rj sj, is_sym rk sk & all match_cl th2].

Try to compute the base vector permutation for a given row and column permutation. We assume each base vector is determined by the entries of which it is a proper constituent, and that there are at most two columns.
Definition find_sym_k th1 th2 (si sj : seq nat) :=
  let store_lit c kv ksig :=
    let: (k, v) := kv in if v == 0 then ksig else let cv := (c, v) in
    let fix insert_in (cvs : seq (nat × int)) :=
      if cvs is cv' :: cvs' then
        if (c < cv'.1)%N then cv :: cvs else cv' :: insert_in cvs'
      else [:: cv] in
    set_nth nil ksig k (insert_in (nth nil ksig k)) in
  let fix read_lit ksig1 ksig2 :=
    if ksig1 is cvs :: ksig1' then
      let k := index cvs ksig2 in
      k :: read_lit ksig1' (set_nth nil ksig2 k nil)
    else nil in
  let fix store2 ksig1 ksig2 cls1 :=
    if cls1 is (i1, j1, kvs1) :: cls1' then
      if get_cl (nth 0 si i1, nth 0 sj j1)%N th2 is Some (_, kvs2) then
        let st_kvs := foldr (store_lit (i1.*2 + j1)%N) in (* assume j1 <= 1 *)
        store2 (st_kvs ksig1 kvs1) (st_kvs ksig2 kvs2) cls1'
      else None
      let sk := read_lit ksig1 ksig2 in
      if all (gtn (size ksig2)) sk then Some (Sym si sj sk) else None in
  store2 nil nil th1.

Try to find a symmetry that maps th1 to th2, assuming the same number of rows and columns, and considering at most one row exchange.
Definition find_sym th1 th2 :=
  let: (ri, rj) := th_bbox th2 in let si := iota 0 ri in let sj := iota 0 rj in
  if find_sym_k th1 th2 si sj is Some _ as s then s else
  let fix loop m :=
    if m is i.+1 then
      let fix inner_loop m' :=
        if m' is i'.+1 then
          let si' := (set_nth 0 (set_nth 0 si i i') i' i)%N in
          if find_sym_k th1 th2 si' sj is Some _ as s then s else inner_loop i'
        else None in
      if inner_loop i is Some _ as s then s else loop i
    else None in
  loop ri.

Section Interpretation.

Variables (gT : finGroupType) (G : {group gT}).

Definition is_Lmodel bb b :=
  [/\ [/\ odd bb.1.+1, odd bb.2.+1, bb.1 > 1, bb.2 > 1 & bb.1 != bb.2]%N,
       ij, b ij \in 'Z[irr G]
    & {in wf_ref bb &, ij1 ij2, '[b ij1, b ij2] = (dot_ref ij1 ij2)%:R}].

Definition is_Rmodel X := orthonormal X {subset X 'Z[irr G]}.

Inductive model := Model bb f X of is_Lmodel bb f & is_Rmodel X.

Coercion model_bbox m := let: Model d _ _ _ _ := m in d.
Definition model_entry m := let: Model _ f _ _ _ := m in f.
Coercion model_entry : model >-> Funclass.
Coercion model_basis m := let: Model _ _ X _ _ := m in X.
Lemma LmodelP (m : model) : is_Lmodel m m.
Lemma RmodelP (m : model) : is_Rmodel m.

Fact nil_RmodelP : is_Rmodel nil.

Definition eval_cl (m : model) kvs := \sum_(kv <- kvs) m`_kv.1 *~ kv.2.

Definition sat_lit (m : model) ij kv := '[m ij, m`_kv.1] == kv.2%:~R.
Definition sat_cl m cl := uniq (unzip1 cl.2) && all (sat_lit m cl.1) cl.2.

Definition sat (m : model) th :=
  [&& sub_bbox (th_bbox th) m, th_dim th size m & all (sat_cl m) th]%N.
Definition unsat th := m, ¬ sat m th.

Lemma satP (m : model) th :
  reflect {in th, cl,
              [/\ cl.1 \in wf_ref m, uniq (unzip1 cl.2)
                & {in cl.2, kv, kv.1 < size m sat_lit m cl.1 kv}%N]}
          (sat m th).
Implicit Arguments satP [m th].

Reflexion of the dot product.

Lemma norm_clP m th cl :
    sat m thcl \in th
  let norm := norm_cl cl.2 in let beta := m cl.1 in
  [/\ (norm 3)%N, norm == 3 → beta = eval_cl m cl.2
    & (norm < 3)%Nsize cl.2 == size m
      exists2 dk, dk \in dirr_constt beta & orthogonal (dchi dk) m].

Lemma norm_cl_eq3 m th cl :
  sat m thcl \in thnorm_cl cl.2 == 3 → m cl.1 = eval_cl m cl.2.

Lemma norm_lit m th cl kv :
  sat m thcl \in thkv \in cl.2 → (`|kv.2| 1)%N.

Decision procedure framework (in which we will define O and L).

Definition is_sat_test (tO : pred theory) := m th, sat m thtO th.

Lemma sat_testP (rO : rel clause) ij12 :
    ( m th cl1 cl2, sat m thcl1 \in thcl2 \in thrO cl1 cl2) →
  is_sat_test (sat_test rO ij12).

Case analysis on the value of a specific projection.

Definition lit_vals : seq int := [:: 0; 1; -1].

Lemma sat_cases (m : model) th k cl :
    sat m thcl \in thwf_ext_cl cl k (size m) →
  exists2 v, v \in lit_vals & sat m (unwrap (ext_cl th cl k v)).
Implicit Arguments sat_cases [m th cl].

Definition unsat_cases_hyp th0 kvs tO cl :=
  let: (k, _) := head (2, 0) kvs in let thk_ := ext_cl th0 cl k in
  let th's := [seq unwrap (thk_ v) | v <- lit_vals & v \notin unzip2 kvs] in
  let add hyp kv :=
    let: (_, v) := kv in let: Wrap th := thk_ v in hyp unsat th in
  foldl add (wf_ext_cl cl k (th_dim th0) && all (predC tO) th's) kvs.

Lemma unsat_cases th ij kvs tO :
    is_sat_test tOoapp (unsat_cases_hyp th kvs tO) False (get_cl ij th) →
  unsat th.

Dot product reflection.

Lemma O ij12 : is_sat_test (sat_test Otest ij12).

"Without loss" cut rules.

Lemma unsat_wlog cl th :
   (let: Wrap th1 := set_cl cl th in (unsat th1unsat th) unsat th1) →
  unsat th.

Lemma unsat_wlog_cases th1 th2 :
  (unsat th1unsat th2) → unsat th1(true unsat th1) unsat th2.

Extend the orthonormal basis

Lemma sat_fill m th cl (k := th_dim th) :
    sat m thcl \in thwf_fill k cl.2
   mr : {CFk | is_Rmodel CFk},
    sat (Model (LmodelP m) (svalP mr)) (unwrap (ext_cl th cl k 1)).

Lemma unsat_fill ij th :
  let fill_cl cl :=
    if (th_dim th).+1 %/ 1 is k.+1 then
      let: Wrap thk := ext_cl th cl k 1 in wf_fill k cl.2 unsat thk
      else True in
  oapp fill_cl False (get_cl ij th) → unsat th.

Matching an assumption exactly.

Lemma sat_exact m th1 th2 : sub_match th1 th2sat m th2sat m th1.

Lemma unsat_exact th1 th2 : sub_match th1 th2unsat th1unsat th2.

Transpose (W1 / W2 symmetry).

Fact tr_Lmodel_subproof (m : model) : is_Lmodel (tr m) (fun ijm (tr ij)).

Definition tr_model m := Model (tr_Lmodel_subproof m) (RmodelP m).

Lemma sat_tr m th : sat m thsat (tr_model m) (tr_th th).

Extend the theory (add a new empty clause).

Lemma unsat_consider ij th :
  wf_consider ij thunsat (AddClause th (& ? in ij)) → unsat th.

Matching up to a permutation of the rows, columns, and base vectors.

Lemma unsat_match s th1 th2 : sym_match s th1 th2unsat th2unsat th1.

Lemma unsat_sym th1 th2 :
  (if find_sym th1 th2 is Some s then sym_match s th2 th1 else false) →
  unsat th1unsat th2.

End Interpretation.

Implicit Arguments satP [gT G m th].
Implicit Arguments unsat [gT G].
Implicit Arguments sat_cases [gT G m th cl].
Implicit Arguments unsat_cases [gT G th tO].
Implicit Arguments unsat_wlog [gT G].
Implicit Arguments unsat_fill [gT G].
Implicit Arguments unsat_consider [gT G].
Implicit Arguments unsat_match [gT G th1 th2].

The domain-specific tactic language.

Tactic Notation "consider" constr(ij) :=
  apply: (unsat_consider ij); first exact isT.

Note that "split" here would be significantly less efficient, because it would evaluate the reflected assumption four times.
Tactic Notation "fill" constr(ij) :=
  apply: (unsat_fill ij); apply: (conj isT _).

Tactic Notation "uwlog" simple_intropattern(IH) ":" constr(cl) :=
  apply: (unsat_wlog cl); split⇒ [IH | ].

Tactic Notation "uwlog" simple_intropattern(IH) ":" constr(cl)
                   "by" tactic4(tac) :=
  apply: (unsat_wlog cl); split⇒ [IH | ]; first by [tac].

Tactic Notation "uhave" constr(kv) "in" constr(ij)
                   "as" constr(T) constr(ij12) :=
  apply: (unsat_cases ij [:: kv] (T ij12)); apply: (conj isT _).

Tactic Notation "uhave" constr(kv1) "," constr(kv2) "in" constr(ij)
                   "as" constr(T) constr(ij12) :=
  uhave kv1 in ij as T ij12; uhave kv2 in ij as T ij12.

Tactic Notation "uhave" constr(kv1) "|" constr(kv2) "in" constr(ij)
                   "as" constr(T) constr(ij12) :=
  apply: (unsat_cases ij [:: kv1; kv2] (T ij12)); apply: (conj (conj isT _) _).

Tactic Notation "uhave" constr(kv1) "|" constr(kv2) "|" constr(kv3)
                   "in" constr(ij) :=
  apply: (unsat_cases ij [:: kv1; kv2; kv3] (fun _ _ _isT));
  apply: (conj (conj (conj isT _) _) _).

Tactic Notation "uwlog" simple_intropattern(IH) ":"
                        constr(kv1) "|" constr(kv2) "in" constr(ij)
                   "as" constr(T) constr(ij12) :=
  apply: (unsat_cases ij [:: kv1; kv2] (T ij12));
  apply: unsat_wlog_cases ⇒ [IH | ].

Tactic Notation "counter" "to" constr(T) constr(ij12) := by move⇒ ? /(T ij12).

Tactic Notation "uexact" constr(IH) := apply: unsat_exact IH; exact isT.

Tactic Notation "symmetric" "to" constr(IH) := apply: unsat_sym (IH); exact isT.

End CyclicTIisoReflexion.

Section Three.

Variables (gT : finGroupType) (G W W1 W2 : {group gT}).
Hypothesis defW : W1 \x W2 = W.

Let V := cyclicTIset defW.
Let w_ i j := cyclicTIirr defW i j.
Let w1 := #|W1|.
Let w2 := #|W2|.

Lemma cyclicTIirrC (defW21 : W2 \x W1 = W) i j :
  cyclicTIirr defW21 j i = w_ i j.

Lemma cycTIirrP chi : chi \in irr W{i : Iirr W1 & {j | chi = w_ i j}}.

Lemma cycTIirr_aut u i j : w_ (aut_Iirr u i) (aut_Iirr u j) = cfAut u (w_ i j).

Let sW1W : W1 \subset W.
Let sW2W : W2 \subset W.

Lemma card_cycTIset : #|V| = (w1.-1 × w2.-1)%N.

Definition cfCyclicTIset i j := cfDprod defW (1 - 'chi_i) (1 - 'chi_j).
Local Notation alpha_ := cfCyclicTIset.

Lemma cycTIirr00 : w_ 0 0 = 1.
Local Notation w_00 := cycTIirr00.

Lemma cycTIirr_split i j : w_ i j = w_ i 0 × w_ 0 j.

Lemma cfker_cycTIl j : W1 \subset cfker (w_ 0 j).

Lemma cfker_cycTIr i : W2 \subset cfker (w_ i 0).

Let cfdot_w i1 j1 i2 j2 : '[w_ i1 j1, w_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.

Lemma cfCycTI_E i j : alpha_ i j = 1 - w_ i 0 - w_ 0 j + w_ i j.
Local Notation alphaE := cfCycTI_E.

Lemma cfCycTI_vchar i j : alpha_ i j \in 'Z[irr W].

Definition cfCyclicTIsetBase :=
  [seq alpha_ ij.1 ij.2 | ij in setX [set¬ 0] [set¬ 0]].
Local Notation cfWVbase := cfCyclicTIsetBase.

Let cfdot_alpha_w i1 j1 i2 j2 :
  i2 != 0 → j2 != 0 → '[alpha_ i1 j1, w_ i2 j2] = [&& i1 == i2 & j1 == j2]%:R.

Let cfdot_alpha_1 i j : i != 0 → j != 0 → '[alpha_ i j, 1] = 1.

Let cfnorm_alpha i j : i != 0 → j != 0 → '[alpha_ i j] = 4%:R.

Lemma cfCycTIbase_free : free cfWVbase.

Further results on alpha_ depend on the assumption that W is cyclic.

Hypothesis ctiW : cyclicTI_hypothesis G defW.

Let cycW : cyclic W.
Let oddW : odd #|W|.
Let tiV : normedTI V G W.
Let ntV : V != set0.

Lemma cyclicTIhyp_sym (defW21 : W2 \x W1 = W) : cyclicTI_hypothesis G defW21.

Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.
Let coW12 : coprime w1 w2.

Let Wlin k : 'chi[W]_k \is a linear_char.
Let W1lin i : 'chi[W1]_i \is a linear_char.
Let W2lin i : 'chi[W2]_i \is a linear_char.
Let w_lin i j : w_ i j \is a linear_char.

Let nirrW1 : #|Iirr W1| = w1.
Let nirrW2 : #|Iirr W2| = w2.
Let NirrW1 : Nirr W1 = w1.
Let NirrW2 : Nirr W2 = w2.

Lemma cycTI_nontrivial : W1 :!=: 1%g W2 :!=: 1%g.

Let ntW1 : W1 :!=: 1%g.
Let ntW2 : W2 :!=: 1%g.
Let oddW1 : odd w1.
Let oddW2 : odd w2.
Let w1gt2 : (2 < w1)%N.
Let w2gt2 : (2 < w2)%N.

Let neq_w12 : w1 != w2.

Let cWW : abelian W.
Let nsVW : V <| W.
Let sWG : W \subset G.
Let sVG : V \subset G^#.

Let alpha1 i j : alpha_ i j 1%g = 0.

This first part of Peterfalvi (3.4) will be used in (4.10) and (13.9).
Lemma cfCycTI_on i j : alpha_ i j \in 'CF(W, V).

This is Peterfalvi (3.4).
Lemma cfCycTIbase_basis : basis_of 'CF(W, V) cfWVbase.
Local Notation cfWVbasis := cfCycTIbase_basis.

Section CyclicTIisoBasis.

Import CyclicTIisoReflexion ssrint.

Local Notation unsat := (@unsat gT G).
Local Notation O := (@O gT G).
Local Notation "#1" := (inord 1).

This is the combinatorial core of Peterfalvi (3.5.2). Peterfalvi uses evaluation at 1%g to conclude after the second step; since this is not covered by our model, we have used the dot product constraints between b12 and b11, b21 instead.
Let unsat_J : unsat |= & x1 in b11 & -x1 in b21.

Let unsat_II: unsat |= & x1, x2 in b11 & x1, x2 in b21.

This reflects the application of (3.5.2), but only to rule out nonzero components of the first entry that conflict with positive components of the second entry; Otest covers all the other uses of (3.5.2) in the proof.
Let Ltest (cl1 cl2 : clause) :=
  let: (i1, j1, kvs1) := cl1 in let: (i2, j2, kvs2) := cl2 in
  let fix loop mm kvs2' :=
    if kvs2' is (k, v2) :: kvs2'' then
      let v1 := odflt 0 (get_lit k kvs1) in
      if (v2 != 1) || (v1 == 0) then loop mm kvs2'' else
      if (v1 != 1) || mm then false else loop true kvs2''
    else true in
  (i1 == i2) (+) (j1 == j2) ==> loop false kvs2.

Let L ij12 : is_sat_test G (sat_test Ltest ij12).

This is the combinatorial core of Peterfalvi (3.5.4). We have made a few simplifications to the combinatorial analysis in the text: we omit the (unused) step ( entirely, which lets us inline step ( in the proof of (; we clear the assumptions on b31 and b32 before the final step (, exposing a hidden symmetry.
Let unsat_Ii : unsat |= & x1 in b11 & x1 in b21 & ¬x1 in b31.

Let unsat_C : unsat |= & x1 in b11 & x1 in b21 & x1 in b12.

This refinement of Peterfalvi (3.5.4) is the essential part of (3.5.5).
Let column_pivot (m : model G) (j0 : 'I_m.2.+1) :
   dk, (i : 'I_m.1.+1) (j : 'I_m.2.+1),
    j0 != 0 → i != 0 → j != 0 → '[m (i.-1, j.-1), dchi dk] = (j == j0)%:R.

This is Peterfalvi (3.5). We have inlined part of the proof of (3.5.5) in this main proof, replacing some combinatorial arguments with direct computation of the dot product, this avoids the duplicate case analysis required to exploit (3.5.5) as it is stated in the text.
Lemma cyclicTIiso_basis_exists :
  xi_ : Iirr W1Iirr W2'CF(G),
   [/\ xi_ 0 0 = 1, i j, xi_ i j \in 'Z[irr G],
        i j, i != 0 → j != 0 →
         'Ind (alpha_ i j) = 1 - xi_ i 0 - xi_ 0 j + xi_ i j
     & i1 j1 i2 j2, '[xi_ i1 j1, xi_ i2 j2] = ((i1, j1) == (i2, j2))%:R].

End CyclicTIisoBasis.

This is PeterFalvi, Theorem (3.2)(a, b, c).
Theorem cyclicTIiso_exists :
  {sigma : {linear 'CF(W)'CF(G)} |
    [/\ {in 'Z[irr W], isometry sigma, to 'Z[irr G]}, sigma 1 = 1
      & {in 'CF(W, V), phi : 'CF(W), sigma phi = 'Ind[G] phi}]}.

Fact cyclicTIiso_key : unit.
Definition cyclicTIiso :=
  locked_with cyclicTIiso_key (sval cyclicTIiso_exists).
Local Notation sigma := cyclicTIiso.
Let im_sigma := map sigma (irr W).
Let eta_ i j := sigma (w_ i j).

Lemma cycTI_Zisometry : {in 'Z[irr W], isometry sigma, to 'Z[irr G]}.

Let Isigma : {in 'Z[irr W] &, isometry sigma}.
Let Zsigma : {in 'Z[irr W], phi, sigma phi \in 'Z[irr G]}.

Lemma cycTIisometry : isometry sigma.

Lemma cycTIiso_vchar i j : eta_ i j \in 'Z[irr G].

Lemma cfdot_cycTIiso i1 i2 j1 j2 :
  '[eta_ i1 j1, eta_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.

Lemma cfnorm_cycTIiso i j : '[eta_ i j] = 1.

Lemma cycTIiso_dirr i j : sigma (w_ i j) \in dirr G.

Lemma cycTIiso_orthonormal : orthonormal im_sigma.

Lemma cycTIiso_eqE i1 i2 j1 j2 :
  (eta_ i1 j1 == eta_ i2 j2) = ((i1 == i2) && (j1 == j2)).

Lemma cycTIiso_neqN i1 i2 j1 j2 : (eta_ i1 j1 == - eta_ i2 j2) = false.

Lemma cycTIiso1 : sigma 1 = 1.

Lemma cycTIiso_Ind : {in 'CF(W, V), phi, sigma phi = 'Ind[G, W] phi}.

Let sigma_Res_V :
  [/\ phi, {in V, sigma phi =1 phi}
    & psi : 'CF(G), orthogonal psi im_sigma{in V, psi =1 \0}].

This is Peterfalvi, Theorem (3.2)(d).
Theorem cycTIiso_restrict phi : {in V, sigma phi =1 phi}.

This is Peterfalvi, Theorem (3.2)(e).
Theorem ortho_cycTIiso_vanish (psi : 'CF(G)) :
  orthogonal psi im_sigma{in V, x, psi x = 0}.

This is PeterFalvi (3.7).
Lemma cycTIiso_cfdot_exchange (psi : 'CF(G)) i1 i2 j1 j2 :
    {in V, x, psi x = 0}
  '[psi, eta_ i1 j1] + '[psi, eta_ i2 j2]
     = '[psi, eta_ i1 j2] + '[psi, eta_ i2 j1].

This is NC as defined in PeterFalvi (3.6).
Definition cyclicTI_NC phi := #|[set ij | '[phi, eta_ ij.1 ij.2] != 0]|.
Local Notation NC := cyclicTI_NC.

Lemma cycTI_NC_opp (phi : 'CF(G)) : (NC (- phi)%R = NC phi)%N.

Lemma cycTI_NC_sign (phi : 'CF(G)) n : (NC ((-1) ^+ n *: phi)%R = NC phi)%N.

Lemma cycTI_NC_iso i j : NC (eta_ i j) = 1%N.

Lemma cycTI_NC_irr i : (NC 'chi_i 1)%N.

Lemma cycTI_NC_dirr f : f \in dirr G → (NC f 1)%N.

Lemma cycTI_NC_dchi di : (NC (dchi di) 1)%N.

Lemma cycTI_NC_0 : NC 0 = 0%N.

Lemma cycTI_NC_add n1 n2 phi1 phi2 :
  (NC phi1 n1NC phi2 n2NC (phi1 + phi2)%R n1 + n2)%N.

Lemma cycTI_NC_sub n1 n2 phi1 phi2 :
  (NC phi1 n1NC phi2 n2NC (phi1 - phi2)%R n1 + n2)%N.

Lemma cycTI_NC_scale_nz a phi : a != 0 → NC (a *: phi) = NC phi.

Lemma cycTI_NC_scale a phi n : (NC phi nNC (a *: phi) n)%N.

Lemma cycTI_NC_norm phi n :
  phi \in 'Z[irr G]'[phi] n%:R → (NC phi n)%N.

This is PeterFalvi (3.8).
Lemma small_cycTI_NC phi i0 j0 (a0 := '[phi, eta_ i0 j0]) :
    {in V, x, phi x = 0} → (NC phi < 2 × minn w1 w2)%Na0 != 0 →
     ( i j, '[phi, eta_ i j] = (j == j0)%:R × a0)
   ( i j, '[phi, eta_ i j] = (i == i0)%:R × a0).

A weaker version of PeterFalvi (3.8).
Lemma cycTI_NC_minn (phi : 'CF(G)) :
    {in V, x, phi x = 0} → (0 < NC phi < 2 × minn w1 w2)%N
  (minn w1 w2 NC phi)%N.

Another consequence of (3.8), used in (4.8), (10.5), (10.10) and (11.8).
Lemma eq_signed_sub_cTIiso phi e i j1 j2 :
    let rho := (-1) ^+ e *: (eta_ i j1 - eta_ i j2) in
    phi \in 'Z[irr G]'[phi] = 2%:Rj1 != j2
  {in V, phi =1 rho}phi = rho.

This is PeterFalvi (3.9)(a).
Lemma eq_in_cycTIiso (i : Iirr W) (phi : 'CF(G)) :
  phi \in dirr G{in V, phi =1 'chi_i}phi = sigma 'chi_i.

This is the second part of Peterfalvi (3.9)(a).
Lemma cfAut_cycTIiso u phi : cfAut u (sigma phi) = sigma (cfAut u phi).

Section AutCyclicTI.

Variable iw : Iirr W.
Let w := 'chi_iw.
Let a := #[w]%CF.

Let Zsigw : sigma w \in 'Z[irr G].

Let lin_w: w \is a linear_char := Wlin iw.

This is Peterfalvi (3.9)(b).
Lemma cycTIiso_aut_exists k :
    coprime k a
  [/\ u, sigma (w ^+ k) = cfAut u (sigma w)
    & x, coprime #[x] asigma (w ^+ k) x = sigma w x].

This is Peterfalvi (3.9)(c).
Lemma Cint_cycTIiso_coprime x : coprime #[x] asigma w x \in Cint.

End AutCyclicTI.

End Three.

Implicit Arguments ortho_cycTIiso_vanish [gT G W W1 W2 defW psi].

Lemma cycTIisoC (gT : finGroupType) (G W W1 W2 : {group gT})
                (defW12 : W1 \x W2 = W) (ctiW12 : cyclicTI_hypothesis G defW12)
                (defW21 : W2 \x W1 = W) (ctiW21 : cyclicTI_hypothesis G defW21)
                i j :
   cyclicTIiso ctiW12 (cyclicTIirr defW12 i j)
     = cyclicTIiso ctiW21 (cyclicTIirr defW21 j i).

Lemma cycTIiso_irrel (gT : finGroupType) (G W W1 W2 : {group gT})
                (defW : W1 \x W2 = W) (ctiW : cyclicTI_hypothesis G defW)
                (defW' : W1 \x W2 = W) (ctiW' : cyclicTI_hypothesis G defW') :
   cyclicTIiso ctiW = cyclicTIiso ctiW'.