Zulip Chat Archive

Stream: new members

Topic: Finding a contradiction


Shadman Sakib (Jul 25 2021 at 18:13):

The contradiction should be that since a : Z then a ≠ n would mean a is not in Z but Lean does not understand. How can I make this contradiction more explicit?

Shadman Sakib (Jul 25 2021 at 18:13):

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

local notation `|` x `|` := complex.abs x
local notation `π` := real.pi

example (R : Type*) (n : ) (θ : ) (a : ) (h : 2  0)
  (h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
  [linear_ordered_ring R]
  (this : θ * I + I * -(θ / 2) = I * (θ / 2))
  (ha : I * 2 + I * (θ / 2) =
          -(I * 2) + I * (θ / 2) + a * (2 * π * I))
  (this : (2 : ) = a * π)
  (h₀ : (a :) = 2 / π)
  (h₂ : 0 < a)
  (h₄ : a < 1)
  (this₁ : a < 1  0 < a  ¬a = n)
  (this₃ : ¬a = n) :
  false :=
begin
  admit,
end

Adam Topaz (Jul 25 2021 at 18:31):

I think you're misunderstanding something here... it looks like a and n are both terms of Z, so there is no contradiction in saying that a and n are different. However, you can get a contradiction from 0<a0<a and a<1a<1 since a is an integer.

Shadman Sakib (Jul 25 2021 at 18:47):

Yes, I have a lemma that I proved showing that if 0 < a and a < 1 then a cannot equal any integer and this1 was the result. Lean will not let me create a have statement saying a is not in Z.

Shadman Sakib (Jul 25 2021 at 18:52):

Maybe this state will help

Shadman Sakib (Jul 25 2021 at 18:53):

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

local notation `|` x `|` := complex.abs x
local notation `π` := real.pi

example (R : Type*) (n : ) (θ : ) (a : ) (h : 2  0)
  (h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
  [linear_ordered_ring R]
  (this : θ * I + I * -(θ / 2) = I * (θ / 2))
  (ha : I * 2 + I * (θ / 2) =
          -(I * 2) + I * (θ / 2) + a * (2 * π * I))
  (this : (2 : ) = a * π)
  (h₀ : (a : ) = 2 / π)
  (h₂ : 0 < a)
  (h₄ : a < 1)
  (this₁ :  (n : ), a < 1  0 < a  ¬a = n) :
  false :=
begin
  admit,
end

Shadman Sakib (Jul 25 2021 at 18:54):

I introduced an n to this1, and applied this1 to h2 and h4, that is why in the previous #mwe this3 has a ≠ n

Adam Topaz (Jul 25 2021 at 18:59):

Saying "a is not in Z" when a : Z makes no sense in type theory.

Adam Topaz (Jul 25 2021 at 19:00):

It seems that this is an issue about understanding type theory, so I suggest looking at the relevant sections of #tpil

Adam Topaz (Jul 25 2021 at 19:01):

(i.e. ch. 2)


Last updated: Dec 20 2023 at 11:08 UTC