Logic & Proof

Stream: general

[Kaushik Chakraborty]

Hi, I am going through the online course Logic and Proof. I am stuck in the exercises. Is this the right place to ask such questions?

[Chris Hughes]

Yes

[Kaushik Chakraborty]

Thanks. So I'm stuck progressing with the last prob. of Chapter 4's exercises i.e. prove ¬ (A ↔ ¬ A)

[Kaushik Chakraborty]

I am thinking of following the rules mentioned in the book till now and start with the assumption that (A ↔ ¬ A)is true and then progress to show false so that I can prove the negation. But I can't figure out a way forward

[Kenny Lau]

hint: prove ¬ A from your assumption

[Chris Hughes]

This actually came up in M1F, and I was annoyed with myself for assuming excluded middle.

[Kenny Lau]

not constructive enough, eh :P

[Kaushik Chakraborty]

am failing to get how can I get ¬ A with just assuming A ↔ ¬ A. I can get it if I also assume A and apply left elimination to the iff to get ¬ A. Is my understanding correct ?

[Kenny Lau]

no, you need to assume A and prove false

[Kenny Lau]

ok, which you get via deducing ¬ A

[Chris Hughes]

Try have h : ¬ A

[Kaushik Chakraborty]

I am trying to do something like that but I am getting a type mismatch error coz of the additional assumption.
Could you please look at this LEAN code

[Chris Hughes]

You can only do assume a : A if your goal is A → something

[Chris Hughes]

Have you used have before?

[Kenny Lau]

variables A : Prop

example : ¬ (A ↔ ¬ A) :=
assume h,
have h1 : ¬ A, from _,
show false, from _

[Kenny Lau]

so your code should look like this

[Kaushik Chakraborty]

yeah that's what I am trying but could not think of any intro/elim rule to apply to get ¬ A from h

[Moses Schönfinkel]

The biggest hint here was the innocuous sentence "...and I was annoyed with myself for assuming excluded middle" :). You can't conjure not A from thin air, but you can conjure something almost as good.

[Kaushik Chakraborty]

Ok I think I got it

variables A : Prop

example : ¬ (A ↔ ¬ A) :=
assume h,
have h1 : ¬ A, from
    assume a : A,
    show false, from (h.mp a) a,
show false, from h1 (h.mpr h1)

[Kaushik Chakraborty]

thanks a lot for the guidance

[Kaushik Chakraborty]

Hello again. I want to do the exercise 17.1 of the course on proving the equivalence of principle of complete induction to principle of least element in Lean. So in that regard does the following setup make sense? I still need to do the actual proof.

variable P : ℕ → Prop

example : ∀ n, (∀ m, m < n ∧ P(m) →  P(n)) → ∀ x, P(x) ↔
                ∀ n, P(n) ∧ ∃ m x, m < n ∧ ¬ (x < m) → P(m) :=
sorry

[Mario Carneiro]

the parentheses seem to be off in a few places

[Mario Carneiro]

I think this is correct with minimal parentheses:

variable P : ℕ → Prop

example : ((∀ n, (∀ m, m < n → P m) → P n) → ∀ x, P x) ↔
            ∀ n, P n → ∃ m, P m ∧ ∀ x, x < m → ¬ P x :=
sorry

[Mario Carneiro]

the statement of the principle of least element you gave looks really weird and is probably incorrect - I've changed the statement a bit

[Mario Carneiro]

I expect it to say something like "if P(n) for some n, then there exists an m such that P(m), and ¬ P(x) for all smaller x"

[Johan Commelin]

The current statement reads to me as "I can prove P by induction iff the principle of least element holds for P"

[Mario Carneiro]

My point is that the right hand side doesn't look like the PLE to me

[Johan Commelin]

Oooh, you are completely right. The right hand side should start with \exists. As stated it is trivial: take m = 0.

[Mario Carneiro]

Also, I don't think this will actually work (unless you prove both sides individually), since the traditional reduction of induction to PLE and vice versa involves negating P

[Mario Carneiro]

this can be rectified by quantifying P individually on each side:

example : (∀ P : ℕ → Prop, (∀ n, (∀ m, m < n → P m) → P n) → ∀ x, P x) ↔
           ∀ (P : ℕ → Prop) n, P n → ∃ m, P m ∧ ∀ x, x < m → ¬ P x :=
sorry

[Kaushik Chakraborty]

Ok. I got the formalization of PLE. Thanks

[Kaushik Chakraborty]

although in your formalization of PLE, there is no relation between n and m. Shouldn't we mention that m < n ?

[Mario Carneiro]

There is no need, in the same way that there is no relation between n and x in the statement of induction

[Mario Carneiro]

You can prove, given the conclusion, that m <= n, but it is possible that m = n if n is already the minimal witness

[Mario Carneiro]

