Zulip Chat Archive

Stream: maths

Topic: proofs in cocalc


view this post on Zulip Jane (Feb 29 2020 at 00:38):

Hey guys, can someone please help me with two problem using some of the axioms?

def has_min_element {A : Type} (R : A  A  Prop) : Prop :=
     x,  y, R x y
axiom ax1 {n m: } : (n  m)  ( l : , n + l = m)
axiom ax2 {m n x y: } (h1 : x + n = y) (h2 : y + m = x): x = y  (m = 0)  (n = 0)
axiom ax3 {m n x y z : } (h1 : x + n = y) (h2 : y + m = z) : x + (n + m) = z
axiom ax4 : 1  2
axiom ax5 (m n : ) :  l : , m + l = n  n + l = m
axiom ax6 (n : ) : 0 + n = n

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
sorry

example : ¬ (equivalence nat.less_than_or_equal) :=
sorry

Thank you guys soooo much !!!

view this post on Zulip Anne Baanen (Mar 02 2020 at 10:24):

To get started, it's good to realize ¬ p is the same as p → false, and x ≠ y is the same as ¬ (x = y), which is the same as (x = y) → false.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 10:33):

A lot of these axioms are things which one can prove in Lean anyway. Here's an axiom-free proof of the first one:

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
begin
  intro h, -- proof by "mathematician's contradiction", i.e. assume it's symmetric
  -- and get a contradiction
  unfold symmetric at h, -- says x ≤ y → y ≤ x
  have h12 : 1  2 := dec_trivial,
  have h21 : ¬ 2  1 := dec_trivial,
  apply h21,
  apply h,
  exact h12,
end

but it's hard to work out if this is what you're looking for.


Last updated: May 19 2021 at 02:10 UTC