Theory Congruence_Backward

theory Congruence_Backward
  imports
    Congruence_Arithmetic
    "Voblint_Nonrelational.Exec_Backward"
    "HOL-Computational_Algebra.Euclidean_Algorithm"
begin

section ‹Multiplication preimages›

text ‹
  For a known factor k, the preimage of c modulo m solves the linear
  congruence k*x = c modulo m. Dividing by gcd(k,m) and using the executable
  Bezout coefficient yields the complete solution class.
›

fun preimage_times_const_rep ::
    "congruence_rep => int => congruence_rep"
where
  "preimage_times_const_rep None k = None"
| "preimage_times_const_rep (Some (c, m)) k =
     normalize_congruence_rep
       (if m = 0 then
          if k = 0 then
            if c = 0 then Some (0, 1) else None
          else if k dvd c then Some (c div k, 0) else None
        else
          let g = gcd k m
          in if g dvd c then
               let s = fst (bezout_coefficients k m)
               in Some ((c div g) * s, m div g)
             else None)"

lemma normalized_preimage_times_const_rep [simp]:
  "normalized_congruence_rep (preimage_times_const_rep r k)"
  by (cases r)
     (auto simp: split_def split: if_splits prod.splits)

lift_definition preimage_times_const ::
    "congruence => int => congruence"
  is preimage_times_const_rep
  by simp

lemma bezout_linear_congruence:
  assumes g_nonzero: "gcd k m ~= 0"
      and compatible: "gcd k m dvd c"
  shows
    "m div gcd k m dvd
       x - (c div gcd k m) * fst (bezout_coefficients k m)
     ⟷
     m dvd k * x - c"
proof -
  let ?g = "gcd k m"
  let ?s = "fst (bezout_coefficients k m)"
  let ?t = "snd (bezout_coefficients k m)"
  let ?q = "c div ?g"
  let ?kp = "k div ?g"
  let ?mp = "m div ?g"
  have gk: "?g dvd k"
    by (rule gcd_dvd1)
  have gm: "?g dvd m"
    by (rule gcd_dvd2)
  have k_eq: "?g * ?kp = k"
    using dvd_mult_div_cancel[OF gk]
    by (simp add: mult.commute)
  have m_eq: "?g * ?mp = m"
    using dvd_mult_div_cancel[OF gm]
    by (simp add: mult.commute)
  have c_eq: "?g * ?q = c"
    using dvd_mult_div_cancel[OF compatible]
    by (simp add: mult.commute)
  have bezout:
    "?s * k + ?t * m = ?g"
    by (rule bezout_coefficients_fst_snd)
  have scaled:
    "?g * (?s * ?kp + ?t * ?mp) = ?g"
  proof -
    have
      "?g * (?s * ?kp + ?t * ?mp) =
       ?s * (?g * ?kp) + ?t * (?g * ?mp)"
      by (simp only: ring_distribs mult.assoc mult.commute
          mult.left_commute)
    also have "... = ?s * k + ?t * m"
      by (simp only: k_eq m_eq)
    also have "... = ?g"
      by (rule bezout)
    finally show ?thesis .
  qed
  have scaled':
    "?g * (?s * ?kp + ?t * ?mp) = ?g * 1"
    using scaled by simp
  have unit: "?s * ?kp + ?t * ?mp = 1"
    using scaled'
    by (simp only: mult_left_cancel[OF g_nonzero])
  show ?thesis
  proof
    assume solution: "?mp dvd x - ?q * ?s"
    obtain u where solution_eq:
      "x - ?q * ?s = ?mp * u"
      using solution unfolding dvd_def by blast
    have q_unit:
      "?q * (?s * ?kp + ?t * ?mp) = ?q"
      using unit by simp
    have reduced:
      "?kp * x - ?q = ?mp * (?kp * u + ?q * (- ?t))"
      using solution_eq q_unit
      by (simp add: algebra_simps)
    show "m dvd k * x - c"
      unfolding dvd_def
    proof (rule exI[of _ "?kp * u + ?q * (- ?t)"])
      have scaled_reduced:
        "?g * (?kp * x - ?q) =
         ?g * (?mp * (?kp * u + ?q * (- ?t)))"
        by (rule arg_cong[OF reduced])
      show
        "k * x - c =
         m * (?kp * u + ?q * (- ?t))"
      proof -
        have "k * x - c = ?g * (?kp * x - ?q)"
          using k_eq c_eq by (simp add: algebra_simps)
        also have "... =
          ?g * (?mp * (?kp * u + ?q * (- ?t)))"
          by (rule scaled_reduced)
        also have "... =
          (?g * ?mp) * (?kp * u + ?q * (- ?t))"
          by (simp only: mult.assoc)
        also have "... = m * (?kp * u + ?q * (- ?t))"
          by (simp only: m_eq)
        finally show ?thesis .
      qed
    qed
  next
    assume target: "m dvd k * x - c"
    obtain u where target_eq:
      "k * x - c = m * u"
      using target unfolding dvd_def by blast
    have scaled_reduced:
      "?g * (?kp * x - ?q) = ?g * (?mp * u)"
      using target_eq k_eq m_eq c_eq
      by (simp add: algebra_simps)
    have reduced: "?kp * x - ?q = ?mp * u"
      using scaled_reduced
      by (simp only: mult_left_cancel[OF g_nonzero])
    show "?mp dvd x - ?q * ?s"
      unfolding dvd_def
    proof (rule exI[of _ "?s * u + ?t * x"])
      have scaled_solution:
        "?s * (?kp * x - ?q) = ?s * (?mp * u)"
        using reduced by simp
      have unit_x:
        "x * (?s * ?kp + ?t * ?mp) = x"
        using unit by simp
      show
        "x - ?q * ?s = ?mp * (?s * u + ?t * x)"
        using scaled_solution unit_x
        by (simp add: algebra_simps)
    qed
  qed
