import types.bool types.prod hit.trunc

open eq eq.ops is_trunc trunc unit prod prod.ops sum bool

namespace cegar_hott

inductive Formula (A : Type) : Type :=
| top : Formula A
| bot : Formula A
| atom : A -> Formula A
| both : Formula A -> Formula A -> Formula A
| either : Formula A -> Formula A -> Formula A
| impl : Formula A -> Formula A -> Formula A

open Formula

definition Holds {A : Type} (v : A -> bool) (f : Formula A) : Type0 :=
  @Formula.rec_on A (fun  f, Type0) f unit empty (fun  a, v a = tt)
    (fun  p q P Q, P * Q)
    (fun  p q P Q, trunc -1 (P + Q))
    (fun  p q P Q, P -> Q)

definition test {A : Type} (v : A -> bool) (f : Formula A) : bool :=
  Formula.rec_on f tt ff v
    (fun  p q b c, band b c)
    (fun  p q b c, bor b c)
    (fun  p q b c, bor (bnot b) c)

structure Reflection (b : bool) (P : Type) :=
  (decode : b = tt -> P)
  (encode : P -> b = tt)

open Reflection

definition ref_both {b c : bool} {P Q : Type} (r : Reflection b P)
  (s : Reflection c Q) : Reflection (band b c) (P * Q) :=
  Reflection.mk
    (fun  h, (decode r (band_elim_left h), decode s (band_elim_right h)))
    (fun  h, band_intro (encode r h.1) (encode s h.2))

definition ref_either {b c : bool} {P Q : Type} (r : Reflection b P)
  (s : Reflection c Q) : Reflection (bor b c) (trunc -1 (P + Q)) :=
  Reflection.mk
    (fun  h, sum.elim (or_of_bor_eq h)
      (fun  p, tr (sum.inl (decode r p)))
      (fun  q, tr (sum.inr (decode s q))))
    (trunc.elim (fun  z, sum.elim z
      (fun  p, bor_inl (encode r p))
      (fun  q, bor_inr (encode s q))))

definition ref_impl {b c : bool} {P Q : Type} (r : Reflection b P)
  (s : Reflection c Q) : Reflection (bor (bnot b) c) (P -> Q) :=
begin
  induction b,
  { exact Reflection.mk (fun  h p, empty.elim (ff_ne_tt (encode r p))) (fun  f, idp) },
  { exact Reflection.mk (fun  h p, decode s ((ff_bor c)-1  @  h))
      (fun  f, ff_bor c  @  encode s (f (decode r idp))) }
end

definition reflect {A : Type} (v : A -> bool) (f : Formula A) :
  Reflection (test v f) (Holds v f) :=
  Formula.rec_on f
    (Reflection.mk (fun  h, star) (fun  h, idp))
    (Reflection.mk ff_ne_tt (fun  e, empty.elim e))
    (fun  a, Reflection.mk (fun  h, h) (fun  h, h))
    (fun  p q r s, ref_both r s)
    (fun  p q r s, ref_either r s)
    (fun  p q r s, ref_impl r s)

definition rename {A B : Type} (f : A -> B) (p : Formula A) : Formula B :=
  Formula.rec_on p (@top B) (@bot B) (fun  a, atom (f a))
    (fun  p q r s, both r s)
    (fun  p q r s, either r s)
    (fun  p q r s, impl r s)

definition check_rename {A B : Type} (f : A -> B) (v : B -> bool)
  (p : Formula A) : test v (rename f p) = test (fun  a, v (f a)) p :=
begin
  induction p with a p q hp hq p q hp hq p q hp hq,
  { reflexivity },
  { reflexivity },
  { reflexivity },
  { exact ap011 band hp hq },
  { exact ap011 bor hp hq },
  { exact ap011 (fun  x y, bor (bnot x) y) hp hq }
end

definition positive_case : Holds (fun  a : bool, a) (impl (both (atom tt) (@top bool)) (atom tt)) :=
  decode (reflect (fun  a : bool, a) (impl (both (atom tt) (@top bool)) (atom tt))) idp

definition negative_case : Holds (fun  a : bool, a) (both (atom tt) (atom ff)) -> empty :=
  fun  p, ff_ne_tt (encode (reflect (fun  a : bool, a) (both (atom tt) (atom ff))) p)

end cegar_hott
