meta.v

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype path tuple finfun bigop finset order.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section EqSeq.

Variables (T : eqType).
Implicit Type (xs ys p : seq T).

Variant split_first x : seq T -> seq T -> seq T -> Type :=
  SplitFirst p1 p2 : x \notin p1 -> split_first x (rcons p1 x ++ p2) p1 p2.

Lemma split_firstP p x (i := index x p) :
  x \in p -> split_first x p (take i p) (drop i.+1 p).
Proof.
have: x \notin take i p by apply/negP => /index_ltn; rewrite ltnn.
by move=> + x_in_p; case/splitP: x_in_p; constructor.
Qed.

Variant split_last x : seq T -> Type :=
  SplitLast p1 p2 : x \notin p2 -> split_last x (rcons p1 x ++ p2).

Lemma split_lastP p x : x \in p -> split_last x p.
Proof.
rewrite -[p]revK mem_rev => /split_firstP[p1 p2].
by rewrite -mem_rev rev_cat rev_rcons -cat_rcons; constructor.
Qed.

End EqSeq.

Definition oadd (T : Type) (x y : option T) : option T :=
  if x is Some _ then x else y.

(******************************************************************************)
(* PART I : soundness and completeness of coherence checking                  *)
(******************************************************************************)
Module coherence_checking.
Section coherence_checking.

Variable (V : finType).  (* set of coercion classes, stands for vectices      *)
Variable (E : eqType).   (* set of implicit coercions, stands for edges       *)
Variable (source_class target_class : E -> V).
                         (* source and target classes of a coercion           *)

(* set of declared implicit coercions, listed newest first, to oldest last    *)
Implicit Types (delta : seq E).
(* coercion classes                                                           *)
Implicit Types (source middle target : V).
(* coercion paths                                                             *)
Implicit Types (p q : seq E).

(* [pathcoe delta source target p]: [p] is a coercion path from [source] to   *)
(* [target] under the set of declared implicit coercions [delta].             *)
Fixpoint path delta source target p :=
  if p is f :: p then
    [&& f \in delta, source == source_class f &
                     path delta (target_class f) target p]
  else
    source == target.

Lemma path_nil delta class : path delta class class [::]. Proof. by simpl. Qed.
Hint Resolve path_nil.

