Conditionally assigning variables

Stream: new members

[Marc Masdeu]

Hi,

I have written this MWE to illustrate my question.

lemma test {p q : ℕ}  (h : p = 3 ∨ q = 5) : ∃ (n : ℕ), n = 3 ∨ n = 5 :=
begin
    cases h with h1 h2,
    {
        let n := p,
        left,
        use n,
        exact h1
    },
    {
        let n := q,
        right,
        use n,
        exact h2
    }
end

I would like to write a proof that was closer to:

lemma test {p q : ℕ}  (h : p = 3 ∨ q = 5) : ∃ (n : ℕ), n = 3 ∨ n = 5 :=
begin
    cases h with hi hi,
    {
        let n := p,
        left,
    },
    {
        let n := q,
        right,
    }
   use n,
  exact hi
end

How would I do that?

[Johan Commelin]

And what exactly is the question :smile: ?

[Kenny Lau]

import tactic

lemma test {p q : ℕ} : p = 3 ∨ q = 5 → ∃ (n : ℕ), n = 3 ∨ n = 5 :=
begin
  intro h,
  cases h with h1 h2,
  { use p,
    left,
    exact h1 },
  { use q,
    right,
    exact h2 }
end

[Adam Topaz]

or.elim?

[Marc Masdeu]

@Kenny Lau this works for this example, but I want something general. I want to apply a bunch of tactics to the two goals that I obtain from the cases, after I set some variables for example.

[Marc Masdeu]

Here is the proof that I really have (you can ignore what key_lemma is for the purpose of this question).

lemma pr_dvd_xm1_or_xp1 (x : ℤ) (h : (x : zmod (p^r))^2 = 1) (h_odd : 2 < p) :
    (p^r : ℤ) ∣ (x - 1) ∨ (p^r : ℤ) ∣ (x + 1) :=
begin
    tactic.unfreeze_local_instances,
    cases key_lemma x h with hp hm,
    {
        let ε := (1 : ℤ),
        left,
        apply part1 ε h h_odd,
        dec_trivial,
        exact_mod_cast hp,
    },
    {
        let ε := (-1 : ℤ),
        right,
        apply part1 ε h h_odd,
        dec_trivial,
        exact_mod_cast hm,
    }
end

[Johan Commelin]

@Marc Masdeu You mean that you want to apply the same tactics to both goals, after doing some groundwork?

[Marc Masdeu]

@Johan Commelin exactly, in the proof I set epsilon to either 1 or -1, then the rest is the same.

[Johan Commelin]

cases foobar with h h; [use 1; left, use -1; right]; { tactics, for, both, goals }

[Johan Commelin]

Note that you have a hp in the first goal, and hm in the second.

[Marc Masdeu]

Adam Topaz said:

or.elim?

Maybe it's doable with this? I'll have to look closer...

[Johan Commelin]

You will have to give hp and hm the same name, so that you can call exact_mod_cast same_name in both branches.

[Marc Masdeu]

Johan Commelin said:

You will have to give hp and hm the same name, so that you can call exact_mod_cast same_name in both branches.

Yes, I was assuming I'd have to do that. Great!! I was looking for the syntax with the square brackets and so on...

[Adam Topaz]

Marc Masdeu said:

Adam Topaz said:

or.elim?

Maybe it's doable with this? I'll have to look closer...

lemma test {p q : ℕ} : p = 3 ∨ q = 5 → ∃ (n : ℕ), n = 3 ∨ n = 5 :=
  λ h, h.elim (λ h, ⟨p, or.inl h⟩) (λ h, ⟨q, or.inr h⟩)

[Adam Topaz]

but this is essentially what's going on in your original proof :)

[Johan Commelin]

Alternative:

cases foobar with hp hm,
use 1, left
swap,
use -1, right,
all_goals {
apply part1 e h h_odd,
dec_trivial,
assumption_mod_cast
}

[Yakov Pechersky]

Is there a lemma that distributes the \Ex over the \or?

[Marc Masdeu]

The first solutions is giving me trouble... I want to set \epsilon to either 1 or -1, so I don't want to use "use".

[Marc Masdeu]

This doesn't work:

    cases (key_lemma x h) with hkl hkl; [let ε := (1 : ℤ); left, let ε := (-1 : ℤ); right],
    {
        apply part1 ε h h_odd,
        dec_trivial,
        exact_mod_cast hkl,
    },

It says "focus' tactic failed, insufficient number of tactics"

[Floris van Doorn]

Yakov Pechersky said:

