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 + )] + |
+
+