another way to bracket it is ∀ (P : ℕ → Prop), (∃ n, P n) → ∃ m, P m ∧ ∀ x, x < m → ¬ P x

[Kaushik Chakraborty]

Ok got it.

[Kaushik Chakraborty]

I'm stuck at this simple proof. how do I go from n * n < m * m to n ^ 2 < m ^2

open nat
variables n m : ℕ

example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 :=
assume h,
have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left,
have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right),
have n * n < m * m, from lt_trans ‹ n * n < n * m › ‹ n * m < m * m ›,
sorry

[Kenny Lau]

open nat
variables n m : ℕ

example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 :=
assume h,
calc  n ^ 2
    = nat.pow n 2 : by dsimp [(^)]; refl
... = 1 * (n * n) : nat.mul_assoc 1 n n
... = n * n : nat.one_mul _
... < n * m : mul_lt_mul_of_pos_left h.right h.left
... < m * m : mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right)
... = m ^ 2 : by simp [(^), nat.pow]

[Kenny Lau]

@Mario Carneiro why can't I replace by dsimp [(^)]; refl with rfl?

[Chris Hughes]

Definitional equality is not transitive.

[Kenny Lau]

but then why does this work?

[Kenny Lau]

example : n ^ 2 = nat.pow n 2 := rfl

[Kenny Lau]

Definitional equality is not consistent either?

[Kaushik Chakraborty]

thanks @Kenny Lau . I still don't understand tactics. Maybe the theorem proving in lean course will help. Logic and Proof course have few mentions of tactics.

[Johan Commelin]

Kaushik, to answer your original question, there is pow_two which you can use to rewrite between n * n and n^2.

[Kenny Lau]

it's not available without further import though

[Johan Commelin]

Right, you need to import algebra.group_power, I think.

[Kaushik Chakraborty]

thanks @Johan Commelin. but am still not sure how to use pow_two in my proof. I think I have to use rewrite tactic but not sure how. Here is how I've changed my earlier proof

import algebra.group_power
open nat
variables n m : ℕ

example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 :=
assume h,
have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left,
have n ^ 2 < n * m, by sorry,
have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right),
have n * m < m ^ 2, by sorry,
lt_trans ‹ n ^ 2 < n * m ›  ‹ n * m < m ^ 2 ›

[Johan Commelin]

example (n : ℤ) : n ^ 2 = n * n :=
begin
  rewrite pow_two
end

[Kenny Lau]

example (n : ℤ) : n ^ 2 = n * n := pow_two n

[Kaushik Chakraborty]

yeah I got the function usage part but how do I use pow_two when I've the lt relation i.e. replace sorry in have n ^ 2 < n * m, by sorry when I've established n * n < n * m. Or I'm approaching it wrong ?

[Kevin Buzzard]

You should be able to do this with rw

[Kevin Buzzard]

import algebra.group_power

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m :=
begin
  have H : n ^ 2 = n * n := pow_two n,
  rw H,
  exact h
end

[Kevin Buzzard]

You should also be able to do it with eq.subst but I can never ever ever for the life of me get it to work.

[Kenny Lau]

\t

[Kevin Buzzard]

import algebra.group_power

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

[doesn't work]

[Kevin Buzzard]

Can you fix it Kenny?

[Kenny Lau]

I think you would like by convert h

[Kenny Lau]

import algebra.group_power

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m :=
have H : n * n = n ^ 2, from eq.symm $ pow_two n,
H ▸ h

[Kenny Lau]

I'm not sure why your original version doesn't work

[Kenny Lau]

import algebra.group_power

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m :=
by convert h; from pow_two n

[Kevin Buzzard]

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m :=
((((pow_two n).symm : n * n = n ^ 2) ▸ (h : n * n < n * m)) : n ^ 2 < n * m)

[Kenny Lau]

:o

[Kevin Buzzard]

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  n ^ 2 < n * m

[Kevin Buzzard]

I see no metavariables!

[Kenny Lau]

yeah I'm puzzled too

[Chris Hughes]

example (m n : ℤ) (h : n * n < n * m) : n ^ (2 : ℕ) < n * m := (pow_two n).symm ▸ h

[Kenny Lau]

...

[Chris Hughes]

works

[Kevin Buzzard]

...

[Kevin Buzzard]

The well-known metavariable 2

[Kevin Buzzard]

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  @has_lt.lt.{0} int int.has_lt
    (@has_pow.pow.{0 ?l_1} int ?m_2 ?m_3 n (@bit0.{?l_1} ?m_2 ?m_4 (@has_one.one.{?l_1} ?m_2 ?m_5)))
    (@has_mul.mul.{0} int int.has_mul n m)

[Kevin Buzzard]

Indeed there was a metavariable

[Chris Hughes]

This works lemma thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

[Kenny Lau]

?????????????????

[Chris Hughes]

not this though def thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

[Kevin Buzzard]

I think this is a bug in pow_two -- the inbuilt 2 is a nat

[Kevin Buzzard]

Clearly pow_two should be a definition not a theorem

[Kevin Buzzard]

Or am I barking up the wrong tree ;-)