Is there a lemma that distributes the \Ex over the \or?

docs#exists_or_distrib

[Yakov Pechersky]

@Marc Masdeu what happens if you use a ; instead of , after the [ ... ] block?

[Floris van Doorn]

Use exists_or_distrib you can do something like:

import logic.basic

lemma test {p q : ℕ}  (h : p = 3 ∨ q = 5) : ∃ (n : ℕ), n = 3 ∨ n = 5 :=
by { rw [exists_or_distrib], refine h.imp _ _; exact λ h2, ⟨_, h2⟩ }

[Marc Masdeu]

Johan Commelin said:

Alternative:

cases foobar with hp hm,
use 1, left
swap,
use -1, right,
all_goals {
apply part1 e h h_odd,
dec_trivial,
assumption_mod_cast
}

This one is the kind of solution that I was looking for! (I couldn't make to work the other one you gave me).

Thanks all!

[Johan Commelin]

@Marc Masdeu you might also like the work_on_goal tactic.

[Marc Masdeu]

Yes @Johan Commelin, that was liked indeed. Here is the proof in a more readable format:

lemma pr_dvd_xm1_or_xp1 (x : ℤ) (h : (x : zmod (p^r))^2 = 1) (h_odd : 2 < p) :
    (p^r : ℤ) ∣ (x - 1) ∨ (p^r : ℤ) ∣ (x + 1) :=
begin
    tactic.unfreeze_local_instances,
    cases (key_lemma x h) with hkl hkl,
    work_on_goal 0
    {
        let ε := (1 : ℤ),
        left
    },
    work_on_goal 1
    {
        let ε := (-1 : ℤ),
        right
    },
    all_goals {
        apply part1 ε h h_odd,
        dec_trivial,
        exact_mod_cast hkl,
    },
end

[Marc Masdeu]

Yakov Pechersky said:

Marc Masdeu what happens if you use a ; instead of , after the [ ... ] block?

It still didn't work :-(. I like the answer provided by @Johan Commelin, since it's the most readable (to me, at least).

[Yakov Pechersky]

Do you mind sharing key_lemma and part1? I want to try some refine tactics.

[Marc Masdeu]

The proofs are super long, and I am sure that they can be simplified a whole lot...sorry for that!

import group_theory.subgroup
import group_theory.coset
import data.fintype.card
import data.set.finite
import data.zmod.basic
import algebra.gcd_monoid
import basic
import tactic

open_locale classical big_operators
noncomputable theory

variables {p r n m: ℕ} [fact p.prime] [fact (0 < n)] [fact (0 < m)] [fact (1 ≤ r)]

instance : fact (0 < p^r) := by exact nat.pos_pow_of_pos r (nat.prime.pos _inst_1)

lemma key_lemma (x : ℤ) (h : (x : zmod (p^r))^2 = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
    tactic.unfreeze_local_instances,
    have hp : nat.prime p, by assumption,
    have h1 : (p : ℤ)^r ∣ x^2 - 1,
    {
        rw ←sub_eq_zero at h,
        have h' : (((x^2 - 1) : ℤ) : zmod(p^r)) = 0, by finish,
        apply_mod_cast (zmod.int_coe_zmod_eq_zero_iff_dvd _ _).mp h',
    },
    have h2 : (p : ℤ) ∣ x^2 -1,
    {
        cases h1 with w h1w,
        rw h1w,
        ring,
        fconstructor,
        use (p^(r-1)) * w,
        rw ← int.mul_assoc,
        have hp : (p : ℤ)^r = p * p^(r-1),
        {
            cases r,
            norm_num,
            exfalso,
            exact nat.lt_asymm _inst_4 _inst_4,
            induction r with d cases _inst_4, refl,
            {
                ring,
                ring,
            }
        },
        rw ←hp,
        exact mul_comm w (↑p ^ r),
    },
    have h3 : (p : ℤ) ∣ x - 1 ∨ (p : ℤ) ∣ x + 1,
    {
        have hfac : x^2 -1 = (x - 1) * (x + 1), by ring,
        rw hfac at h2,
        apply int.prime.dvd_mul' hp h2,
    },
    cases h3 with h3l h3r,
    {
        left,
        suffices : (x : zmod p) - 1 = 0, by exact sub_eq_zero.mp this,
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (x-1) p at h3l,
        push_cast at *,
        exact h3l,
    },
    {
        right,
        suffices : (x : zmod p) + 1 = 0, by exact eq_neg_of_add_eq_zero this,
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (x + 1) p at h3r,
        push_cast at *,
        exact h3r,
    }
end


lemma part1 {x : ℤ} (ε : ℤ) (h : (x : zmod (p^r))^2 = 1) (h_odd : 2 < p) (h_eps : ε = 1 ∨ ε = -1) :
    (x : zmod p) = ε → (p^r : ℤ) ∣ (x-ε) :=
begin
    tactic.unfreeze_local_instances,
    have p_ne_zero : (p : ℤ) ≠ 0,
        by exact_mod_cast nat.prime.ne_zero _inst_1,
    have h_prdiv : (p^r : ℤ) ∣ (x^2 - 1),
    {
        rw ←eq_iff_n_divides',
        exact_mod_cast h,
    },
    have h_fact : (p^r : ℤ) = p * p^(r-1),
        by exact_mod_cast (@pr_eq_p_mul_pr1 p r _inst_1 _inst_4),
    cases h_prdiv with f hf,
    intro hp,
    replace hp : ((x - ε :ℤ) : zmod p) = 0, by exact_mod_cast sub_eq_zero.mpr hp,
    rw zero_iff_n_divides' at hp,
    cases hp with e he,
    suffices : (p^(r-1) : ℤ) ∣ e,
    {
        cases this with f hf,
        use f,
        rw [he, hf, ←mul_assoc, ←h_fact],
    },
    have hcalc :=
        calc
        (p : ℤ) * (p ^ (r-1) * f) = p^r * f : by rw [←mul_assoc, h_fact]
        ...    = x^2 - 1 : by rw hf
        ...    = x^2 - ε^2 : by {cases h_eps; finish}
        ...    = (x-ε)^2 + 2*ε*(x-ε) : by ring
        ...    =  (p * e)^2 + 2 * ε * (p*e) : by rw he at *
        ...    = p * (2 * ε * e + p * e^2)  : by ring,
    rw mul_right_inj' p_ne_zero at hcalc,
    replace hcalc : (p^(r-1) : ℤ) ∣ 2 * ε * e + p * e^2 := dvd.intro f hcalc,
    rw [mul_comm, mul_comm (p : ℤ), pow_two, mul_assoc, ←mul_add e] at hcalc,
    have p_not_dvd_2pe : ¬ (p : ℤ) ∣ (2 * ε + e * p),
    {
        rintro ⟨ s, hs ⟩,
        have p_dvd_2 : p ∣ 2,
        {
            suffices : (p : ℤ) ∣ 2, from int.coe_nat_dvd_left.mp this,
            use ε * (s-e),
            rw mul_sub,
            cases h_eps;
            {
                rw h_eps at *,
                ring,
                simp only [mul_one, int.mul_neg_eq_neg_mul_symm] at hs,
                simp only [mul_sub, neg_sub_neg],
                rw ←hs,
                ring,
            },
        },
        rw nat.prime_dvd_prime_iff_eq  _inst_1 nat.prime_two at p_dvd_2,
        rw p_dvd_2 at h_odd,
        exact nat.lt_asymm h_odd h_odd,
    },
    have h_coprime : (p^(r-1)).coprime (2 * ε + e * p).nat_abs,
    {
        suffices : p.coprime (2 * ε + e *p).nat_abs, from nat.coprime.pow_left (r - 1) this,
        refine (nat.prime.coprime_iff_not_dvd _inst_1).mpr _,
        intro hc,
        apply p_not_dvd_2pe,
        rw ←int.coe_nat_dvd_left at hc,
        simp only [mul_comm] at *,
        exact hc,
    },
    have pow_div_abs : p^(r-1) ∣ e.nat_abs,
    {
        apply nat.coprime.dvd_of_dvd_mul_right h_coprime,
        rw ←int.nat_abs_mul,
        cases hcalc with s hs,
        use s.nat_abs,
        rw [hs, int.nat_abs_mul],
        norm_cast,
    },
    cases pow_div_abs with t ht,
    use (t * e.sign),
    replace ht : e.sign * abs e = p^(r-1) * (t * e.sign),
    {
        rw [int.abs_eq_nat_abs, ht],
        finish,
    },
    rw int.sign_mul_abs e at ht,
    exact ht,
end

[Alex J. Best]

I know you didn't ask but I read through your proofs that could be simplified and made some tweaks to maybe make it simpler, but still with the same proof strategy. Hope something here is useful to you!

lemma key_lemma (x : ℤ) (h : (x : zmod (p^r))^2 = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
    haveI hp : nat.prime p := by assumption,
    -- using haveI casesI tactics instead of unfreezing local instances
    -- personally i like this more when it works, as tactic.unfreeze_local_instances isnt a mathematical proof step
    have h1 : (p : ℤ)^r ∣ x^2 - 1,
    {
        rw ←sub_eq_zero at h,
        have h' : (((x^2 - 1) : ℤ) : zmod(p^r)) = 0, by finish,
        apply_mod_cast (zmod.int_coe_zmod_eq_zero_iff_dvd _ _).mp h',
    },
    have h2 : (p : ℤ) ∣ x^2 -1,
    {
        cases h1 with w h1w,
        rw h1w,
        -- ring wasn't doing anything now
        -- fconstructor isnt needed lean works out what you want to use
        use (p^(r-1)) * w,
        rw ← int.mul_assoc,
        congr, -- just a simpler way of ending up in the same place you did, two things times w are equal because the two things were
        casesI r,
        norm_num,
        exfalso,
        exact nat.lt_asymm _inst_4 _inst_4,
        simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero], -- simp and then library search
        exact pow_succ ↑p r,
    },
    have h3 : (p : ℤ) ∣ x - 1 ∨ (p : ℤ) ∣ x + 1,
    {
        have hfac : x^2 -1 = (x - 1) * (x + 1), by ring,
        rw hfac at h2,
        apply int.prime.dvd_mul' hp h2,
    },
    cases h3 with h3l h3r,
    {
        left,
        rw ← sub_eq_zero,
        -- i removed suffices when the proof was simpler without, if its a long proof suffices is good
        -- but if its a one-liner in my opinion its clear enough just to rewrite
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (x-1) p at h3l,
        assumption_mod_cast, -- combine a couple of steps
    },
    {
        right,
        apply eq_neg_of_add_eq_zero,
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (x + 1) p at h3r,
        assumption_mod_cast, -- combine a couple of steps
    }
end

[Yakov Pechersky]

And here are the steps after h3 that are simplified, in a way that uses the common structure:

lemma key_lemma (x : ℤ) (h : (x : zmod (p^r))^2 = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
    haveI hp : nat.prime p := by assumption,
    -- using haveI casesI tactics instead of unfreezing local instances
    -- personally i like this more when it works, as tactic.unfreeze_local_instances isnt a mathematical proof step
    have h1 : (p : ℤ)^r ∣ x^2 - 1,
    {
        rw ←sub_eq_zero at h,
        have h' : (((x^2 - 1) : ℤ) : zmod(p^r)) = 0, by finish,
        apply_mod_cast (zmod.int_coe_zmod_eq_zero_iff_dvd _ _).mp h',
    },
    have h2 : (p : ℤ) ∣ x^2 -1,
    {
        cases h1 with w h1w,
        rw h1w,
        -- ring wasn't doing anything now
        -- fconstructor isnt needed lean works out what you want to use
        use (p^(r-1)) * w,
        rw ← int.mul_assoc,
        congr, -- just a simpler way of ending up in the same place you did, two things times w are equal because the two things were
        casesI r,
        norm_num,
        exfalso,
        exact nat.lt_asymm _inst_4 _inst_4,
        simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero], -- simp and then library search
        exact pow_succ ↑p r,
    },
    have h3 : (p : ℤ) ∣ x - 1 ∨ (p : ℤ) ∣ x + 1,
    {
        have hfac : x^2 -1 = (x - 1) * (x + 1), by ring,
        rw hfac at h2,
        apply int.prime.dvd_mul' hp h2,
    },
    simp only [←zmod.int_coe_zmod_eq_zero_iff_dvd, int.cast_add, int.cast_one, int.cast_sub] at h3,
    exact h3.imp sub_eq_zero.mp eq_neg_of_add_eq_zero
end

[Yakov Pechersky]

Which uses the fact that p and the summands are inferrable.

[Marc Masdeu]

Thanks @Yakov Pechersky and @Alex J. Best ! I had arrived at this version after reading Alex's improvements:

lemma key_lemma (x : ℤ) (h : (x : zmod (p^r))^2 = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
    haveI hp : nat.prime p := by assumption,
    rw ←sub_eq_zero at h,
    rw_mod_cast zmod.int_coe_zmod_eq_zero_iff_dvd at h,
    have h_p_dvd : (p : ℤ) ∣ (x - 1) * (x + 1),
    {
        cases h with w hw,
        ring,
        rw hw,
        casesI r,
        {
            exfalso,
            exact nat.lt_asymm _inst_4 _inst_4,
        },
        {
            refine dvd_mul_of_dvd_left _ w,
            use p^r,
            exact int.coe_nat_pow p (r + 1),
        }
    },
    cases (int.prime.dvd_mul' hp h_p_dvd) with h' h',
    left,
    let x' := x - 1,
    swap,
    right,
    let x' := x + 1,
    all_goals
    {
        rw ←sub_eq_zero,
        try {ring},
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd x' p at h',
        assumption_mod_cast
    },
end

[Marc Masdeu]

@Yakov Pechersky I don't see how I would get the last two lines of your proof. Plain simp did not succeed, and for the last line library_search didn't work either!

[Yakov Pechersky]

I took Alex's proof and saw the common zmod.int_coe_zmod_eq_zero_iff_dvd. So I wanted to rw it in the h3, but didn't feel like doing rw twice or repeat { rw ... }. So I did simp [<-zmod.int_coe_zmod_eq_zero_iff_dvd _ p] at h3 prior to the cases h3.

[Yakov Pechersky]

Then I changed it to a squeeze_simp which gave the more detailed and faster simp only.

[Yakov Pechersky]

Then instead of cases C, { left, ..., exact F }, { right, ..., exact G }, one can try something like refine or.imp _ _ C, or using projection notation, refine C.imp _ _.

[Yakov Pechersky]

Then you have two subgoals that you know how to solve. rw <-iff_lemma is using the iff_lemma.mpr implication.

[Yakov Pechersky]

So, a little bit of golfing.

[Yakov Pechersky]

I'm not a fan of explicitly invoking _inst_4. Trying to find a way to hide that atm.

[Yakov Pechersky]

I'm not familiar with the zmod side of the lib, is storing positivity or nonnegativity in fact instances the common way to do it there? As opposed to

variables (rpos : 0 < r)
include rpos

[Marc Masdeu]

These explanations are really useful!

[Yakov Pechersky]

More golf:

lemma key_lemma (x : ℤ) (h : (x : zmod (p^r))^2 = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
  haveI hp : nat.prime p := by assumption,
  rw ←sub_eq_zero at h,
  rw_mod_cast zmod.int_coe_zmod_eq_zero_iff_dvd at h,
  have h_p_dvd : (p : ℤ) ∣ (x - 1) * (x + 1),
  { obtain ⟨w, hw⟩ := h,
    ring,
    rw hw,
    refine dvd_mul_of_dvd_left _ w,
    casesI r,
    { have : 1 ≤ 0 := by assumption,
      exact absurd nat.one_pos (not_lt_of_le this) },
    { use p^r,
      exact int.coe_nat_pow p (r + 1) } },
  refine or.imp _ _ (int.prime.dvd_mul' hp h_p_dvd);
  { intro h',
    simpa [←zmod.int_coe_zmod_eq_zero_iff_dvd, ←sub_eq_zero] using h' },
end

[Yakov Pechersky]

Remove the explicit _inst_4 by using by assumption. That tactic will still work if you switch away from fact ... instance to a provided hypothesis (along with casesI r to cases r. Skipped doing an exfalso step into an exact absurd ... step.

[Yakov Pechersky]

Changed a cases h with w hwto an obtain to be more explicit about picking a value and a corresponding proof of what it satisfies, as opposed to cases, which works, but I usually use for disjunctions.

[Yakov Pechersky]

And since you finish the proof with an all_goals, convert the final block to something that is valid for both. You had some left, right, swap to provide two distinct values for x. I just let them work implicitly. Whatever the value, we have one of the two implications from the dvd_mul' disjunction, so in either case, moving the summand and using zero_iff_dvd is enough for the hypothesis in the implication.

[Yakov Pechersky]

simpa [...] using H is good for when you have tactic steps like simp [...] at H, simp only [...], exact H or similar.

[Yakov Pechersky]

I've also made the eps argument to part1 implicit, which allows the following for the original lemma you posted about:

[Yakov Pechersky]

lemma pr_dvd_xm1_or_xp1 (x : ℤ) (h : (x : zmod (p^r))^2 = 1) (h_odd : 2 < p) :
    (p^r : ℤ) ∣ (x - 1) ∨ (p^r : ℤ) ∣ (x + 1) :=
begin
    have : (x + 1) = x - (-1), by ring,
    refine (key_lemma x h).imp _ _;
    { intro H,
      try { rw this },
      apply part1 h h_odd,
      dec_trivial,
      exact_mod_cast H },
end