Lemma path_subgraph delta delta' source target p :
  {subset delta <= delta'} ->
  path delta source target p -> path delta' source target p.
Proof.
by elim: p source => //= f p IHp source Hsub /and3P[/Hsub -> ->]; exact: IHp.
Qed.

Lemma path_cons coe delta source target p :
  path delta source target p -> path (coe :: delta) source target p.
Proof. by apply: path_subgraph => ? ?; rewrite inE; apply/orP; right. Qed.

Lemma path_consE coe delta source target p :
  coe \notin p ->
  path (coe :: delta) source target p = path delta source target p.
Proof.
elim: p source => //= f p IHp source; rewrite !inE negb_or.
by move=> /andP[coe_f /IHp ->]; rewrite eq_sym (negbTE coe_f).
Qed.

Lemma path_subset_coes delta source target p :
  path delta source target p -> {subset p <= delta}.
Proof.
elim: p source => //= f p IHp source /and3P[f_delta _ /IHp p_delta ?].
by rewrite inE => /predU1P[->|/p_delta].
Qed.

Lemma path_cat delta source middle target p q :
  path delta source middle p -> path delta middle target q ->
  path delta source target (p ++ q).
Proof.
elim: p source => [source /eqP -> //|].
move=> f p IHp source /= /and3P[-> ->]; exact: IHp.
Qed.

Lemma path_catP delta source target p q :
  reflect
    (exists2 middle, path delta source middle p & path delta middle target q)
    (path delta source target (p ++ q)).
Proof.
apply: (iffP idP) => [|[middle]]; last exact: path_cat.
elim: p source => [|f p IHp] source /=; first by exists source.
by move=> /and3P[-> ->] /IHp[middle ? ?]; exists middle.
Qed.
Arguments path_catP {delta source target p q}.

Lemma path_rcons delta source target p f :
  path delta source target (rcons p f) =
  [&& f \in delta, target == target_class f &
                   path delta source (source_class f) p].
Proof.
elim: p source => [? | g p IHp source] /=; last by rewrite IHp; do !bool_congr.
by do !bool_congr; rewrite eq_sym.
Qed.

Lemma path_undup delta source target p :
  path (undup delta) source target p = path delta source target p.
Proof. by elim: p source => //= f p IHp source; rewrite mem_undup IHp. Qed.

(* [connect delta source target] is [true] iff there is a coercion path from  *)
(* [source] to [target] under the set of declared implicit coercions [delta]. *)
Fixpoint connect delta source target : bool :=
  if delta is coe :: delta then
    connect delta source target
    || connect delta source (source_class coe)
    && connect delta (target_class coe) target
  else source == target.

Lemma path_connect delta source target p :
  path delta source target p -> connect delta source target.
Proof.
elim: delta p => [[] //|coe delta IHdelta p] in source target *.
have [{p} /split_firstP[p1 p2 coe_p1]|coe_p] := boolP (coe \in p); last first.
  by rewrite path_consE => //= /IHdelta ->.
move=> /path_catP[?]; rewrite path_rcons mem_head /= => /andP[/eqP ->].
rewrite path_consE // => /IHdelta ->.
have [/split_lastP[{}p2 p3 coe_p3]|coe_p2] := boolP (coe \in p2); last first.
  by rewrite path_consE // => /IHdelta ->; rewrite orbT.
move=> /path_catP[middle]; rewrite path_rcons mem_head /= => /andP[/eqP -> _].
by rewrite path_consE // => /IHdelta ->; rewrite orbT.
Qed.
Arguments path_connect {delta source target} p.

Lemma connectP delta source target :
  reflect (exists p, path delta source target p) (connect delta source target).
Proof.
apply: (iffP idP) => [|[p]]; last exact: path_connect.
elim: delta => [|coe delta IHdelta] in source target *; first by exists [::].
move=> /= /orP[/IHdelta[p Hp]|/andP[/IHdelta[p Hp] /IHdelta[q Hq]]].
  by exists p; apply: path_cons.
exists (rcons p coe ++ q); apply/path_cat/path_cons/Hq.
by rewrite path_rcons mem_head eqxx path_cons.
Qed.

Lemma connect_refl delta : reflexive (connect delta).
Proof. by move=> ?; apply/connectP; exists [::] => /=. Qed.
Hint Resolve connect_refl.

Lemma connect_cc delta class : connect delta class class.
Proof. exact: connect_refl. Qed.
Hint Resolve connect_cc.

Lemma connect_trans delta : transitive (connect delta).
Proof.
move=> y x z /connectP [p path_p] /connectP [q path_q].
by apply/connectP; exists (p ++ q); apply/path_catP; exists y.
Qed.

Lemma connect_stepl delta f target :
  f \in delta -> connect delta (target_class f) target ->
  connect delta (source_class f) target.
Proof.
move=> f_delta; apply/connect_trans/connectP; exists [:: f].
by rewrite /= f_delta !eqxx.
Qed.

Lemma connect_stepr delta source f :
  f \in delta -> connect delta source (source_class f) ->
  connect delta source (target_class f).
Proof.
move=> f_delta /connect_trans; apply; apply/connectP; exists [:: f].
by rewrite /= f_delta !eqxx.
Qed.

Lemma connect_undup delta : connect (undup delta) =2 connect delta.
Proof.
move=> source target.
by apply/connectP/connectP => [] [p Hp]; exists p; move: Hp; rewrite path_undup.
Qed.

(* [repr delta class] is the representative element of the strongly connected *)
(* component including [class] in the graph [delta].                          *)
Fixpoint repr delta class : V :=
  if delta is coe :: delta then
    if connect delta (target_class coe) class
       && connect delta class (source_class coe) then
      repr delta (target_class coe)
    else
      repr delta class
  else
    class.

Lemma connect_repr delta class : connect delta class (repr delta class).
Proof.
elim: delta class => //= coe delta IHdelta class.
by case: ifP; rewrite ?IHdelta //= => /andP[_ ->]; rewrite orbT.
Qed.

Lemma repr_connect delta class : connect delta (repr delta class) class.
Proof.
elim: delta class => //= coe delta IHdelta class.
case: ifP; rewrite ?IHdelta //= => /andP[connect_tc connect_cs].
rewrite (connect_trans _ (connect_trans connect_tc connect_cs)) //=.
by rewrite connect_tc orbT.
Qed.

Lemma connect_reprEl delta source target :
  connect delta (repr delta source) target = connect delta source target.
Proof.
by apply/idP/idP; apply/connect_trans;
  [apply/connect_repr | apply/repr_connect].
Qed.

Lemma connect_reprEr delta source target :
  connect delta source (repr delta target) = connect delta source target.
Proof.
by apply/idP/idP => /connect_trans; apply;
  [apply/repr_connect | apply/connect_repr].
Qed.

Lemma reprE delta class class' :
  repr delta class == repr delta class' =
  connect delta class class' && connect delta class' class.
Proof.
apply/eqP/idP => [reprE|/andP[]].
  by apply/andP; split; apply/connect_trans/repr_connect;
    rewrite (reprE, =^~reprE) connect_repr.
elim: delta class class' => /= [class class' /eqP -> //|].
move=> coe delta IHdelta class class'.
case: (boolP (connect _ class (source_class _))) => connect_cs;
  case: (boolP (connect _ class' (source_class _))) => connect_cs';
  rewrite ?orbF ?andbT ?andbF /=; last first.
- exact: IHdelta.
- by move=> cc' _; move: connect_cs; rewrite (connect_trans cc').
- by move=> _ c'c; move: connect_cs'; rewrite (connect_trans c'c).
case: (boolP (connect _ (target_class _) class)) => connect_tc;
  case: (boolP (connect _ (target_class _) class')) => connect_tc';
  rewrite ?orbF ?orbT => //= cc' c'c.
- by move: connect_tc'; rewrite (connect_trans connect_tc).
- by move: connect_tc; rewrite (connect_trans connect_tc').
- exact: IHdelta.
Qed.

Lemma reprI delta class : repr delta (repr delta class) = repr delta class.
Proof. by apply/eqP; rewrite reprE repr_connect connect_repr. Qed.

Lemma repr_undup delta : repr (undup delta) =1 repr delta.
Proof.
elim: delta => //= coe delta IHdelta class.
case: ifP; rewrite /= ?IHdelta ?connect_undup //.
case: ifP => // /andP[connect_tc connect_cs] coe_delta.
by apply/eqP; rewrite reprE connect_tc connect_stepr.
Qed.

(* [eq_closure_paths eqps p q] is true if (p, q) is in the congruence closure *)
(* of [eqps].                                                                 *)
Inductive eq_closure (eqps : seq (seq E * seq E)) :
  seq E -> seq E -> Prop :=
  | eq_closure_refl p : eq_closure eqps p p
  | eq_closure_sym p1 p2 : eq_closure eqps p1 p2 -> eq_closure eqps p2 p1
  | eq_closure_trans p1 p2 p3 :
      eq_closure eqps p1 p2 -> eq_closure eqps p2 p3 -> eq_closure eqps p1 p3
  | eq_closure_cat p1 q1 p2 q2 :
      eq_closure eqps p1 p2 -> eq_closure eqps q1 q2 ->
      eq_closure eqps (p1 ++ q1) (p2 ++ q2)
  | eq_closure_atom p1 p2 : (p1, p2) \in eqps -> eq_closure eqps p1 p2.

Lemma eq_closure_catl eqps p q1 q2 :
  eq_closure eqps q1 q2 -> eq_closure eqps (p ++ q1) (p ++ q2).
Proof. by do 2 constructor => //. Qed.

Lemma eq_closure_catr eqps p1 p2 q :
  eq_closure eqps p1 p2 -> eq_closure eqps (p1 ++ q) (p2 ++ q).
Proof. by do 2 constructor => //. Qed.

Lemma eq_closure_subset eqps eqps' p q :
  {subset eqps <= eqps'} -> eq_closure eqps p q -> eq_closure eqps' p q.
Proof.
move=> subeqps; elim/eq_closure_ind: p q /; try by constructor.
  by move=> p1 p2 p3 _ p12 _; apply: eq_closure_trans.
by move=> p1 p2 /subeqps; constructor.
Qed.

(* [validcoe delta source target] is [Some p] where [p] is the valid coercion *)
(* path from [source] to [target]. It is [None] if there is no path.          *)
Fixpoint validcoe delta source target : option (seq E) :=
  if delta is coe :: delta then
    let new_path :=
        match validcoe delta source (source_class coe),
              validcoe delta (target_class coe) target with
        | Some p, Some q => Some (rcons p coe ++ q)
        | _, _ => None
        end
    in oadd (validcoe delta source target) new_path
  else
    if source == target then Some [::] else None.

Lemma valid_path delta source target p :
  validcoe delta source target = Some p -> path delta source target p.
Proof.
suff {p}: if validcoe delta source target is Some p then
            path delta source target p else true.
  by case: validcoe => //= ? ? [<-].
elim: delta source target => [|coe delta IHdelta] source target /=.
  by case: eqVneq => [->|neq_st] //=.
case: validcoe (IHdelta source target) => [p|_] /=; first exact: path_cons.
case: validcoe (IHdelta source (source_class coe)) => // p Hp.
case: validcoe (IHdelta (target_class coe) target) => // q Hq.
by apply/path_cat/path_cons/Hq; rewrite path_rcons mem_head eqxx path_cons.
Qed.

Lemma connectE delta source target :
  connect delta source target = (validcoe delta source target != None).
Proof.
elim: delta => [/= |coe delta IHdelta] in source target *; first by case: eqP.
by rewrite /= !IHdelta; do 3 case: validcoe => [?|] //=.
Qed.

Lemma valid_cycle delta class : validcoe delta class class = Some [::].
Proof. by elim: delta => /= [|coe delta ->]; rewrite ?eqxx. Qed.

Lemma path_valid delta source target p :
  path delta source target p -> validcoe delta source target != None.
Proof. by move/path_connect; rewrite connectE. Qed.
Arguments path_valid {delta source target} p.

Lemma valid_undup delta : validcoe (undup delta) =2 validcoe delta.
Proof.
elim: delta => //= coe delta IHdelta source target; rewrite -!IHdelta.
case: (boolP (coe \in delta)) => coe_delta //=.
case def_p: validcoe => [p|] //=.
case def_q1: validcoe => [q1|] //=; case def_q2: validcoe => [q2|] //=.
apply/contra_eq: def_p => _; rewrite -connectE.
apply: (connect_trans (y := source_class coe)).
  exact/path_connect/valid_path/def_q1.
by apply/connect_stepl/path_connect/valid_path/def_q2; rewrite mem_undup.
Qed.

Definition eq_paths_step coe delta source target : option (seq E * seq E) :=
  match validcoe delta source (source_class coe),
        validcoe delta (target_class coe) target,
        validcoe delta source target with
  | Some p1, Some p2, Some q =>
    if [|| repr delta source != source,
           repr delta target != target |
           [exists mid,
               [&& connect delta source mid, connect delta mid target
                   & connect delta mid (source_class coe)
                     && ~~ connect delta mid source
                     || connect delta (target_class coe) mid
                     && ~~ connect delta target mid]]]
    then None else Some (rcons p1 coe ++ p2, q)
  | _, _, _ => None
  end.

Fixpoint eq_paths delta : seq (seq E * seq E) :=
  if delta is coe :: delta then
    if coe \in delta then
      eq_paths delta
    else
      pmap (fun '(source, target) => eq_paths_step coe delta source target)
           (enum {:V * V}) ++ eq_paths delta
  else
    [::].

Lemma eq_paths_undup delta : eq_paths (undup delta) = eq_paths delta.
Proof.
elim: delta => //= coe delta; case: ifP => //=; rewrite mem_undup => -> ->.
congr cat; apply/eq_pmap => -[source target].
rewrite /eq_paths_step !valid_undup !repr_undup; do 3 case: validcoe => // ?.
congr (if [||_, _ | _] then _ else _); apply/eq_existsb => ?.
by rewrite !connect_undup.
Qed.

Lemma eq_paths_sound delta p q : (p, q) \in eq_paths delta ->
  exists source target,
    path delta source target p && path delta source target q.
Proof.
elim: delta => //= coe delta IHdelta.
case: (boolP (coe \in delta)) => [coe_delta /IHdelta[s [t /andP[]]]|coe_delta].
  by exists s, t; rewrite !path_cons.
rewrite mem_cat => /orP[|/IHdelta[s [t /andP[]]]]; last first.
  by exists s, t; rewrite !path_cons.
rewrite mem_pmap => /mapP [[source target] _]; rewrite /eq_paths_step.
case p1_def: validcoe => [p1|] //; case p2_def: validcoe => [p2|] //.
case q_def: validcoe => [q'|] //; case: ifP => // _ [-> ->].
exists source, target; rewrite (path_cons _ (valid_path q_def)) andbT.
apply/path_cat/path_cons/valid_path/p2_def.
by rewrite path_rcons mem_head eqxx path_cons // valid_path.
Qed.

Lemma eq_paths_complete delta source target p q :
  path delta source target p -> path delta source target q ->
  eq_closure (eq_paths delta) p q.
Proof.
elim: delta => [|coe delta IHdelta] in source target p q *.
  by case: p q => // -[] // _ _; constructor.
rewrite [eq_paths _]/=; case: (boolP (coe \in delta)) => coe_delta.
  rewrite -![path (_ :: _) _ _ _]path_undup /= coe_delta !path_undup.
  exact/IHdelta.
set eqs := _ ++ eq_paths _.
have {}IHdelta source' target' p' q' : path delta source' target' p' ->
    path delta source' target' q' -> eq_closure eqs p' q'.
  move=> Hp' Hq'; apply/eq_closure_subset/IHdelta/Hq'/Hp' => ?.
  by rewrite mem_cat => ->; rewrite orbT.
suff Hwlog p' q' : path (coe :: delta) source target p' ->
                   validcoe (coe :: delta) source target = Some q' ->
                   eq_closure eqs p' q'.
  move=> /[dup] /path_valid + /Hwlog + /Hwlog; case: validcoe => //= p' _ Hp Hq.
  exact/eq_closure_trans/eq_closure_sym/Hq/erefl/Hp.
move: p' q' => {}p {}q; have [n] := ubnP (size p).
elim: n => // n IHn in source target p q * => /ltnSE.
case: (boolP (coe \in p)) => [/split_firstP[p1 p2 coe_p1]|coe_p]; last first.
  rewrite path_consE //= => _ /[dup] /path_valid.
  case def_q: validcoe => [{}q|] //= _ path_p [<-].
  exact/IHdelta/valid_path/def_q.
move=> le_n /path_catP[mid]; rewrite path_rcons => /and3P[_ /eqP->] {p mid}.
case: (boolP (coe \in p2)) le_n => [/split_lastP[{}p2 p3 coe_p3] | coe_p2 _].
  move=> le_n path_p1 /path_catP [mid].
  rewrite path_rcons => /and3P[_ /eqP-> path_p2] path_p3 def_q.
  have: path (coe :: delta) source target (rcons p1 coe ++ p3).
    by apply/path_cat/path_p3; rewrite path_rcons mem_head eqxx.
  move=> /(IHn _ _ (rcons p1 coe ++ p3) q (leq_trans _ le_n)).
  rewrite !size_cat ltn_add2l -add1n leq_add2r size_rcons => /(_ isT def_q).
  rewrite -{1}[p3]cat0s; apply/eq_closure_trans/eq_closure_catl/eq_closure_catr.
  apply/IHn/(valid_cycle _ (target_class coe));
    last by rewrite path_rcons mem_head eqxx.
  apply: leq_trans le_n.
  by rewrite !size_cat !size_rcons !addSn addnS addnCA leq_addr.
rewrite !path_consE //= => {n IHn coe_p1 coe_p2} path_p1 path_p2.
(******************************************************************************)
case def_q: validcoe => [q'|] /=; last first.
  case def_p1: validcoe (path_valid _ path_p1) => [p1'|] // _.
  case def_p2: validcoe (path_valid _ path_p2) => [p2'|] // _ [<-].
  apply/eq_closure_cat/IHdelta/valid_path/def_p2/path_p2.
  by rewrite -!cats1; apply/eq_closure_catr/IHdelta/valid_path/def_p1/path_p1.
move: q' def_q => {}q /valid_path path_q [<-].
pose classes_between source target :=
  #|predI (connect delta source) (connect delta ^~ target)|.
have [n] := ubnP (classes_between source target).
elim: n => // n IHn in source target p1 p2 q path_p1 path_p2 path_q *.
move=> /ltnSE le_n.
have/connectP[s1 path_s1] := repr_connect delta source.
have/connectP[s2 path_s2] := connect_repr delta source.
have/connectP[t1 path_t1] := connect_repr delta target.
have/connectP[t2 path_t2] := repr_connect delta target.
suff Hrepr: eq_closure eqs (rcons (s1 ++ p1) coe ++ p2 ++ t1) (s1 ++ q ++ t1).
  have path_s := path_cat path_s2 path_s1.
  have path_t := path_cat path_t1 path_t2; rewrite -[q]cat0s.
  apply/eq_closure_trans/eq_closure_catr/eq_closure_sym/IHdelta/path_s => //.
  rewrite -[(_ ++ _) ++ _]cats0.
  apply/eq_closure_trans/eq_closure_catl/eq_closure_sym/IHdelta/path_t => //.
  rewrite catA -2!(catA s2) -(catA s1).
  apply/eq_closure_trans/eq_closure_catr/eq_closure_catl/Hrepr.
  rewrite 2![_ ++ _ ++ t1]catA -catA.
  apply/eq_closure_trans/eq_closure_catl/IHdelta/path_t => //.
  rewrite cats0 catA -rcons_cat catA rcons_cat -catA.
  by apply/eq_closure_trans/eq_closure_catr/IHdelta/path_s => //; constructor.
move: (path_cat path_s1 (path_cat path_q path_t1)).
move: (path_cat path_s1 path_p1) (path_cat path_p2 path_t1).
move: (_ ++ p1) (p2 ++ _) (_ ++ q ++ _).
move=> {s1 s2 t1 t2 path_s1 path_s2 path_t1 path_t2}.
set source' := repr delta source; set target' := repr delta target.
move=> {}p1 {}p2 {}q {}path_p1 {}path_p2 {}path_q.
case def_p1: validcoe (path_valid _ path_p1) => [p1'|] _ //.
case def_p2: validcoe (path_valid _ path_p2) => [p2'|] _ //.
case def_q: validcoe (path_valid _ path_q) => [q'|] _ //.
apply/eq_closure_trans/IHdelta/path_q/valid_path/def_q.
suff {path_p1 path_p2 path_q} : eq_closure eqs (rcons p1' coe ++ p2') q'.
  apply/eq_closure_trans/eq_closure_cat/IHdelta/valid_path/def_p2/path_p2.
  by rewrite -!cats1; apply/eq_closure_catr/IHdelta/valid_path/def_p1/path_p1.
move: p1' p2' q' => {}p1 {}p2 {}q in def_p1 def_p2 def_q *.
case def_eq: (eq_paths_step coe delta source' target') => [[p' q']|].
  apply/eq_closure_atom; rewrite mem_cat mem_pmap; apply/orP; left; apply/mapP.
  exists (source', target'); rewrite ?mem_enum //; move: def_eq.
  by rewrite /eq_paths_step def_p1 def_p2 def_q /=; case: ifP.
move: def_eq; rewrite /eq_paths_step def_p1 def_p2 def_q; case: ifP => // + _.
rewrite /source' /target' !reprI !eqxx /= -/source' -/target'.
move=> /existsP[mid] /and3P[/connectP[sm path_sm] /connectP[mt path_mt]]
       /orP[/andP[/connectP[mc path_mc]] | /andP[/connectP[cm path_cm]]].
- rewrite connect_reprEr => connectNms.
  apply/eq_closure_trans/IHdelta/valid_path/def_q/path_cat/path_mt/path_sm.
  rewrite cat_rcons; apply/eq_closure_sym/eq_closure_trans/eq_closure_catr
                          /IHdelta/valid_path/def_p1/path_cat/path_mc/path_sm.
  rewrite -catA -cat_rcons; apply/eq_closure_catl/eq_closure_sym.
  apply: IHn path_mc (valid_path def_p2) path_mt _; apply: leq_trans le_n.
  apply/proper_card/properP; split.
    apply/subsetP => ?; rewrite !inE connect_reprEr => /andP[+ ->].
    move/path_connect: path_sm; rewrite connect_reprEl andbT.
    exact: connect_trans.
  have:= path_connect _ (valid_path def_q).
  rewrite connect_reprEl connect_reprEr => connect_st.
  by exists source; rewrite !inE ?connect_reprEr connect_st ?andbT.
- rewrite connect_reprEl => connectNtm.
  apply/eq_closure_trans/IHdelta/valid_path/def_q/path_cat/path_mt/path_sm
       /eq_closure_sym/eq_closure_trans/eq_closure_catl/IHdelta/valid_path
       /def_p2/path_cat/path_mt/path_cm.
  rewrite catA; apply/eq_closure_catr/eq_closure_sym.
  apply: IHn (valid_path def_p1) path_cm path_sm _; apply:leq_trans le_n.
  apply/proper_card/properP; split.
    apply/subsetP => ?; rewrite !inE connect_reprEl.
    move=> /andP[->] /connect_trans -> //; move: (path_connect _ path_mt).
    by rewrite connect_reprEr.
  have:= path_connect _ (valid_path def_q).
  rewrite connect_reprEl connect_reprEr => connect_st.
  by exists target; rewrite !inE ?connect_reprEl connect_st /=.
Qed.

End coherence_checking.
End coherence_checking.