The Coq mailing list

[Julien Forest <julien.forest AT ensiie.fr>]

Or you cqn simply use Function to define F which, in particular,
produces the induction principle attached to your function F leading to
a quite trivial proof as below :



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

Function 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.
  intros c;functional induction (F c). 
  - exact I.
  - assumption.
Qed.


Hope this helps even if not answer you first question.

Best regards,

Julien Forest


On Sun, 19 Jan 2014 16:25:09 -0500
Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 wrote:

> In this case, you can easily define a size function and do induction
> on size.
> 
> Inductive C : Set :=
>    Build_C : option C -> C.
> 
> Fixpoint size (c: C):=
> match c with
> | Build_C (Some cc) => 1+ size cc
> | Build_C None => 0
> end.
> 
> Fixpoint F (c : C) : Prop :=
>    match c with |
>       Build_C None => True |
>       Build_C (Some c') => F c'
>    end.
> 
> Lemma L_aux : forall n c, size c = n -> F c.
> Proof.
>   induction n; intros c Heq; destruct c; destruct o; inversion Heq;
> simpl; auto.
> Qed.
> 
> 
> Lemma L : forall c : C, F c.
> Proof.
>   intro c.
>   pose proof (L_aux (size c) c).
>   auto.
> Qed.
> 
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
> 
> 
> On Sun, Jan 19, 2014 at 3:55 PM, Terrell, Jeffrey
> <jeffrey.terrell AT kcl.ac.uk
> > wrote:
> 
> >  Thanks for the advice. I'm using [fix] because I don't know how to
> > prove lemmas of this kind by [induction]. Would you mind jotting
> > the proof down for me? Thanks.
> >
> > Regards,
> > Jeff.
> >
> >  On 19 Jan 2014, at 19:34, Abhishek Anand wrote:
> >
> >
> > 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.
> >>
> >
> >
> >