dmytrish (dmytrish) wrote,
dmytrish
dmytrish

destruct them all

Є, значить, тут теоремка із першого розділу 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.

Tags: coq, fp, програмістське
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded 

  • 9 comments