The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Hi,

In the manual, it says that [Guarded] verifies that the guard condition 
hasn't been violated at some point in a proof.

1.  What does that mean in the context of the following example?

2.  Why does the first [Guarded] fail?

3.  Is [Guarded] automatically called by [Qed]?

4.  Presumably, [Guarded] can be used to debug a proof based on [fix]. 
However, is there another, possibly better, way? 

Thanks.

Inductive C : Set :=
   Build_C : option C -> C.

Fixpoint F (c : C) : Prop :=
   match c with |
      Build_C None => True |
      Build_C (Some c') => F c'
   end.

Lemma L : forall c : C, F c.
Proof.
   fix H 1.
(* Guarded - Fails *)
   intro c.
Guarded.
   destruct c as [o].
Guarded.
   destruct o as [| c'].
Guarded.
   unfold F.
Guarded.
   exact (H c).
Guarded.
   unfold F.
Guarded.
   trivial.
Qed.

Regards,
Jeff.