qed

lemma gamma_preimage_times_const_rep:
  assumes "normalized_congruence_rep r"
  shows
    "gamma_congruence_rep (preimage_times_const_rep r k) =
     {x. k * x : gamma_congruence_rep r}"
proof (cases r)
  case None
  then show ?thesis by simp
next
  case (Some cm)
  note r_some = Some
  obtain c m where cm: "cm = (c, m)"
    by (cases cm)
  show ?thesis
  proof (cases "m = 0")
    case m_zero: True
    show ?thesis
    proof (cases "k = 0")
      case k_zero: True
      show ?thesis
      proof (cases "c = 0")
        case True
        with r_some cm m_zero k_zero show ?thesis by simp
      next
        case False
        with r_some cm m_zero k_zero show ?thesis by simp
      qed
    next
      case k_nonzero: False
      show ?thesis
      proof (cases "k dvd c")
        case compatible: True
        have quotient: "k * (c div k) = c"
          by (rule dvd_mult_div_cancel[OF compatible])
        have solution_iff:
          "k * x = c ⟷ x = c div k" for x
        proof -
          have
            "(k * x = c) =
             (k * x = k * (c div k))"
            using quotient by simp
          also have "... = (x = c div k)"
            by (rule mult_left_cancel[OF k_nonzero])
          finally show ?thesis .
        qed
        with r_some cm m_zero k_nonzero compatible
        show ?thesis
          by simp
      next
        case incompatible: False
        have no_solution: "k * x ~= c" for x
        proof
          assume "k * x = c"
          then have "k dvd c"
            unfolding dvd_def by blast
          with incompatible show False by contradiction
        qed
        with r_some cm m_zero k_nonzero incompatible
        show ?thesis
          by simp
      qed
    qed
  next
    case m_nonzero: False
    let ?g = "gcd k m"
    let ?q = "c div ?g"
    let ?s = "fst (bezout_coefficients k m)"
    have g_nonzero: "?g ~= 0"
      using m_nonzero by simp
    show ?thesis
    proof (cases "?g dvd c")
      case incompatible: False
      have no_solution: "~ m dvd k * x - c" for x
      proof
        assume target: "m dvd k * x - c"
        have g_product: "?g dvd k * x"
          by (rule dvd_mult2[OF gcd_dvd1])
        have g_target: "?g dvd k * x - c"
          using gcd_dvd2 target by (rule dvd_trans)
        have "?g dvd k * x - (k * x - c)"
          by (rule dvd_diff[OF g_product g_target])
        then have "?g dvd c"
          by simp
        with incompatible show False by contradiction
      qed
      with r_some cm m_nonzero incompatible
      show ?thesis by simp
    next
      case compatible: True
      have solution_iff:
        "m div ?g dvd x - ?q * ?s ⟷
         m dvd k * x - c" for x
        by (rule bezout_linear_congruence[OF g_nonzero compatible])
      have normalized_gamma:
        "gamma_congruence_rep
           (normalize_congruence_rep
             (Some (?q * ?s, m div ?g))) =
         {x. m div ?g dvd x - ?q * ?s}"
        by (simp only: gamma_normalize_congruence_rep
            gamma_congruence_rep.simps)
      from r_some cm m_nonzero compatible normalized_gamma
        solution_iff
      show ?thesis
        by (simp only: preimage_times_const_rep.simps if_False
            if_True Let_def gamma_congruence_rep.simps
            Set.set_eq_iff mem_Collect_eq;
            simp)
    qed
  qed
