The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Once again, the sentence "interp (DE y) should be convertible to m"
should not be written. The correct way to write it is "interp (DE y)  
has type m".

To take a caricatural example, we do not say "3+8 is convertible to nat",
but "3+8 is convertible with 11", and "3+8 has type nat".

Here is a simple proof of your lemma:


 Lemma o_dec_xx : forall x, (if o_dec x x then true else false) = true.
  intro x;case (o_dec x x);[reflexivity | destruct 1;auto].
 Qed.

Lemma existselement:forall d:Diag,
  exists o':o, set_mem  o_dec o' (interp d )=true.
Proof.
  intro d ;  induction d as [y]; simpl.
 exists ((y::nil)::nil).
 rewrite o_dec_xx;trivial.
Qed.


Pierre




Quoting 
ldou AT cs.ecnu.edu.cn:

> Thanks for your detail reply.
> i think  "interp (DE y)" should be convertible to m ,thus to (list  
> (list (list string))) and not to  (list (list string)) .
> the problem now is that the proof of lemma "existselement" cann't go on:
> ------------------------------------------
> Lemma existelement:forall d:Diag,
>   exists o':o, set_mem  o_dec o' (interp d )=true.
> Proof.
>   intro d.
>   induction d.
>   exists ((e0 :: nil)::nil).
>   simpl.
> ---------------------------------
> then the proof gets stuck.
>
>
>
> ------------------ 原始邮件 ------------------
> > From: Pierre Casteran 
> > <pierre.casteran AT labri.fr>
> > Reply-To:
> > To: 
> > ldou AT cs.ecnu.edu.cn
> > Subject: Re: [Coq-Club] [Coq Club]a strange question when using function
> > Date: Thu, 25 Aug 2011 06:55:50 +0200
> >
> > Hi,
> >
> >
> > Like Adam, I  don't see any error.
> >
> > For clarity's sake, I decomposed your example into small pieces, adding
> > some "Compute" and "Check" commands, and renaming the variable e0 into y
> > for avoiding confusion with the string "e0".
> >
> >
> > First, you should not write such sentences like
> > " the type of m should be set (set (list string))" :
> >
> > The correct statement are :
> > "the type of m is Type" , and "m is convertible to (set (set (list  
> > string)))",
> > thus to (list (list (list string)))"
> >
> >
> >
> > In the proof of existselement, you can see that the type of o' should be
> > convertible to (list (list string)) and not to (list (list (list string)))
> >
> > Pierre
> >
> >
> >
> >
> >
> > Quoting 
> > ldou AT cs.ecnu.edu.cn:
> >
> > > thanks for your reply!
> > > when proving lemma "existselement", i do "induction d" and  "simpl",
> > > then Coq system produce a paticular "e0:e" and replace "d" with "(DE
> > > e0)". That's why you see such a particular constant string.
> > >
> > > What confuse me is the difference when Coq compute the "interp"
> > > function. if i do:
> > >
> > > Compute (interp (DE "e0")).
> > >
> > > then i can get the following result  which is what i expect :
> > >      = (("e0" :: nil) :: nil) :: nil
> > >      : m
> > >
> > > but when do "induction d" and  "simpl" in lemma "existselement", i
> > > get a different result:
> > > ((e0 :: nil) :: nil)
> > > which i think is wrong.
> > > because due to  definition ,the type of m should be set (set (list  
> > > string)).
> > >
> > >
> > >
> > > ------------------ 原始邮件 ------------------
> > > > From: Adam Chlipala
>
> > > > Reply-To:
> > > > To: 
> > > > ldou AT cs.ecnu.edu.cn
> > > > Subject: Re: [Coq-Club] [Coq Club]a strange question when using function
> > > > Date: Wed, 24 Aug 2011 10:47:53 -0400
> > > >
> > > > ldou AT cs.ecnu.edu.cn
> > > >  wrote:
> > > > > the result turns out to be:
> > > > > exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else false)
> > > > > = true
> > > > > but it should be :
> > > > > exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true
> > > > > else false) = true
> > > > > Why is that?
> > > >
> > > > Can you explain why you expected a different result? This looks correct
> > > > to me. Why would you expect an arbitrary [Diag] to be known to contain a
> > > > particular constant string?
> > >
> > > --------------------------
> > > Hi,everyone. I just meet a strange issue below:
> > > =======================
> > >
> > > Require Import String Bool ListSet List Classical.
> > > Open Scope nat_scope.
> > > Open Scope type_scope.
> > > Open Scope string_scope.
> > > Open Scope list_scope.
> > > Definition e:=string.
> > > Definition t := list e.
> > > Definition o := set t.
> > > Definition m:=set o.
> > >
> > > Definition o_dec:forall (a b:o) ,{a = b} + {a <> b}.
> > >    repeat decide equality.
> > > Defined.
> > >
> > > Inductive Diag:Set :=
> > >  DE: e->Diag.
> > >
> > > Fixpoint interp (D:Diag) {struct D}: m  :=
> > > match D with
> > > |DE e => ((e::nil)::nil)::nil
> > > end.
> > >
> > > Lemma test: set_mem o_dec
> > >    (("e0" :: nil) :: nil) ((("e0" :: nil) :: nil) ::nil)=true.
> > > Proof.
> > >   simpl. auto.
> > > Qed.
> > >
> > > Lemma existselement:forall d:Diag,
> > >   exists o':o, set_mem  o_dec o' (interp d )=true.
> > > Proof.
> > >   intro d.
> > >   induction d. simpl.
> > > =============
> > > the problem is :when do simpl in existselement, the result turns out to be:
> > > exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else  
> > > false) = true
> > > but it should be :
> > > exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true
> > > else false) = true
> > > Why is that?