Как доказать пример в Lean?

Ниже представлена ​​моя неправильная попытка. Есть предложения о том, как действовать?

def le(f g : ℕ) : Prop := ∃ a : ℕ , a + f = g

local notation a ≤ b := le a b

    example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
    begin
      assume f g fg gf,
      dsimp[le.nat] at fg,
      dsimp[le.nat] at gf,
      cases fg with a b,
      cases gf with c d,
      rewrite←  b at d,
      rewrite← d at b,
      induction f with f' ih,
      rewrite← d,
      ring,
      ring at d,
      rewrite← b,
      ring,
      ring at b,
      rewrite d,
      ring,
      cases a,
      refl,
      rewrite← d,
      cases c,
      ring,
      contradiction,
      cases c,
      ring at d,
      rewrite← d,
      cases a,
      ring,
      ring at d,
      ring at b,
      exact b,
    
    end

lean
person HippoMan    schedule 22.11.2020    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Если вы import tactic, тогда

example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
begin
  rintro f g ⟨a, rfl⟩ ⟨b, hb⟩,
  omega
end
person Kevin Buzzard    schedule 22.11.2020
comment
@HippoMan, ринтрос такой же, как первые 7 строк вашего доказательства - person Eric; 22.11.2020

arrow_upward
1
arrow_downward

Если по педагогическим причинам вы хотите избежать omega:

example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
begin
  rintro f g ⟨a, rfl⟩ ⟨b, hb⟩,
  rw ←add_assoc at hb,
  conv_rhs at hb {rw ←zero_add f},
  obtain ⟨-, rfl⟩ := nat.eq_zero_of_add_eq_zero (nat.add_right_cancel hb),
  rw zero_add,
end
person Eric    schedule 22.11.2020