import .Logic .Residual

open eq eq.ops unit bool sum sigma sigma.ops prod prod.ops trunc trunc_index

namespace cegar_hott

structure BoolGraph :=
  (initial : bool -> bool)
  (edge : bool -> bool -> bool)
  (bad : bool -> bool)

inductive KeyPath : Type0 :=
| start : bool -> KeyPath
| next : bool -> KeyPath -> KeyPath

definition equal_bool (x y : bool) : bool :=
  bool.rec_on x (bnot y) y

definition eq_reflect (x y : bool) : Reflection (equal_bool x y) (x = y) :=
begin
  cases x,
  { cases y,
    { exact Reflection.mk (fun  h, idp) (fun  h, idp) },
    { exact Reflection.mk (fun  h, h) (fun  h, h) } },
  { cases y,
    { exact Reflection.mk (fun  h, h-1) (fun  h, h-1) },
    { exact Reflection.mk (fun  h, idp) (fun  h, idp) } }
end

definition ref_exists_bool {P : bool -> Type0} {f : bool -> bool}
  (rf : Reflection (f ff) (P ff)) (rt : Reflection (f tt) (P tt)) :
  Reflection (bor (f ff) (f tt)) (Sigma  x : bool, P x) :=
  Reflection.mk
    (fun  h, sum.elim (or_of_bor_eq h)
      (fun  p, <ff, Reflection.decode rf p>)
      (fun  p, <tt, Reflection.decode rt p>))
    (fun  w, (bool.rec_on w.1
      (fun  p, bor_inl (Reflection.encode rf p))
      (fun  p, bor_inr (Reflection.encode rt p))) w.2)

definition EndLift (g : BoolGraph) (q : bool -> bool) (w : KeyPath) :
  bool -> Type0 :=
  KeyPath.rec_on w
    (fun  a x, (q x = a) * (BoolGraph.initial g x = tt))
    (fun  a p L y, (q y = a) *
      (Sigma  x : bool, L x * (BoolGraph.edge g x y = tt)))

definition EndTest (g : BoolGraph) (q : bool -> bool) (w : KeyPath) :
  bool -> bool :=
  KeyPath.rec_on w
    (fun  a x, band (equal_bool (q x) a) (BoolGraph.initial g x))
    (fun  a p L y, band (equal_bool (q y) a)
      (bor (band (L ff) (BoolGraph.edge g ff y))
           (band (L tt) (BoolGraph.edge g tt y))))

definition ref_atom (b : bool) : Reflection b (b = tt) :=
  Reflection.mk (fun  h, h) (fun  h, h)

definition end_reflect (g : BoolGraph) (q : bool -> bool) (w : KeyPath) :
  Pi  x : bool, Reflection (EndTest g q w x) (EndLift g q w x) :=
  KeyPath.rec_on w
    (fun  a x, ref_both (eq_reflect (q x) a) (ref_atom (BoolGraph.initial g x)))
    (fun  a p R y, ref_both (eq_reflect (q y) a)
      (ref_exists_bool
        (ref_both (R ff) (ref_atom (BoolGraph.edge g ff y)))
        (ref_both (R tt) (ref_atom (BoolGraph.edge g tt y)))))

definition BadLift (g : BoolGraph) (q : bool -> bool) (w : KeyPath) : Type0 :=
  Sigma  x : bool, EndLift g q w x * (BoolGraph.bad g x = tt)

definition BadTest (g : BoolGraph) (q : bool -> bool) (w : KeyPath) : bool :=
  bor (band (EndTest g q w ff) (BoolGraph.bad g ff))
      (band (EndTest g q w tt) (BoolGraph.bad g tt))

definition bad_reflect (g : BoolGraph) (q : bool -> bool) (w : KeyPath) :
  Reflection (BadTest g q w) (BadLift g q w) :=
  ref_exists_bool
    (ref_both (end_reflect g q w ff) (ref_atom (BoolGraph.bad g ff)))
    (ref_both (end_reflect g q w tt) (ref_atom (BoolGraph.bad g tt)))

definition lift_from_test {g : BoolGraph} {q : bool -> bool} {w : KeyPath}
  (h : BadTest g q w = tt) : BadLift g q w :=
  Reflection.decode (bad_reflect g q w) h

definition no_lift_from_test {g : BoolGraph} {q : bool -> bool} {w : KeyPath}
  (h : BadTest g q w = ff) : BadLift g q w -> empty :=
  fun  z, ff_ne_tt (h-1  @  Reflection.encode (bad_reflect g q w) z)

definition support_from_test {g : BoolGraph} {q : bool -> bool} {w : KeyPath}
  (h : BadTest g q w = tt) : trunc -1 (BadLift g q w) :=
  tr (lift_from_test h)

definition spurious_graph : BoolGraph :=
  BoolGraph.mk bnot equal_bool (fun  x, x)

definition merge_keys : bool -> bool := fun  x, ff

definition spurious_path : KeyPath := KeyPath.start ff

definition spurious_start_may :
  (Sigma  x : bool, (merge_keys x = ff) * (BoolGraph.initial spurious_graph x = tt)) :=
  <ff, (idp, idp)>

definition spurious_bad_may :
  (Sigma  x : bool, (merge_keys x = ff) * (BoolGraph.bad spurious_graph x = tt)) :=
  <tt, (idp, idp)>

definition spurious_path_refuted :
  BadLift spurious_graph merge_keys spurious_path -> empty :=
  no_lift_from_test idp

definition reachable_graph : BoolGraph :=
  BoolGraph.mk bnot (fun  x y, band (bnot x) y) (fun  x, x)

definition reachable_path : KeyPath := KeyPath.next ff spurious_path

definition reachable_path_lifts :
  BadLift reachable_graph merge_keys reachable_path :=
  lift_from_test idp

end cegar_hott
