8.1 Refine

8.1 `Refine`

This feature is new in version 6.2. It's still experimental.

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 synthetised by the system or declared by an explicit cast like (?::nat->Prop). This relatively 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 n.

Coq < Auto.

Coq < Destruct n.

Coq < Tauto.

Coq < Destruct n.

Coq < Tauto.

Coq < Destruct n.

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!

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.3.0.html at 8/10/98