Whelp Input Syntax

• locate <pattern>

  <pattern> is a shell like pattern which could include * (denoting any sequence of 0 or more characters) and ? (denoting any single character).
  

  Examples:

  • nat pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only
  • n?t pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) and cic:/Coq/Init/Logic/not.con
  • nat* pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1), cic:/Coq/Init/Peano/nat_case.con and many more

• match <term>

  Examples:

  • \forall x,y:nat.x+y=y+x (commutativity of natural plus)
  • \forall x,y,z:R.x*(y+z)=x*y+x*z (distributivity of real times over real plus)
  • nat \to nat \to nat (all binary functions over naturals)

• hint <term>

  Examples:

  • \forall n:nat. (fact n) = n * (fact (n - 1)) (how could we prove n! = (n-1)! * n ?)
  • \forall n:nat.n \lt n+5 (how could we prove n < n + 5 ?)
  • \forall x,y:nat. x*y \lt (S x)*(S y) (how could we prove x*y < (x+1)*(y+1) ?)

• elim <identifier>

  Examples:

  • nat (induction/elimination principles over natural numbers)
  • list (induction/elimination principles over lists)