The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The difference between Defined and Qed is exactly the question of whether tactics like cbv, reflexivity, unfold, etc can see their definition.  See also https://coq.inria.fr/refman/proof-engine/proof-handling.html#coq:cmd.defined and https://stackoverflow.com/questions/25478682/what-is-the-difference-between-qed-and-defined .

I believe there exist automated ways of doing lemma transport, such as https://arxiv.org/abs/1909.05027 (The Marriage of Univalence and Parametricity) and Talia Ringer's PUMPKIN PATCH and DEVOID (https://github.com/uwplse/pumpkin-pi).  I've cc'd Talia so she can say more.

The way I'd suggest doing it is:

1. First prove that the various functions you want to lift preserve non-emptyness.  Look at (2) for the comment on how to phrase non-emptyness.

2. Write wrapper functions that combine the functions with the proofs so that you have functions on the sigma type { ls : list _ | match ls with nil => False | _ => True end }.  (Note that you could use `ls <> nil` as the proof property, but then you will need function extensionality or proof irrelevance to prove that two proofs of non-nil are equal.)

3. Prove that your sigma type is isomorphic to your inductive type.

4. Use DEVOID or univalent/parametric transport (or just make the isomorphism functions be coercions and do the rewriting manually) to automatically lift all the functions and proofs from the sigma types to your inductive type.

-Jason

On Thu, Oct 29, 2020, 11:38 Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

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