Table of Contents
Table 8.1. tactics
tactic | ::= | = term [auto_params | using term | using once term | proof] [done] |
| | assume id : sterm | |
| | by induction hypothesis we know term ( id ) | |
| | case id [( id : term )] … [( id : term )] | |
| | conclude term | |
| | justification done | |
| | justification let id : term such that term ( id ) | |
| | let id = term | |
| | obtain id term | |
| | suppose term ( id ) | |
| | that is equivalent to term | |
| | the thesis becomes term | |
| | we need to prove term [(id )] | |
| | we proceed by cases on term to prove term | |
| | we proceed by induction on term to prove term | |
| | justification we proved term [( id )] |