The Coq mailing list

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

Thanks for all your comments. They were very helpful.

The problem I'm trying to solve is more like the one below, in which C is 
built from option C and list A, and A is built from C. I've tried proving 
L_aux in the same way as before but I didn't get very far. Any help would be 
most appreciated. Thanks.

Require Import List.

Inductive C : Set :=
   Build_C : option C -> list A -> C
with A : Set :=
   Build_A : C -> A.

Fixpoint size (c : C) : nat :=
   match c with Build_C o la =>
      (fix f (l : list A) : nat :=
         match l with |
            nil => 0 |
            a :: l' =>
               match a with 
                  Build_A c' => S (size c') 
               end + f l'
         end) la 
      +
      match o with |
         None => 0 |
         Some c' => S (size c')
      end
   end.

Fixpoint 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_aux : forall n : nat, forall c : C, size c = n -> F c.
Proof.
   induction n.
   {
      intros c Heq.
      destruct c.
      destruct o.
      {
         inversion Heq.
         induction l.
         {
            inversion H0.
         }
         <stuck>

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.
>>>> 
>>> 
>>> 
>>> 
>