qed

lemma gamma_preimage_times_const [simp]:
  "gamma_congruence (preimage_times_const r k) =
   {x. k * x : gamma_congruence r}"
proof -
  have norm_r:
    "normalized_congruence_rep (Rep_congruence r)"
    by simp
  show ?thesis
    using gamma_preimage_times_const_rep[OF norm_r, of k]
    by (simp add: gamma_congruence_def preimage_times_const.rep_eq)
qed

lemma preimage_times_const_mono:
  assumes "r1 <= r2"
  shows "preimage_times_const r1 k <= preimage_times_const r2 k"
  using assms
  unfolding less_eq_congruence_iff_gamma
  by auto

fun inverse_times_candidate_rep ::
    "congruence_rep => congruence_rep => congruence_rep"
where
  "inverse_times_candidate_rep None factor = None"
| "inverse_times_candidate_rep r None = None"
| "inverse_times_candidate_rep
     (Some (c, m)) (Some (k, n)) =
     (if n = 0
      then preimage_times_const_rep (Some (c, m)) k
      else Some (0, 1))"

lemma normalized_inverse_times_candidate_rep [simp]:
  assumes "normalized_congruence_rep r"
      and "normalized_congruence_rep factor"
  shows
    "normalized_congruence_rep
       (inverse_times_candidate_rep r factor)"
  using assms
  by (cases r; cases factor)
     (auto split: prod.splits if_splits)

lift_definition inverse_times_candidate ::
    "congruence => congruence => congruence"
  is inverse_times_candidate_rep
  by simp

lemma inverse_times_candidate_sound:
  assumes "z : gamma_congruence r"
      and "y : gamma_congruence factor"
      and "x * y = z"
  shows "x : gamma_congruence (inverse_times_candidate r factor)"
proof (cases "Rep_congruence r")
  case None
  with assms(1) show ?thesis
    unfolding gamma_congruence_def by simp
next
  case (Some rp)
  note r_some = Some
  obtain c m where rp: "rp = (c, m)"
    by (cases rp)
  show ?thesis
  proof (cases "Rep_congruence factor")
    case None
    with assms(2) show ?thesis
      unfolding gamma_congruence_def by simp
  next
    case (Some fp)
    note factor_some = Some
    obtain k n where fp: "fp = (k, n)"
      by (cases fp)
    show ?thesis
    proof (cases "n = 0")
      case singleton: True
      have y_eq: "y = k"
        using assms(2) factor_some fp singleton
        unfolding gamma_congruence_def by simp
      have x_preimage:
        "x : gamma_congruence (preimage_times_const r k)"
        using assms(1,3) y_eq
        by (simp add: mult.commute)
      from x_preimage r_some factor_some rp fp singleton
      show ?thesis
        unfolding gamma_congruence_def
        by (simp add: inverse_times_candidate.rep_eq
            preimage_times_const.rep_eq)
    next
      case nonsingleton: False
      with r_some factor_some rp fp show ?thesis
        unfolding gamma_congruence_def
        by (simp add: inverse_times_candidate.rep_eq)
    qed
  qed
qed

lemma inverse_times_candidate_mono:
  assumes "r1 <= r2" and "factor1 <= factor2"
  shows
    "inverse_times_candidate r1 factor1 <=
     inverse_times_candidate r2 factor2"