[Kenny Lau]

I agree. Split the definition into more cases for easier definitional equality.

[Chris Hughes]

I don't think it has anything to do with pow_two

lemma two_add_three : 2 + 3 = 5 := add_comm 0 5 ▸ rfl -- works

example : 2 + 3 = 5 := add_comm 0 5 ▸ rfl -- doesn't work

[Kevin Buzzard]

example : (2 : ℕ) + 3 = 5 := add_comm 0 5 ▸ rfl -- works

[Kevin Buzzard]

So the bit where it says "Ok I can't figure out the type of this 2 thing, let's let it be nat just so we can get on" is not occurring in the examples

[Kevin Buzzard]

Maybe pow_two should have been an example. Wait...

[Mario Carneiro]

The reason that example and def fail while theorem succeeds is due to the separation of statement and proof done with theorem

[Mario Carneiro]

Remember how I mentioned a long time ago that nat is the default type for numerals but it occurs very late in the elaboration? It's basically the last resort if there is a numeral of indeterminate type

[Mario Carneiro]

In regard to this example, what happens is that since def/example allows the statement and proof to be elaborated together, it checks the proof to see if that will give a hint what is alpha in (2:alpha) + 3 = 5. But that means that when it hits the eq.subst it will still have a lingering metavariable. In the theorem case, there is no information to be had, since the proof doesn't contribute to elaborating the statement, so it goes with the default nat type for numerals. Then when it elaborates the proof, there are no metavariables

[Kaushik Chakraborty]

For this code in the LEAN live in-browser IDE

import algebra.group_power
theorem thing (m n : ℕ) (h : n * n < n * m) : (n ^ 2 < n * m) := (pow_two n).symm ▸ h

am getting following error

"eliminator" elaborator type mismatch, term
  h
has type
  n * n < n * m
but is expected to have type
  n ^ 2 < n * m
Additional information:
/test.lean:2:82: context: the inferred motive for the eliminator-like application is
  λ (_x : ℕ), n ^ 2 < n * m

[Kevin Buzzard]

Join the ▸-haters club!

[Kevin Buzzard]

Sometimes the issue is that higher-order unification is undecidable, sometimes I've just made a silly mistake.

[Chris Hughes]

The mistake here is that pow_two is a theorem about monoid.pow and not nat.pow

[Kevin Buzzard]

yes, I just realised that when trying to solve without the triangle

[Kevin Buzzard]

invalid type ascription, term has type
  @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat (@monoid.has_pow nat nat.monoid) n 2)
    (@has_mul.mul nat nat.has_mul n m)
but is expected to have type
  @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat nat.has_pow n 2) (@has_mul.mul nat nat.has_mul n m)

[Kevin Buzzard]

theorem nat.pow_two (a : ℕ) : a ^ 2 = a * a := show (1 * a) * a = a * a, by rw one_mul

theorem thing (m n : ℕ) (h : n * n < n * m) : (n ^ 2 < n * m) := (nat.pow_two n).symm ▸ h

[Kaushik Chakraborty]

thanks @Kevin Buzzard this worked. however, I have some doubts about the nat.pow_two theorem. In your proof, you showed a different equality than what is in the sig. of the theorem. Is Lean somehow guessing the fact that (1 * a) * a = a ^ 2. Or how is the rewrite tactics working here?

[Nicholas Scheel]

that’s obtained by unfolding the definition of pow, which basically is that n^a = (((1*n)*n)*...)*n (with a ns of course)

[Kaushik Chakraborty]

got it. thanks, @Nicholas Scheel

[Kevin Buzzard]

Yes, there are two kinds of equality in Lean. There's "equal by definition" and "equal because of a theorem". a^2=1*a*a is true by definition of ^ (you can discover this sort of thing by continually unfolding everything -- switch off notation and just get unfolding in tactic mode and see where you go) but 1*a=a is true because of a theorem. Things that are equal by definition you can just use interchangeably (I used show to change the goal to a goal which Lean thinks is the same goal by definition), but then I used a rewrite to apply the theorem.

[Kaushik Chakraborty]

I am trying to attempt a Lean proof of quotient-remainder theorem shown here and, as usual, clueless on the approach. I've tried to chalk out a rough skeleton of the proof based on my understandings from an earlier chapter on doing induction in Lean & some exploration of Lean's types and functions. Does it make sense?

open int
open nat

 -- quotient / remainder theorem
