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

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

Я определил индуктивный тип с 3 конструкторами в Lean и бинарным отношением для этого типа. Я включил аксиомы, потому что 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 строк). Есть ли другой способ получить более короткое доказательство?


theorem-proving lean
person LyX2394    schedule 28.04.2019    source источник
comment
Можете ли вы опубликовать свое доказательство в Интернете (может быть, как Github gist или pastebin). Вы используете терминологический или тактический режим? Или задайте вопрос на leanprover.zulipchat.com, чтобы получить больше информации.   -  person jmc    schedule 29.04.2019
comment
@jmc Я использовал тактику. Вот ссылка на доказательство: pastebin.com/VR4H5g10.   -  person LyX2394    schedule 30.04.2019
comment
Вы можете сжать свое доказательство, используя тактики all_goals, try и repeat. Однако я не удивлюсь, если вы действительно сможете превратить его в однострочник с dec_trivial. Возможно, вы захотите прочитать последний.   -  person jmc    schedule 01.05.2019
comment
Здорово! Я сократил длину доказательства до одной четвертой от его первоначальной длины. Спасибо.   -  person LyX2394    schedule 23.05.2019

Ответы (1)


arrow_upward
2
arrow_downward

Обратите внимание, что ваши первые две аксиомы на самом деле являются теоремами, которые можно доказать с помощью сопоставления с пустым образцом. (Предполагается, что конструкторы индуктивных типов сюръективны.) Точки на концах этих строк указывают на то, что объявление окончено и тело не ожидается. Внутренне Lean рекурсивно переходит к доказательству 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
person Rob Lewis    schedule 04.06.2019
comment
Спасибо за Ваш ответ. В последнем абзаце вашего ответа, я думаю, вы имеете в виду третий и четвертый конструкторы. Почему последнее предложение этого абзаца верно? - person LyX2394; 29.06.2019
comment
Нет, я имею в виду r2 и r3, второй и третий конструкторы rel. Я добавил в свой ответ доказательства rel a c и rel c b с использованием этих конструкторов. - person Rob Lewis; 29.06.2019
comment
Намерение состояло в том, чтобы определить бинарное отношение на Fintype следующим образом: для любого предложения P всегда должно выполняться rel Fintype.a Fintype.b; rel Fintype.a Fintype.c должен удерживаться, если выполняется P, и rel Fintype.c Fintype.b должен удерживаться, если выполняется (не P). - person LyX2394; 01.07.2019
comment
Похоже, вы хотите, чтобы отношение rel зависело от аргумента P. Вам, вероятно, следует определить inductive rel (P : Prop) : Fintype → Fintype → Prop. - person Rob Lewis; 01.07.2019
comment
Да, мне нужна зависимость от P. Попробую вот это: inductive rel2 (P : Prop) : Fintype → Fintype → Prop |s1 : rel2 Fintype.a Fintype.b |s2 : P → rel2 Fintype.a Fintype.c |s3 : ¬ P → rel2 Fintype.c Fintype.b - person LyX2394; 03.07.2019
comment
Я определил бинарное отношение по отношению к Prop; см. pastebin.com/Vpmk7wE4. Но я бы хотел, чтобы конструкторы s2 и s3 были эквивалентными. В конечном итоге мне нужно сказать, что rel2 Fintype.a Fintype.c выполняется именно тогда, когда не выполняется p. В бережливом производстве, я полагаю, это могло быть переведено на существование эквивалентности между rel2 Fintype.a Fintype.c и «не p». Я не понимаю, как это сделать в Lean; Я полагаю, решение состоит в том, чтобы наложить аксиомы «тривиальный8» и «тривиальный9». - person LyX2394; 22.07.2019
comment
Легко вывести rel2 p Fintype.a Fintype.c из доказательства ¬ ¬ p, это просто конструктор s2. В другую сторону: lemma not_not_p_of_rel2 (p : Prop) : rel2 p Fintype.a Fintype.c → ¬ ¬ p | (rel2.s2 h) := h Но я не уверен, что это подходящее место для обсуждения. Я бы порекомендовал посетить чат Lean Zulip по адресу leanprover.zulipchat.com. - person Rob Lewis; 22.07.2019
comment
Понятно. Спасибо! - person LyX2394; 24.07.2019