Matita HomeMatita HomeTable 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 )] |