Chapter 8. Declarative Tactics

Table of Contents

Quick reference card
by induction hypothesis we know
let such that
the thesis becomes
we need to prove
we have
we proceed by cases on
we proceed by induction on
we proved

Quick reference card

Table 8.1. tactics

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