theorem qt (n m q r : ℤ) : m > 0 → n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume h,
show (n = m * q + r) ∧ (0 ≤ r ∧ r < m), from
  int.rec_on n
  (assume k,
  show (of_nat k = m * q + r) ∧ ( 0 ≤ r ∧ r < m ), from
    nat.rec_on k
      (show (of_nat 0 = m * q + r) ∧ (0 ≤ r ∧ r < m), from sorry)
      (assume k ih,
        show of_nat (succ k) = m * q + r ∧ (0 ≤ r ∧ r < m), from sorry)
  )
  (assume k,
    have h11 : -of_nat (k + 1) = m * q + r, from sorry,
    have h22 : 0 ≤ r ∧ r < m, from sorry,
    ⟨ h11 , h22 ⟩)

[Chris Hughes]

The theorem isn't true. This says for all n m q r, ... Whereas you want forall m n, exists q r,...

[Chris Hughes]

the proof of this theorem in the lean library is a combination of int.mod_add_div, int.mod_lt and int.mod_nonneg.

[Kaushik Chakraborty]

Oh, thanks for clarifying. Does this theorem statement make sense?

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, (n = m * q + r) ∧ (0 ≤ r ∧ r < m) :=
sorry

[Kaushik Chakraborty]

I tried to solve the above statement with the functions you mentioned but I could not figure out how to come up with the existential terms q & r from n and m and hence the proof does not type check. I must be formulating the theorem statement wrong or missing some approach in the proof.

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume n m h,

assume q r,
assume h2 : q = n / m,
assume h1 : r = n % m,

have HH:  n = m * q + r, from calc
  n = n % m + m * (n / m) : by rw [int.mod_add_div]
  ... = r + m * (n / m) : by rw h1
  ... = r + (m * q) : by rw h2
  ... = (m * q) + r : by rw add_comm,

have HH1: 0 ≤ r, from calc
  0 ≤ n % m : int.mod_nonneg n (ne_of_gt h)
  ... ≤ r : by rw h1,

have HH2: r < m, from calc
  r = n % m : by rw h1
  ... < abs m : int.mod_lt n (ne_of_gt h)
  ... = m : abs_of_pos h,

exists.intro q (exists.intro r (and.intro HH  (and.intro HH1 HH2) ))

[Mario Carneiro]

This is an incorrect use of the assume keyword. assume is used only for proving a forall or pi or implication, and it introduces a variable with the type specified in the domain. To prove an existential, you use exists.intro and provide the witness you want

[Mario Carneiro]

So after assume n m h, you should write exists.intro (n / m) $ exists.intro (n % m) $ instead of assume q r, assume h2 : q = n / m, assume h1 : r = n % m,

[Mario Carneiro]

(The dollar signs are to save on having to close parentheses at the end of the proof)

[Mario Carneiro]

After that, q and r will no longer be present in the statement, so you won't need to rewrite with h1 anymore

[Kaushik Chakraborty]

I knew what was wrong with that assume but your tip on the exists.intro was helpful. Here's my updated proof which type checks

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume n m h,

exists.intro (n / m) $ exists.intro (n % m) $

  have HH:  n = m * (n / m)  + (n % m), from calc
    n = n % m + m * (n / m) : by rw [int.mod_add_div]
    ... = m * (n / m) + (n % m) : by rw add_comm,

  have HH1: 0 ≤ (n % m), from int.mod_nonneg n (ne_of_gt h),

  have HH2: (n % m) < m, from calc
    (n % m) < abs m : int.mod_lt n (ne_of_gt h)
    ... = m : abs_of_pos h,

  ⟨ HH , ⟨ HH1 , HH2 ⟩ ⟩

[Olivier de G.]

I am working on exercice 2 of Chapter 2. The exercise states that the first clue can be represented as

$((FA \lor SA) \rightarrow (MW \lor DW)) \land ((MA \lor DA) \rightarrow (FW \lor SW))$

Should the implications be replaced with iff as follows ?

$((FA \lor SA) \leftrightarrow (MW \lor DW)) \land ((MA \lor DA) \leftrightarrow (FW \lor SW))$

[Olivier de G.]

Humm maybe it's actually equivalent because of

$FW \lor SW \lor MW \lor DW$

and

$FA \lor SA \lor MA \lor DA$

[Kevin Buzzard]

I think you're right. Both interpretations are valid translations of the sentence and. as you say, both are equivalent in the context (but of course they are not equal).

This is a common theme I guess. I found it interesting watching computer scientists claiming that they had proved there were infinitely many primes by showing that given a finite set of primes, they could find a prime not in this set. I initially thought "that's not what infinite means" but then I realised that actually it's a perfectly reasonable way of formalising it ("no finite set of primes is all the primes") and actually I didn't really know what infinite meant -- there are several definitions of infinite, all equivalent, but not at all equal, and one has to make a choice at some point.