Previous Entry —>другу Next Entry
destruct them all
sicp
dmytrish
Є, значить, тут теоремка із першого розділу Software Foundations:

Theorem andb_eq_orb:
  forall (b c : bool), (andb b c = orb b c) -> b = c.




В принципі, ясно, що твердження покладається на семантику операцій andb та orb, і тому доводити його треба через аналіз можливих випадків b і c. Тактику destruct в книжці уже показували, тому, здавалось би, залишилось проаналізувати випадки:

1 subgoal
  
  ============================
   forall b c : bool, (b && c)%bool = (b || c)%bool -> b = c

andb_eq_orb < intros b c.
1 subgoal
  
  b : bool
  c : bool
  ============================
   (b && c)%bool = (b || c)%bool -> b = c

andb_eq_orb < destruct b.
2 subgoals
  
  c : bool
  ============================
   (true && c)%bool = (true || c)%bool -> true = c

subgoal 2 is:
 (false && c)%bool = (false || c)%bool -> false = c

andb_eq_orb < destruct c.
3 subgoals
  
  ============================
   andb true true = orb true true -> true = true

subgoal 2 is:
 andb true false = orb true false -> true = false
subgoal 3 is:
 forall c : bool, andb false c = orb false c -> false = c

andb_eq_orb < reflexivity.
2 subgoals
  
  ============================
   andb true false = orb true false -> true = false

subgoal 2 is:
 forall c : bool, andb false c = orb false c -> false = c

andb_eq_orb < reflexivity.
Toplevel input, characters 0-11:
> reflexivity.
> ^^^^^^^^^^^
Error: Impossible to unify "false" with "true".



А от тут я перестаю розумію, чому Coq не може обчислити, що andb true false = orb true false -> true = false це правда. Здавалось би, простий reflexivity:

andb true false = orb true false -> true = false;
false = orb true false -> true = false;
false = true -> true = false;
false -> false;
true.




Підкажіть новачку, що тут не так.

P.S. simpl допоміг, цікаво, перечитаю про різницю між ним і reflexivity.
P.P.S. Довелось ще поборотись із зведенням false = true -> true = false, неочевидний трюк: intro H. rewrite H.. В результаті таки довів (хоч і почуваюсь індусом, який пише на Coq):

Proof.
  destruct b. 
   destruct c. 
    simpl. reflexivity. 
    simpl. intro H. rewrite H. reflexivity. 
   destruct c. 
    simpl. intro H. rewrite H. reflexivity. 
    simpl. reflexivity. 
Qed.


  • 1
"andb true false = orb true false -> true = false"

а не навпаки?

andb true false = orb true false -> false = true

Та ні, якраз так, як у пості написано. І тому при ситуації, коли ціль false = true -> true = false довелось викручуватись із винесенням false = true в гіпотезу (але ж чорт, це суперечність, взагалі перестаю щось розуміти)

Суперечність також має право на існування. Це не доведення, це лише "вислів".

Не знаю, як там в Coq, але рівність - це ж просто конструктор з двома аргументами.

В даному випадку інтерпретація така: якщо вдалось довести, що and true false = or true false, то можна довести, що true = false. Звичайно, останнє - суперечність, але і перше - також суперечність (and true false = or true false is not inhabited)

Не знаю, як там в Coq, але ∀ f A B -> f B A - це функція flip.

Ну так. я думав про те, щоб довести комутативність and/or, навіть довів, от тільки не зрозумів, як її застосувати до частини виразу.

Щодо імплікації, то мене дивує, що simpl не може просто взяти і порахувати її як логічний вираз.

Що означає "порахувати її як логічний вираз"?

Комутативність and/or тут, здається, не допоможе, бо окрім їх комутативності треба довести "внутрішню" комутативність рівності: (and a b) == (or a b) -> (and b a) == (or b a). Це зазвичай робиться за одни крок (∀ x y f -> x == y -> f x == f y), але тут його не має змоги застосувати, бо у нас різні функції коммутативності.

Імплікація — це ж просто ще одна логічна операція, ні? І її результат просто зводиться або до true, або до false.

Я Coq не знаю, не скажу, чи є імплікація там чимось особливим.

По Каррі-Говарду імплікація - це тип функції, стрілка з одного типу в інший. Але це ще не доведення імплікації. Доведення - це вже тіло функції, її реалізація.

А до того ж, ми знаходимось в якомусь варіанті інтуіціоністської логіки - окрім true і false, маємо справу з non-termination.

Звичайно, може здаватись дивним, чому б не реалізувати імплікацію для типу bool - там же маленька кількість варіантів. Але чому bool такий особливий? Або чому імплікація така особлива? Чому б не реалізувати будь-яку іншу операцію "автоматично"? Бо немає "автоматичного" способу довести (non-)termination для будь-якої операції.


Скажімо, вислів (and a b == or a b -> a == b) - це насправді функція від трьох аргументів: a, b та рівність (and a b == or a b) (можна розглядати як функцію типу a -> b -> and a b == or a b -> a == b - тут цілих три залежних типи є). Мусимо побудувати функцію, яка маючи оці три аргументи будує об’єкт a == b.

Патерн-матчимо. У випадках

false false f==f
true true t==t
false true f==t

нам уже передано аргумент правильного типу: третій аргумент уже є рівністю того типу, який нам треба повернути.

Четвертий випадок

true false f==t

має "зворотній" порядок аргументів у типі третього аргумента (маємо значення залежного типу false == true, а функція має повернути true == false), але ми можемо отримати "правильний" порядок з лемми симетрії рівності (a == b -> b == a). Це, власне, що там відбувається. Решта писанини - це спосіб висловити це в Coq.

а, тьху, так, ми ж отримуємо b = c, то справді треба побудувати true = false.

Да, в моєму ручному «приведенні» була помилка, груба, але несуттєва.

  • 1
?

Log in

No account? Create an account