The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

On Sun, Jan 19, 2014 at 1:49 PM, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:

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?

My opinion is that using induction principle of the type of the decreasing argument is a much better way than fix.

I think that if you never use fix and cofix, you never have to worry about your proof being rejected at Qed time.

Many people hate the idea of proofs being rejected at Qed time. Also, opaqe definitions can lead to rejection of legitimate proofs(I observed that with cofix).

Once, Coq did not give us the desired induction principle when we defined an inductive type. The first thing we did was to use fix to prove the induction principle and then we never used fix after that.

 

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.