Как упростить доказательство по индукции в Lean? - PullRequest
Новая
       16

Как упростить доказательство по индукции в Lean?

0 голосов
/ 29 апреля 2019

Я бы хотел упростить доказательство по индукции в Lean.

Я определил индуктивный тип с 3 конструкторами в Lean и бинарным отношением для этого типа. Я включил аксиомы, потому что Лин не позволил мне использовать их в качестве конструкторов для rel. 


inductive Fintype : Type
| a : Fintype
| b : Fintype
| c : Fintype

inductive rel : Fintype → Fintype →  Prop 
| r1 : rel Fintype.a Fintype.b
| r2 : ∀ p : Prop, (p → rel Fintype.a Fintype.c )
| r3 : ∀ p : Prop, (¬ p → rel Fintype.c Fintype.b) 


axiom asymmetry_for_Fintype : ∀ x y : Fintype, rel x y → ¬ rel y x
axiom trivial1 : ¬ rel Fintype.c Fintype.a
axiom trivial2 : ¬ rel Fintype.b Fintype.c
axiom trivial3 : ∀ p : Prop, rel Fintype.a Fintype.c → p 
axiom trivial4 : ∀ p : Prop, rel Fintype.c Fintype.b → ¬ p

Целью было доказать следующую теорему: 

def nw_o_2 (X : Type) (binrel : X → X → Prop) (x y : X) : Prop := ¬ binrel y x
def pw_o_2 (X : Type) (binrel : X → X → Prop )(x y : X) : Prop := ∀ z : X, (binrel z x → binrel z y) ∧ (binrel y z → binrel x z)

theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=

Я доказал это индукцией по x, y и z; «z» происходит из определения pw_o_2 выше. Но доказательство довольно длинное (~ 136 строк). Есть ли другой способ получить более короткое доказательство?

1 Ответ

1 голос
/ 04 июня 2019

Обратите внимание, что ваши первые две аксиомы - это действительно теоремы, доказуемые пустым совпадением с образцом. (Конструкторы индуктивных типов предполагаются сюръективными.) Точки в концах этих строк указывают, что объявление закончено, что тело не ожидается. Внутренне, Лин повторяет доказательство rel Fintype.c Fintype.a и показывает, что каждый случай структурно невозможен. 

lemma trivial1 : ¬ rel Fintype.c Fintype.a.
lemma trivial2 : ¬ rel Fintype.b Fintype.c.

Ваши вторые две аксиомы противоречивы, что делает доказательство вашей теоремы простым, но неинтересным. 

theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=
false.elim (trivial3 _ (rel.r2 _ trivial))

Я не уверен, что вы определили rel так, как вы хотели. Второй и третий конструкторы эквивалентны просто rel Fintype.a Fintype.c и rel Fintype.c Fintype.b соответственно. 

lemma rel_a_c : rel Fintype.a Fintype.c :=
rel.r2 true trivial

lemma rel_c_b : rel Fintype.c Fintype.b :=
rel.r3 false not_false
...