proof -
  have r_subset:
    "gamma_congruence r1 ⊆ gamma_congruence r2"
    using assms(1)
    unfolding less_eq_congruence_iff_gamma .
  have factor_subset:
    "gamma_congruence factor1 ⊆ gamma_congruence factor2"
    using assms(2)
    unfolding less_eq_congruence_iff_gamma .
  show ?thesis
  proof (cases "Rep_congruence r1")
    case None
    then show ?thesis
      unfolding less_eq_congruence_iff_gamma
        gamma_congruence_def
      by (simp add: inverse_times_candidate.rep_eq)
  next
    case (Some rp1)
    note r1_some = Some
    obtain c1 m1 where rp1: "rp1 = (c1, m1)"
      by (cases rp1)
    have c1_member: "c1 : gamma_congruence r1"
      using r1_some rp1
      by (simp add: gamma_congruence_def)
    show ?thesis
    proof (cases "Rep_congruence factor1")
      case None
      with r1_some rp1 show ?thesis
        unfolding less_eq_congruence_iff_gamma
          gamma_congruence_def
        by (simp add: inverse_times_candidate.rep_eq)
    next
      case (Some fp1)
      note factor1_some = Some
      obtain k1 n1 where fp1: "fp1 = (k1, n1)"
        by (cases fp1)
      have k1_member: "k1 : gamma_congruence factor1"
        using factor1_some fp1
        by (simp add: gamma_congruence_def)
      have shifted_member:
        "k1 + n1 : gamma_congruence factor1"
        using factor1_some fp1
        by (simp add: gamma_congruence_def)
      show ?thesis
      proof (cases "Rep_congruence r2")
        case None
        have "c1 : gamma_congruence r2"
          by (rule subsetD[OF r_subset c1_member])
        with None show ?thesis
          unfolding gamma_congruence_def by simp
      next
        case (Some rp2)
        note r2_some = Some
        obtain c2 m2 where rp2: "rp2 = (c2, m2)"
          by (cases rp2)
        show ?thesis
        proof (cases "Rep_congruence factor2")
          case None
          have "k1 : gamma_congruence factor2"
            by (rule subsetD[OF factor_subset k1_member])
          with None show ?thesis
            unfolding gamma_congruence_def by simp
        next
          case (Some fp2)
          note factor2_some = Some
          obtain k2 n2 where fp2: "fp2 = (k2, n2)"
            by (cases fp2)
          show ?thesis
          proof (cases "n2 = 0")
            case factor2_singleton: True
            have k1_in_factor2:
              "k1 : gamma_congruence factor2"
              by (rule subsetD[OF factor_subset k1_member])
            have shifted_in_factor2:
              "k1 + n1 : gamma_congruence factor2"
              by (rule subsetD[OF factor_subset shifted_member])
            have k1_eq: "k1 = k2"
              using k1_in_factor2 factor2_some fp2
                factor2_singleton
              unfolding gamma_congruence_def by simp
            have shifted_eq: "k1 + n1 = k2"
              using shifted_in_factor2 factor2_some fp2
                factor2_singleton
              unfolding gamma_congruence_def by simp
            have n1_zero: "n1 = 0"
              using k1_eq shifted_eq by simp
            have preimage_le:
              "preimage_times_const r1 k1 <=
               preimage_times_const r2 k2"
              using preimage_times_const_mono[OF assms(1), of k1]
                k1_eq
              by simp
            from preimage_le r1_some factor1_some rp1 fp1
              r2_some factor2_some rp2 fp2 n1_zero
              factor2_singleton
            show ?thesis
              unfolding less_eq_congruence_iff_gamma
                gamma_congruence_def
              by (simp add: inverse_times_candidate.rep_eq
                  preimage_times_const.rep_eq)
          next
            case factor2_nonsingleton: False
            with r2_some factor2_some rp2 fp2
            show ?thesis
              unfolding less_eq_congruence_iff_gamma
                gamma_congruence_def
              by (simp add: inverse_times_candidate.rep_eq)
          qed
        qed
      qed
    qed
  qed
qed


section ‹Backward inverse operators›

