8.1 Refine

8.1 `Refine`

This tactic applies to any goal. It behaves like Exact with a big difference : the user can leave some holes (denoted by ? or (?::type)) in the term. Refine will generate as many subgoals as they are holes in the term. The type of holes must be either synthesized by the system or declared by an explicit cast like (?::nat->Prop). This low-level tactic can be useful to advanced users.

Example 1:

Coq < Require Refine.

Coq < Inductive Option: Set := Fail : Option | Ok : bool->Option.

Coq < Definition get: (x:Option)~x=Fail->bool.
1 subgoal

  ============================
   (x:Option)~x=Fail->bool

Coq < Refine
Coq <   [x:Option]<[x:Option]~x=Fail->bool>Cases x of
Coq <         Fail   =>  ?
Coq <       | (Ok b) =>  [_:?]b end.
1 subgoal

  x : Option
  ============================
   ~Fail=Fail->bool

Coq < Intros;Absurd Fail=Fail;Trivial.
Subtree proved!

Coq < Defined.

Example 2: Using Refine to build a poor-man's ``Cases'' tactic Refine is actually the only way for the user to do a proof with the same structure as a Cases definition. Actually, the tactics Case (see 7.7.2) and Elim (see 7.7.1) only allow one step of elementary induction.

Coq < Require Bool.

Coq < Require Arith.

Coq < Definition one_two_or_five := [x:nat]
Coq <   Cases x of
Coq <     (1) => true
Coq <   | (2) => true
Coq <   | (5) => true
Coq <   | _ => false
Coq <   end.
one_two_or_five is defined

Coq < Goal (x:nat)(Is_true (one_two_or_five x)) -> x=(1)\/x=(2)\/x=(5).
1 subgoal

  ============================
   (x:nat)(Is_true (one_two_or_five x))->x=(1)\/x=(2)\/x=(5)

A traditional script would be the following:

Coq < Destruct x.

Coq < Tauto.

Coq < Destruct n.

Coq < Auto.

Coq < Destruct n0.

Coq < Auto.

Coq < Destruct n1.

Coq < Tauto.

Coq < Destruct n2.

Coq < Tauto.

Coq < Destruct n3.

Coq < Auto.

Coq < Intros; Inversion H.

With the tactic Refine, it becomes quite shorter:

Coq < Restart.

Coq < Require Refine.

Coq < Refine [x:nat]
Coq <   <[y:nat](Is_true (one_two_or_five y))->(y=(1)\/y=(2)\/y=(5))>
Coq <   Cases x of
Coq <     (1) => [H]?
Coq <   | (2) => [H]?
Coq <   | (5) => [H]?
Coq <   | _ => [H](False_ind ? H)
Coq <   end; Auto.
Subtree proved!