Lesson 3: summary

• proofs by backchaining/backward reasoning
• proofs by induction
• stack model, tacticials => and :
• operations on the stack

Proofs by backward chaining

• move=> names introduces hypotheses in the context.
• apply: term does backward reasoning.

Remark dvdn_addr has a side condition.

Remark rewrite accepts

• many rewrite rules,
• the minus switch - to rewrite right to left,
• // to solve simple goals,
• /= to call the simplification heuristic,
• /name to unfold definition name,
• {x} to clear x from the context.

  cf ssreflect documentation on rewrite

Remark n <= m <= p is n <= m && m <= p.

Proofs by induction

The elim: tactic is like case: but gives you an induction hypothesis.

The first pitfall when proving programs by induction is not generalizing enough the property being proved before starting the induction.

Goal management

• naming everything can become bothersome
• but, we should not let the system give random names
• we adopt some sort of stack & heap model

The stack model of a goal

ci : Ti
…
dj := ej : Tj
…
Fk : Pk ci
…
=================
forall (xl : Tl) …,
let ym := bm in … in
Pn xl -> … ->
Conclusion

Managing the stack

• tactic=> names executes tactics, pops and names
• tactic: names pushes the named objects, then execute tactic
• move is the tactic that does nothing (no-op, idtac)

intro-pattern and discharge partterns

You can write

• tactic=> i_items where i_item could be a name, or
  • ? name chosen by the system, no user access,
  • _ remove the top of the stack (if possible),
  • // close trivial subgoals,
  • /= perform simplifications,
  • //= do both the previous,
  • -> rewrite using the top of the stack, left to right,
  • <- same but right to left,
  • {x} clear name x from the context.
  • [i_items|..|i_items] introductions on various sub-goals when immediately tactic is case or elim

  cf ssreflect documentation on introduction to the context

• tactic: d_items where d_item could be a name or a pattern, and
  • tactic must be move, case, elim, apply, exact or congr,
  • move: name clears the name from the context,
  • move: pattern generalize a subterm of the goal that match the pattern,
  • move: (name) forces name to be a pattern, hence not clearing it.

  cf ssreflect documentation on discharge

Example

elim and case work on the top of the stack

elim: x y z => [t u v | w] is the same as

• move: x y z.
• elim.
• move=> t u v. in one sub-goal, move=> w. in the other.

Example of foldl_cat

Lesson 3: sum up

• rewrite takes many arguments
• apply: t backward reasonning on the whole goal
• => is pop to context and : is push
• case case analysis on the top of the stack
• elim induction on the top of the stack