text ‹
  Congruences carry divisibility information but no order, so less-than cannot
  refine either operand. True equality is representable as intersection; false
  equality remains the identity because a congruence generally cannot represent
  a complement. Addition and subtraction use algebraic rearrangement, while
  multiplication uses the preimage construction proved above.
›

definition inv_less_congruence ::
    "bool => congruence => congruence => congruence * congruence"
where
  "inv_less_congruence result a b = (a, b)"

fun inv_eq_congruence ::
    "bool => congruence => congruence => congruence * congruence"
where
  "inv_eq_congruence True a b =
     (a ⊓ b, a ⊓ b)"
| "inv_eq_congruence False a b = (a, b)"

definition inv_plus_congruence ::
    "congruence => congruence => congruence =>
     congruence * congruence"
where
  "inv_plus_congruence r a b =
     (a ⊓ (r - b),
      b ⊓ (r - a))"

definition inv_minus_congruence ::
    "congruence => congruence => congruence =>
     congruence * congruence"
where
  "inv_minus_congruence r a b =
     (a ⊓ (r + b),
      b ⊓ (a - r))"

definition inv_times_congruence ::
    "congruence => congruence => congruence =>
     congruence * congruence"
where
  "inv_times_congruence r a b =
     (a ⊓ inverse_times_candidate r b,
      b ⊓ inverse_times_candidate r a)"

lemma inv_less_congruence_sound:
  assumes "x : gamma_congruence a"
      and "y : gamma_congruence b"
  shows
    "x : gamma_congruence
       (fst (inv_less_congruence result a b)) ∧
     y : gamma_congruence
       (snd (inv_less_congruence result a b))"
  using assms by (simp add: inv_less_congruence_def)

lemma inv_eq_congruence_sound:
  assumes "x : gamma_congruence a"
      and "y : gamma_congruence b"
      and "(x = y) = result"
  shows
    "x : gamma_congruence
       (fst (inv_eq_congruence result a b)) ∧
     y : gamma_congruence
       (snd (inv_eq_congruence result a b))"
  using assms
  by (cases result) auto

lemma inv_plus_congruence_sound:
  assumes "x : gamma_congruence a"
      and "y : gamma_congruence b"
      and "x + y : gamma_congruence r"
  shows
    "x : gamma_congruence
       (fst (inv_plus_congruence r a b)) ∧
     y : gamma_congruence
       (snd (inv_plus_congruence r a b))"
proof -
  have x_candidate: "x : gamma_congruence (r - b)"
    using congruence_minus_sound[OF assms(3) assms(2)]
    by simp
  have y_candidate: "y : gamma_congruence (r - a)"
    using congruence_minus_sound[OF assms(3) assms(1)]
    by simp
  show ?thesis
    using assms(1,2) x_candidate y_candidate
    by (simp add: inv_plus_congruence_def)
qed

lemma inv_minus_congruence_sound:
  assumes "x : gamma_congruence a"
      and "y : gamma_congruence b"
      and "x - y : gamma_congruence r"
  shows
    "x : gamma_congruence
       (fst (inv_minus_congruence r a b)) ∧
     y : gamma_congruence
       (snd (inv_minus_congruence r a b))"
proof -
  have x_candidate: "x : gamma_congruence (r + b)"
    using congruence_plus_sound[OF assms(3) assms(2)]
    by simp
  have y_candidate: "y : gamma_congruence (a - r)"
    using congruence_minus_sound[OF assms(1) assms(3)]
    by simp
  show ?thesis
    using assms(1,2) x_candidate y_candidate
    by (simp add: inv_minus_congruence_def)
qed

lemma inv_times_congruence_sound:
  assumes "x : gamma_congruence a"
      and "y : gamma_congruence b"
      and "x * y : gamma_congruence r"
  shows
    "x : gamma_congruence
       (fst (inv_times_congruence r a b)) ∧
     y : gamma_congruence
       (snd (inv_times_congruence r a b))"
