The Coq mailing list

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

Dear Jeffrey, 
I'm sorry but, as mentioned in Section 2.3 of the reference manual,
Function  does not support local Fixpoint and thus cannot be used in
your case. 

Best regards,

Julien.

On Mon, 20 Jan 2014 16:26:38 +0000
"Terrell, Jeffrey" 
<jeffrey.terrell AT kcl.ac.uk>
 wrote:

> Dear Julien,
> 
> I tried your suggestion but Coq rejected the function definition with
> "Error: GRec not handled".
> 
> Require Import List.
> 
> Inductive C : Set :=
>    Build_C : option C -> list A -> C
> with A : Set :=
>    Build_A : C -> A.
> 
> Function F (c : C) : Prop :=
>    match c with Build_C o la =>
>       (fix f (l : list A) : Prop :=
>          match l with |
>             nil => True |
>             a :: l' =>
>                match a with 
>                   Build_A c' => F c' 
>                end /\ f l'
>          end) la 
>       /\
>       match o with |
>          None => True |
>          Some c' => F c'
>       end
>    end.
> 
> Lemma L : forall c : C, F c.
> 
> Regards,
> Jeff.
> 
> On 20 Jan 2014, at 13:21, Julien Forest wrote:
> 
> > 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.
> >>>> 
> >>> 
> >>> 
> >>> 
> > 
>