Как переключать типы в доказательстве теоремы Лин, когда константы задействованы? - PullRequest
Новая
       43

Как переключать типы в доказательстве теоремы Лин, когда константы задействованы?

1 голос
/ 09 января 2020

Для новичка, работающего с документацией LEAN, иногда бывает довольно обидно видеть, что некоторые простые проблемы превращаются в настоящие узкие места, когда, по-видимому, решаются более сложные. Вот то, что должно было быть простым самостоятельным упражнением, которое превратилось в несколько часов разочарования (конечно, нет другого способа УЗНАТЬ): 

theorem prByCont : ∀ P : Prop, ( P → false ) → ¬ P :=
    λ (P : Prop) (prf : P → false), prf
#check prByCont

example ( a b : ℕ ) (p: a = 2) (q: b=3) : ¬ (a ≥ b) :=
begin
    apply prByCont,
    assume h : a ≥ b,
    have order : 2 < 3 := dec_trivial,
    contradiction
end

Кажется, проблема в том, что order имеет тип 2<3, но необходимо a<b, и хотя мне кажется, что должно быть ясно, что a=2 и b=3, LEAN так не считает. Пожалуйста, помогите мне увидеть, что мне здесь не хватает!

...