proof -
  have x_candidate:
    "x : gamma_congruence (inverse_times_candidate r b)"
  proof (rule inverse_times_candidate_sound[
      where z = "x * y" and y = y])
    show "x * y : gamma_congruence r"
      by (rule assms(3))
    show "y : gamma_congruence b"
      by (rule assms(2))
    show "x * y = x * y" by simp
  qed
  have y_candidate:
    "y : gamma_congruence (inverse_times_candidate r a)"
  proof (rule inverse_times_candidate_sound[
      where z = "x * y" and y = x])
    show "x * y : gamma_congruence r"
      by (rule assms(3))
    show "x : gamma_congruence a"
      by (rule assms(1))
    show "y * x = x * y"
      by (simp add: mult.commute)
  qed
  show ?thesis
    using assms(1,2) x_candidate y_candidate
    by (simp add: inv_times_congruence_def)
qed

lemma inv_less_congruence_mono:
  assumes "a1 <= a2" and "b1 <= b2"
  shows
    "le_pair
      (inv_less_congruence result a1 b1)
      (inv_less_congruence result a2 b2)"
  using assms by (simp add: inv_less_congruence_def)

lemma inv_eq_congruence_mono:
  assumes "a1 <= a2" and "b1 <= b2"
  shows
    "le_pair
      (inv_eq_congruence result a1 b1)
      (inv_eq_congruence result a2 b2)"
  using assms inf_mono
  by (cases result) auto

lemma inv_plus_congruence_mono:
  assumes "r1 <= r2" and "a1 <= a2" and "b1 <= b2"
  shows
    "le_pair
      (inv_plus_congruence r1 a1 b1)
      (inv_plus_congruence r2 a2 b2)"
  using assms congruence_minus_mono
  by (auto simp: inv_plus_congruence_def intro: le_infI1 le_infI2)

lemma inv_minus_congruence_mono:
  assumes "r1 <= r2" and "a1 <= a2" and "b1 <= b2"
  shows
    "le_pair
      (inv_minus_congruence r1 a1 b1)
      (inv_minus_congruence r2 a2 b2)"
  using assms congruence_plus_mono congruence_minus_mono
  by (auto simp: inv_minus_congruence_def intro: le_infI1 le_infI2)

lemma inv_times_congruence_mono:
  assumes "r1 <= r2" and "a1 <= a2" and "b1 <= b2"
  shows
    "le_pair
      (inv_times_congruence r1 a1 b1)
      (inv_times_congruence r2 a2 b2)"
  using assms inverse_times_candidate_mono
  by (auto simp: inv_times_congruence_def intro: le_infI1 le_infI2)

subsection ‹The refinement operations and their certificate›

text ‹
  Congruence's refinement choices: the lattice meet, and an inverse for every
  comparison and arithmetic operator. The guard filters and the branch are
  derived from this record and the evaluator in ‹Congruence_Transfer›.
›

definition congruence_refine_ops :: "congruence refine_ops" where
  "congruence_refine_ops =
     ⦇r_tobool = congruence_tobool, r_inv_less = inv_less_congruence,
      r_inv_eq = inv_eq_congruence, r_inv_plus = inv_plus_congruence,
      r_inv_minus = inv_minus_congruence, r_inv_times = inv_times_congruence,
      r_intersect = inf⦈"

lemma congruence_refine_ops_simps [simp]:
  "r_tobool congruence_refine_ops = congruence_tobool"
  "r_inv_less congruence_refine_ops = inv_less_congruence"
  "r_inv_eq congruence_refine_ops = inv_eq_congruence"
  "r_inv_plus congruence_refine_ops = inv_plus_congruence"
  "r_inv_minus congruence_refine_ops = inv_minus_congruence"
  "r_inv_times congruence_refine_ops = inv_times_congruence"
  "r_intersect congruence_refine_ops = inf"
  by (simp_all add: congruence_refine_ops_def)

lemma congruence_backward_domain:
  "mono_refinement inf aval_congruence congruence_tobool
     inv_less_congruence inv_eq_congruence
     inv_plus_congruence inv_minus_congruence inv_times_congruence"
proof unfold_locales
qed (simp_all add: inv_less_congruence_sound inv_eq_congruence_sound
       inv_plus_congruence_sound inv_minus_congruence_sound inv_times_congruence_sound
       congruence_tobool_sound inf_mono congruence_arith.aval_dom_mono
       inv_less_congruence_mono inv_eq_congruence_mono inv_plus_congruence_mono
       inv_minus_congruence_mono inv_times_congruence_mono
       le_infI1 le_infI2 congruence_tobool_mono)

end