The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thanks! That worked.

What is the difference between Defined and Qed?

Also, is this method (i.e, transporting lemmas and functions from the standard library lists to my type) advisable for what I am trying to do?

On Thu, Oct 29, 2020 at 10:20 AM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

If you do "cbv" in your proof, you will get the goal

   match list_nil_dec nat nil with
   | left _ => < 1 >
   | right pr => match pr eq_refl return (nonEmpty nat) with
                 end :| 1
   end = < 1 >

this means reduction is blocked by your lemma list_nil_dec.
If you change the Qed to Defined for list_nil_dec, reflexivity works.

Gaëtan Gilbert

On 29/10/2020 16:09, Agnishom Chattopadhyay wrote:
> Hi;
>
> For an application, non-empty lists occur naturally. One way to deal with this would be to define a type of non-empty lists and then all the necessary functions and lemmas for them.
>
> However, I am trying to recycle the theorems available in the standard library. To do this, I am defining a function which lifts functions on list to functions on my non-empty type provided they preserve non-emptiness.
>
> But I am facing some trouble with this. For example, I cannot prove the lemma simple <https://gist.github.com/Agnishom/573a697dab82ddb72360136014065f7f>, over here.
>
> What am I doing wrong?
>
> --Agnishom