search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Proper use of eauto #109

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

In the homework, there is a line in question 14:

eauto using andb_true_l, andb_true_r, andb_false_l, andb_false_r.

Can someone explain to me how eauto works? My guess is that it's sort of like auto, but we can "point it" in certain directions with the theorems we provide it as arguments. Is that correct?

Also, what's the difference between auto, tauto, and eauto?

jaewooklee93 commented 9 years ago

I don't know the deep theory behind *auto tactics, but I really enjoy working with eauto and never use auto or tauto. Moreover, with eauto using, we can provide a hint to Coq about which lemma should be used to clear the goal here, but I'm satisfied with simple eauto without using, because it is enough smart. At least, you don't need to type reflexivity, which is very easy to mistype, because eauto already contains its functionality.

jeehoonkang commented 9 years ago

I guess you experienced some terms starting with ? like: ?1345. Those are called _evariable_s; we don't know what is it yet, but we will get to know in the course of proof. eauto better deals with those evariables than auto. For example, if you have a hypothesis H: a = 3 and the goal ?1345 = 3, auto does not solve the goal but eauto solves the goal by instantiating ?1345 = a.

Similar to other e-tactics: eauto, etransitivity, etc.